Action of an initial functor on sections

Given F : C ⥤ D and P : D ⥤ Type w, we define a map sectionsPrecomp F : P.sections → (F ⋙ P).sections and show that it is a bijection when F is initial. As Functor.sections identify to limits of functors to types (at least under suitable universe assumptions), this could be deduced from general results about limits and initial functors, but we provide a more down to earth proof.

We also obtain the dual result that if F is final, then F.colimitTypePrecomp : (F ⋙ P).ColimitType → P.ColimitType is a bijection.

def CategoryTheory.Functor.sectionsPrecomp {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) {P : Functor D (Type w)} (x : ↑P.sections) : ↑(F.comp P).sections

When F : C ⥤ D and P : D ⥤ Type _, this is the obvious map P.sections → (F ⋙ P).sections.

Equations

• F.sectionsPrecomp x = ⟨fun (x_1 : C) => ↑x (F.obj x_1), ⋯⟩

@[simp]

theorem CategoryTheory.Functor.sectionsPrecomp_coe {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) {P : Functor D (Type w)} (x : ↑P.sections) (x✝ : C) : ↑(F.sectionsPrecomp x) x✝ = ↑x (F.obj x✝)

theorem CategoryTheory.Functor.bijective_sectionsPrecomp {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) (P : Functor D (Type w)) [F.Initial] : Function.Bijective F.sectionsPrecomp

def CategoryTheory.Functor.colimitTypePrecomp {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) (P : Functor D (Type w)) : (F.comp P).ColimitType → P.ColimitType

Given P : D ⥤ Type w and F : C ⥤ D, this is the obvious map (F ⋙ P).ColimitType → P.ColimitType.

Equations

• F.colimitTypePrecomp P = (F.comp P).descColimitType (P.coconeTypes.precomp F)

@[simp]

theorem CategoryTheory.Functor.colimitTypePrecomp_ιColimitType {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) {P : Functor D (Type w)} (i : C) (x : P.obj (F.obj i)) : F.colimitTypePrecomp P ((F.comp P).ιColimitType i x) = P.ιColimitType (F.obj i) x

theorem CategoryTheory.Functor.bijective_colimitTypePrecomp {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) (P : Functor D (Type w)) [F.Final] : Function.Bijective (F.colimitTypePrecomp P)