# Documentation

Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

# 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₁} [] {D : Type u₂} [] (G : ) {W : C} {X : C} {Y : C} {Z : C} {f : X Z} {g : Y Z} {h : W X} {k : W Y} (comm : ) :

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.

Instances For
def CategoryTheory.Limits.isLimitPullbackConeMapOfIsLimit {C : Type u₁} [] {D : Type u₂} [] (G : ) {W : C} {X : C} {Y : C} {Z : C} {f : X Z} {g : Y Z} {h : W X} {k : W Y} (comm : ) (l : ) :
let_fun this := (_ : CategoryTheory.CategoryStruct.comp (G.map h) (G.map f) = CategoryTheory.CategoryStruct.comp (G.map k) (G.map g)); 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.

Instances For
def CategoryTheory.Limits.isLimitOfIsLimitPullbackConeMap {C : Type u₁} [] {D : Type u₂} [] (G : ) {W : C} {X : C} {Y : C} {Z : C} {f : X Z} {g : Y Z} {h : W X} {k : W Y} (comm : ) (l : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk (G.map h) (G.map k) (_ : CategoryTheory.CategoryStruct.comp (G.map h) (G.map f) = CategoryTheory.CategoryStruct.comp (G.map k) (G.map g)))) :

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

Instances For
def CategoryTheory.Limits.isLimitOfHasPullbackOfPreservesLimit {C : Type u₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} {Z : C} (f : X Z) (g : Y Z) [i : ] :
let_fun this := (_ : CategoryTheory.CategoryStruct.comp (G.map CategoryTheory.Limits.pullback.fst) (G.map f) = CategoryTheory.CategoryStruct.comp (G.map CategoryTheory.Limits.pullback.snd) (G.map g)); 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.

Instances For
def CategoryTheory.Limits.preservesPullbackSymmetry {C : Type u₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} {Z : C} (f : X Z) (g : Y Z) :

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

Instances For
theorem CategoryTheory.Limits.hasPullback_of_preservesPullback {C : Type u₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} {Z : C} (f : X Z) (g : Y Z) :
def CategoryTheory.Limits.PreservesPullback.iso {C : Type u₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} {Z : C} (f : X Z) (g : Y Z) [CategoryTheory.Limits.HasPullback (G.map f) (G.map g)] :
G.obj () 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.

Instances For
theorem CategoryTheory.Limits.PreservesPullback.iso_hom_fst_assoc {C : Type u₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} {Z : C} (f : X Z) (g : Y Z) [CategoryTheory.Limits.HasPullback (G.map f) (G.map g)] {Z : D} (h : G.obj X Z) :
CategoryTheory.CategoryStruct.comp ().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₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} {Z : C} (f : X Z) (g : Y Z) [CategoryTheory.Limits.HasPullback (G.map f) (G.map g)] :
CategoryTheory.CategoryStruct.comp ().hom CategoryTheory.Limits.pullback.fst = G.map CategoryTheory.Limits.pullback.fst
theorem CategoryTheory.Limits.PreservesPullback.iso_hom_snd_assoc {C : Type u₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} {Z : C} (f : X Z) (g : Y Z) [CategoryTheory.Limits.HasPullback (G.map f) (G.map g)] {Z : D} (h : G.obj Y Z) :
CategoryTheory.CategoryStruct.comp ().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₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} {Z : C} (f : X Z) (g : Y Z) [CategoryTheory.Limits.HasPullback (G.map f) (G.map g)] :
CategoryTheory.CategoryStruct.comp ().hom CategoryTheory.Limits.pullback.snd = G.map CategoryTheory.Limits.pullback.snd
@[simp]
theorem CategoryTheory.Limits.PreservesPullback.iso_inv_fst_assoc {C : Type u₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} {Z : C} (f : X Z) (g : Y Z) [CategoryTheory.Limits.HasPullback (G.map f) (G.map g)] {Z : D} (h : G.obj X Z) :
CategoryTheory.CategoryStruct.comp ().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₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} {Z : C} (f : X Z) (g : Y Z) [CategoryTheory.Limits.HasPullback (G.map f) (G.map g)] :
CategoryTheory.CategoryStruct.comp ().inv (G.map CategoryTheory.Limits.pullback.fst) = CategoryTheory.Limits.pullback.fst
@[simp]
theorem CategoryTheory.Limits.PreservesPullback.iso_inv_snd_assoc {C : Type u₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} {Z : C} (f : X Z) (g : Y Z) [CategoryTheory.Limits.HasPullback (G.map f) (G.map g)] {Z : D} (h : G.obj Y Z) :
CategoryTheory.CategoryStruct.comp ().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₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} {Z : C} (f : X Z) (g : Y Z) [CategoryTheory.Limits.HasPullback (G.map f) (G.map g)] :
CategoryTheory.CategoryStruct.comp ().inv (G.map CategoryTheory.Limits.pullback.snd) = CategoryTheory.Limits.pullback.snd
def CategoryTheory.Limits.isColimitMapCoconePushoutCoconeEquiv {C : Type u₁} [] {D : Type u₂} [] (G : ) {W : C} {X : C} {Y : C} {Z : C} {h : X Z} {k : Y Z} {f : W X} {g : W Y} (comm : ) :

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.

