# mathlibdocumentation

category_theory.limits.creates

# Creating (co)limits #

We say that F creates limits of K if, given any limit cone c for K ⋙ F (i.e. below) we can lift it to a cone "above", and further that F reflects limits for K.

structure category_theory.liftable_cone {C : Type u₁} {D : Type u₂} {J : Type w} (K : J C) (F : C D) (c : category_theory.limits.cone (K F)) :
Type (max u₁ v₁ v₂ w)

Define the lift of a cone: For a cone c for K ⋙ F, give a cone for K which is a lift of c, i.e. the image of it under F is (iso) to c.

We will then use this as part of the definition of creation of limits: every limit cone has a lift.

Note this definition is really only useful when c is a limit already.

Instances for category_theory.liftable_cone
structure category_theory.liftable_cocone {C : Type u₁} {D : Type u₂} {J : Type w} (K : J C) (F : C D) (c : category_theory.limits.cocone (K F)) :
Type (max u₁ v₁ v₂ w)

Define the lift of a cocone: For a cocone c for K ⋙ F, give a cocone for K which is a lift of c, i.e. the image of it under F is (iso) to c.

We will then use this as part of the definition of creation of colimits: every limit cocone has a lift.

Note this definition is really only useful when c is a colimit already.

Instances for category_theory.liftable_cocone
@[class]
structure category_theory.creates_limit {C : Type u₁} {D : Type u₂} {J : Type w} (K : J C) (F : C D) :
Type (max u₁ u₂ v₁ v₂ w)

Definition 3.3.1 of [Riehl]. We say that F creates limits of K if, given any limit cone c for K ⋙ F (i.e. below) we can lift it to a cone "above", and further that F reflects limits for K.

If F reflects isomorphisms, it suffices to show only that the lifted cone is a limit - see creates_limit_of_reflects_iso.

