mathlibdocumentation

category_theory.limits.creates

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

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.

structure category_theory.liftable_cocone {C : Type u₁} {D : Type u₂} {J : Type v} (K : J C) (F : C D) :
Type (max u₁ v)

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.

@[class]
structure category_theory.creates_limit {C : Type u₁} {D : Type u₂} {J : Type v}  :
J CC DType (max u₁ u₂ v)

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
@[class]
structure category_theory.creates_limits_of_shape {C : Type u₁} {D : Type u₂} (J : Type v)  :
C DType (max u₁ u₂ v)
• creates_limit : Π {K : J C},

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

Instances
@[class]
structure category_theory.creates_limits {C : Type u₁} {D : Type u₂}  :
C DType (max u₁ u₂ (v+1))
• creates_limits_of_shape : Π {J : Type ?} {𝒥 : ,

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

Instances
@[class]
structure category_theory.creates_colimit {C : Type u₁} {D : Type u₂} {J : Type v}  :
J CC DType (max u₁ u₂ v)
• 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
@[class]
structure category_theory.creates_colimits_of_shape {C : Type u₁} {D : Type u₂} (J : Type v)  :
C DType (max u₁ u₂ v)
• creates_colimit : Π {K : J C},

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

Instances
@[class]
structure category_theory.creates_colimits {C : Type u₁} {D : Type u₂}  :
C DType (max u₁ u₂ (v+1))
• creates_colimits_of_shape : Π {J : Type ?} {𝒥 : ,

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

Instances
def category_theory.lift_limit {C : Type u₁} {D : Type u₂} {J : Type v} {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 v} {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 v} {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 v} (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 v} (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 v} {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 v} {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 v} {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 v} (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 v} (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.

structure category_theory.lifts_to_limit {C : Type u₁} {D : Type u₂} {J : Type v} (K : J C) (F : C D) (c : category_theory.limits.cone (K F)) :
Type (max u₁ v)
• 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.

structure category_theory.lifts_to_colimit {C : Type u₁} {D : Type u₂} {J : Type v} (K : J C) (F : C D) (c : category_theory.limits.cocone (K F)) :
Type (max u₁ v)
• 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.

def category_theory.creates_limit_of_reflects_iso {C : Type u₁} {D : Type u₂} {J : Type v} {K : J C} {F : C D}  :
(Π (c : category_theory.limits.cone (K F)) (t : , 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
def category_theory.creates_limit_of_fully_faithful_of_lift {C : Type u₁} {D : Type u₂} {J : Type v} {K : J C} {F : C D}  :
(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
def category_theory.creates_limit_of_fully_faithful_of_iso {C : Type u₁} {D : Type u₂} {J : Type v} {K : J C} {F : C D} (X : C) :
(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
@[instance]
def category_theory.preserves_limit_of_creates_limit_and_has_limit {C : Type u₁} {D : Type u₂} {J : Type v} (K : J C) (F : C D)  :

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

Equations
@[instance]
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 v} (F : C D)  :

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

Equations
@[instance]
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
def category_theory.creates_colimit_of_reflects_iso {C : Type u₁} {D : Type u₂} {J : Type v} {K : J C} {F : C D}  :
(Π (c : (t : , t)

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

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

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

Equations
@[instance]

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

Equations
@[instance]
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.lifts_to_limit_of_creates {C : Type u₁} {D : Type u₂} {J : Type v} (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 v} (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 v} {K : J C} (c : category_theory.limits.cone (K 𝟭 C)) :
c

Any cone lifts through the identity functor.

Equations
@[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 v} {K : J C} (c : category_theory.limits.cocone (K 𝟭 C)) :
c

Any cocone lifts through the identity functor.

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

The identity functor creates all colimits.

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

Satisfy the inhabited linter

Equations
@[instance]
def category_theory.inhabited_liftable_cocone {C : Type u₁} {J : Type v} {K : J C} (c : category_theory.limits.cocone (K 𝟭 C)) :

Equations
@[instance]
def category_theory.inhabited_lifts_to_limit {C : Type u₁} {D : Type u₂} {J : Type v} (K : J C) (F : C D) (c : category_theory.limits.cone (K F))  :

Satisfy the inhabited linter

Equations
@[instance]
def category_theory.inhabited_lifts_to_colimit {C : Type u₁} {D : Type u₂} {J : Type v} (K : J C) (F : C D) (c : category_theory.limits.cocone (K F))  :

Equations
@[instance]
def category_theory.comp_creates_limit {C : Type u₁} {D : Type u₂} {J : Type v} {K : J C} {E : Type u₃} [ℰ : category_theory.category E] (F : C D) (G : D E) [i₁ : F] [i₂ : G] :
(F G)

Equations