Preserving pullbacks

Constructions to relate the notions of preserving pullbacks and reflecting pullbacks to concrete pullback cones.

In particular, we show that pullbackComparison G f g is an isomorphism iff G preserves the pullback of f and g.

The dual is also given.

TODO

• Generalise to wide pullbacks

def CategoryTheory.Limits.isLimitMapConePullbackConeEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {W : C} {X : C} {Y : C} {Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {h : W ⟶ X} {k : W ⟶ Y} (comm : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g) : CategoryTheory.Limits.IsLimit (G.mapCone (CategoryTheory.Limits.PullbackCone.mk h k comm)) ≃ CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk (G.map h) (G.map k) ⋯)

The map of a pullback cone is a limit iff the fork consisting of the mapped morphisms is a limit. This essentially lets us commute PullbackCone.mk with Functor.mapCone.

Equations

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

def CategoryTheory.Limits.isLimitPullbackConeMapOfIsLimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {W : C} {X : C} {Y : C} {Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {h : W ⟶ X} {k : W ⟶ Y} (comm : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) G] (l : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk h k comm)) : let_fun this := ⋯; CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk (G.map h) (G.map k) this)

The property of preserving pullbacks expressed in terms of binary fans.

Equations

• CategoryTheory.Limits.isLimitPullbackConeMapOfIsLimit G comm l = (CategoryTheory.Limits.isLimitMapConePullbackConeEquiv G comm) (CategoryTheory.Limits.PreservesLimit.preserves l)

def CategoryTheory.Limits.isLimitOfIsLimitPullbackConeMap {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {W : C} {X : C} {Y : C} {Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {h : W ⟶ X} {k : W ⟶ Y} (comm : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g) [CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Limits.cospan f g) G] (l : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk (G.map h) (G.map k) ⋯)) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk h k comm)

The property of reflecting pullbacks expressed in terms of binary fans.

Equations

• CategoryTheory.Limits.isLimitOfIsLimitPullbackConeMap G comm l = CategoryTheory.Limits.ReflectsLimit.reflects ((CategoryTheory.Limits.isLimitMapConePullbackConeEquiv G comm).symm l)

def CategoryTheory.Limits.isLimitOfHasPullbackOfPreservesLimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} {Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) G] [i : CategoryTheory.Limits.HasPullback f g] : let_fun this := ⋯; CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk (G.map CategoryTheory.Limits.pullback.fst) (G.map CategoryTheory.Limits.pullback.snd) this)

If G preserves pullbacks and C has them, then the pullback cone constructed of the mapped morphisms of the pullback cone is a limit.

Equations

• CategoryTheory.Limits.isLimitOfHasPullbackOfPreservesLimit G f g = CategoryTheory.Limits.isLimitPullbackConeMapOfIsLimit G ⋯ (CategoryTheory.Limits.pullbackIsPullback f g)

def CategoryTheory.Limits.preservesPullbackSymmetry {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} {Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) G] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan g f) G

If F preserves the pullback of f, g, it also preserves the pullback of g, f.

Equations

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

theorem CategoryTheory.Limits.hasPullback_of_preservesPullback {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} {Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) G] [CategoryTheory.Limits.HasPullback f g] : CategoryTheory.Limits.HasPullback (G.map f) (G.map g)

def CategoryTheory.Limits.PreservesPullback.iso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} {Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) G] [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback (G.map f) (G.map g)] : G.obj (CategoryTheory.Limits.pullback f g) ≅ CategoryTheory.Limits.pullback (G.map f) (G.map g)

If G preserves the pullback of (f,g), then the pullback comparison map for G at (f,g) is an isomorphism.

Equations

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

theorem CategoryTheory.Limits.PreservesPullback.iso_hom_fst_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} {Z : C} (f : X ⟶ Z✝) (g : Y ⟶ Z✝) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) G] [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback (G.map f) (G.map g)] {Z : D} (h : G.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesPullback.iso G f g).hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h) = CategoryTheory.CategoryStruct.comp (G.map CategoryTheory.Limits.pullback.fst) h

theorem CategoryTheory.Limits.PreservesPullback.iso_hom_fst {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} {Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) G] [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback (G.map f) (G.map g)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesPullback.iso G f g).hom CategoryTheory.Limits.pullback.fst = G.map CategoryTheory.Limits.pullback.fst

