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

• bigSquareIsPullback 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.

def CategoryTheory.Limits.bigSquareIsPullback {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} {Y₃ : C} (f₁ : X₁ ⟶ X₂) (f₂ : X₂ ⟶ X₃) (g₁ : Y₁ ⟶ Y₂) (g₂ : Y₂ ⟶ Y₃) (i₁ : X₁ ⟶ Y₁) (i₂ : X₂ ⟶ Y₂) (i₃ : X₃ ⟶ Y₃) (h₁ : CategoryTheory.CategoryStruct.comp i₁ g₁ = CategoryTheory.CategoryStruct.comp f₁ i₂) (h₂ : CategoryTheory.CategoryStruct.comp i₂ g₂ = CategoryTheory.CategoryStruct.comp f₂ i₃) (H : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk i₂ f₂ h₂)) (H' : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk i₁ f₁ h₁)) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk i₁ (CategoryTheory.CategoryStruct.comp f₁ f₂) ⋯)

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.bigSquareIsPushout {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} {Y₃ : C} (f₁ : X₁ ⟶ X₂) (f₂ : X₂ ⟶ X₃) (g₁ : Y₁ ⟶ Y₂) (g₂ : Y₂ ⟶ Y₃) (i₁ : X₁ ⟶ Y₁) (i₂ : X₂ ⟶ Y₂) (i₃ : X₃ ⟶ Y₃) (h₁ : CategoryTheory.CategoryStruct.comp i₁ g₁ = CategoryTheory.CategoryStruct.comp f₁ i₂) (h₂ : CategoryTheory.CategoryStruct.comp i₂ g₂ = CategoryTheory.CategoryStruct.comp f₂ i₃) (H : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk g₂ i₃ h₂)) (H' : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk g₁ i₂ h₁)) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk (CategoryTheory.CategoryStruct.comp g₁ g₂) i₃ ⋯)

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.leftSquareIsPullback {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} {Y₃ : C} (f₁ : X₁ ⟶ X₂) (f₂ : X₂ ⟶ X₃) (g₁ : Y₁ ⟶ Y₂) (g₂ : Y₂ ⟶ Y₃) (i₁ : X₁ ⟶ Y₁) (i₂ : X₂ ⟶ Y₂) (i₃ : X₃ ⟶ Y₃) (h₁ : CategoryTheory.CategoryStruct.comp i₁ g₁ = CategoryTheory.CategoryStruct.comp f₁ i₂) (h₂ : CategoryTheory.CategoryStruct.comp i₂ g₂ = CategoryTheory.CategoryStruct.comp f₂ i₃) (H : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk i₂ f₂ h₂)) (H' : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk i₁ (CategoryTheory.CategoryStruct.comp f₁ f₂) ⋯)) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk i₁ f₁ h₁)

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.rightSquareIsPushout {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} {Y₃ : C} (f₁ : X₁ ⟶ X₂) (f₂ : X₂ ⟶ X₃) (g₁ : Y₁ ⟶ Y₂) (g₂ : Y₂ ⟶ Y₃) (i₁ : X₁ ⟶ Y₁) (i₂ : X₂ ⟶ Y₂) (i₃ : X₃ ⟶ Y₃) (h₁ : CategoryTheory.CategoryStruct.comp i₁ g₁ = CategoryTheory.CategoryStruct.comp f₁ i₂) (h₂ : CategoryTheory.CategoryStruct.comp i₂ g₂ = CategoryTheory.CategoryStruct.comp f₂ i₃) (H : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk g₁ i₂ h₁)) (H' : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk (CategoryTheory.CategoryStruct.comp g₁ g₂) i₃ ⋯)) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk g₂ i₃ h₂)

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.

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] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f' f) g] : CategoryTheory.Limits.pullback f' CategoryTheory.Limits.pullback.fst ≅ 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] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f' f) g] {Z : C} (h : W ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackRightPullbackFstIso f g f').hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst 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] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f' f) g] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackRightPullbackFstIso f g f').hom CategoryTheory.Limits.pullback.fst = CategoryTheory.Limits.pullback.fst

