# Documentation

Mathlib.CategoryTheory.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 preservesLimitsIso : G.obj (Limit F) ≅ Limit (F ⋙ G). We also show that we can commute IsLimit.lift of a preserved limit with Functor.mapCone: (PreservesLimit.preserves t).lift (G.mapCone 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 CategoryTheory.preserves_lift_mapCone {C : Type u₁} [] {D : Type u₂} [] (G : ) {J : Type w} (F : ) (c₁ : ) (c₂ : ) (t : ) :
= G.map ()
def CategoryTheory.preservesLimitIso {C : Type u₁} [] {D : Type u₂} [] (G : ) {J : Type w} (F : ) :

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.

Instances For
@[simp]
theorem CategoryTheory.preservesLimitsIso_hom_π_assoc {C : Type u₁} [] {D : Type u₂} [] (G : ) {J : Type w} (F : ) (j : J) {Z : D} (h : ().obj j Z) :
@[simp]
theorem CategoryTheory.preservesLimitsIso_hom_π {C : Type u₁} [] {D : Type u₂} [] (G : ) {J : Type w} (F : ) (j : J) :
= G.map ()
@[simp]
theorem CategoryTheory.preservesLimitsIso_inv_π_assoc {C : Type u₁} [] {D : Type u₂} [] (G : ) {J : Type w} (F : ) (j : J) {Z : D} (h : G.obj (F.obj j) Z) :
@[simp]
theorem CategoryTheory.preservesLimitsIso_inv_π {C : Type u₁} [] {D : Type u₂} [] (G : ) {J : Type w} (F : ) (j : J) :
@[simp]
theorem CategoryTheory.lift_comp_preservesLimitsIso_hom_assoc {C : Type u₁} [] {D : Type u₂} [] (G : ) {J : Type w} (F : ) (t : ) {Z : D} (h : ) :
@[simp]
theorem CategoryTheory.lift_comp_preservesLimitsIso_hom {C : Type u₁} [] {D : Type u₂} [] (G : ) {J : Type w} (F : ) (t : ) :
@[simp]
theorem CategoryTheory.preservesLimitNatIso_hom_app {C : Type u₁} [] {D : Type u₂} [] (G : ) {J : Type w} (X : ) :
.app X = ().hom
@[simp]
theorem CategoryTheory.preservesLimitNatIso_inv_app {C : Type u₁} [] {D : Type u₂} [] (G : ) {J : Type w} (X : ) :
.app X = ().inv
def CategoryTheory.preservesLimitNatIso {C : Type u₁} [] {D : Type u₂} [] (G : ) {J : Type w} :
CategoryTheory.Functor.comp CategoryTheory.Limits.lim G CategoryTheory.Functor.comp (().obj G) CategoryTheory.Limits.lim

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

Instances For
@[simp]
theorem CategoryTheory.preserves_desc_mapCocone {C : Type u₁} [] {D : Type u₂} [] (G : ) {J : Type w} (F : ) (c₁ : ) (c₂ : ) (t : ) :
CategoryTheory.Limits.IsColimit.desc () (G.mapCocone c₂) = G.map ()
def CategoryTheory.preservesColimitIso {C : Type u₁} [] {D : Type u₂} [] (G : ) {J : Type w} (F : ) :

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.

Instances For
@[simp]
theorem CategoryTheory.ι_preservesColimitsIso_inv_assoc {C : Type u₁} [] {D : Type u₂} [] (G : ) {J : Type w} (F : ) (j : J) {Z : D} (h : G.obj () Z) :
@[simp]
theorem CategoryTheory.ι_preservesColimitsIso_inv {C : Type u₁} [] {D : Type u₂} [] (G : ) {J : Type w} (F : ) (j : J) :
@[simp]
theorem CategoryTheory.ι_preservesColimitsIso_hom_assoc {C : Type u₁} [] {D : Type u₂} [] (G : ) {J : Type w} (F : ) (j : J) {Z : D} (h : ) :
@[simp]
theorem CategoryTheory.ι_preservesColimitsIso_hom {C : Type u₁} [] {D : Type u₂} [] (G : ) {J : Type w} (F : ) (j : J) :
@[simp]
theorem CategoryTheory.preservesColimitsIso_inv_comp_desc_assoc {C : Type u₁} [] {D : Type u₂} [] (G : ) {J : Type w} (F : ) (t : ) {Z : D} (h : G.obj t.pt Z) :
@[simp]
theorem CategoryTheory.preservesColimitsIso_inv_comp_desc {C : Type u₁} [] {D : Type u₂} [] (G : ) {J : Type w} (F : ) (t : ) :
@[simp]
theorem CategoryTheory.preservesColimitNatIso_hom_app {C : Type u₁} [] {D : Type u₂} [] (G : ) {J : Type w} (X : ) :
.app X = ().hom
@[simp]
theorem CategoryTheory.preservesColimitNatIso_inv_app {C : Type u₁} [] {D : Type u₂} [] (G : ) {J : Type w} (X : ) :
.app X = ().inv
def CategoryTheory.preservesColimitNatIso {C : Type u₁} [] {D : Type u₂} [] (G : ) {J : Type w} :
CategoryTheory.Functor.comp CategoryTheory.Limits.colim G CategoryTheory.Functor.comp (().obj G) CategoryTheory.Limits.colim

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

Instances For