theorem CategoryTheory.Limits.PreservesPullback.iso_hom_snd_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} {Z : C} (f : X ⟶ Z✝) (g : Y ⟶ Z✝) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) G] [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback (G.map f) (G.map g)] {Z : D} (h : G.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesPullback.iso G f g).hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h) = CategoryTheory.CategoryStruct.comp (G.map CategoryTheory.Limits.pullback.snd) h

theorem CategoryTheory.Limits.PreservesPullback.iso_hom_snd {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} {Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) G] [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback (G.map f) (G.map g)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesPullback.iso G f g).hom CategoryTheory.Limits.pullback.snd = G.map CategoryTheory.Limits.pullback.snd

@[simp]

theorem CategoryTheory.Limits.PreservesPullback.iso_inv_fst_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} {Z : C} (f : X ⟶ Z✝) (g : Y ⟶ Z✝) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) G] [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback (G.map f) (G.map g)] {Z : D} (h : G.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesPullback.iso G f g).inv (CategoryTheory.CategoryStruct.comp (G.map CategoryTheory.Limits.pullback.fst) h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h

@[simp]

theorem CategoryTheory.Limits.PreservesPullback.iso_inv_fst {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} {Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) G] [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback (G.map f) (G.map g)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesPullback.iso G f g).inv (G.map CategoryTheory.Limits.pullback.fst) = CategoryTheory.Limits.pullback.fst

@[simp]

theorem CategoryTheory.Limits.PreservesPullback.iso_inv_snd_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} {Z : C} (f : X ⟶ Z✝) (g : Y ⟶ Z✝) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) G] [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback (G.map f) (G.map g)] {Z : D} (h : G.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesPullback.iso G f g).inv (CategoryTheory.CategoryStruct.comp (G.map CategoryTheory.Limits.pullback.snd) h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h

@[simp]

theorem CategoryTheory.Limits.PreservesPullback.iso_inv_snd {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} {Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) G] [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback (G.map f) (G.map g)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesPullback.iso G f g).inv (G.map CategoryTheory.Limits.pullback.snd) = CategoryTheory.Limits.pullback.snd

def CategoryTheory.Limits.isColimitMapCoconePushoutCoconeEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {W : C} {X : C} {Y : C} {Z : C} {h : X ⟶ Z} {k : Y ⟶ Z} {f : W ⟶ X} {g : W ⟶ Y} (comm : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k) : CategoryTheory.Limits.IsColimit (G.mapCocone (CategoryTheory.Limits.PushoutCocone.mk h k comm)) ≃ CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk (G.map h) (G.map k) ⋯)

The map of a pushout cocone is a colimit iff the cofork consisting of the mapped morphisms is a colimit. This essentially lets us commute PushoutCocone.mk with Functor.mapCocone.

Equations

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

def CategoryTheory.Limits.isColimitPushoutCoconeMapOfIsColimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {W : C} {X : C} {Y : C} {Z : C} {h : X ⟶ Z} {k : Y ⟶ Z} {f : W ⟶ X} {g : W ⟶ Y} (comm : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) G] (l : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk h k comm)) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk (G.map h) (G.map k) ⋯)

The property of preserving pushouts expressed in terms of binary cofans.

Equations

• CategoryTheory.Limits.isColimitPushoutCoconeMapOfIsColimit G comm l = (CategoryTheory.Limits.isColimitMapCoconePushoutCoconeEquiv G comm) (CategoryTheory.Limits.PreservesColimit.preserves l)

def CategoryTheory.Limits.isColimitOfIsColimitPushoutCoconeMap {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {W : C} {X : C} {Y : C} {Z : C} {h : X ⟶ Z} {k : Y ⟶ Z} {f : W ⟶ X} {g : W ⟶ Y} (comm : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k) [CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Limits.span f g) G] (l : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk (G.map h) (G.map k) ⋯)) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk h k comm)

The property of reflecting pushouts expressed in terms of binary cofans.

Equations

• CategoryTheory.Limits.isColimitOfIsColimitPushoutCoconeMap G comm l = CategoryTheory.Limits.ReflectsColimit.reflects ((CategoryTheory.Limits.isColimitMapCoconePushoutCoconeEquiv G comm).symm l)

