Slice polynomial functors: categorical wrapper

Packages the constructive core (Slice.Basic) as a CategoryTheory.Functor between Over categories. mathlib's Over is Classical.choice-dependent at the type level, so this categorical packaging is kept in a separate module from the choice-free core.

Main definitions

SliceDomPFunctor.domSubfunctor — the compatible assignments as a subfunctor of the underlying polynomial functor.

SliceDomPFunctor.domFunctor — the functor Over dom ⥤ Type.

SlicePFunctor.functor — the functor Over dom ⥤ Over cod.

Main statements

SlicePFunctor.functor_obj / functor_map — the categorical functor's object and morphism maps are definitionally the core SlicePFunctor.obj / map.

SlicePFunctor.functor_comp_forget — the wrapper forgets back to domFunctor.

Implementation notes

domSubfunctor is the subfunctor of Over.forget dom ⋙ PFunctor.functor cut out by the compatibility predicate, and domFunctor reads it as a functor, so the functor laws come from Subfunctor.toFunctor and Subfunctor.ι is the inclusion into the underlying polynomial functor. Over structure maps are read through ConcreteCategory.hom, the slice-morphism hypothesis is SliceDomPFunctor.over_hom_comp (the function-level form of Over.w), and the subfunctor's closure condition is the core map's output compatibility. The composite instantiates PFunctor.functor at v := uD, written explicitly as PFunctor.functor.{uA, uB, uD}. functor is the Functor.toOver lift along the shape-output map q; it is @[expose] so functor_obj / functor_map can state the definitional equalities as exported rfl theorems. cod is pinned to domFunctor's codomain universe max uA uB uD because Functor.toOver requires its over-base object to inhabit the codomain category of the lifted functor, so the core's cod-universe polymorphism cannot survive into the categorical layer.

References

[AltenkirchGhaniHancockMcBrideMorris2015]

[GambinoHyland2004]

[GambinoKock2013]

Tags

polynomial functor, slice category, Over, container, PFunctor

The function-level form of Over.w: a slice morphism g : Y ⟶ Z commutes with the projections, Z.hom ∘ g.left = Y.hom, read through ConcreteCategory.hom.

The r-compatible assignments, as a subfunctor of the underlying polynomial functor pulled back along the forgetful functor. The obj field is the compatibility predicate; the map field is its closure under the polynomial functor's action, supplied by the core map.

The functor Over dom ⥤ Type restricting the PFunctor interpretation to r-compatible assignments: the subfunctor domSubfunctor read as a functor. Subfunctor.ι is the inclusion into the underlying polynomial functor.

Output-index naturality: domFunctor.map g fixes the shape component, so post-composing with the shape-output map q is preserved. This is the Functor.toOver triangle obligation for functor, shared with functor_comp_forget.

The slice polynomial functor Over dom ⥤ Over cod: the Functor.toOver lift of domFunctor along the shape-output map q.

The wrapper forgets back to domFunctor.

functor.obj is the core obj, packaged with Over.mk. The categorical object map carries no data beyond the core.

functor.map's underlying function is the core map. An Over morphism's only data is its left component, so this fixes the categorical morphism map up to its Prop-valued commuting condition.