# mathlibdocumentation

category_theory.limits.preserves.limits

# Isomorphisms about functors which preserve (co)limits #

If G preserves limits, and C and D have limits, then for any diagram F : J ⥤ C we have a canonical isomorphism preserves_limit_iso : G.obj (limit F) ≅ limit (F ⋙ G). We also show that we can commute is_limit.lift of a preserved limit with functor.map_cone: (preserves_limit.preserves t).lift (G.map_cone c₂) = G.map (t.lift c₂).

The duals of these are also given. For functors which preserve (co)limits of specific shapes, see preserves/shapes.lean.

@[simp]
theorem category_theory.preserves_lift_map_cone {C : Type u₁} {D : Type u₂} (G : C D) {J : Type w} (F : J C) (c₁ c₂ : category_theory.limits.cone F)  :
= G.map (t.lift c₂)
noncomputable def category_theory.preserves_limit_iso {C : Type u₁} {D : Type u₂} (G : C D) {J : Type w} (F : J C)  :

If G preserves limits, we have an isomorphism from the image of the limit of a functor F to the limit of the functor F ⋙ G.

Equations
@[simp]
theorem category_theory.preserves_limits_iso_hom_π {C : Type u₁} {D : Type u₂} (G : C D) {J : Type w} (F : J C) (j : J) :
=
@[simp]
theorem category_theory.preserves_limits_iso_hom_π_assoc {C : Type u₁} {D : Type u₂} (G : C D) {J : Type w} (F : J C) (j : J) {X' : D} (f' : (F G).obj j X') :
j f' = f'
@[simp]
theorem category_theory.preserves_limits_iso_inv_π_assoc {C : Type u₁} {D : Type u₂} (G : C D) {J : Type w} (F : J C) (j : J) {X' : D} (f' : G.obj (F.obj j) X') :
f' = j f'
@[simp]
theorem category_theory.preserves_limits_iso_inv_π {C : Type u₁} {D : Type u₂} (G : C D) {J : Type w} (F : J C) (j : J) :
= j
@[simp]
theorem category_theory.lift_comp_preserves_limits_iso_hom {C : Type u₁} {D : Type u₂} (G : C D) {J : Type w} (F : J C)  :
= (G.map_cone t)
@[simp]
theorem category_theory.lift_comp_preserves_limits_iso_hom_assoc {C : Type u₁} {D : Type u₂} (G : C D) {J : Type w} (F : J C) {X' : D} (f' : X') :
= (G.map_cone t) f'
@[simp]
theorem category_theory.preserves_limit_nat_iso_hom_app {C : Type u₁} {D : Type u₂} (G : C D) {J : Type w} (X : J C) :
noncomputable def category_theory.preserves_limit_nat_iso {C : Type u₁} {D : Type u₂} (G : C D) {J : Type w}  :

If C, D has all limits of shape J, and G preserves them, then preserves_limit_iso is functorial wrt F.

Equations
@[simp]
theorem category_theory.preserves_limit_nat_iso_inv_app {C : Type u₁} {D : Type u₂} (G : C D) {J : Type w} (X : J C) :
@[simp]
theorem category_theory.preserves_desc_map_cocone {C : Type u₁} {D : Type u₂} (G : C D) {J : Type w} (F : J C) (c₁ c₂ : category_theory.limits.cocone F)  :
= G.map (t.desc c₂)
noncomputable def category_theory.preserves_colimit_iso {C : Type u₁} {D : Type u₂} (G : C D) {J : Type w} (F : J C)  :

If G preserves colimits, we have an isomorphism from the image of the colimit of a functor F to the colimit of the functor F ⋙ G.

Equations
@[simp]
theorem category_theory.ι_preserves_colimits_iso_inv_assoc {C : Type u₁} {D : Type u₂} (G : C D) {J : Type w} (F : J C) (j : J) {X' : D} (f' : X') :
= f'
@[simp]
theorem category_theory.ι_preserves_colimits_iso_inv {C : Type u₁} {D : Type u₂} (G : C D) {J : Type w} (F : J C) (j : J) :
@[simp]
theorem category_theory.ι_preserves_colimits_iso_hom {C : Type u₁} {D : Type u₂} (G : C D) {J : Type w} (F : J C) (j : J) :
@[simp]
theorem category_theory.ι_preserves_colimits_iso_hom_assoc {C : Type u₁} {D : Type u₂} (G : C D) {J : Type w} (F : J C) (j : J) {X' : D} (f' : X') :
= f'
@[simp]
theorem category_theory.preserves_colimits_iso_inv_comp_desc {C : Type u₁} {D : Type u₂} (G : C D) {J : Type w} (F : J C)  :
= (G.map_cocone t)
@[simp]
theorem category_theory.preserves_colimits_iso_inv_comp_desc_assoc {C : Type u₁} {D : Type u₂} (G : C D) {J : Type w} (F : J C) {X' : D} (f' : G.obj t.X X') :
f' = (G.map_cocone t) f'
noncomputable def category_theory.preserves_colimit_nat_iso {C : Type u₁} {D : Type u₂} (G : C D) {J : Type w}  :

If C, D has all colimits of shape J, and G preserves them, then preserves_colimit_iso is functorial wrt F.

Equations
@[simp]
theorem category_theory.preserves_colimit_nat_iso_inv_app {C : Type u₁} {D : Type u₂} (G : C D) {J : Type w} (X : J C) :
@[simp]
theorem category_theory.preserves_colimit_nat_iso_hom_app {C : Type u₁} {D : Type u₂} (G : C D) {J : Type w} (X : J C) :