@[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] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f' f) g] {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackRightPullbackFstIso f g f').hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd 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] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f' f) g] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackRightPullbackFstIso f g f').hom CategoryTheory.Limits.pullback.snd = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd

@[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] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f' f) g] {Z : C} (h : W ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackRightPullbackFstIso f g f').inv (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst 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] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f' f) g] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackRightPullbackFstIso f g f').inv CategoryTheory.Limits.pullback.fst = CategoryTheory.Limits.pullback.fst

@[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] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f' f) g] {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackRightPullbackFstIso f g f').inv (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd 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] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f' f) g] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackRightPullbackFstIso f g f').inv (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd) = CategoryTheory.Limits.pullback.snd

@[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] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f' f) g] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackRightPullbackFstIso f g f').inv (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (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] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f' f) g] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackRightPullbackFstIso f g f').inv (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.fst) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f'

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 g'] [CategoryTheory.Limits.HasPushout f (CategoryTheory.CategoryStruct.comp g g')] : CategoryTheory.Limits.pushout CategoryTheory.Limits.pushout.inr 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 g'] [CategoryTheory.Limits.HasPushout f (CategoryTheory.CategoryStruct.comp g g')] {Z : C} (h : CategoryTheory.Limits.pushout CategoryTheory.Limits.pushout.inr g' ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutLeftPushoutInrIso f g g').inv h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl 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 g'] [CategoryTheory.Limits.HasPushout f (CategoryTheory.CategoryStruct.comp g g')] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.pushoutLeftPushoutInrIso f g g').inv = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl CategoryTheory.Limits.pushout.inl

@[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 g'] [CategoryTheory.Limits.HasPushout f (CategoryTheory.CategoryStruct.comp g g')] {Z : C} (h : CategoryTheory.Limits.pushout f (CategoryTheory.CategoryStruct.comp g g') ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutLeftPushoutInrIso f g g').hom h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr 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 g'] [CategoryTheory.Limits.HasPushout f (CategoryTheory.CategoryStruct.comp g g')] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.pushoutLeftPushoutInrIso f g g').hom = CategoryTheory.Limits.pushout.inr

@[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 g'] [CategoryTheory.Limits.HasPushout f (CategoryTheory.CategoryStruct.comp g g')] {Z : C} (h : CategoryTheory.Limits.pushout CategoryTheory.Limits.pushout.inr g' ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutLeftPushoutInrIso f g g').inv h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr 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 g'] [CategoryTheory.Limits.HasPushout f (CategoryTheory.CategoryStruct.comp g g')] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.pushoutLeftPushoutInrIso f g g').inv = CategoryTheory.Limits.pushout.inr

@[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 g'] [CategoryTheory.Limits.HasPushout f (CategoryTheory.CategoryStruct.comp g g')] {Z : C} (h : CategoryTheory.Limits.pushout f (CategoryTheory.CategoryStruct.comp g g') ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutLeftPushoutInrIso f g g').hom h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl 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 g'] [CategoryTheory.Limits.HasPushout f (CategoryTheory.CategoryStruct.comp g g')] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.pushoutLeftPushoutInrIso f g g').hom) = CategoryTheory.Limits.pushout.inl

@[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 g'] [CategoryTheory.Limits.HasPushout f (CategoryTheory.CategoryStruct.comp g g')] {Z : C} (h : CategoryTheory.Limits.pushout f (CategoryTheory.CategoryStruct.comp g g') ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutLeftPushoutInrIso f g g').hom h)) = CategoryTheory.CategoryStruct.comp g' (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr 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 g'] [CategoryTheory.Limits.HasPushout f (CategoryTheory.CategoryStruct.comp g g')] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.pushoutLeftPushoutInrIso f g g').hom) = CategoryTheory.CategoryStruct.comp g' CategoryTheory.Limits.pushout.inr