def CategoryTheory.Limits.isColimitOfHasPushoutOfPreservesColimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {W : C} {X : C} {Y : C} (f : W ⟶ X) (g : W ⟶ Y) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) G] [i : CategoryTheory.Limits.HasPushout f g] : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk (G.map CategoryTheory.Limits.pushout.inl) (G.map CategoryTheory.Limits.pushout.inr) ⋯)

If G preserves pushouts and C has them, then the pushout cocone constructed of the mapped morphisms of the pushout cocone is a colimit.

Equations

• CategoryTheory.Limits.isColimitOfHasPushoutOfPreservesColimit G f g = CategoryTheory.Limits.isColimitPushoutCoconeMapOfIsColimit G ⋯ (CategoryTheory.Limits.pushoutIsPushout f g)

def CategoryTheory.Limits.preservesPushoutSymmetry {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {W : C} {X : C} {Y : C} (f : W ⟶ X) (g : W ⟶ Y) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) G] : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span g f) G

If F preserves the pushout of f, g, it also preserves the pushout of g, f.

Equations

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

theorem CategoryTheory.Limits.hasPushout_of_preservesPushout {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {W : C} {X : C} {Y : C} (f : W ⟶ X) (g : W ⟶ Y) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) G] [CategoryTheory.Limits.HasPushout f g] : CategoryTheory.Limits.HasPushout (G.map f) (G.map g)

def CategoryTheory.Limits.PreservesPushout.iso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {W : C} {X : C} {Y : C} (f : W ⟶ X) (g : W ⟶ Y) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) G] [CategoryTheory.Limits.HasPushout f g] [CategoryTheory.Limits.HasPushout (G.map f) (G.map g)] : CategoryTheory.Limits.pushout (G.map f) (G.map g) ≅ G.obj (CategoryTheory.Limits.pushout f g)

If G preserves the pushout of (f,g), then the pushout comparison map for G at (f,g) is an isomorphism.

Equations

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

theorem CategoryTheory.Limits.PreservesPushout.inl_iso_hom_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {W : C} {X : C} {Y : C} (f : W ⟶ X) (g : W ⟶ Y) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) G] [CategoryTheory.Limits.HasPushout f g] [CategoryTheory.Limits.HasPushout (G.map f) (G.map g)] {Z : D} (h : G.obj (CategoryTheory.Limits.pushout f g) ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesPushout.iso G f g).hom h) = CategoryTheory.CategoryStruct.comp (G.map CategoryTheory.Limits.pushout.inl) h

theorem CategoryTheory.Limits.PreservesPushout.inl_iso_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {W : C} {X : C} {Y : C} (f : W ⟶ X) (g : W ⟶ Y) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) G] [CategoryTheory.Limits.HasPushout f g] [CategoryTheory.Limits.HasPushout (G.map f) (G.map g)] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.PreservesPushout.iso G f g).hom = G.map CategoryTheory.Limits.pushout.inl

theorem CategoryTheory.Limits.PreservesPushout.inr_iso_hom_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {W : C} {X : C} {Y : C} (f : W ⟶ X) (g : W ⟶ Y) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) G] [CategoryTheory.Limits.HasPushout f g] [CategoryTheory.Limits.HasPushout (G.map f) (G.map g)] {Z : D} (h : G.obj (CategoryTheory.Limits.pushout f g) ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesPushout.iso G f g).hom h) = CategoryTheory.CategoryStruct.comp (G.map CategoryTheory.Limits.pushout.inr) h

theorem CategoryTheory.Limits.PreservesPushout.inr_iso_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {W : C} {X : C} {Y : C} (f : W ⟶ X) (g : W ⟶ Y) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) G] [CategoryTheory.Limits.HasPushout f g] [CategoryTheory.Limits.HasPushout (G.map f) (G.map g)] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.PreservesPushout.iso G f g).hom = G.map CategoryTheory.Limits.pushout.inr

@[simp]

theorem CategoryTheory.Limits.PreservesPushout.inl_iso_inv_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {W : C} {X : C} {Y : C} (f : W ⟶ X) (g : W ⟶ Y) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) G] [CategoryTheory.Limits.HasPushout f g] [CategoryTheory.Limits.HasPushout (G.map f) (G.map g)] {Z : D} (h : CategoryTheory.Limits.pushout (G.map f) (G.map g) ⟶ Z) : CategoryTheory.CategoryStruct.comp (G.map CategoryTheory.Limits.pushout.inl) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesPushout.iso G f g).inv h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl h

