Pullback and pushout squares #
We restate some results about pullbacks/pushouts in the language of IsPullback and IsPushout,
among which the pasting lemmas
theorem
CategoryTheory.IsPullback.of_is_product
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
{c : Limits.BinaryFan X Y}
(h : Limits.IsLimit c)
(t : Limits.IsTerminal Z)
:
IsPullback c.fst c.snd (t.from ((Limits.pair X Y).obj { as := Limits.WalkingPair.left }))
(t.from ((Limits.pair X Y).obj { as := Limits.WalkingPair.right }))
If c is a limiting binary product cone, and we have a terminal object,
then we have IsPullback c.fst c.snd 0 0
(where each 0 is the unique morphism to the terminal object).
theorem
CategoryTheory.IsPullback.of_is_product'
{C : Type u₁}
[Category.{v₁, u₁} C]
{P X Y Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
(h : Limits.IsLimit (Limits.BinaryFan.mk fst snd))
(t : Limits.IsTerminal Z)
:
IsPullback fst snd (t.from X) (t.from Y)
A variant of of_is_product that is more useful with apply.
theorem
CategoryTheory.IsPullback.of_hasBinaryProduct'
{C : Type u₁}
[Category.{v₁, u₁} C]
(X Y : C)
[Limits.HasBinaryProduct X Y]
[Limits.HasTerminal C]
:
theorem
CategoryTheory.IsPullback.of_iso_pullback
{C : Type u₁}
[Category.{v₁, u₁} C]
{P X Y Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(h : CommSq fst snd f g)
[Limits.HasPullback f g]
(i : P ≅ Limits.pullback f g)
(w₁ : CategoryStruct.comp i.hom (Limits.pullback.fst f g) = fst)
(w₂ : CategoryStruct.comp i.hom (Limits.pullback.snd f g) = snd)
:
IsPullback fst snd f g
theorem
CategoryTheory.IsPullback.of_horiz_isIso_mono
{C : Type u₁}
[Category.{v₁, u₁} C]
{P X Y Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[IsIso fst]
[Mono g]
(sq : CommSq fst snd f g)
:
IsPullback fst snd f g
theorem
CategoryTheory.IsPullback.of_horiz_isIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{P X Y Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[IsIso fst]
[IsIso g]
(sq : CommSq fst snd f g)
:
IsPullback fst snd f g
theorem
CategoryTheory.IsPullback.of_iso
{C : Type u₁}
[Category.{v₁, u₁} C]
{P X Y Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(h : IsPullback fst snd f g)
{P' X' Y' Z' : C}
{fst' : P' ⟶ X'}
{snd' : P' ⟶ Y'}
{f' : X' ⟶ Z'}
{g' : Y' ⟶ Z'}
(e₁ : P ≅ P')
(e₂ : X ≅ X')
(e₃ : Y ≅ Y')
(e₄ : Z ≅ Z')
(commfst : CategoryStruct.comp fst e₂.hom = CategoryStruct.comp e₁.hom fst')
(commsnd : CategoryStruct.comp snd e₃.hom = CategoryStruct.comp e₁.hom snd')
(commf : CategoryStruct.comp f e₄.hom = CategoryStruct.comp e₂.hom f')
(commg : CategoryStruct.comp g e₄.hom = CategoryStruct.comp e₃.hom g')
:
IsPullback fst' snd' f' g'
theorem
CategoryTheory.IsPullback.of_iso'
{C : Type u₁}
[Category.{v₁, u₁} C]
{P X Y Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(h : IsPullback fst snd f g)
{P' X' Y' Z' : C}
{fst' : P' ⟶ X'}
{snd' : P' ⟶ Y'}
{f' : X' ⟶ Z'}
{g' : Y' ⟶ Z'}
(e₁ : P' ≅ P)
(e₂ : X' ≅ X)
(e₃ : Y' ≅ Y)
(e₄ : Z' ≅ Z)
(commfst : CategoryStruct.comp e₁.hom fst = CategoryStruct.comp fst' e₂.hom)
(commsnd : CategoryStruct.comp e₁.hom snd = CategoryStruct.comp snd' e₃.hom)
(commf : CategoryStruct.comp e₂.hom f = CategoryStruct.comp f' e₄.hom)
(commg : CategoryStruct.comp e₃.hom g = CategoryStruct.comp g' e₄.hom)
:
IsPullback fst' snd' f' g'
Same as IsPullback.of_iso, but using the data and compatibilities involving
the inverse isomorphisms instead.
theorem
CategoryTheory.IsPullback.isIso_fst_of_mono
{C : Type u₁}
[Category.{v₁, u₁} C]
{P X Y : C}
{fst snd : P ⟶ X}
{f : X ⟶ Y}
[Mono f]
(h : IsPullback fst snd f f)
:
IsIso fst
theorem
CategoryTheory.IsPullback.isIso_snd_iso_of_mono
{C : Type u₁}
[Category.{v₁, u₁} C]
{P X Y : C}
{fst snd : P ⟶ X}
{f : X ⟶ Y}
[Mono f]
(h : IsPullback fst snd f f)
:
IsIso snd
theorem
CategoryTheory.IsPullback.isIso_fst_of_isIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{P X Y Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(h : IsPullback fst snd f g)
[IsIso g]
:
IsIso fst
theorem
CategoryTheory.IsPullback.isIso_snd_of_isIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{P X Y Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(h : IsPullback fst snd f g)
[IsIso f]
:
IsIso snd
theorem
CategoryTheory.IsPullback.paste_vert
{C : Type u₁}
[Category.{v₁, u₁} C]
{X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C}
{h₁₁ : X₁₁ ⟶ X₁₂}
{h₂₁ : X₂₁ ⟶ X₂₂}
{h₃₁ : X₃₁ ⟶ X₃₂}
{v₁₁ : X₁₁ ⟶ X₂₁}
{v₁₂ : X₁₂ ⟶ X₂₂}
{v₂₁ : X₂₁ ⟶ X₃₁}
{v₂₂ : X₂₂ ⟶ X₃₂}
(s : IsPullback h₁₁ v₁₁ v₁₂ h₂₁)
(t : IsPullback h₂₁ v₂₁ v₂₂ h₃₁)
:
IsPullback h₁₁ (CategoryStruct.comp v₁₁ v₂₁) (CategoryStruct.comp v₁₂ v₂₂) h₃₁
Paste two pullback squares "vertically" to obtain another pullback square.
The objects in the statement fit into the following diagram:
X₁₁ - h₁₁ -> X₁₂
| |
v₁₁ v₁₂
↓ ↓
X₂₁ - h₂₁ -> X₂₂
| |
v₂₁ v₂₂
↓ ↓
X₃₁ - h₃₁ -> X₃₂
theorem
CategoryTheory.IsPullback.paste_horiz
{C : Type u₁}
[Category.{v₁, u₁} C]
{X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C}
{h₁₁ : X₁₁ ⟶ X₁₂}
{h₁₂ : X₁₂ ⟶ X₁₃}
{h₂₁ : X₂₁ ⟶ X₂₂}
{h₂₂ : X₂₂ ⟶ X₂₃}
{v₁₁ : X₁₁ ⟶ X₂₁}
{v₁₂ : X₁₂ ⟶ X₂₂}
{v₁₃ : X₁₃ ⟶ X₂₃}
(s : IsPullback h₁₁ v₁₁ v₁₂ h₂₁)
(t : IsPullback h₁₂ v₁₂ v₁₃ h₂₂)
:
IsPullback (CategoryStruct.comp h₁₁ h₁₂) v₁₁ v₁₃ (CategoryStruct.comp h₂₁ h₂₂)
Paste two pullback squares "horizontally" to obtain another pullback square.
The objects in the statement fit into the following diagram:
X₁₁ - h₁₁ -> X₁₂ - h₁₂ -> X₁₃
| | |
v₁₁ v₁₂ v₁₃
↓ ↓ ↓
X₂₁ - h₂₁ -> X₂₂ - h₂₂ -> X₂₃
theorem
CategoryTheory.IsPullback.of_bot
{C : Type u₁}
[Category.{v₁, u₁} C]
{X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C}
{h₁₁ : X₁₁ ⟶ X₁₂}
{h₂₁ : X₂₁ ⟶ X₂₂}
{h₃₁ : X₃₁ ⟶ X₃₂}
{v₁₁ : X₁₁ ⟶ X₂₁}
{v₁₂ : X₁₂ ⟶ X₂₂}
{v₂₁ : X₂₁ ⟶ X₃₁}
{v₂₂ : X₂₂ ⟶ X₃₂}
(s : IsPullback h₁₁ (CategoryStruct.comp v₁₁ v₂₁) (CategoryStruct.comp v₁₂ v₂₂) h₃₁)
(p : CategoryStruct.comp h₁₁ v₁₂ = CategoryStruct.comp v₁₁ h₂₁)
(t : IsPullback h₂₁ v₂₁ v₂₂ h₃₁)
:
IsPullback h₁₁ v₁₁ v₁₂ h₂₁
Given a pullback square assembled from a commuting square on the top and a pullback square on the bottom, the top square is a pullback square.
The objects in the statement fit into the following diagram:
X₁₁ - h₁₁ -> X₁₂
| |
v₁₁ v₁₂
↓ ↓
X₂₁ - h₂₁ -> X₂₂
| |
v₂₁ v₂₂
↓ ↓
X₃₁ - h₃₁ -> X₃₂
theorem
CategoryTheory.IsPullback.of_right
{C : Type u₁}
[Category.{v₁, u₁} C]
{X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C}
{h₁₁ : X₁₁ ⟶ X₁₂}
{h₁₂ : X₁₂ ⟶ X₁₃}
{h₂₁ : X₂₁ ⟶ X₂₂}
{h₂₂ : X₂₂ ⟶ X₂₃}
{v₁₁ : X₁₁ ⟶ X₂₁}
{v₁₂ : X₁₂ ⟶ X₂₂}
{v₁₃ : X₁₃ ⟶ X₂₃}
(s : IsPullback (CategoryStruct.comp h₁₁ h₁₂) v₁₁ v₁₃ (CategoryStruct.comp h₂₁ h₂₂))
(p : CategoryStruct.comp h₁₁ v₁₂ = CategoryStruct.comp v₁₁ h₂₁)
(t : IsPullback h₁₂ v₁₂ v₁₃ h₂₂)
:
IsPullback h₁₁ v₁₁ v₁₂ h₂₁
Given a pullback square assembled from a commuting square on the left and a pullback square on the right, the left square is a pullback square.
The objects in the statement fit into the following diagram:
X₁₁ - h₁₁ -> X₁₂ - h₁₂ -> X₁₃
| | |
v₁₁ v₁₂ v₁₃
↓ ↓ ↓
X₂₁ - h₂₁ -> X₂₂ - h₂₂ -> X₂₃
theorem
CategoryTheory.IsPullback.paste_vert_iff
{C : Type u₁}
[Category.{v₁, u₁} C]
{X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C}
{h₁₁ : X₁₁ ⟶ X₁₂}
{h₂₁ : X₂₁ ⟶ X₂₂}
{h₃₁ : X₃₁ ⟶ X₃₂}
{v₁₁ : X₁₁ ⟶ X₂₁}
{v₁₂ : X₁₂ ⟶ X₂₂}
{v₂₁ : X₂₁ ⟶ X₃₁}
{v₂₂ : X₂₂ ⟶ X₃₂}
(s : IsPullback h₂₁ v₂₁ v₂₂ h₃₁)
(e : CategoryStruct.comp h₁₁ v₁₂ = CategoryStruct.comp v₁₁ h₂₁)
:
IsPullback h₁₁ (CategoryStruct.comp v₁₁ v₂₁) (CategoryStruct.comp v₁₂ v₂₂) h₃₁ ↔ IsPullback h₁₁ v₁₁ v₁₂ h₂₁
theorem
CategoryTheory.IsPullback.paste_horiz_iff
{C : Type u₁}
[Category.{v₁, u₁} C]
{X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C}
{h₁₁ : X₁₁ ⟶ X₁₂}
{h₁₂ : X₁₂ ⟶ X₁₃}
{h₂₁ : X₂₁ ⟶ X₂₂}
{h₂₂ : X₂₂ ⟶ X₂₃}
{v₁₁ : X₁₁ ⟶ X₂₁}
{v₁₂ : X₁₂ ⟶ X₂₂}
{v₁₃ : X₁₃ ⟶ X₂₃}
(s : IsPullback h₁₂ v₁₂ v₁₃ h₂₂)
(e : CategoryStruct.comp h₁₁ v₁₂ = CategoryStruct.comp v₁₁ h₂₁)
:
IsPullback (CategoryStruct.comp h₁₁ h₁₂) v₁₁ v₁₃ (CategoryStruct.comp h₂₁ h₂₂) ↔ IsPullback h₁₁ v₁₁ v₁₂ h₂₁
theorem
CategoryTheory.IsPullback.of_right'
{C : Type u₁}
[Category.{v₁, u₁} C]
{X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C}
{h₁₂ : X₁₂ ⟶ X₁₃}
{h₂₁ : X₂₁ ⟶ X₂₂}
{h₂₂ : X₂₂ ⟶ X₂₃}
{h₁₃ : X₁₁ ⟶ X₁₃}
{v₁₁ : X₁₁ ⟶ X₂₁}
{v₁₂ : X₁₂ ⟶ X₂₂}
{v₁₃ : X₁₃ ⟶ X₂₃}
(s : IsPullback h₁₃ v₁₁ v₁₃ (CategoryStruct.comp h₂₁ h₂₂))
(t : IsPullback h₁₂ v₁₂ v₁₃ h₂₂)
:
IsPullback (t.lift h₁₃ (CategoryStruct.comp v₁₁ h₂₁) ⋯) v₁₁ v₁₂ h₂₁
Variant of IsPullback.of_right where h₁₁ is induced from a morphism h₁₃ : X₁₁ ⟶ X₁₃, and
the universal property of the right square.
The objects fit in the following diagram:
X₁₁ - h₁₁ -> X₁₂ - h₁₂ -> X₁₃
| | |
v₁₁ v₁₂ v₁₃
↓ ↓ ↓
X₂₁ - h₂₁ -> X₂₂ - h₂₂ -> X₂₃
theorem
CategoryTheory.IsPullback.of_bot'
{C : Type u₁}
[Category.{v₁, u₁} C]
{X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C}
{h₁₁ : X₁₁ ⟶ X₁₂}
{h₂₁ : X₂₁ ⟶ X₂₂}
{h₃₁ : X₃₁ ⟶ X₃₂}
{v₃₁ : X₁₁ ⟶ X₃₁}
{v₁₂ : X₁₂ ⟶ X₂₂}
{v₂₁ : X₂₁ ⟶ X₃₁}
{v₂₂ : X₂₂ ⟶ X₃₂}
(s : IsPullback h₁₁ v₃₁ (CategoryStruct.comp v₁₂ v₂₂) h₃₁)
(t : IsPullback h₂₁ v₂₁ v₂₂ h₃₁)
:
IsPullback h₁₁ (t.lift (CategoryStruct.comp h₁₁ v₁₂) v₃₁ ⋯) v₁₂ h₂₁
Variant of IsPullback.of_bot, where v₁₁ is induced from a morphism v₃₁ : X₁₁ ⟶ X₃₁, and
the universal property of the bottom square.
The objects in the statement fit into the following diagram:
X₁₁ - h₁₁ -> X₁₂
| |
v₁₁ v₁₂
↓ ↓
X₂₁ - h₂₁ -> X₂₂
| |
v₂₁ v₂₂
↓ ↓
X₃₁ - h₃₁ -> X₃₂
instance
CategoryTheory.IsPullback.instHasPullbackFst
{C : Type u₁}
[Category.{v₁, u₁} C]
{P X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[Limits.HasPullbacksAlong f]
(h : P ⟶ Y)
:
theorem
CategoryTheory.IsPullback.of_vert_isIso_mono
{C : Type u₁}
[Category.{v₁, u₁} C]
{P X Y Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[IsIso snd]
[Mono f]
(sq : CommSq fst snd f g)
:
IsPullback fst snd f g
theorem
CategoryTheory.IsPullback.of_vert_isIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{P X Y Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[IsIso snd]
[IsIso f]
(sq : CommSq fst snd f g)
:
IsPullback fst snd f g
theorem
CategoryTheory.IsPullback.of_id_fst
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Z : C}
{f : X ⟶ Z}
:
IsPullback (CategoryStruct.id X) f f (CategoryStruct.id Z)
theorem
CategoryTheory.IsPullback.of_id_snd
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Z : C}
{f : X ⟶ Z}
:
IsPullback f (CategoryStruct.id X) (CategoryStruct.id Z) f
theorem
CategoryTheory.IsPullback.id_vert
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Z : C}
(f : X ⟶ Z)
:
IsPullback f (CategoryStruct.id X) (CategoryStruct.id Z) f
The following diagram is a pullback
X --f--> Z
| |
id id
v v
X --f--> Z
theorem
CategoryTheory.IsPullback.id_horiz
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Z : C}
(f : X ⟶ Z)
:
IsPullback (CategoryStruct.id X) f f (CategoryStruct.id Z)
The following diagram is a pullback
X --id--> X
| |
f f
v v
Z --id--> Z
theorem
CategoryTheory.IsPullback.of_prod_fst_with_id
{C : Type u₁}
[Category.{v₁, u₁} C]
{A B : C}
(f : A ⟶ B)
(X : C)
[Limits.HasBinaryProduct A X]
[Limits.HasBinaryProduct B X]
:
In a category, given a morphism f : A ⟶ B and an object X,
this is the obvious pullback diagram:
A ⨯ X ⟶ A
| |
v v
B ⨯ X ⟶ B
theorem
CategoryTheory.IsPullback.of_isLimit_binaryFan_of_isTerminal
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y : C}
{c : Limits.BinaryFan X Y}
(hc : Limits.IsLimit c)
{T : C}
(hT : Limits.IsTerminal T)
:
IsPullback c.fst c.snd (hT.from ((Limits.pair X Y).obj { as := Limits.WalkingPair.left }))
(hT.from ((Limits.pair X Y).obj { as := Limits.WalkingPair.right }))
theorem
CategoryTheory.IsPushout.of_is_coproduct
{C : Type u₁}
[Category.{v₁, u₁} C]
{Z X Y : C}
{c : Limits.BinaryCofan X Y}
(h : Limits.IsColimit c)
(t : Limits.IsInitial Z)
:
IsPushout (t.to ((Limits.pair X Y).obj { as := Limits.WalkingPair.left }))
(t.to ((Limits.pair X Y).obj { as := Limits.WalkingPair.right })) c.inl c.inr
If c is a colimiting binary coproduct cocone, and we have an initial object,
then we have IsPushout 0 0 c.inl c.inr
(where each 0 is the unique morphism from the initial object).
theorem
CategoryTheory.IsPushout.of_is_coproduct'
{C : Type u₁}
[Category.{v₁, u₁} C]
{Z X Y P : C}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(h : Limits.IsColimit (Limits.BinaryCofan.mk inl inr))
(t : Limits.IsInitial Z)
:
A variant of of_is_coproduct that is more useful with apply.
theorem
CategoryTheory.IsPushout.of_hasBinaryCoproduct'
{C : Type u₁}
[Category.{v₁, u₁} C]
(X Y : C)
[Limits.HasBinaryCoproduct X Y]
[Limits.HasInitial C]
:
theorem
CategoryTheory.IsPushout.of_iso_pushout
{C : Type u₁}
[Category.{v₁, u₁} C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(h : CommSq f g inl inr)
[Limits.HasPushout f g]
(i : P ≅ Limits.pushout f g)
(w₁ : CategoryStruct.comp inl i.hom = Limits.pushout.inl f g)
(w₂ : CategoryStruct.comp inr i.hom = Limits.pushout.inr f g)
:
IsPushout f g inl inr
theorem
CategoryTheory.IsPushout.of_iso
{C : Type u₁}
[Category.{v₁, u₁} C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(h : IsPushout f g inl inr)
{Z' X' Y' P' : C}
{f' : Z' ⟶ X'}
{g' : Z' ⟶ Y'}
{inl' : X' ⟶ P'}
{inr' : Y' ⟶ P'}
(e₁ : Z ≅ Z')
(e₂ : X ≅ X')
(e₃ : Y ≅ Y')
(e₄ : P ≅ P')
(commf : CategoryStruct.comp f e₂.hom = CategoryStruct.comp e₁.hom f')
(commg : CategoryStruct.comp g e₃.hom = CategoryStruct.comp e₁.hom g')
(comminl : CategoryStruct.comp inl e₄.hom = CategoryStruct.comp e₂.hom inl')
(comminr : CategoryStruct.comp inr e₄.hom = CategoryStruct.comp e₃.hom inr')
:
IsPushout f' g' inl' inr'
theorem
CategoryTheory.IsPushout.of_iso'
{C : Type u₁}
[Category.{v₁, u₁} C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(h : IsPushout f g inl inr)
{Z' X' Y' P' : C}
{f' : Z' ⟶ X'}
{g' : Z' ⟶ Y'}
{inl' : X' ⟶ P'}
{inr' : Y' ⟶ P'}
(e₁ : Z' ≅ Z)
(e₂ : X' ≅ X)
(e₃ : Y' ≅ Y)
(e₄ : P' ≅ P)
(commf : CategoryStruct.comp e₁.hom f = CategoryStruct.comp f' e₂.hom)
(commg : CategoryStruct.comp e₁.hom g = CategoryStruct.comp g' e₃.hom)
(comminl : CategoryStruct.comp e₂.hom inl = CategoryStruct.comp inl' e₄.hom)
(comminr : CategoryStruct.comp e₃.hom inr = CategoryStruct.comp inr' e₄.hom)
:
IsPushout f' g' inl' inr'
Same as IsPushout.of_iso, but using the data and compatibilities involving
the inverse isomorphisms instead.
theorem
CategoryTheory.IsPushout.isIso_inl_iso_of_epi
{C : Type u₁}
[Category.{v₁, u₁} C]
{P X Y : C}
{inl inr : X ⟶ P}
{f : Y ⟶ X}
[Epi f]
(h : IsPushout f f inl inr)
:
IsIso inl
theorem
CategoryTheory.IsPushout.isIso_inr_iso_of_epi
{C : Type u₁}
[Category.{v₁, u₁} C]
{P X Y : C}
{inl inr : X ⟶ P}
{f : Y ⟶ X}
[Epi f]
(h : IsPushout f f inl inr)
:
IsIso inr
theorem
CategoryTheory.IsPushout.paste_vert
{C : Type u₁}
[Category.{v₁, u₁} C]
{X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C}
{h₁₁ : X₁₁ ⟶ X₁₂}
{h₂₁ : X₂₁ ⟶ X₂₂}
{h₃₁ : X₃₁ ⟶ X₃₂}
{v₁₁ : X₁₁ ⟶ X₂₁}
{v₁₂ : X₁₂ ⟶ X₂₂}
{v₂₁ : X₂₁ ⟶ X₃₁}
{v₂₂ : X₂₂ ⟶ X₃₂}
(s : IsPushout h₁₁ v₁₁ v₁₂ h₂₁)
(t : IsPushout h₂₁ v₂₁ v₂₂ h₃₁)
:
IsPushout h₁₁ (CategoryStruct.comp v₁₁ v₂₁) (CategoryStruct.comp v₁₂ v₂₂) h₃₁
Paste two pushout squares "vertically" to obtain another pushout square.
The objects in the statement fit into the following diagram:
X₁₁ - h₁₁ -> X₁₂
| |
v₁₁ v₁₂
↓ ↓
X₂₁ - h₂₁ -> X₂₂
| |
v₂₁ v₂₂
↓ ↓
X₃₁ - h₃₁ -> X₃₂
theorem
CategoryTheory.IsPushout.paste_horiz
{C : Type u₁}
[Category.{v₁, u₁} C]
{X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C}
{h₁₁ : X₁₁ ⟶ X₁₂}
{h₁₂ : X₁₂ ⟶ X₁₃}
{h₂₁ : X₂₁ ⟶ X₂₂}
{h₂₂ : X₂₂ ⟶ X₂₃}
{v₁₁ : X₁₁ ⟶ X₂₁}
{v₁₂ : X₁₂ ⟶ X₂₂}
{v₁₃ : X₁₃ ⟶ X₂₃}
(s : IsPushout h₁₁ v₁₁ v₁₂ h₂₁)
(t : IsPushout h₁₂ v₁₂ v₁₃ h₂₂)
:
IsPushout (CategoryStruct.comp h₁₁ h₁₂) v₁₁ v₁₃ (CategoryStruct.comp h₂₁ h₂₂)
Paste two pushout squares "horizontally" to obtain another pushout square.
The objects in the statement fit into the following diagram:
X₁₁ - h₁₁ -> X₁₂ - h₁₂ -> X₁₃
| | |
v₁₁ v₁₂ v₁₃
↓ ↓ ↓
X₂₁ - h₂₁ -> X₂₂ - h₂₂ -> X₂₃
theorem
CategoryTheory.IsPushout.of_top
{C : Type u₁}
[Category.{v₁, u₁} C]
{X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C}
{h₁₁ : X₁₁ ⟶ X₁₂}
{h₂₁ : X₂₁ ⟶ X₂₂}
{h₃₁ : X₃₁ ⟶ X₃₂}
{v₁₁ : X₁₁ ⟶ X₂₁}
{v₁₂ : X₁₂ ⟶ X₂₂}
{v₂₁ : X₂₁ ⟶ X₃₁}
{v₂₂ : X₂₂ ⟶ X₃₂}
(s : IsPushout h₁₁ (CategoryStruct.comp v₁₁ v₂₁) (CategoryStruct.comp v₁₂ v₂₂) h₃₁)
(p : CategoryStruct.comp h₂₁ v₂₂ = CategoryStruct.comp v₂₁ h₃₁)
(t : IsPushout h₁₁ v₁₁ v₁₂ h₂₁)
:
IsPushout h₂₁ v₂₁ v₂₂ h₃₁
Given a pushout square assembled from a pushout square on the top and a commuting square on the bottom, the bottom square is a pushout square.
The objects in the statement fit into the following diagram:
X₁₁ - h₁₁ -> X₁₂
| |
v₁₁ v₁₂
↓ ↓
X₂₁ - h₂₁ -> X₂₂
| |
v₂₁ v₂₂
↓ ↓
X₃₁ - h₃₁ -> X₃₂
theorem
CategoryTheory.IsPushout.of_left
{C : Type u₁}
[Category.{v₁, u₁} C]
{X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C}
{h₁₁ : X₁₁ ⟶ X₁₂}
{h₁₂ : X₁₂ ⟶ X₁₃}
{h₂₁ : X₂₁ ⟶ X₂₂}
{h₂₂ : X₂₂ ⟶ X₂₃}
{v₁₁ : X₁₁ ⟶ X₂₁}
{v₁₂ : X₁₂ ⟶ X₂₂}
{v₁₃ : X₁₃ ⟶ X₂₃}
(s : IsPushout (CategoryStruct.comp h₁₁ h₁₂) v₁₁ v₁₃ (CategoryStruct.comp h₂₁ h₂₂))
(p : CategoryStruct.comp h₁₂ v₁₃ = CategoryStruct.comp v₁₂ h₂₂)
(t : IsPushout h₁₁ v₁₁ v₁₂ h₂₁)
:
IsPushout h₁₂ v₁₂ v₁₃ h₂₂
Given a pushout square assembled from a pushout square on the left and a commuting square on the right, the right square is a pushout square.
The objects in the statement fit into the following diagram:
X₁₁ - h₁₁ -> X₁₂ - h₁₂ -> X₁₃
| | |
v₁₁ v₁₂ v₁₃
↓ ↓ ↓
X₂₁ - h₂₁ -> X₂₂ - h₂₂ -> X₂₃
theorem
CategoryTheory.IsPushout.paste_vert_iff
{C : Type u₁}
[Category.{v₁, u₁} C]
{X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C}
{h₁₁ : X₁₁ ⟶ X₁₂}
{h₂₁ : X₂₁ ⟶ X₂₂}
{h₃₁ : X₃₁ ⟶ X₃₂}
{v₁₁ : X₁₁ ⟶ X₂₁}
{v₁₂ : X₁₂ ⟶ X₂₂}
{v₂₁ : X₂₁ ⟶ X₃₁}
{v₂₂ : X₂₂ ⟶ X₃₂}
(s : IsPushout h₁₁ v₁₁ v₁₂ h₂₁)
(e : CategoryStruct.comp h₂₁ v₂₂ = CategoryStruct.comp v₂₁ h₃₁)
:
IsPushout h₁₁ (CategoryStruct.comp v₁₁ v₂₁) (CategoryStruct.comp v₁₂ v₂₂) h₃₁ ↔ IsPushout h₂₁ v₂₁ v₂₂ h₃₁
theorem
CategoryTheory.IsPushout.paste_horiz_iff
{C : Type u₁}
[Category.{v₁, u₁} C]
{X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C}
{h₁₁ : X₁₁ ⟶ X₁₂}
{h₁₂ : X₁₂ ⟶ X₁₃}
{h₂₁ : X₂₁ ⟶ X₂₂}
{h₂₂ : X₂₂ ⟶ X₂₃}
{v₁₁ : X₁₁ ⟶ X₂₁}
{v₁₂ : X₁₂ ⟶ X₂₂}
{v₁₃ : X₁₃ ⟶ X₂₃}
(s : IsPushout h₁₁ v₁₁ v₁₂ h₂₁)
(e : CategoryStruct.comp h₁₂ v₁₃ = CategoryStruct.comp v₁₂ h₂₂)
:
IsPushout (CategoryStruct.comp h₁₁ h₁₂) v₁₁ v₁₃ (CategoryStruct.comp h₂₁ h₂₂) ↔ IsPushout h₁₂ v₁₂ v₁₃ h₂₂
theorem
CategoryTheory.IsPushout.of_top'
{C : Type u₁}
[Category.{v₁, u₁} C]
{X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C}
{h₁₁ : X₁₁ ⟶ X₁₂}
{h₂₁ : X₂₁ ⟶ X₂₂}
{h₃₁ : X₃₁ ⟶ X₃₂}
{v₁₁ : X₁₁ ⟶ X₂₁}
{v₁₂ : X₁₂ ⟶ X₂₂}
{v₁₃ : X₁₂ ⟶ X₃₂}
{v₂₁ : X₂₁ ⟶ X₃₁}
(s : IsPushout h₁₁ (CategoryStruct.comp v₁₁ v₂₁) v₁₃ h₃₁)
(t : IsPushout h₁₁ v₁₁ v₁₂ h₂₁)
:
IsPushout h₂₁ v₂₁ (t.desc v₁₃ (CategoryStruct.comp v₂₁ h₃₁) ⋯) h₃₁
Variant of IsPushout.of_top where v₂₂ is induced from a morphism v₁₃ : X₁₂ ⟶ X₃₂, and
the universal property of the top square.
The objects in the statement fit into the following diagram:
X₁₁ - h₁₁ -> X₁₂
| |
v₁₁ v₁₂
↓ ↓
X₂₁ - h₂₁ -> X₂₂
| |
v₂₁ v₂₂
↓ ↓
X₃₁ - h₃₁ -> X₃₂
theorem
CategoryTheory.IsPushout.of_left'
{C : Type u₁}
[Category.{v₁, u₁} C]
{X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C}
{h₁₁ : X₁₁ ⟶ X₁₂}
{h₁₂ : X₁₂ ⟶ X₁₃}
{h₂₁ : X₂₁ ⟶ X₂₂}
{h₂₃ : X₂₁ ⟶ X₂₃}
{v₁₁ : X₁₁ ⟶ X₂₁}
{v₁₂ : X₁₂ ⟶ X₂₂}
{v₁₃ : X₁₃ ⟶ X₂₃}
(s : IsPushout (CategoryStruct.comp h₁₁ h₁₂) v₁₁ v₁₃ h₂₃)
(t : IsPushout h₁₁ v₁₁ v₁₂ h₂₁)
:
IsPushout h₁₂ v₁₂ v₁₃ (t.desc (CategoryStruct.comp h₁₂ v₁₃) h₂₃ ⋯)
Variant of IsPushout.of_right where h₂₂ is induced from a morphism h₂₃ : X₂₁ ⟶ X₂₃, and
the universal property of the left square.
The objects in the statement fit into the following diagram:
X₁₁ - h₁₁ -> X₁₂ - h₁₂ -> X₁₃
| | |
v₁₁ v₁₂ v₁₃
↓ ↓ ↓
X₂₁ - h₂₁ -> X₂₂ - h₂₂ -> X₂₃
theorem
CategoryTheory.IsPushout.of_id_fst
{C : Type u₁}
[Category.{v₁, u₁} C]
{Z X : C}
{f : Z ⟶ X}
:
IsPushout (CategoryStruct.id Z) f f (CategoryStruct.id X)
theorem
CategoryTheory.IsPushout.of_id_snd
{C : Type u₁}
[Category.{v₁, u₁} C]
{Z X : C}
{f : Z ⟶ X}
:
IsPushout f (CategoryStruct.id Z) (CategoryStruct.id X) f
theorem
CategoryTheory.IsPushout.id_vert
{C : Type u₁}
[Category.{v₁, u₁} C]
{Z X : C}
(f : X ⟶ Z)
:
IsPushout f (CategoryStruct.id X) (CategoryStruct.id Z) f
The following diagram is a pullback
X --f--> Z
| |
id id
v v
X --f--> Z
theorem
CategoryTheory.IsPushout.id_horiz
{C : Type u₁}
[Category.{v₁, u₁} C]
{Z X : C}
(f : X ⟶ Z)
:
IsPushout (CategoryStruct.id X) f f (CategoryStruct.id Z)
The following diagram is a pullback
X --id--> X
| |
f f
v v
Z --id--> Z
theorem
CategoryTheory.IsPushout.of_coprod_inl_with_id
{C : Type u₁}
[Category.{v₁, u₁} C]
{A B : C}
(f : A ⟶ B)
(X : C)
[Limits.HasBinaryCoproduct A X]
[Limits.HasBinaryCoproduct B X]
:
In a category, given a morphism f : A ⟶ B and an object X,
this is the obvious pushout diagram:
A ⟶ A ⨿ X
| |
v v
B ⟶ B ⨿ X
theorem
CategoryTheory.IsPushout.of_isColimit_binaryCofan_of_isInitial
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y : C}
{c : Limits.BinaryCofan X Y}
(hc : Limits.IsColimit c)
{I : C}
(hI : Limits.IsInitial I)
:
IsPushout (hI.to ((Limits.pair X Y).obj { as := Limits.WalkingPair.right }))
(hI.to ((Limits.pair X Y).obj { as := Limits.WalkingPair.left })) c.inr c.inl
noncomputable def
CategoryTheory.IsPullback.isLimitFork
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
{f : X ⟶ Y}
{g g' : Y ⟶ Z}
(H : IsPullback f f g g')
:
If f : X ⟶ Y, g g' : Y ⟶ Z forms a pullback square, then f is the equalizer of
g and g'.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CategoryTheory.IsPushout.isLimitFork
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
{f f' : X ⟶ Y}
{g : Y ⟶ Z}
(H : IsPushout f f' g g)
:
If f f' : X ⟶ Y, g : Y ⟶ Z forms a pushout square, then g is the coequalizer of
f and f'.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Functor.map_isPullback
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
[Limits.PreservesLimit (Limits.cospan h i) F]
(s : IsPullback f g h i)
:
IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
theorem
CategoryTheory.Functor.map_isPushout
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
[Limits.PreservesColimit (Limits.span f g) F]
(s : IsPushout f g h i)
:
theorem
CategoryTheory.IsPullback.map
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
[Limits.PreservesLimit (Limits.cospan h i) F]
(s : IsPullback f g h i)
:
IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
Alias of CategoryTheory.Functor.map_isPullback.
theorem
CategoryTheory.IsPushout.map
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
[Limits.PreservesColimit (Limits.span f g) F]
(s : IsPushout f g h i)
:
Alias of CategoryTheory.Functor.map_isPushout.
theorem
CategoryTheory.IsPullback.of_map
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
[Limits.ReflectsLimit (Limits.cospan h i) F]
(e : CategoryStruct.comp f h = CategoryStruct.comp g i)
(H : IsPullback (F.map f) (F.map g) (F.map h) (F.map i))
:
IsPullback f g h i
theorem
CategoryTheory.IsPullback.of_map_of_faithful
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
[Limits.ReflectsLimit (Limits.cospan h i) F]
[F.Faithful]
(H : IsPullback (F.map f) (F.map g) (F.map h) (F.map i))
:
IsPullback f g h i
theorem
CategoryTheory.IsPullback.map_iff
{C : Type u₁}
[Category.{v₁, u₁} C]
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
{D : Type u_1}
[Category.{v_1, u_1} D]
(F : Functor C D)
[Limits.PreservesLimit (Limits.cospan h i) F]
[Limits.ReflectsLimit (Limits.cospan h i) F]
(e : CategoryStruct.comp f h = CategoryStruct.comp g i)
:
theorem
CategoryTheory.IsPushout.of_map
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
[Limits.ReflectsColimit (Limits.span f g) F]
(e : CategoryStruct.comp f h = CategoryStruct.comp g i)
(H : IsPushout (F.map f) (F.map g) (F.map h) (F.map i))
:
IsPushout f g h i
theorem
CategoryTheory.IsPushout.of_map_of_faithful
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
[Limits.ReflectsColimit (Limits.span f g) F]
[F.Faithful]
(H : IsPushout (F.map f) (F.map g) (F.map h) (F.map i))
:
IsPushout f g h i
theorem
CategoryTheory.IsPushout.map_iff
{C : Type u₁}
[Category.{v₁, u₁} C]
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
{D : Type u_1}
[Category.{v_1, u_1} D]
(F : Functor C D)
[Limits.PreservesColimit (Limits.span f g) F]
[Limits.ReflectsColimit (Limits.span f g) F]
(e : CategoryStruct.comp f h = CategoryStruct.comp g i)
: