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.

source

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.

Instances For

source

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.

Instances For

source

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.

Instances For

source

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.

Instances For

source

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.HasPullback (CategoryTheory.CategoryStruct.comp f' 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.

Instances For

source

@[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)] [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 (CategoryTheory.CategoryStruct.comp f' f) g) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f' (CategoryTheory.Limits.pullback.fst f g)) h

source

@[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.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f' 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)

source

@[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)] [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 (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)

source

@[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.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 f' f) g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f' (CategoryTheory.Limits.pullback.fst f g)) (CategoryTheory.Limits.pullback.snd f g)

source

@[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)] [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 f' (CategoryTheory.Limits.pullback.fst f g)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp f' f) g) h

source

@[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.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f' 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

source

@[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)] [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 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

source

@[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.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 f' (CategoryTheory.Limits.pullback.fst f g)) (CategoryTheory.Limits.pullback.snd f g)) = CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp f' f) g

source

@[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)] [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 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)

source

@[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.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 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'

source

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.HasPushout f (CategoryTheory.CategoryStruct.comp 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.

Instances For

source

@[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'] [CategoryTheory.Limits.HasPushout f (CategoryTheory.CategoryStruct.comp 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)

source

@[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.Limits.HasPushout f (CategoryTheory.CategoryStruct.comp 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')

source

@[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'] [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.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

source

@[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.Limits.HasPushout f (CategoryTheory.CategoryStruct.comp 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')

source

@[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'] [CategoryTheory.Limits.HasPushout f (CategoryTheory.CategoryStruct.comp 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

source

@[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.Limits.HasPushout f (CategoryTheory.CategoryStruct.comp 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'

source

@[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'] [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 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

source

@[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.Limits.HasPushout f (CategoryTheory.CategoryStruct.comp 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')

source

@[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'] [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 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)

source

@[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.Limits.HasPushout f (CategoryTheory.CategoryStruct.comp 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'))

Documentation

Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Pasting lemma #

Main results #