Pasting lemma

This file proves the pasting lemma for pullbacks. That is, given the following diagram:

  X₁ - f₁ -> X₂ - f₂ -> X₃
  |          |          |
  i₁         i₂         i₃
  ∨          ∨          ∨
  Y₁ - g₁ -> Y₂ - g₂ -> Y₃

if the right square is a pullback, then the left square is a pullback iff the big square is a pullback.

Main results

• pasteHorizIsPullback shows that the big square is a pullback if both the small squares are.
• leftSquareIsPullback shows that the left square is a pullback if the other two are.
• pullbackRightPullbackFstIso shows, using the pullback API, that W ×[X] (X ×[Z] Y) ≅ W ×[Z] Y.
• pullbackLeftPullbackSndIso shows, using the pullback API, that (X ×[Z] Y) ×[Y] W ≅ X ×[Z] W.

@[reducible, inline]

abbrev CategoryTheory.Limits.PullbackCone.pasteHoriz {C : Type u} [Category.{v, u} C] {X₃ Y₁ Y₂ Y₃ : C} {g₁ : Y₁ ⟶ Y₂} {g₂ : Y₂ ⟶ Y₃} {i₃ : X₃ ⟶ Y₃} (t₂ : PullbackCone g₂ i₃) {i₂ : t₂.pt ⟶ Y₂} (t₁ : PullbackCone g₁ i₂) (hi₂ : i₂ = t₂.fst) : PullbackCone (CategoryStruct.comp g₁ g₂) i₃

The PullbackCone obtained by pasting two PullbackCone's horizontally

Equations

• t₂.pasteHoriz t₁ hi₂ = CategoryTheory.Limits.PullbackCone.mk t₁.fst (CategoryTheory.CategoryStruct.comp t₁.snd t₂.snd) ⋯

