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.mapCone c₂) = G.map (t.lift c₂)
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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.preservesLimitsIso_hom_π_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_hom_π {C : Type u₁} [] {D : Type u₂} [] (G : ) {J : Type w} (F : ) (j : J) :
@[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 : CategoryTheory.Limits.limit (F.comp G) Z) :
@[simp]
theorem CategoryTheory.lift_comp_preservesLimitsIso_hom {C : Type u₁} [] {D : Type u₂} [] (G : ) {J : Type w} (F : ) (t : ) :
= CategoryTheory.Limits.limit.lift (F.comp G) (G.mapCone t)
instance CategoryTheory.instIsIsoPost {C : Type u₁} [] {D : Type u₂} [] (G : ) {J : Type w} (F : ) :
Equations
• =
@[simp]
theorem CategoryTheory.preservesLimitNatIso_inv_app {C : Type u₁} [] {D : Type u₂} [] (G : ) {J : Type w} (X : ) :
.app X = .inv
@[simp]
theorem CategoryTheory.preservesLimitNatIso_hom_app {C : Type u₁} [] {D : Type u₂} [] (G : ) {J : Type w} (X : ) :
.app X = .hom
def CategoryTheory.preservesLimitNatIso {C : Type u₁} [] {D : Type u₂} [] (G : ) {J : Type w} :
CategoryTheory.Limits.lim.comp G (.obj G).comp CategoryTheory.Limits.lim

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

Equations
Instances For
def CategoryTheory.preservesLimitOfIsIsoPost {C : Type u₁} [] {D : Type u₂} [] (G : ) {J : Type w} (F : ) [CategoryTheory.Limits.HasLimit (F.comp G)] :

If the comparison morphism G.obj (limit F) ⟶ limit (F ⋙ G) is an isomorphism, then G preserves limits of F.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.preserves_desc_mapCocone {C : Type u₁} [] {D : Type u₂} [] (G : ) {J : Type w} (F : ) (c₁ : ) (c₂ : ) (t : ) :
(G.mapCocone c₂) = G.map (t.desc c₂)
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.

Equations
• One or more equations did not get rendered due to their size.
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 : CategoryTheory.Limits.colimit (F.comp G) Z) :
=
@[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 : ) :
= CategoryTheory.Limits.colimit.desc (F.comp G) (G.mapCocone t)
instance CategoryTheory.instIsIsoPost_1 {C : Type u₁} [] {D : Type u₂} [] (G : ) {J : Type w} (F : ) :
Equations
• =
@[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.Limits.colim.comp G (.obj G).comp CategoryTheory.Limits.colim

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

Equations
Instances For
def CategoryTheory.preservesColimitOfIsIsoPost {C : Type u₁} [] {D : Type u₂} [] (G : ) {J : Type w} (F : ) [CategoryTheory.Limits.HasColimit (F.comp G)] :

If the comparison morphism colimit (F ⋙ G) ⟶ G.obj (colimit F) is an isomorphism, then G preserves colimits of F.

Equations
• One or more equations did not get rendered due to their size.
Instances For