mathlib documentation

category_theory.limits.creates

structure category_theory.liftable_cone {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type v} [category_theory.small_category J] (K : J C) (F : C D) :
category_theory.limits.cone (K F)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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type v} [category_theory.small_category J] (K : J C) (F : C D) :
category_theory.limits.cocone (K F)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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type v} [category_theory.small_category J] :
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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (J : Type v) [category_theory.small_category J] :
C DType (max u₁ u₂ v)

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

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

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

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

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

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

Instances

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.

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

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, and D has all colimits, then C has all colimits.

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

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

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.

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 show that the chosen limit point is in the essential image of F.

Equations

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