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.

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).

Equations

• One or more equations did not get rendered due to their size.

@[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) : (ConcreteCategory.hom (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).

Equations

• One or more equations did not get rendered due to their size.

@[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) : (ConcreteCategory.hom (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) : (ConcreteCategory.hom (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.

Equations

• One or more equations did not get rendered due to their size.

@[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))

@[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

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

@[instance_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)

Equations

• One or more equations did not get rendered due to their size.

@[instance_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)

Equations

• CategoryTheory.CategoryOfElements.instCreatesLimitsOfShapeElementsπ = { CreatesLimit := fun {K : CategoryTheory.Functor I A.Elements} => inferInstance }

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

def CategoryTheory.Functor.Elements.corepresentableByOfIsInitial {C : Type u} [Category.{v, u} C] {F : Functor C (Type w)} {E : F.Elements} (he : Limits.IsInitial E) : F.CorepresentableBy E.fst

An initial object in the category F.Elements of a covariant functor defines a corepresentation for that functor.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Functor.Elements.isCorepresentable_of_hasInitial {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) [Limits.HasInitial F.Elements] : F.IsCorepresentable

theorem CategoryTheory.Functor.Elements.hasInitial_iff_isCorepresentable {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) : Limits.HasInitial F.Elements ↔ F.IsCorepresentable

def CategoryTheory.Functor.Elements.representableByOfIsInitial {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {E : F.Elements} (he : Limits.IsInitial E) : F.RepresentableBy (Opposite.unop E.fst)

An initial object in the category F.Elements of a contravariant functor defines a representation for that functor.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Functor.Elements.isRepresentable_of_hasInitial {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type w)) [Limits.HasInitial F.Elements] : F.IsRepresentable

theorem CategoryTheory.Functor.Elements.hasInitial_iff_isRepresentable {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type w)) : Limits.HasInitial F.Elements ↔ F.IsRepresentable