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

@[reducible, inline]

abbrev CategoryTheory.Limits.PullbackCone.map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X : C} {Y : C} {Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (c : CategoryTheory.Limits.PullbackCone f g) (G : CategoryTheory.Functor C D) : CategoryTheory.Limits.PullbackCone (G.map f) (G.map g)

The image of a pullback cone by a functor.

Equations

• c.map G = CategoryTheory.Limits.PullbackCone.mk (G.map c.fst) (G.map c.snd) ⋯

def CategoryTheory.Limits.PullbackCone.isLimitMapConeEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X : C} {Y : C} {Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (c : CategoryTheory.Limits.PullbackCone f g) (G : CategoryTheory.Functor C D) : CategoryTheory.Limits.IsLimit (G.mapCone c) ≃ CategoryTheory.Limits.IsLimit (c.map G)

The map (as a cone) of a pullback cone is limit iff the map (as a pullback cone) is limit.

Equations

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

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

• CategoryTheory.Limits.isLimitMapConePullbackConeEquiv G comm = (CategoryTheory.Limits.PullbackCone.mk h k comm).isLimitMapConeEquiv G

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

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

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.PullbackCone.mk h k comm).isLimitMapConeEquiv G).invFun 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] [CategoryTheory.Limits.HasPullback f g] : let_fun this := ⋯; CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk (G.map (CategoryTheory.Limits.pullback.fst f g)) (G.map (CategoryTheory.Limits.pullback.snd f g)) 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.

@[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.PreservesLimit (CategoryTheory.Limits.cospan f g) G] [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback (G.map f) (G.map g)] : (CategoryTheory.Limits.PreservesPullback.iso G f g).hom = CategoryTheory.Limits.pullbackComparison G f g

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 (G.map f) (G.map g)) h) = CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.pullback.fst f g)) 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 f) (G.map g)) = G.map (CategoryTheory.Limits.pullback.fst f g)

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 (G.map f) (G.map g)) h) = CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.pullback.snd f g)) 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 f) (G.map g)) = G.map (CategoryTheory.Limits.pullback.snd f g)

@[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 f g)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (G.map f) (G.map g)) 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 f g)) = CategoryTheory.Limits.pullback.fst (G.map f) (G.map g)

@[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 f g)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (G.map f) (G.map g)) 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 f g)) = CategoryTheory.Limits.pullback.snd (G.map f) (G.map g)

def CategoryTheory.Limits.PullbackCone.isLimitCoyonedaEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (c : CategoryTheory.Limits.PullbackCone f g) : CategoryTheory.Limits.IsLimit c ≃ ((X_1 : Cᵒᵖ) → CategoryTheory.Limits.IsLimit (c.map (CategoryTheory.coyoneda.obj X_1)))

A pullback cone in C is limit iff if it is so after the application of coyoneda.obj X for all X : Cᵒᵖ.

Equations

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

@[reducible, inline]

abbrev CategoryTheory.Limits.PushoutCocone.map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {W : C} {X : C} {Y : C} {f : W ⟶ X} {g : W ⟶ Y} (c : CategoryTheory.Limits.PushoutCocone f g) (G : CategoryTheory.Functor C D) : CategoryTheory.Limits.PushoutCocone (G.map f) (G.map g)

The image of a pullback cone by a functor.

Equations

• c.map G = CategoryTheory.Limits.PushoutCocone.mk (G.map c.inl) (G.map c.inr) ⋯

def CategoryTheory.Limits.PushoutCocone.isColimitMapCoconeEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {W : C} {X : C} {Y : C} {f : W ⟶ X} {g : W ⟶ Y} (c : CategoryTheory.Limits.PushoutCocone f g) (G : CategoryTheory.Functor C D) : CategoryTheory.Limits.IsColimit (G.mapCocone c) ≃ CategoryTheory.Limits.IsColimit (c.map G)

The map (as a cocone) of a pushout cocone is colimit iff the map (as a pushout cocone) is limit.

Equations

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

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 f g)) (G.map (CategoryTheory.Limits.pushout.inr f g)) ⋯)

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.

@[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) {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.PreservesPushout.iso G f g).hom = CategoryTheory.Limits.pushoutComparison G f g

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 (G.map f) (G.map g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesPushout.iso G f g).hom h) = CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.pushout.inl f g)) 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 (G.map f) (G.map g)) (CategoryTheory.Limits.PreservesPushout.iso G f g).hom = G.map (CategoryTheory.Limits.pushout.inl f g)

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 (G.map f) (G.map g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesPushout.iso G f g).hom h) = CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.pushout.inr f g)) 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 (G.map f) (G.map g)) (CategoryTheory.Limits.PreservesPushout.iso G f g).hom = G.map (CategoryTheory.Limits.pushout.inr f g)

@[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 f g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesPushout.iso G f g).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl (G.map f) (G.map g)) 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 f g)) (CategoryTheory.Limits.PreservesPushout.iso G f g).inv = CategoryTheory.Limits.pushout.inl (G.map f) (G.map g)

@[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 f g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesPushout.iso G f g).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr (G.map f) (G.map g)) 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 f g)) (CategoryTheory.Limits.PreservesPushout.iso G f g).inv = CategoryTheory.Limits.pushout.inr (G.map f) (G.map g)

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.

instance CategoryTheory.Limits.instIsIsoPullbackComparison {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.

instance CategoryTheory.Limits.instIsIsoPushoutComparison {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

• ⋯ = ⋯

def CategoryTheory.Limits.PushoutCocone.isColimitYonedaEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (c : CategoryTheory.Limits.PushoutCocone f g) : CategoryTheory.Limits.IsColimit c ≃ ((X_1 : C) → CategoryTheory.Limits.IsLimit (c.op.map (CategoryTheory.yoneda.obj X_1)))

A pushout cocone in C is colimit iff it becomes limit after the application of yoneda.obj X for all X : C.

Equations

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