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.
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) ⋯))
:
The property of reflecting pullbacks expressed in terms of binary fans.
Equations
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.
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]
:
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.
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) ⋯))
:
The property of reflecting pushouts expressed in terms of binary cofans.
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.
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]
:
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)]
:
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]
:
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]
:
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)]
:
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]
:
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]
:
Equations
- ⋯ = ⋯