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} [CategoryTheory.Category.{v, u} C] {X₃ : C} {Y₁ : C} {Y₂ : C} {Y₃ : C} {g₁ : Y₁ ⟶ Y₂} {g₂ : Y₂ ⟶ Y₃} {i₃ : X₃ ⟶ Y₃} (t₂ : CategoryTheory.Limits.PullbackCone g₂ i₃) {i₂ : t₂.pt ⟶ Y₂} (t₁ : CategoryTheory.Limits.PullbackCone g₁ i₂) (hi₂ : i₂ = t₂.fst) : CategoryTheory.Limits.PullbackCone (CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {X₃ : C} {Y₁ : C} {Y₂ : C} {Y₃ : C} {g₁ : Y₁ ⟶ Y₂} {g₂ : Y₂ ⟶ Y₃} {i₃ : X₃ ⟶ Y₃} {t₂ : CategoryTheory.Limits.PullbackCone g₂ i₃} {i₂ : t₂.pt ⟶ Y₂} {t₁ : CategoryTheory.Limits.PullbackCone g₁ i₂} (hi₂ : i₂ = t₂.fst) (H : CategoryTheory.Limits.IsLimit t₂) (H' : CategoryTheory.Limits.IsLimit t₁) : CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {X₃ : C} {Y₁ : C} {Y₂ : C} {Y₃ : C} {g₁ : Y₁ ⟶ Y₂} {g₂ : Y₂ ⟶ Y₃} {i₃ : X₃ ⟶ Y₃} {t₂ : CategoryTheory.Limits.PullbackCone g₂ i₃} {i₂ : t₂.pt ⟶ Y₂} (t₁ : CategoryTheory.Limits.PullbackCone g₁ i₂) (hi₂ : i₂ = t₂.fst) (H : CategoryTheory.Limits.IsLimit t₂) (H' : CategoryTheory.Limits.IsLimit (t₂.pasteHoriz t₁ hi₂)) : CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {X₃ : C} {Y₁ : C} {Y₂ : C} {Y₃ : C} {g₁ : Y₁ ⟶ Y₂} {g₂ : Y₂ ⟶ Y₃} {i₃ : X₃ ⟶ Y₃} {t₂ : CategoryTheory.Limits.PullbackCone g₂ i₃} {i₂ : t₂.pt ⟶ Y₂} (t₁ : CategoryTheory.Limits.PullbackCone g₁ i₂) (hi₂ : i₂ = t₂.fst) (H : CategoryTheory.Limits.IsLimit t₂) : CategoryTheory.Limits.IsLimit (t₂.pasteHoriz t₁ hi₂) ≃ CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {f₁ : X₂ ⟶ X₁} {f₂ : X₃ ⟶ X₂} {i₁ : Y₁ ⟶ X₁} (t₁ : CategoryTheory.Limits.PullbackCone i₁ f₁) {i₂ : t₁.pt ⟶ X₂} (t₂ : CategoryTheory.Limits.PullbackCone i₂ f₂) (hi₂ : i₂ = t₁.snd) : CategoryTheory.Limits.PullbackCone i₁ (CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {f₁ : X₂ ⟶ X₁} {f₂ : X₃ ⟶ X₂} {i₁ : Y₁ ⟶ X₁} (t₁ : CategoryTheory.Limits.PullbackCone i₁ f₁) {i₂ : t₁.pt ⟶ X₂} (t₂ : CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {f₁ : X₂ ⟶ X₁} {f₂ : X₃ ⟶ X₂} {i₁ : Y₁ ⟶ X₁} {t₁ : CategoryTheory.Limits.PullbackCone i₁ f₁} {i₂ : t₁.pt ⟶ X₂} {t₂ : CategoryTheory.Limits.PullbackCone i₂ f₂} (hi₂ : i₂ = t₁.snd) (H₁ : CategoryTheory.Limits.IsLimit t₁) (H₂ : CategoryTheory.Limits.IsLimit t₂) : CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {f₁ : X₂ ⟶ X₁} {f₂ : X₃ ⟶ X₂} {i₁ : Y₁ ⟶ X₁} {t₁ : CategoryTheory.Limits.PullbackCone i₁ f₁} {i₂ : t₁.pt ⟶ X₂} (t₂ : CategoryTheory.Limits.PullbackCone i₂ f₂) (hi₂ : i₂ = t₁.snd) (H₁ : CategoryTheory.Limits.IsLimit t₁) (H₂ : CategoryTheory.Limits.IsLimit (t₁.pasteVert t₂ hi₂)) : CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {f₁ : X₂ ⟶ X₁} {f₂ : X₃ ⟶ X₂} {i₁ : Y₁ ⟶ X₁} {t₁ : CategoryTheory.Limits.PullbackCone i₁ f₁} {i₂ : t₁.pt ⟶ X₂} (t₂ : CategoryTheory.Limits.PullbackCone i₂ f₂) (hi₂ : i₂ = t₁.snd) (H : CategoryTheory.Limits.IsLimit t₁) : CategoryTheory.Limits.IsLimit (t₁.pasteVert t₂ hi₂) ≃ CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {f₁ : X₁ ⟶ X₂} {f₂ : X₂ ⟶ X₃} {i₁ : X₁ ⟶ Y₁} (t₁ : CategoryTheory.Limits.PushoutCocone i₁ f₁) {i₂ : X₂ ⟶ t₁.pt} (t₂ : CategoryTheory.Limits.PushoutCocone i₂ f₂) (hi₂ : i₂ = t₁.inr) : CategoryTheory.Limits.PushoutCocone i₁ (CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {f₁ : X₁ ⟶ X₂} {f₂ : X₂ ⟶ X₃} {i₁ : X₁ ⟶ Y₁} {t₁ : CategoryTheory.Limits.PushoutCocone i₁ f₁} {i₂ : X₂ ⟶ t₁.pt} {t₂ : CategoryTheory.Limits.PushoutCocone i₂ f₂} (hi₂ : i₂ = t₁.inr) (H : CategoryTheory.Limits.IsColimit t₁) (H' : CategoryTheory.Limits.IsColimit t₂) : CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {f₁ : X₁ ⟶ X₂} {f₂ : X₂ ⟶ X₃} {i₁ : X₁ ⟶ Y₁} {t₁ : CategoryTheory.Limits.PushoutCocone i₁ f₁} {i₂ : X₂ ⟶ t₁.pt} (t₂ : CategoryTheory.Limits.PushoutCocone i₂ f₂) (hi₂ : i₂ = t₁.inr) (H : CategoryTheory.Limits.IsColimit t₁) (H' : CategoryTheory.Limits.IsColimit (t₁.pasteHoriz t₂ hi₂)) : CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {f₁ : X₁ ⟶ X₂} {f₂ : X₂ ⟶ X₃} {i₁ : X₁ ⟶ Y₁} {t₁ : CategoryTheory.Limits.PushoutCocone i₁ f₁} {i₂ : X₂ ⟶ t₁.pt} (t₂ : CategoryTheory.Limits.PushoutCocone i₂ f₂) (hi₂ : i₂ = t₁.inr) (H : CategoryTheory.Limits.IsColimit t₁) : CategoryTheory.Limits.IsColimit (t₁.pasteHoriz t₂ hi₂) ≃ CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {Y₃ : C} {Y₂ : C} {Y₁ : C} {X₃ : C} {g₂ : Y₃ ⟶ Y₂} {g₁ : Y₂ ⟶ Y₁} {i₃ : Y₃ ⟶ X₃} (t₁ : CategoryTheory.Limits.PushoutCocone g₂ i₃) {i₂ : Y₂ ⟶ t₁.pt} (t₂ : CategoryTheory.Limits.PushoutCocone g₁ i₂) (hi₂ : i₂ = t₁.inl) : CategoryTheory.Limits.PushoutCocone (CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {Y₃ : C} {Y₂ : C} {Y₁ : C} {X₃ : C} {g₂ : Y₃ ⟶ Y₂} {g₁ : Y₂ ⟶ Y₁} {i₃ : Y₃ ⟶ X₃} (t₁ : CategoryTheory.Limits.PushoutCocone g₂ i₃) {i₂ : Y₂ ⟶ t₁.pt} (t₂ : CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {Y₃ : C} {Y₂ : C} {Y₁ : C} {X₃ : C} {g₂ : Y₃ ⟶ Y₂} {g₁ : Y₂ ⟶ Y₁} {i₃ : Y₃ ⟶ X₃} {t₁ : CategoryTheory.Limits.PushoutCocone g₂ i₃} {i₂ : Y₂ ⟶ t₁.pt} {t₂ : CategoryTheory.Limits.PushoutCocone g₁ i₂} (hi₂ : i₂ = t₁.inl) (H₁ : CategoryTheory.Limits.IsColimit t₁) (H₂ : CategoryTheory.Limits.IsColimit t₂) : CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {Y₃ : C} {Y₂ : C} {Y₁ : C} {X₃ : C} {g₂ : Y₃ ⟶ Y₂} {g₁ : Y₂ ⟶ Y₁} {i₃ : Y₃ ⟶ X₃} {t₁ : CategoryTheory.Limits.PushoutCocone g₂ i₃} {i₂ : Y₂ ⟶ t₁.pt} (t₂ : CategoryTheory.Limits.PushoutCocone g₁ i₂) (hi₂ : i₂ = t₁.inl) (H₁ : CategoryTheory.Limits.IsColimit t₁) (H₂ : CategoryTheory.Limits.IsColimit (t₁.pasteVert t₂ hi₂)) : CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {Y₃ : C} {Y₂ : C} {Y₁ : C} {X₃ : C} {g₂ : Y₃ ⟶ Y₂} {g₁ : Y₂ ⟶ Y₁} {i₃ : Y₃ ⟶ X₃} {t₁ : CategoryTheory.Limits.PushoutCocone g₂ i₃} {i₂ : Y₂ ⟶ t₁.pt} (t₂ : CategoryTheory.Limits.PushoutCocone g₁ i₂) (hi₂ : i₂ = t₁.inl) (H : CategoryTheory.Limits.IsColimit t₁) : CategoryTheory.Limits.IsColimit (t₁.pasteVert t₂ hi₂) ≃ CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (f' : W ⟶ X) [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback f' (CategoryTheory.Limits.pullback.fst f g)] : CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f' f) g

Equations

• ⋯ = ⋯

noncomputable def CategoryTheory.Limits.pullbackRightPullbackFstIso {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (f' : W ⟶ X) [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback f' (CategoryTheory.Limits.pullback.fst f g)] : CategoryTheory.Limits.pullback f' (CategoryTheory.Limits.pullback.fst f g) ≅ CategoryTheory.Limits.pullback (CategoryTheory.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_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} (f : X ⟶ Z✝) (g : Y ⟶ Z✝) (f' : W ⟶ X) [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback f' (CategoryTheory.Limits.pullback.fst f g)] {Z : C} (h : W ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackRightPullbackFstIso f g f').hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp f' f) g) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f' (CategoryTheory.Limits.pullback.fst f g)) h

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• ⋯ = ⋯

def CategoryTheory.Limits.pullbackLeftPullbackSndIso {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (g' : W ⟶ Y) [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.snd f g) g'] : CategoryTheory.Limits.pullback (CategoryTheory.Limits.pullback.snd f g) g' ≅ CategoryTheory.Limits.pullback f (CategoryTheory.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_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} (f : X ⟶ Z✝) (g : Y ⟶ Z✝) (g' : W ⟶ Y) [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.snd f g) g'] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackLeftPullbackSndIso f g g').hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f (CategoryTheory.CategoryStruct.comp g' g)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd f g) g') (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) h)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• ⋯ = ⋯

noncomputable def CategoryTheory.Limits.pushoutLeftPushoutInrIso {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (g' : Z ⟶ W) [CategoryTheory.Limits.HasPushout f g] [CategoryTheory.Limits.HasPushout (CategoryTheory.Limits.pushout.inr f g) g'] : CategoryTheory.Limits.pushout (CategoryTheory.Limits.pushout.inr f g) g' ≅ CategoryTheory.Limits.pushout f (CategoryTheory.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_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : X ⟶ Z✝) (g' : Z✝ ⟶ W) [CategoryTheory.Limits.HasPushout f g] [CategoryTheory.Limits.HasPushout (CategoryTheory.Limits.pushout.inr f g) g'] {Z : C} (h : CategoryTheory.Limits.pushout (CategoryTheory.Limits.pushout.inr f g) g' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f (CategoryTheory.CategoryStruct.comp g g')) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutLeftPushoutInrIso f g g').inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.pushout.inr f g) g') h)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• ⋯ = ⋯

noncomputable def CategoryTheory.Limits.pushoutRightPushoutInlIso {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (f' : Y ⟶ W) [CategoryTheory.Limits.HasPushout f g] [CategoryTheory.Limits.HasPushout f' (CategoryTheory.Limits.pushout.inl f g)] : CategoryTheory.Limits.pushout f' (CategoryTheory.Limits.pushout.inl f g) ≅ CategoryTheory.Limits.pushout (CategoryTheory.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_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : X ⟶ Z✝) (f' : Y ⟶ W) [CategoryTheory.Limits.HasPushout f g] [CategoryTheory.Limits.HasPushout f' (CategoryTheory.Limits.pushout.inl f g)] {Z : C} (h : CategoryTheory.Limits.pushout f' (CategoryTheory.Limits.pushout.inl f g) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp f f') g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutRightPushoutInlIso f g f').inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f' (CategoryTheory.Limits.pushout.inl f g)) h

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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