@[simp]

theorem CategoryTheory.Limits.PreservesPushout.inl_iso_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {W : C} {X : C} {Y : C} (f : W ⟶ X) (g : W ⟶ Y) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) G] [CategoryTheory.Limits.HasPushout f g] [CategoryTheory.Limits.HasPushout (G.map f) (G.map g)] : CategoryTheory.CategoryStruct.comp (G.map CategoryTheory.Limits.pushout.inl) (CategoryTheory.Limits.PreservesPushout.iso G f g).inv = CategoryTheory.Limits.pushout.inl

@[simp]

theorem CategoryTheory.Limits.PreservesPushout.inr_iso_inv_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {W : C} {X : C} {Y : C} (f : W ⟶ X) (g : W ⟶ Y) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) G] [CategoryTheory.Limits.HasPushout f g] [CategoryTheory.Limits.HasPushout (G.map f) (G.map g)] {Z : D} (h : CategoryTheory.Limits.pushout (G.map f) (G.map g) ⟶ Z) : CategoryTheory.CategoryStruct.comp (G.map CategoryTheory.Limits.pushout.inr) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesPushout.iso G f g).inv h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr h

@[simp]

theorem CategoryTheory.Limits.PreservesPushout.inr_iso_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {W : C} {X : C} {Y : C} (f : W ⟶ X) (g : W ⟶ Y) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) G] [CategoryTheory.Limits.HasPushout f g] [CategoryTheory.Limits.HasPushout (G.map f) (G.map g)] : CategoryTheory.CategoryStruct.comp (G.map CategoryTheory.Limits.pushout.inr) (CategoryTheory.Limits.PreservesPushout.iso G f g).inv = CategoryTheory.Limits.pushout.inr

def CategoryTheory.Limits.PreservesPullback.ofIsoComparison {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} {Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback (G.map f) (G.map g)] [i : CategoryTheory.IsIso (CategoryTheory.Limits.pullbackComparison G f g)] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) G

If the pullback comparison map for G at (f,g) is an isomorphism, then G preserves the pullback of (f,g).

Equations

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

@[simp]

theorem CategoryTheory.Limits.PreservesPullback.iso_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} {Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback (G.map f) (G.map g)] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) G] : (CategoryTheory.Limits.PreservesPullback.iso G f g).hom = CategoryTheory.Limits.pullbackComparison G f g

instance CategoryTheory.Limits.instIsIsoObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorPullbackPullbackMapPullbackComparison {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} {Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback (G.map f) (G.map g)] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) G] : CategoryTheory.IsIso (CategoryTheory.Limits.pullbackComparison G f g)

Equations

• ⋯ = ⋯

def CategoryTheory.Limits.PreservesPushout.ofIsoComparison {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} {Z : C} {f : X ⟶ Y} {g : X ⟶ Z} [CategoryTheory.Limits.HasPushout f g] [CategoryTheory.Limits.HasPushout (G.map f) (G.map g)] [i : CategoryTheory.IsIso (CategoryTheory.Limits.pushoutComparison G f g)] : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) G

If the pushout comparison map for G at (f,g) is an isomorphism, then G preserves the pushout of (f,g).

Equations

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

@[simp]

theorem CategoryTheory.Limits.PreservesPushout.iso_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} {Z : C} {f : X ⟶ Y} {g : X ⟶ Z} [CategoryTheory.Limits.HasPushout f g] [CategoryTheory.Limits.HasPushout (G.map f) (G.map g)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) G] : (CategoryTheory.Limits.PreservesPushout.iso G f g).hom = CategoryTheory.Limits.pushoutComparison G f g

instance CategoryTheory.Limits.instIsIsoPushoutObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorMapPushoutPushoutComparison {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} {Z : C} {f : X ⟶ Y} {g : X ⟶ Z} [CategoryTheory.Limits.HasPushout f g] [CategoryTheory.Limits.HasPushout (G.map f) (G.map g)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) G] : CategoryTheory.IsIso (CategoryTheory.Limits.pushoutComparison G f g)

Equations

• ⋯ = ⋯