mathlib documentation

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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type w} [category_theory.category J] (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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type w} [category_theory.category J] (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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type w} [category_theory.category J] (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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (J : Type w) [category_theory.category J] (F : C D) :
Type (max u₁ u₂ v₁ v₂ w w')

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
@[reducible]
def category_theory.creates_limits {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type w} [category_theory.category J] (K : J C) (F : C D) :
Type (max u₁ u₂ v₁ v₂ w)

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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (J : Type w) [category_theory.category J] (F : C D) :
Type (max u₁ u₂ v₁ v₂ w w')

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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C D) :
Type (max u₁ u₂ v₁ v₂ (w+1) (w'+1))

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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (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.

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

Equations

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

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

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

Equations

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

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

structure category_theory.lifts_to_limit {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type w} [category_theory.category J] (K : J C) (F : C D) (c : category_theory.limits.cone (K F)) (t : category_theory.limits.is_limit c) :
Type (max u₁ v₁ v₂ w)

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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type w} [category_theory.category J] (K : J C) (F : C D) (c : category_theory.limits.cocone (K F)) (t : category_theory.limits.is_colimit c) :
Type (max u₁ v₁ v₂ w)

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

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

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

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

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

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

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

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

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
def category_theory.creates_limit_of_iso_diagram {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type w} [category_theory.category J] {K₁ K₂ : J C} (F : C D) (h : K₁ K₂) [category_theory.creates_limit K₁ F] :

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

Equations

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

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

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

Equations

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

Equations