# mathlib3documentation

category_theory.limits.creates

# Creating (co)limits #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 :

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.

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.

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.

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

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

@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
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]

`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]

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

Equations
@[protected, instance]

`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]

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]

The identity functor creates all colimits.

Equations
@[protected, instance]

Satisfy the inhabited linter

Equations
@[protected, instance]
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