Instances For
def CategoryTheory.Limits.isColimitPushoutCoconeMapOfIsColimit {C : Type u₁} [] {D : Type u₂} [] (G : ) {W : C} {X : C} {Y : C} {Z : C} {h : X Z} {k : Y Z} {f : W X} {g : W Y} (comm : ) :

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

Instances For
def CategoryTheory.Limits.isColimitOfIsColimitPushoutCoconeMap {C : Type u₁} [] {D : Type u₂} [] (G : ) {W : C} {X : C} {Y : C} {Z : C} {h : X Z} {k : Y Z} {f : W X} {g : W Y} (comm : ) (l : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk (G.map h) (G.map k) (_ : CategoryTheory.CategoryStruct.comp (G.map f) (G.map h) = CategoryTheory.CategoryStruct.comp (G.map g) (G.map k)))) :

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

Instances For
def CategoryTheory.Limits.isColimitOfHasPushoutOfPreservesColimit {C : Type u₁} [] {D : Type u₂} [] (G : ) {W : C} {X : C} {Y : C} (f : W X) (g : W Y) [i : ] :
CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk (G.map CategoryTheory.Limits.pushout.inl) (G.map CategoryTheory.Limits.pushout.inr) (_ : CategoryTheory.CategoryStruct.comp (G.map f) (G.map CategoryTheory.Limits.pushout.inl) = CategoryTheory.CategoryStruct.comp (G.map g) (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.

Instances For
def CategoryTheory.Limits.preservesPushoutSymmetry {C : Type u₁} [] {D : Type u₂} [] (G : ) {W : C} {X : C} {Y : C} (f : W X) (g : W Y) :

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

Instances For
theorem CategoryTheory.Limits.hasPushout_of_preservesPushout {C : Type u₁} [] {D : Type u₂} [] (G : ) {W : C} {X : C} {Y : C} (f : W X) (g : W Y) :
def CategoryTheory.Limits.PreservesPushout.iso {C : Type u₁} [] {D : Type u₂} [] (G : ) {W : C} {X : C} {Y : C} (f : W X) (g : W Y) [CategoryTheory.Limits.HasPushout (G.map f) (G.map g)] :
CategoryTheory.Limits.pushout (G.map f) (G.map g) G.obj ()

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

Instances For
theorem CategoryTheory.Limits.PreservesPushout.inl_iso_hom_assoc {C : Type u₁} [] {D : Type u₂} [] (G : ) {W : C} {X : C} {Y : C} (f : W X) (g : W Y) [CategoryTheory.Limits.HasPushout (G.map f) (G.map g)] {Z : D} (h : G.obj () Z) :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl () = CategoryTheory.CategoryStruct.comp (G.map CategoryTheory.Limits.pushout.inl) h
theorem CategoryTheory.Limits.PreservesPushout.inl_iso_hom {C : Type u₁} [] {D : Type u₂} [] (G : ) {W : C} {X : C} {Y : C} (f : W X) (g : W Y) [CategoryTheory.Limits.HasPushout (G.map f) (G.map g)] :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl ().hom = G.map CategoryTheory.Limits.pushout.inl
theorem CategoryTheory.Limits.PreservesPushout.inr_iso_hom_assoc {C : Type u₁} [] {D : Type u₂} [] (G : ) {W : C} {X : C} {Y : C} (f : W X) (g : W Y) [CategoryTheory.Limits.HasPushout (G.map f) (G.map g)] {Z : D} (h : G.obj () Z) :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr () = CategoryTheory.CategoryStruct.comp (G.map CategoryTheory.Limits.pushout.inr) h
theorem CategoryTheory.Limits.PreservesPushout.inr_iso_hom {C : Type u₁} [] {D : Type u₂} [] (G : ) {W : C} {X : C} {Y : C} (f : W X) (g : W Y) [CategoryTheory.Limits.HasPushout (G.map f) (G.map g)] :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr ().hom = G.map CategoryTheory.Limits.pushout.inr
@[simp]
theorem CategoryTheory.Limits.PreservesPushout.inl_iso_inv_assoc {C : Type u₁} [] {D : Type u₂} [] (G : ) {W : C} {X : C} {Y : C} (f : W X) (g : W Y) [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.pushout.inl h
@[simp]
theorem CategoryTheory.Limits.PreservesPushout.inl_iso_inv {C : Type u₁} [] {D : Type u₂} [] (G : ) {W : C} {X : C} {Y : C} (f : W X) (g : W Y) [CategoryTheory.Limits.HasPushout (G.map f) (G.map g)] :
CategoryTheory.CategoryStruct.comp (G.map CategoryTheory.Limits.pushout.inl) ().inv = CategoryTheory.Limits.pushout.inl
@[simp]
theorem CategoryTheory.Limits.PreservesPushout.inr_iso_inv_assoc {C : Type u₁} [] {D : Type u₂} [] (G : ) {W : C} {X : C} {Y : C} (f : W X) (g : W Y) [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.pushout.inr h
@[simp]
theorem CategoryTheory.Limits.PreservesPushout.inr_iso_inv {C : Type u₁} [] {D : Type u₂} [] (G : ) {W : C} {X : C} {Y : C} (f : W X) (g : W Y) [CategoryTheory.Limits.HasPushout (G.map f) (G.map g)] :
CategoryTheory.CategoryStruct.comp (G.map CategoryTheory.Limits.pushout.inr) ().inv = CategoryTheory.Limits.pushout.inr
def CategoryTheory.Limits.PreservesPullback.ofIsoComparison {C : Type u₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} {Z : C} {f : X Z} {g : Y Z} [CategoryTheory.Limits.HasPullback (G.map f) (G.map g)] :

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

Instances For
@[simp]
theorem CategoryTheory.Limits.PreservesPullback.iso_hom {C : Type u₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} {Z : C} {f : X Z} {g : Y Z} [CategoryTheory.Limits.HasPullback (G.map f) (G.map g)] :
def CategoryTheory.Limits.PreservesPushout.ofIsoComparison {C : Type u₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} {Z : C} {f : X Y} {g : X Z} [CategoryTheory.Limits.HasPushout (G.map f) (G.map g)] :

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

Instances For
@[simp]
theorem CategoryTheory.Limits.PreservesPushout.iso_hom {C : Type u₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} {Z : C} {f : X Y} {g : X Z} [CategoryTheory.Limits.HasPushout (G.map f) (G.map g)] :