mathlib documentation

• lifted_cone : category_theory.limits.cone K
• valid_lift : F.map_cone c_1.lifted_cone ≅ c

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.

• lifted_cocone : category_theory.limits.cocone K
• valid_lift : F.map_cocone c_1.lifted_cocone ≅ c

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.

• to_reflects_limit : category_theory.limits.reflects_limit K F
• lifts : Π (c : category_theory.limits.cone (K ⋙ F)), category_theory.limits.is_limit c → category_theory.liftable_cone K F c

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.

• creates_limit : Π {K : J ⥤ C}, category_theory.creates_limit K F

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

• creates_limits_of_shape : Π {J : Type ?} {𝒥 : category_theory.small_category J}, category_theory.creates_limits_of_shape J F

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

• to_reflects_colimit : category_theory.limits.reflects_colimit K F
• lifts : Π (c : category_theory.limits.cocone (K ⋙ F)), category_theory.limits.is_colimit c → category_theory.liftable_cocone K F 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.

• creates_colimit : Π {K : J ⥤ C}, category_theory.creates_colimit K F

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

• creates_colimits_of_shape : Π {J : Type ?} {𝒥 : category_theory.small_category J}, category_theory.creates_colimits_of_shape J F

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

• to_liftable_cone : category_theory.liftable_cone K F c
• makes_limit : category_theory.limits.is_limit c_1.to_liftable_cone.lifted_cone

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.

• to_liftable_cocone : category_theory.liftable_cocone K F c
• makes_colimit : category_theory.limits.is_colimit c_1.to_liftable_cocone.lifted_cocone

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.