Limits in the category of elements

We show that if C has limits of shape I and A : C ⥤ Type w preserves limits of shape I, then the category of elements of A has limits of shape I and the forgetful functor π : A.Elements ⥤ C creates them.

Further results

• If A is (co)representable, then A.Elements has an initial object.

TODOs

• Show that A is (co)representable if A.Elements has an initial object.

noncomputable def CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedConeElement' {C : Type u} [Category.{v, u} C] {A : Functor C (Type w)} {I : Type u₁} [Category.{v₁, u₁} I] [Small.{w, u₁} I] (F : Functor I A.Elements) : Limits.limit ((F.comp (π A)).comp A)

(implementation) A system (Fi, fi)_i of elements induces an element in lim_i A(Fi).

@[simp]

theorem CategoryTheory.CategoryOfElements.CreatesLimitsAux.π_liftedConeElement' {C : Type u} [Category.{v, u} C] {A : Functor C (Type w)} {I : Type u₁} [Category.{v₁, u₁} I] [Small.{w, u₁} I] (F : Functor I A.Elements) (i : I) : Limits.limit.π ((F.comp (π A)).comp A) i (liftedConeElement' F) = (F.obj i).snd

noncomputable def CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedConeElement {C : Type u} [Category.{v, u} C] {A : Functor C (Type w)} {I : Type u₁} [Category.{v₁, u₁} I] [Small.{w, u₁} I] (F : Functor I A.Elements) [Limits.HasLimitsOfShape I C] [Limits.PreservesLimitsOfShape I A] : A.obj (Limits.limit (F.comp (π A)))

(implementation) A system (Fi, fi)_i of elements induces an element in A(lim_i Fi).

@[simp]

theorem CategoryTheory.CategoryOfElements.CreatesLimitsAux.map_lift_mapCone {C : Type u} [Category.{v, u} C] {A : Functor C (Type w)} {I : Type u₁} [Category.{v₁, u₁} I] [Small.{w, u₁} I] (F : Functor I A.Elements) [Limits.HasLimitsOfShape I C] [Limits.PreservesLimitsOfShape I A] (c : Limits.Cone F) : A.map (Limits.limit.lift (F.comp (π A)) ((π A).mapCone c)) c.pt.snd = liftedConeElement F

@[simp]

theorem CategoryTheory.CategoryOfElements.CreatesLimitsAux.map_π_liftedConeElement {C : Type u} [Category.{v, u} C] {A : Functor C (Type w)} {I : Type u₁} [Category.{v₁, u₁} I] [Small.{w, u₁} I] (F : Functor I A.Elements) [Limits.HasLimitsOfShape I C] [Limits.PreservesLimitsOfShape I A] (i : I) : A.map (Limits.limit.π (F.comp (π A)) i) (liftedConeElement F) = (F.obj i).snd

noncomputable def CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedCone {C : Type u} [Category.{v, u} C] {A : Functor C (Type w)} {I : Type u₁} [Category.{v₁, u₁} I] [Small.{w, u₁} I] (F : Functor I A.Elements) [Limits.HasLimitsOfShape I C] [Limits.PreservesLimitsOfShape I A] : Limits.Cone F

(implementation) The constructed limit cone.

@[simp]

theorem CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedCone_pt_snd {C : Type u} [Category.{v, u} C] {A : Functor C (Type w)} {I : Type u₁} [Category.{v₁, u₁} I] [Small.{w, u₁} I] (F : Functor I A.Elements) [Limits.HasLimitsOfShape I C] [Limits.PreservesLimitsOfShape I A] : (liftedCone F).pt.snd = liftedConeElement F

@[simp]

theorem CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedCone_π_app_coe {C : Type u} [Category.{v, u} C] {A : Functor C (Type w)} {I : Type u₁} [Category.{v₁, u₁} I] [Small.{w, u₁} I] (F : Functor I A.Elements) [Limits.HasLimitsOfShape I C] [Limits.PreservesLimitsOfShape I A] (i : I) : ↑((liftedCone F).π.app i) = Limits.limit.π (F.comp (π A)) i

@[simp]

theorem CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedCone_pt_fst {C : Type u} [Category.{v, u} C] {A : Functor C (Type w)} {I : Type u₁} [Category.{v₁, u₁} I] [Small.{w, u₁} I] (F : Functor I A.Elements) [Limits.HasLimitsOfShape I C] [Limits.PreservesLimitsOfShape I A] : (liftedCone F).pt.fst = Limits.limit (F.comp (π A))

noncomputable def CategoryTheory.CategoryOfElements.CreatesLimitsAux.isValidLift {C : Type u} [Category.{v, u} C] {A : Functor C (Type w)} {I : Type u₁} [Category.{v₁, u₁} I] [Small.{w, u₁} I] (F : Functor I A.Elements) [Limits.HasLimitsOfShape I C] [Limits.PreservesLimitsOfShape I A] : (π A).mapCone (liftedCone F) ≅ Limits.limit.cone (F.comp (π A))

(implementation) The constructed limit cone is a lift of the limit cone in C.

noncomputable def CategoryTheory.CategoryOfElements.CreatesLimitsAux.isLimit {C : Type u} [Category.{v, u} C] {A : Functor C (Type w)} {I : Type u₁} [Category.{v₁, u₁} I] [Small.{w, u₁} I] (F : Functor I A.Elements) [Limits.HasLimitsOfShape I C] [Limits.PreservesLimitsOfShape I A] : Limits.IsLimit (liftedCone F)

(implementation) The constructed limit cone is a limit cone.

@[implicit_reducible]

noncomputable instance CategoryTheory.CategoryOfElements.instCreatesLimitElementsπ {C : Type u} [Category.{v, u} C] {A : Functor C (Type w)} {I : Type u₁} [Category.{v₁, u₁} I] [Small.{w, u₁} I] [Limits.HasLimitsOfShape I C] [Limits.PreservesLimitsOfShape I A] (F : Functor I A.Elements) : CreatesLimit F (π A)

@[implicit_reducible]

noncomputable instance CategoryTheory.CategoryOfElements.instCreatesLimitsOfShapeElementsπ {C : Type u} [Category.{v, u} C] {A : Functor C (Type w)} {I : Type u₁} [Category.{v₁, u₁} I] [Small.{w, u₁} I] [Limits.HasLimitsOfShape I C] [Limits.PreservesLimitsOfShape I A] : CreatesLimitsOfShape I (π A)

instance CategoryTheory.CategoryOfElements.instHasLimitsOfShapeElements {C : Type u} [Category.{v, u} C] {A : Functor C (Type w)} {I : Type u₁} [Category.{v₁, u₁} I] [Small.{w, u₁} I] [Limits.HasLimitsOfShape I C] [Limits.PreservesLimitsOfShape I A] : Limits.HasLimitsOfShape I A.Elements

instance CategoryTheory.CategoryOfElements.instHasInitialElementsOppositeOfIsRepresentable {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type u_1)} [F.IsRepresentable] : Limits.HasInitial F.Elements

instance CategoryTheory.CategoryOfElements.instHasInitialElementsOfIsCorepresentable {C : Type u} [Category.{v, u} C] {F : Functor C (Type u_1)} [F.IsCorepresentable] : Limits.HasInitial F.Elements