Instances of this typeclass
Instances of other typeclasses for category_theory.creates_limit
• category_theory.creates_limit.has_sizeof_inst
@[class]
structure category_theory.creates_limits_of_shape {C : Type u₁} {D : Type u₂} (J : Type w) (F : C D) :
Type (max u₁ u₂ v₁ v₂ w w')
• creates_limit : (Π {K : J C}, . "apply_instance"

F creates limits of shape J if F creates the limit of any diagram K : J ⥤ C.

Instances of this typeclass
Instances of other typeclasses for category_theory.creates_limits_of_shape
• category_theory.creates_limits_of_shape.has_sizeof_inst
@[nolint, class]
structure category_theory.creates_limits_of_size {C : Type u₁} {D : Type u₂} (F : C D) :
Type (max u₁ u₂ v₁ v₂ (w+1) (w'+1))
• creates_limits_of_shape : (Π {J : Type ?} [_inst_4 : , . "apply_instance"

F creates limits if it creates limits of shape J for any J.

Instances of this typeclass
Instances of other typeclasses for category_theory.creates_limits_of_size
• category_theory.creates_limits_of_size.has_sizeof_inst
@[reducible]
def category_theory.creates_limits {C : Type u₁} {D : Type u₂} (F : C D) :
Type (max u₁ u₂ v₁ (v₂+1))

F creates small limits if it creates limits of shape J for any small J.

@[class]
structure category_theory.creates_colimit {C : Type u₁} {D : Type u₂} {J : Type w} (K : J C) (F : C D) :
Type (max u₁ u₂ v₁ v₂ w)
• to_reflects_colimit :
• lifts : Π (c : ,

Dual of definition 3.3.1 of [Riehl]. We say that F creates colimits of K if, given any limit cocone c for K ⋙ F (i.e. below) we can lift it to a cocone "above", and further that F reflects limits for K.

If F reflects isomorphisms, it suffices to show only that the lifted cocone is a limit - see creates_limit_of_reflects_iso.

Instances of this typeclass
Instances of other typeclasses for category_theory.creates_colimit
• category_theory.creates_colimit.has_sizeof_inst
@[class]
structure category_theory.creates_colimits_of_shape {C : Type u₁} {D : Type u₂} (J : Type w) (F : C D) :
Type (max u₁ u₂ v₁ v₂ w w')
• creates_colimit : (Π {K : J C}, . "apply_instance"

F creates colimits of shape J if F creates the colimit of any diagram K : J ⥤ C.

Instances of this typeclass
Instances of other typeclasses for category_theory.creates_colimits_of_shape
• category_theory.creates_colimits_of_shape.has_sizeof_inst
@[nolint, class]
structure category_theory.creates_colimits_of_size {C : Type u₁} {D : Type u₂} (F : C D) :
Type (max u₁ u₂ v₁ v₂ (w+1) (w'+1))
• creates_colimits_of_shape : (Π {J : Type ?} [_inst_4 : , . "apply_instance"

F creates colimits if it creates colimits of shape J for any small J.

Instances of this typeclass
Instances of other typeclasses for category_theory.creates_colimits_of_size
• category_theory.creates_colimits_of_size.has_sizeof_inst
@[reducible]
def category_theory.creates_colimits {C : Type u₁} {D : Type u₂} (F : C D) :
Type (max u₁ u₂ v₁ (v₂+1))

F creates small colimits if it creates colimits of shape J for any small J.

def category_theory.lift_limit {C : Type u₁} {D : Type u₂} {J : Type w} {K : J C} {F : C D} {c : category_theory.limits.cone (K F)}  :

lift_limit t is the cone for K given by lifting the limit t for K ⋙ F.

Equations
def category_theory.lifted_limit_maps_to_original {C : Type u₁} {D : Type u₂} {J : Type w} {K : J C} {F : C D} {c : category_theory.limits.cone (K F)}  :

The lifted cone has an image isomorphic to the original cone.

Equations
def category_theory.lifted_limit_is_limit {C : Type u₁} {D : Type u₂} {J : Type w} {K : J C} {F : C D} {c : category_theory.limits.cone (K F)}  :

The lifted cone is a limit.

Equations
theorem category_theory.has_limit_of_created {C : Type u₁} {D : Type u₂} {J : Type w} (K : J C) (F : C D)  :

If F creates the limit of K and K ⋙ F has a limit, then K has a limit.

theorem category_theory.has_limits_of_shape_of_has_limits_of_shape_creates_limits_of_shape {C : Type u₁} {D : Type u₂} {J : Type w} (F : C D)  :

If F creates limits of shape J, and D has limits of shape J, then C has limits of shape J.

theorem category_theory.has_limits_of_has_limits_creates_limits {C : Type u₁} {D : Type u₂} (F : C D)  :

If F creates limits, and D has all limits, then C has all limits.

def category_theory.lift_colimit {C : Type u₁} {D : Type u₂} {J : Type w} {K : J C} {F : C D} {c : category_theory.limits.cocone (K F)}  :

lift_colimit t is the cocone for K given by lifting the colimit t for K ⋙ F.

Equations
def category_theory.lifted_colimit_maps_to_original {C : Type u₁} {D : Type u₂} {J : Type w} {K : J C} {F : C D} {c : category_theory.limits.cocone (K F)}  :

The lifted cocone has an image isomorphic to the original cocone.

Equations
def category_theory.lifted_colimit_is_colimit {C : Type u₁} {D : Type u₂} {J : Type w} {K : J C} {F : C D} {c : category_theory.limits.cocone (K F)}  :

The lifted cocone is a colimit.

Equations
theorem category_theory.has_colimit_of_created {C : Type u₁} {D : Type u₂} {J : Type w} (K : J C) (F : C D)  :

If F creates the limit of K and K ⋙ F has a limit, then K has a limit.

theorem category_theory.has_colimits_of_shape_of_has_colimits_of_shape_creates_colimits_of_shape {C : Type u₁} {D : Type u₂} {J : Type w} (F : C D)  :

If F creates colimits of shape J, and D has colimits of shape J, then C has colimits of shape J.

theorem category_theory.has_colimits_of_has_colimits_creates_colimits {C : Type u₁} {D : Type u₂} (F : C D)  :

If F creates colimits, and D has all colimits, then C has all colimits.

@[protected, instance]
def category_theory.reflects_limits_of_shape_of_creates_limits_of_shape {C : Type u₁} {D : Type u₂} {J : Type w} (F : C D)  :
Equations
@[protected, instance]
def category_theory.reflects_limits_of_creates_limits {C : Type u₁} {D : Type u₂} (F : C D)  :
Equations
@[protected, instance]
def category_theory.reflects_colimits_of_shape_of_creates_colimits_of_shape {C : Type u₁} {D : Type u₂} {J : Type w} (F : C D)  :
Equations
@[protected, instance]
def category_theory.reflects_colimits_of_creates_colimits {C : Type u₁} {D : Type u₂} (F : C D)  :
Equations
structure category_theory.lifts_to_limit {C : Type u₁} {D : Type u₂} {J : Type w} (K : J C) (F : C D) (c : category_theory.limits.cone (K F))  :
Type (max u₁ v₁ v₂ w)
• to_liftable_cone :
• makes_limit :

A helper to show a functor creates limits. In particular, if we can show that for any limit cone c for K ⋙ F, there is a lift of it which is a limit and F reflects isomorphisms, then F creates limits. Usually, F creating limits says that any lift of c is a limit, but here we only need to show that our particular lift of c is a limit.

Instances for category_theory.lifts_to_limit
structure category_theory.lifts_to_colimit {C : Type u₁} {D : Type u₂} {J : Type w} (K : J C) (F : C D) (c : category_theory.limits.cocone (K F))  :
Type (max u₁ v₁ v₂ w)
• to_liftable_cocone :
• makes_colimit :

A helper to show a functor creates colimits. In particular, if we can show that for any limit cocone c for K ⋙ F, there is a lift of it which is a limit and F reflects isomorphisms, then F creates colimits. Usually, F creating colimits says that any lift of c is a colimit, but here we only need to show that our particular lift of c is a colimit.

Instances for category_theory.lifts_to_colimit
noncomputable def category_theory.creates_limit_of_reflects_iso {C : Type u₁} {D : Type u₂} {J : Type w} {K : J C} {F : C D} (h : Π (c : category_theory.limits.cone (K F)) (t : , ) :

If F reflects isomorphisms and we can lift any limit cone to a limit cone, then F creates limits. In particular here we don't need to assume that F reflects limits.

Equations
noncomputable def category_theory.creates_limit_of_fully_faithful_of_lift' {C : Type u₁} {D : Type u₂} {J : Type w} {K : J C} {F : C D} {l : category_theory.limits.cone (K F)} (i : F.map_cone c l) :

When F is fully faithful, to show that F creates the limit for K it suffices to exhibit a lift of a limit cone for K ⋙ F.

Equations
noncomputable def category_theory.creates_limit_of_fully_faithful_of_lift {C : Type u₁} {D : Type u₂} {J : Type w} {K : J C} {F : C D} (i : F.map_cone c ) :

When F is fully faithful, and has_limit (K ⋙ F), to show that F creates the limit for K it suffices to exhibit a lift of the chosen limit cone for K ⋙ F.

Equations
noncomputable def category_theory.creates_limit_of_fully_faithful_of_iso' {C : Type u₁} {D : Type u₂} {J : Type w} {K : J C} {F : C D} {l : category_theory.limits.cone (K F)} (X : C) (i : F.obj X l.X) :

When F is fully faithful, to show that F creates the limit for K it suffices to show that a limit point is in the essential image of F.

Equations
noncomputable def category_theory.creates_limit_of_fully_faithful_of_iso {C : Type u₁} {D : Type u₂} {J : Type w} {K : J C} {F : C D} (X : C) (i : F.obj X ) :

When F is fully faithful, and has_limit (K ⋙ F), to show that F creates the limit for K it suffices to show that the chosen limit point is in the essential image of F.

Equations
@[protected, instance]
noncomputable def category_theory.preserves_limit_of_creates_limit_and_has_limit {C : Type u₁} {D : Type u₂} {J : Type w} (K : J C) (F : C D)  :

F preserves the limit of K if it creates the limit and K ⋙ F has the limit.

Equations
@[protected, instance]
noncomputable def category_theory.preserves_limit_of_shape_of_creates_limits_of_shape_and_has_limits_of_shape {C : Type u₁} {D : Type u₂} {J : Type w} (F : C D)  :

F preserves the limit of shape J if it creates these limits and D has them.

Equations
@[protected, instance]
noncomputable def category_theory.preserves_limits_of_creates_limits_and_has_limits {C : Type u₁} {D : Type u₂} (F : C D)  :

F preserves limits if it creates limits and D has limits.

Equations
noncomputable def category_theory.creates_colimit_of_reflects_iso {C : Type u₁} {D : Type u₂} {J : Type w} {K : J C} {F : C D} (h : Π (c : (t : , ) :

If F reflects isomorphisms and we can lift any colimit cocone to a colimit cocone, then F creates colimits. In particular here we don't need to assume that F reflects colimits.

Equations
noncomputable def category_theory.creates_colimit_of_fully_faithful_of_lift' {C : Type u₁} {D : Type u₂} {J : Type w} {K : J C} {F : C D} {l : category_theory.limits.cocone (K F)} (i : F.map_cocone c l) :

When F is fully faithful, to show that F creates the colimit for K it suffices to exhibit a lift of a colimit cocone for K ⋙ F.

Equations
noncomputable def category_theory.creates_colimit_of_fully_faithful_of_lift {C : Type u₁} {D : Type u₂} {J : Type w} {K : J C} {F : C D} (i : F.map_cocone c ) :

When F is fully faithful, and has_colimit (K ⋙ F), to show that F creates the colimit for K it suffices to exhibit a lift of the chosen colimit cocone for K ⋙ F.

Equations
noncomputable def category_theory.creates_colimit_of_fully_faithful_of_iso' {C : Type u₁} {D : Type u₂} {J : Type w} {K : J C} {F : C D} {l : category_theory.limits.cocone (K F)} (X : C) (i : F.obj X l.X) :

When F is fully faithful, to show that F creates the colimit for K it suffices to show that a colimit point is in the essential image of F.

Equations
noncomputable def category_theory.creates_colimit_of_fully_faithful_of_iso {C : Type u₁} {D : Type u₂} {J : Type w} {K : J C} {F : C D} (X : C) (i : F.obj X ) :

When F is fully faithful, and has_colimit (K ⋙ F), to show that F creates the colimit for K it suffices to show that the chosen colimit point is in the essential image of F.

Equations
@[protected, instance]
noncomputable def category_theory.preserves_colimit_of_creates_colimit_and_has_colimit {C : Type u₁} {D : Type u₂} {J : Type w} (K : J C) (F : C D)  :

F preserves the colimit of K if it creates the colimit and K ⋙ F has the colimit.

Equations
@[protected, instance]
noncomputable def category_theory.preserves_colimit_of_shape_of_creates_colimits_of_shape_and_has_colimits_of_shape {C : Type u₁} {D : Type u₂} {J : Type w} (F : C D)  :

F preserves the colimit of shape J if it creates these colimits and D has them.

Equations
@[protected, instance]
noncomputable def category_theory.preserves_colimits_of_creates_colimits_and_has_colimits {C : Type u₁} {D : Type u₂} (F : C D)  :

F preserves limits if it creates limits and D has limits.

Equations
def category_theory.creates_limit_of_iso_diagram {C : Type u₁} {D : Type u₂} {J : Type w} {K₁ K₂ : J C} (F : C D) (h : K₁ K₂)  :

Transfer creation of limits along a natural isomorphism in the diagram.

Equations
def category_theory.creates_limit_of_nat_iso {C : Type u₁} {D : Type u₂} {J : Type w} {K : J C} {F G : C D} (h : F G)  :

If F creates the limit of K and F ≅ G, then G creates the limit of K.

Equations
def category_theory.creates_limits_of_shape_of_nat_iso {C : Type u₁} {D : Type u₂} {J : Type w} {F G : C D} (h : F G)  :

If F creates limits of shape J and F ≅ G, then G creates limits of shape J.

Equations
def category_theory.creates_limits_of_nat_iso {C : Type u₁} {D : Type u₂} {F G : C D} (h : F G)  :

If F creates limits and F ≅ G, then G creates limits.

Equations
def category_theory.creates_colimit_of_iso_diagram {C : Type u₁} {D : Type u₂} {J : Type w} {K₁ K₂ : J C} (F : C D) (h : K₁ K₂)  :

Transfer creation of colimits along a natural isomorphism in the diagram.

Equations
def category_theory.creates_colimit_of_nat_iso {C : Type u₁} {D : Type u₂} {J : Type w} {K : J C} {F G : C D} (h : F G)  :

If F creates the colimit of K and F ≅ G, then G creates the colimit of K.

Equations
def category_theory.creates_colimits_of_shape_of_nat_iso {C : Type u₁} {D : Type u₂} {J : Type w} {F G : C D} (h : F G)  :

If F creates colimits of shape J and F ≅ G, then G creates colimits of shape J.

Equations
def category_theory.creates_colimits_of_nat_iso {C : Type u₁} {D : Type u₂} {F G : C D} (h : F G)  :

If F creates colimits and F ≅ G, then G creates colimits.

Equations
def category_theory.lifts_to_limit_of_creates {C : Type u₁} {D : Type u₂} {J : Type w} (K : J C) (F : C D) (c : category_theory.limits.cone (K F))  :

If F creates the limit of K, any cone lifts to a limit.

Equations
def category_theory.lifts_to_colimit_of_creates {C : Type u₁} {D : Type u₂} {J : Type w} (K : J C) (F : C D) (c : category_theory.limits.cocone (K F))  :

If F creates the colimit of K, any cocone lifts to a colimit.

Equations
def category_theory.id_lifts_cone {C : Type u₁} {J : Type w} {K : J C} (c : category_theory.limits.cone (K 𝟭 C)) :
c

Any cone lifts through the identity functor.

Equations
@[protected, instance]
def category_theory.id_creates_limits {C : Type u₁}  :

The identity functor creates all limits.

Equations
def category_theory.id_lifts_cocone {C : Type u₁} {J : Type w} {K : J C} (c : category_theory.limits.cocone (K 𝟭 C)) :
c

Any cocone lifts through the identity functor.

Equations
@[protected, instance]
def category_theory.id_creates_colimits {C : Type u₁}  :

The identity functor creates all colimits.

Equations
@[protected, instance]
def category_theory.inhabited_liftable_cone {C : Type u₁} {J : Type w} {K : J C} (c : category_theory.limits.cone (K 𝟭 C)) :

Satisfy the inhabited linter

Equations
@[protected, instance]
def category_theory.inhabited_liftable_cocone {C : Type u₁} {J : Type w} {K : J C} (c : category_theory.limits.cocone (K 𝟭 C)) :
Equations
@[protected, instance]
def category_theory.inhabited_lifts_to_limit {C : Type u₁} {D : Type u₂} {J : Type w} (K : J C) (F : C D) (c : category_theory.limits.cone (K F))  :

Satisfy the inhabited linter

Equations
@[protected, instance]
def category_theory.inhabited_lifts_to_colimit {C : Type u₁} {D : Type u₂} {J : Type w} (K : J C) (F : C D) (c : category_theory.limits.cocone (K F))  :
Equations
@[protected, instance]
def category_theory.comp_creates_limit {C : Type u₁} {D : Type u₂} {J : Type w} {K : J C} {E : Type u₃} [ℰ : category_theory.category E] (F : C D) (G : D E) [ G] :
(F G)
Equations
@[protected, instance]
def category_theory.comp_creates_limits_of_shape {C : Type u₁} {D : Type u₂} {J : Type w} {E : Type u₃} [ℰ : category_theory.category E] (F : C D) (G : D E)  :
Equations
@[protected, instance]
def category_theory.comp_creates_limits {C : Type u₁} {D : Type u₂} {E : Type u₃} [ℰ : category_theory.category E] (F : C D) (G : D E)  :
Equations
@[protected, instance]
def category_theory.comp_creates_colimit {C : Type u₁} {D : Type u₂} {J : Type w} {K : J C} {E : Type u₃} [ℰ : category_theory.category E] (F : C D) (G : D E) [ G] :
(F G)
Equations
@[protected, instance]
def category_theory.comp_creates_colimits_of_shape {C : Type u₁} {D : Type u₂} {J : Type w} {E : Type u₃} [ℰ : category_theory.category E] (F : C D) (G : D E)  :
Equations
@[protected, instance]
def category_theory.comp_creates_colimits {C : Type u₁} {D : Type u₂} {E : Type u₃} [ℰ : category_theory.category E] (F : C D) (G : D E)  :
Equations