def CategoryTheory.Limits.pasteHorizIsPullback {C : Type u} [Category.{v, u} C] {X₃ Y₁ Y₂ Y₃ : C} {g₁ : Y₁ ⟶ Y₂} {g₂ : Y₂ ⟶ Y₃} {i₃ : X₃ ⟶ Y₃} {t₂ : PullbackCone g₂ i₃} {i₂ : t₂.pt ⟶ Y₂} {t₁ : PullbackCone g₁ i₂} (hi₂ : i₂ = t₂.fst) (H : IsLimit t₂) (H' : IsLimit t₁) : IsLimit (t₂.pasteHoriz t₁ hi₂)

Given

X₁ - f₁ -> X₂ - f₂ -> X₃
|          |          |
i₁         i₂         i₃
↓          ↓          ↓
Y₁ - g₁ -> Y₂ - g₂ -> Y₃

Then the big square is a pullback if both the small squares are.

Equations

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

def CategoryTheory.Limits.leftSquareIsPullback {C : Type u} [Category.{v, u} C] {X₃ Y₁ Y₂ Y₃ : C} {g₁ : Y₁ ⟶ Y₂} {g₂ : Y₂ ⟶ Y₃} {i₃ : X₃ ⟶ Y₃} {t₂ : PullbackCone g₂ i₃} {i₂ : t₂.pt ⟶ Y₂} (t₁ : PullbackCone g₁ i₂) (hi₂ : i₂ = t₂.fst) (H : IsLimit t₂) (H' : IsLimit (t₂.pasteHoriz t₁ hi₂)) : IsLimit t₁

Given

X₁ - f₁ -> X₂ - f₂ -> X₃
|          |          |
i₁         i₂         i₃
↓          ↓          ↓
Y₁ - g₁ -> Y₂ - g₂ -> Y₃

Then the left square is a pullback if the right square and the big square are.

Equations

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

def CategoryTheory.Limits.pasteHorizIsPullbackEquiv {C : Type u} [Category.{v, u} C] {X₃ Y₁ Y₂ Y₃ : C} {g₁ : Y₁ ⟶ Y₂} {g₂ : Y₂ ⟶ Y₃} {i₃ : X₃ ⟶ Y₃} {t₂ : PullbackCone g₂ i₃} {i₂ : t₂.pt ⟶ Y₂} (t₁ : PullbackCone g₁ i₂) (hi₂ : i₂ = t₂.fst) (H : IsLimit t₂) : IsLimit (t₂.pasteHoriz t₁ hi₂) ≃ IsLimit t₁

Given that the right square is a pullback, the pasted square is a pullback iff the left square is.

Equations

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

@[reducible, inline]

abbrev CategoryTheory.Limits.PullbackCone.pasteVert {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ Y₁ : C} {f₁ : X₂ ⟶ X₁} {f₂ : X₃ ⟶ X₂} {i₁ : Y₁ ⟶ X₁} (t₁ : PullbackCone i₁ f₁) {i₂ : t₁.pt ⟶ X₂} (t₂ : PullbackCone i₂ f₂) (hi₂ : i₂ = t₁.snd) : PullbackCone i₁ (CategoryStruct.comp f₂ f₁)

The PullbackCone obtained by pasting two PullbackCone's vertically

Equations

• t₁.pasteVert t₂ hi₂ = CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.CategoryStruct.comp t₂.fst t₁.fst) t₂.snd ⋯

def CategoryTheory.Limits.PullbackCone.pasteVertFlip {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ Y₁ : C} {f₁ : X₂ ⟶ X₁} {f₂ : X₃ ⟶ X₂} {i₁ : Y₁ ⟶ X₁} (t₁ : PullbackCone i₁ f₁) {i₂ : t₁.pt ⟶ X₂} (t₂ : PullbackCone i₂ f₂) (hi₂ : i₂ = t₁.snd) : (t₁.pasteVert t₂ hi₂).flip ≅ t₁.flip.pasteHoriz t₂.flip hi₂

Pasting two pullback cones vertically is isomorphic to the pullback cone obtained by flipping them, pasting horizontally, and then flipping the result again.

Equations

• t₁.pasteVertFlip t₂ hi₂ = CategoryTheory.Limits.PullbackCone.ext (CategoryTheory.Iso.refl (t₁.pasteVert t₂ hi₂).flip.pt) ⋯ ⋯

def CategoryTheory.Limits.pasteVertIsPullback {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ Y₁ : C} {f₁ : X₂ ⟶ X₁} {f₂ : X₃ ⟶ X₂} {i₁ : Y₁ ⟶ X₁} {t₁ : PullbackCone i₁ f₁} {i₂ : t₁.pt ⟶ X₂} {t₂ : PullbackCone i₂ f₂} (hi₂ : i₂ = t₁.snd) (H₁ : IsLimit t₁) (H₂ : IsLimit t₂) : IsLimit (t₁.pasteVert t₂ hi₂)

Given

Y₃ - i₃ -> X₃
|          |
g₂         f₂
∨          ∨
Y₂ - i₂ -> X₂
|          |
g₁         f₁
∨          ∨
Y₁ - i₁ -> X₁

The big square is a pullback if both the small squares are.

Equations

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

def CategoryTheory.Limits.topSquareIsPullback {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ Y₁ : C} {f₁ : X₂ ⟶ X₁} {f₂ : X₃ ⟶ X₂} {i₁ : Y₁ ⟶ X₁} {t₁ : PullbackCone i₁ f₁} {i₂ : t₁.pt ⟶ X₂} (t₂ : PullbackCone i₂ f₂) (hi₂ : i₂ = t₁.snd) (H₁ : IsLimit t₁) (H₂ : IsLimit (t₁.pasteVert t₂ hi₂)) : IsLimit t₂

Given

Y₃ - i₃ -> X₃
|          |
g₂         f₂
∨          ∨
Y₂ - i₂ -> X₂
|          |
g₁         f₁
∨          ∨
Y₁ - i₁ -> X₁

The top square is a pullback if the bottom square and the big square are.

Equations

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

def CategoryTheory.Limits.pasteVertIsPullbackEquiv {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ Y₁ : C} {f₁ : X₂ ⟶ X₁} {f₂ : X₃ ⟶ X₂} {i₁ : Y₁ ⟶ X₁} {t₁ : PullbackCone i₁ f₁} {i₂ : t₁.pt ⟶ X₂} (t₂ : PullbackCone i₂ f₂) (hi₂ : i₂ = t₁.snd) (H : IsLimit t₁) : IsLimit (t₁.pasteVert t₂ hi₂) ≃ IsLimit t₂

Given that the bottom square is a pullback, the pasted square is a pullback iff the top square is.

Equations

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

@[reducible, inline]

abbrev CategoryTheory.Limits.PushoutCocone.pasteHoriz {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ Y₁ : C} {f₁ : X₁ ⟶ X₂} {f₂ : X₂ ⟶ X₃} {i₁ : X₁ ⟶ Y₁} (t₁ : PushoutCocone i₁ f₁) {i₂ : X₂ ⟶ t₁.pt} (t₂ : PushoutCocone i₂ f₂) (hi₂ : i₂ = t₁.inr) : PushoutCocone i₁ (CategoryStruct.comp f₁ f₂)

The pushout cocone obtained by pasting two pushout cocones horizontally.

Equations

• t₁.pasteHoriz t₂ hi₂ = CategoryTheory.Limits.PushoutCocone.mk (CategoryTheory.CategoryStruct.comp t₁.inl t₂.inl) t₂.inr ⋯

def CategoryTheory.Limits.pasteHorizIsPushout {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ Y₁ : C} {f₁ : X₁ ⟶ X₂} {f₂ : X₂ ⟶ X₃} {i₁ : X₁ ⟶ Y₁} {t₁ : PushoutCocone i₁ f₁} {i₂ : X₂ ⟶ t₁.pt} {t₂ : PushoutCocone i₂ f₂} (hi₂ : i₂ = t₁.inr) (H : IsColimit t₁) (H' : IsColimit t₂) : IsColimit (t₁.pasteHoriz t₂ hi₂)

Given

X₁ - f₁ -> X₂ - f₂ -> X₃
|          |          |
i₁         i₂         i₃
∨          ∨          ∨
Y₁ - g₁ -> Y₂ - g₂ -> Y₃

Then the big square is a pushout if both the small squares are.

Equations

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

def CategoryTheory.Limits.rightSquareIsPushout {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ Y₁ : C} {f₁ : X₁ ⟶ X₂} {f₂ : X₂ ⟶ X₃} {i₁ : X₁ ⟶ Y₁} {t₁ : PushoutCocone i₁ f₁} {i₂ : X₂ ⟶ t₁.pt} (t₂ : PushoutCocone i₂ f₂) (hi₂ : i₂ = t₁.inr) (H : IsColimit t₁) (H' : IsColimit (t₁.pasteHoriz t₂ hi₂)) : IsColimit t₂

Given

X₁ - f₁ -> X₂ - f₂ -> X₃ | | | i₁ i₂ i₃ ∨ ∨ ∨ Y₁ - g₁ -> Y₂ - g₂ -> Y₃

Then the right square is a pushout if the left square and the big square are.

Equations

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

def CategoryTheory.Limits.pasteHorizIsPushoutEquiv {C : Type u} [Category.{v, u} C] {X₁ X₂ X₃ Y₁ : C} {f₁ : X₁ ⟶ X₂} {f₂ : X₂ ⟶ X₃} {i₁ : X₁ ⟶ Y₁} {t₁ : PushoutCocone i₁ f₁} {i₂ : X₂ ⟶ t₁.pt} (t₂ : PushoutCocone i₂ f₂) (hi₂ : i₂ = t₁.inr) (H : IsColimit t₁) : IsColimit (t₁.pasteHoriz t₂ hi₂) ≃ IsColimit t₂

Given that the left square is a pushout, the pasted square is a pushout iff the right square is.

Equations

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

@[reducible, inline]

abbrev CategoryTheory.Limits.PushoutCocone.pasteVert {C : Type u} [Category.{v, u} C] {Y₃ Y₂ Y₁ X₃ : C} {g₂ : Y₃ ⟶ Y₂} {g₁ : Y₂ ⟶ Y₁} {i₃ : Y₃ ⟶ X₃} (t₁ : PushoutCocone g₂ i₃) {i₂ : Y₂ ⟶ t₁.pt} (t₂ : PushoutCocone g₁ i₂) (hi₂ : i₂ = t₁.inl) : PushoutCocone (CategoryStruct.comp g₂ g₁) i₃

The PullbackCone obtained by pasting two PullbackCone's vertically

Equations

• t₁.pasteVert t₂ hi₂ = CategoryTheory.Limits.PushoutCocone.mk t₂.inl (CategoryTheory.CategoryStruct.comp t₁.inr t₂.inr) ⋯

def CategoryTheory.Limits.PushoutCocone.pasteVertFlip {C : Type u} [Category.{v, u} C] {Y₃ Y₂ Y₁ X₃ : C} {g₂ : Y₃ ⟶ Y₂} {g₁ : Y₂ ⟶ Y₁} {i₃ : Y₃ ⟶ X₃} (t₁ : PushoutCocone g₂ i₃) {i₂ : Y₂ ⟶ t₁.pt} (t₂ : PushoutCocone g₁ i₂) (hi₂ : i₂ = t₁.inl) : (t₁.pasteVert t₂ hi₂).flip ≅ t₁.flip.pasteHoriz t₂.flip hi₂

Pasting two pushout cocones vertically is isomorphic to the pushout cocone obtained by flipping them, pasting horizontally, and then flipping the result again.

Equations

• t₁.pasteVertFlip t₂ hi₂ = CategoryTheory.Limits.PushoutCocone.ext (CategoryTheory.Iso.refl (t₁.pasteVert t₂ hi₂).flip.pt) ⋯ ⋯

def CategoryTheory.Limits.pasteVertIsPushout {C : Type u} [Category.{v, u} C] {Y₃ Y₂ Y₁ X₃ : C} {g₂ : Y₃ ⟶ Y₂} {g₁ : Y₂ ⟶ Y₁} {i₃ : Y₃ ⟶ X₃} {t₁ : PushoutCocone g₂ i₃} {i₂ : Y₂ ⟶ t₁.pt} {t₂ : PushoutCocone g₁ i₂} (hi₂ : i₂ = t₁.inl) (H₁ : IsColimit t₁) (H₂ : IsColimit t₂) : IsColimit (t₁.pasteVert t₂ hi₂)

Given

Y₃ - i₃ -> X₃
|          |
g₂         f₂
∨          ∨
Y₂ - i₂ -> X₂
|          |
g₁         f₁
∨          ∨
Y₁ - i₁ -> X₁

The big square is a pushout if both the small squares are.

Equations

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

def CategoryTheory.Limits.botSquareIsPushout {C : Type u} [Category.{v, u} C] {Y₃ Y₂ Y₁ X₃ : C} {g₂ : Y₃ ⟶ Y₂} {g₁ : Y₂ ⟶ Y₁} {i₃ : Y₃ ⟶ X₃} {t₁ : PushoutCocone g₂ i₃} {i₂ : Y₂ ⟶ t₁.pt} (t₂ : PushoutCocone g₁ i₂) (hi₂ : i₂ = t₁.inl) (H₁ : IsColimit t₁) (H₂ : IsColimit (t₁.pasteVert t₂ hi₂)) : IsColimit t₂

Given

Y₃ - i₃ -> X₃
|          |
g₂         f₂
∨          ∨
Y₂ - i₂ -> X₂
|          |
g₁         f₁
∨          ∨
Y₁ - i₁ -> X₁

The bottom square is a pushout if the top square and the big square are.

Equations

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

def CategoryTheory.Limits.pasteVertIsPushoutEquiv {C : Type u} [Category.{v, u} C] {Y₃ Y₂ Y₁ X₃ : C} {g₂ : Y₃ ⟶ Y₂} {g₁ : Y₂ ⟶ Y₁} {i₃ : Y₃ ⟶ X₃} {t₁ : PushoutCocone g₂ i₃} {i₂ : Y₂ ⟶ t₁.pt} (t₂ : PushoutCocone g₁ i₂) (hi₂ : i₂ = t₁.inl) (H : IsColimit t₁) : IsColimit (t₁.pasteVert t₂ hi₂) ≃ IsColimit t₂

Given that the top square is a pushout, the pasted square is a pushout iff the bottom square is.

Equations

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

instance CategoryTheory.Limits.hasPullbackHorizPaste {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (f' : W ⟶ X) [HasPullback f g] [HasPullback f' (pullback.fst f g)] : HasPullback (CategoryStruct.comp f' f) g

noncomputable def CategoryTheory.Limits.pullbackRightPullbackFstIso {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (f' : W ⟶ X) [HasPullback f g] [HasPullback f' (pullback.fst f g)] : pullback f' (pullback.fst f g) ≅ pullback (CategoryStruct.comp f' f) g

The canonical isomorphism W ×[X] (X ×[Z] Y) ≅ W ×[Z] Y

Equations

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

@[simp]

theorem CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_fst {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (f' : W ⟶ X) [HasPullback f g] [HasPullback f' (pullback.fst f g)] : CategoryStruct.comp (pullbackRightPullbackFstIso f g f').hom (pullback.fst (CategoryStruct.comp f' f) g) = pullback.fst f' (pullback.fst f g)

@[simp]

theorem CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_fst_assoc {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (f' : W ⟶ X) [HasPullback f g] [HasPullback f' (pullback.fst f g)] {Z✝ : C} (h : W ⟶ Z✝) : CategoryStruct.comp (pullbackRightPullbackFstIso f g f').hom (CategoryStruct.comp (pullback.fst (CategoryStruct.comp f' f) g) h) = CategoryStruct.comp (pullback.fst f' (pullback.fst f g)) h

@[simp]

theorem CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_snd {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (f' : W ⟶ X) [HasPullback f g] [HasPullback f' (pullback.fst f g)] : CategoryStruct.comp (pullbackRightPullbackFstIso f g f').hom (pullback.snd (CategoryStruct.comp f' f) g) = CategoryStruct.comp (pullback.snd f' (pullback.fst f g)) (pullback.snd f g)

@[simp]

theorem CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_snd_assoc {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (f' : W ⟶ X) [HasPullback f g] [HasPullback f' (pullback.fst f g)] {Z✝ : C} (h : Y ⟶ Z✝) : CategoryStruct.comp (pullbackRightPullbackFstIso f g f').hom (CategoryStruct.comp (pullback.snd (CategoryStruct.comp f' f) g) h) = CategoryStruct.comp (pullback.snd f' (pullback.fst f g)) (CategoryStruct.comp (pullback.snd f g) h)

@[simp]

theorem CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_fst {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (f' : W ⟶ X) [HasPullback f g] [HasPullback f' (pullback.fst f g)] : CategoryStruct.comp (pullbackRightPullbackFstIso f g f').inv (pullback.fst f' (pullback.fst f g)) = pullback.fst (CategoryStruct.comp f' f) g

@[simp]

theorem CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_fst_assoc {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (f' : W ⟶ X) [HasPullback f g] [HasPullback f' (pullback.fst f g)] {Z✝ : C} (h : W ⟶ Z✝) : CategoryStruct.comp (pullbackRightPullbackFstIso f g f').inv (CategoryStruct.comp (pullback.fst f' (pullback.fst f g)) h) = CategoryStruct.comp (pullback.fst (CategoryStruct.comp f' f) g) h

@[simp]

theorem CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_snd {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (f' : W ⟶ X) [HasPullback f g] [HasPullback f' (pullback.fst f g)] : CategoryStruct.comp (pullbackRightPullbackFstIso f g f').inv (CategoryStruct.comp (pullback.snd f' (pullback.fst f g)) (pullback.snd f g)) = pullback.snd (CategoryStruct.comp f' f) g

@[simp]

theorem CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_snd_assoc {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (f' : W ⟶ X) [HasPullback f g] [HasPullback f' (pullback.fst f g)] {Z✝ : C} (h : Y ⟶ Z✝) : CategoryStruct.comp (pullbackRightPullbackFstIso f g f').inv (CategoryStruct.comp (pullback.snd f' (pullback.fst f g)) (CategoryStruct.comp (pullback.snd f g) h)) = CategoryStruct.comp (pullback.snd (CategoryStruct.comp f' f) g) h

@[simp]

theorem CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_fst {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (f' : W ⟶ X) [HasPullback f g] [HasPullback f' (pullback.fst f g)] : CategoryStruct.comp (pullbackRightPullbackFstIso f g f').inv (CategoryStruct.comp (pullback.snd f' (pullback.fst f g)) (pullback.fst f g)) = CategoryStruct.comp (pullback.fst (CategoryStruct.comp f' f) g) f'

@[simp]

theorem CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_fst_assoc {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (f' : W ⟶ X) [HasPullback f g] [HasPullback f' (pullback.fst f g)] {Z✝ : C} (h : X ⟶ Z✝) : CategoryStruct.comp (pullbackRightPullbackFstIso f g f').inv (CategoryStruct.comp (pullback.snd f' (pullback.fst f g)) (CategoryStruct.comp (pullback.fst f g) h)) = CategoryStruct.comp (pullback.fst (CategoryStruct.comp f' f) g) (CategoryStruct.comp f' h)

instance CategoryTheory.Limits.hasPullbackVertPaste {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (g' : W ⟶ Y) [HasPullback f g] [HasPullback (pullback.snd f g) g'] : HasPullback f (CategoryStruct.comp g' g)

def CategoryTheory.Limits.pullbackLeftPullbackSndIso {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (g' : W ⟶ Y) [HasPullback f g] [HasPullback (pullback.snd f g) g'] : pullback (pullback.snd f g) g' ≅ pullback f (CategoryStruct.comp g' g)

The canonical isomorphism (X ×[Z] Y) ×[Y] W ≅ X ×[Z] W

Equations

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

@[simp]

theorem CategoryTheory.Limits.pullbackLeftPullbackSndIso_hom_fst {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (g' : W ⟶ Y) [HasPullback f g] [HasPullback (pullback.snd f g) g'] : CategoryStruct.comp (pullbackLeftPullbackSndIso f g g').hom (pullback.fst f (CategoryStruct.comp g' g)) = CategoryStruct.comp (pullback.fst (pullback.snd f g) g') (pullback.fst f g)

@[simp]

theorem CategoryTheory.Limits.pullbackLeftPullbackSndIso_hom_fst_assoc {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (g' : W ⟶ Y) [HasPullback f g] [HasPullback (pullback.snd f g) g'] {Z✝ : C} (h : X ⟶ Z✝) : CategoryStruct.comp (pullbackLeftPullbackSndIso f g g').hom (CategoryStruct.comp (pullback.fst f (CategoryStruct.comp g' g)) h) = CategoryStruct.comp (pullback.fst (pullback.snd f g) g') (CategoryStruct.comp (pullback.fst f g) h)

@[simp]

theorem CategoryTheory.Limits.pullbackLeftPullbackSndIso_hom_snd {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (g' : W ⟶ Y) [HasPullback f g] [HasPullback (pullback.snd f g) g'] : CategoryStruct.comp (pullbackLeftPullbackSndIso f g g').hom (pullback.snd f (CategoryStruct.comp g' g)) = pullback.snd (pullback.snd f g) g'

@[simp]

theorem CategoryTheory.Limits.pullbackLeftPullbackSndIso_hom_snd_assoc {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (g' : W ⟶ Y) [HasPullback f g] [HasPullback (pullback.snd f g) g'] {Z✝ : C} (h : W ⟶ Z✝) : CategoryStruct.comp (pullbackLeftPullbackSndIso f g g').hom (CategoryStruct.comp (pullback.snd f (CategoryStruct.comp g' g)) h) = CategoryStruct.comp (pullback.snd (pullback.snd f g) g') h

@[simp]

theorem CategoryTheory.Limits.pullbackLeftPullbackSndIso_inv_fst {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (g' : W ⟶ Y) [HasPullback f g] [HasPullback (pullback.snd f g) g'] : CategoryStruct.comp (pullbackLeftPullbackSndIso f g g').inv (CategoryStruct.comp (pullback.fst (pullback.snd f g) g') (pullback.fst f g)) = pullback.fst f (CategoryStruct.comp g' g)

@[simp]

theorem CategoryTheory.Limits.pullbackLeftPullbackSndIso_inv_fst_assoc {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (g' : W ⟶ Y) [HasPullback f g] [HasPullback (pullback.snd f g) g'] {Z✝ : C} (h : X ⟶ Z✝) : CategoryStruct.comp (pullbackLeftPullbackSndIso f g g').inv (CategoryStruct.comp (pullback.fst (pullback.snd f g) g') (CategoryStruct.comp (pullback.fst f g) h)) = CategoryStruct.comp (pullback.fst f (CategoryStruct.comp g' g)) h

@[simp]

theorem CategoryTheory.Limits.pullbackLeftPullbackSndIso_inv_snd_snd {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (g' : W ⟶ Y) [HasPullback f g] [HasPullback (pullback.snd f g) g'] : CategoryStruct.comp (pullbackLeftPullbackSndIso f g g').inv (pullback.snd (pullback.snd f g) g') = pullback.snd f (CategoryStruct.comp g' g)

@[simp]

theorem CategoryTheory.Limits.pullbackLeftPullbackSndIso_inv_snd_snd_assoc {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (g' : W ⟶ Y) [HasPullback f g] [HasPullback (pullback.snd f g) g'] {Z✝ : C} (h : W ⟶ Z✝) : CategoryStruct.comp (pullbackLeftPullbackSndIso f g g').inv (CategoryStruct.comp (pullback.snd (pullback.snd f g) g') h) = CategoryStruct.comp (pullback.snd f (CategoryStruct.comp g' g)) h

@[simp]

theorem CategoryTheory.Limits.pullbackLeftPullbackSndIso_inv_fst_snd {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (g' : W ⟶ Y) [HasPullback f g] [HasPullback (pullback.snd f g) g'] : CategoryStruct.comp (pullbackLeftPullbackSndIso f g g').inv (CategoryStruct.comp (pullback.fst (pullback.snd f g) g') (pullback.snd f g)) = CategoryStruct.comp (pullback.snd f (CategoryStruct.comp g' g)) g'

@[simp]

theorem CategoryTheory.Limits.pullbackLeftPullbackSndIso_inv_fst_snd_assoc {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (g' : W ⟶ Y) [HasPullback f g] [HasPullback (pullback.snd f g) g'] {Z✝ : C} (h : Y ⟶ Z✝) : CategoryStruct.comp (pullbackLeftPullbackSndIso f g g').inv (CategoryStruct.comp (pullback.fst (pullback.snd f g) g') (CategoryStruct.comp (pullback.snd f g) h)) = CategoryStruct.comp (pullback.snd f (CategoryStruct.comp g' g)) (CategoryStruct.comp g' h)

instance CategoryTheory.Limits.instHasPushoutComp {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (g' : Z ⟶ W) [HasPushout f g] [HasPushout (pushout.inr f g) g'] : HasPushout f (CategoryStruct.comp g g')

noncomputable def CategoryTheory.Limits.pushoutLeftPushoutInrIso {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (g' : Z ⟶ W) [HasPushout f g] [HasPushout (pushout.inr f g) g'] : pushout (pushout.inr f g) g' ≅ pushout f (CategoryStruct.comp g g')

The canonical isomorphism (Y ⨿[X] Z) ⨿[Z] W ≅ Y ⨿[X] W

Equations

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

@[simp]

theorem CategoryTheory.Limits.inl_pushoutLeftPushoutInrIso_inv {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (g' : Z ⟶ W) [HasPushout f g] [HasPushout (pushout.inr f g) g'] : CategoryStruct.comp (pushout.inl f (CategoryStruct.comp g g')) (pushoutLeftPushoutInrIso f g g').inv = CategoryStruct.comp (pushout.inl f g) (pushout.inl (pushout.inr f g) g')

@[simp]

theorem CategoryTheory.Limits.inl_pushoutLeftPushoutInrIso_inv_assoc {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (g' : Z ⟶ W) [HasPushout f g] [HasPushout (pushout.inr f g) g'] {Z✝ : C} (h : pushout (pushout.inr f g) g' ⟶ Z✝) : CategoryStruct.comp (pushout.inl f (CategoryStruct.comp g g')) (CategoryStruct.comp (pushoutLeftPushoutInrIso f g g').inv h) = CategoryStruct.comp (pushout.inl f g) (CategoryStruct.comp (pushout.inl (pushout.inr f g) g') h)

@[simp]

theorem CategoryTheory.Limits.inr_pushoutLeftPushoutInrIso_hom {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (g' : Z ⟶ W) [HasPushout f g] [HasPushout (pushout.inr f g) g'] : CategoryStruct.comp (pushout.inr (pushout.inr f g) g') (pushoutLeftPushoutInrIso f g g').hom = pushout.inr f (CategoryStruct.comp g g')

@[simp]

theorem CategoryTheory.Limits.inr_pushoutLeftPushoutInrIso_hom_assoc {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (g' : Z ⟶ W) [HasPushout f g] [HasPushout (pushout.inr f g) g'] {Z✝ : C} (h : pushout f (CategoryStruct.comp g g') ⟶ Z✝) : CategoryStruct.comp (pushout.inr (pushout.inr f g) g') (CategoryStruct.comp (pushoutLeftPushoutInrIso f g g').hom h) = CategoryStruct.comp (pushout.inr f (CategoryStruct.comp g g')) h

@[simp]

theorem CategoryTheory.Limits.inr_pushoutLeftPushoutInrIso_inv {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (g' : Z ⟶ W) [HasPushout f g] [HasPushout (pushout.inr f g) g'] : CategoryStruct.comp (pushout.inr f (CategoryStruct.comp g g')) (pushoutLeftPushoutInrIso f g g').inv = pushout.inr (pushout.inr f g) g'

@[simp]

theorem CategoryTheory.Limits.inr_pushoutLeftPushoutInrIso_inv_assoc {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (g' : Z ⟶ W) [HasPushout f g] [HasPushout (pushout.inr f g) g'] {Z✝ : C} (h : pushout (pushout.inr f g) g' ⟶ Z✝) : CategoryStruct.comp (pushout.inr f (CategoryStruct.comp g g')) (CategoryStruct.comp (pushoutLeftPushoutInrIso f g g').inv h) = CategoryStruct.comp (pushout.inr (pushout.inr f g) g') h

@[simp]

theorem CategoryTheory.Limits.inl_inl_pushoutLeftPushoutInrIso_hom {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (g' : Z ⟶ W) [HasPushout f g] [HasPushout (pushout.inr f g) g'] : CategoryStruct.comp (pushout.inl f g) (CategoryStruct.comp (pushout.inl (pushout.inr f g) g') (pushoutLeftPushoutInrIso f g g').hom) = pushout.inl f (CategoryStruct.comp g g')

@[simp]

theorem CategoryTheory.Limits.inl_inl_pushoutLeftPushoutInrIso_hom_assoc {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (g' : Z ⟶ W) [HasPushout f g] [HasPushout (pushout.inr f g) g'] {Z✝ : C} (h : pushout f (CategoryStruct.comp g g') ⟶ Z✝) : CategoryStruct.comp (pushout.inl f g) (CategoryStruct.comp (pushout.inl (pushout.inr f g) g') (CategoryStruct.comp (pushoutLeftPushoutInrIso f g g').hom h)) = CategoryStruct.comp (pushout.inl f (CategoryStruct.comp g g')) h

@[simp]

theorem CategoryTheory.Limits.inr_inl_pushoutLeftPushoutInrIso_hom {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (g' : Z ⟶ W) [HasPushout f g] [HasPushout (pushout.inr f g) g'] : CategoryStruct.comp (pushout.inr f g) (CategoryStruct.comp (pushout.inl (pushout.inr f g) g') (pushoutLeftPushoutInrIso f g g').hom) = CategoryStruct.comp g' (pushout.inr f (CategoryStruct.comp g g'))

@[simp]

theorem CategoryTheory.Limits.inr_inl_pushoutLeftPushoutInrIso_hom_assoc {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (g' : Z ⟶ W) [HasPushout f g] [HasPushout (pushout.inr f g) g'] {Z✝ : C} (h : pushout f (CategoryStruct.comp g g') ⟶ Z✝) : CategoryStruct.comp (pushout.inr f g) (CategoryStruct.comp (pushout.inl (pushout.inr f g) g') (CategoryStruct.comp (pushoutLeftPushoutInrIso f g g').hom h)) = CategoryStruct.comp g' (CategoryStruct.comp (pushout.inr f (CategoryStruct.comp g g')) h)

instance CategoryTheory.Limits.hasPushoutVertPaste {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (f' : Y ⟶ W) [HasPushout f g] [HasPushout f' (pushout.inl f g)] : HasPushout (CategoryStruct.comp f f') g

noncomputable def CategoryTheory.Limits.pushoutRightPushoutInlIso {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (f' : Y ⟶ W) [HasPushout f g] [HasPushout f' (pushout.inl f g)] : pushout f' (pushout.inl f g) ≅ pushout (CategoryStruct.comp f f') g

The canonical isomorphism W ⨿[Y] (Y ⨿[X] Z) ≅ W ⨿[X] Z

Equations

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

@[simp]

theorem CategoryTheory.Limits.inl_pushoutRightPushoutInlIso_inv {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (f' : Y ⟶ W) [HasPushout f g] [HasPushout f' (pushout.inl f g)] : CategoryStruct.comp (pushout.inl (CategoryStruct.comp f f') g) (pushoutRightPushoutInlIso f g f').inv = pushout.inl f' (pushout.inl f g)

@[simp]

theorem CategoryTheory.Limits.inl_pushoutRightPushoutInlIso_inv_assoc {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (f' : Y ⟶ W) [HasPushout f g] [HasPushout f' (pushout.inl f g)] {Z✝ : C} (h : pushout f' (pushout.inl f g) ⟶ Z✝) : CategoryStruct.comp (pushout.inl (CategoryStruct.comp f f') g) (CategoryStruct.comp (pushoutRightPushoutInlIso f g f').inv h) = CategoryStruct.comp (pushout.inl f' (pushout.inl f g)) h

@[simp]

theorem CategoryTheory.Limits.inr_inr_pushoutRightPushoutInlIso_hom {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (f' : Y ⟶ W) [HasPushout f g] [HasPushout f' (pushout.inl f g)] : CategoryStruct.comp (pushout.inr f g) (CategoryStruct.comp (pushout.inr f' (pushout.inl f g)) (pushoutRightPushoutInlIso f g f').hom) = pushout.inr (CategoryStruct.comp f f') g

@[simp]

theorem CategoryTheory.Limits.inr_inr_pushoutRightPushoutInlIso_hom_assoc {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (f' : Y ⟶ W) [HasPushout f g] [HasPushout f' (pushout.inl f g)] {Z✝ : C} (h : pushout (CategoryStruct.comp f f') g ⟶ Z✝) : CategoryStruct.comp (pushout.inr f g) (CategoryStruct.comp (pushout.inr f' (pushout.inl f g)) (CategoryStruct.comp (pushoutRightPushoutInlIso f g f').hom h)) = CategoryStruct.comp (pushout.inr (CategoryStruct.comp f f') g) h

@[simp]

theorem CategoryTheory.Limits.inr_pushoutRightPushoutInlIso_inv {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (f' : Y ⟶ W) [HasPushout f g] [HasPushout f' (pushout.inl f g)] : CategoryStruct.comp (pushout.inr (CategoryStruct.comp f f') g) (pushoutRightPushoutInlIso f g f').inv = CategoryStruct.comp (pushout.inr f g) (pushout.inr f' (pushout.inl f g))

@[simp]

theorem CategoryTheory.Limits.inr_pushoutRightPushoutInlIso_inv_assoc {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (f' : Y ⟶ W) [HasPushout f g] [HasPushout f' (pushout.inl f g)] {Z✝ : C} (h : pushout f' (pushout.inl f g) ⟶ Z✝) : CategoryStruct.comp (pushout.inr (CategoryStruct.comp f f') g) (CategoryStruct.comp (pushoutRightPushoutInlIso f g f').inv h) = CategoryStruct.comp (pushout.inr f g) (CategoryStruct.comp (pushout.inr f' (pushout.inl f g)) h)

@[simp]

theorem CategoryTheory.Limits.inl_pushoutRightPushoutInlIso_hom {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (f' : Y ⟶ W) [HasPushout f g] [HasPushout f' (pushout.inl f g)] : CategoryStruct.comp (pushout.inl f' (pushout.inl f g)) (pushoutRightPushoutInlIso f g f').hom = pushout.inl (CategoryStruct.comp f f') g

@[simp]

theorem CategoryTheory.Limits.inl_pushoutRightPushoutInlIso_hom_assoc {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (f' : Y ⟶ W) [HasPushout f g] [HasPushout f' (pushout.inl f g)] {Z✝ : C} (h : pushout (CategoryStruct.comp f f') g ⟶ Z✝) : CategoryStruct.comp (pushout.inl f' (pushout.inl f g)) (CategoryStruct.comp (pushoutRightPushoutInlIso f g f').hom h) = CategoryStruct.comp (pushout.inl (CategoryStruct.comp f f') g) h

@[simp]

theorem CategoryTheory.Limits.inr_inl_pushoutRightPushoutInlIso_hom {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (f' : Y ⟶ W) [HasPushout f g] [HasPushout f' (pushout.inl f g)] : CategoryStruct.comp (pushout.inl f g) (CategoryStruct.comp (pushout.inr f' (pushout.inl f g)) (pushoutRightPushoutInlIso f g f').hom) = CategoryStruct.comp f' (pushout.inl (CategoryStruct.comp f f') g)

@[simp]

theorem CategoryTheory.Limits.inr_inl_pushoutRightPushoutInlIso_hom_assoc {C : Type u} [Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (f' : Y ⟶ W) [HasPushout f g] [HasPushout f' (pushout.inl f g)] {Z✝ : C} (h : pushout (CategoryStruct.comp f f') g ⟶ Z✝) : CategoryStruct.comp (pushout.inl f g) (CategoryStruct.comp (pushout.inr f' (pushout.inl f g)) (CategoryStruct.comp (pushoutRightPushoutInlIso f g f').hom h)) = CategoryStruct.comp f' (CategoryStruct.comp (pushout.inl (CategoryStruct.comp f f') g) h)