Pullback and pushout squares, and bi-Cartesian squares #
We provide another API for pullbacks and pushouts.
IsPullback fst snd f g is the proposition that
P --fst--> X
| |
snd f
| |
v v
Y ---g---> Z
is a pullback square.
(And similarly for IsPushout.)
We provide the glue to go back and forth to the usual IsLimit API for pullbacks, and prove
IsPullback (pullback.fst f g) (pullback.snd f g) f g
for the usual pullback f g provided by the HasLimit API.
We don't attempt to restate everything we know about pullbacks in this language, but do restate the pasting lemmas.
We define bi-Cartesian squares, and show that the pullback and pushout squares for a biproduct are bi-Cartesian.
def
CategoryTheory.CommSq.cone
{C : Type u₁}
[Category.{v₁, u₁} C]
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
(s : CommSq f g h i)
:
The (not necessarily limiting) PullbackCone h i implicit in the statement
that we have CommSq f g h i.
Equations
Instances For
def
CategoryTheory.CommSq.cocone
{C : Type u₁}
[Category.{v₁, u₁} C]
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
(s : CommSq f g h i)
:
The (not necessarily limiting) PushoutCocone f g implicit in the statement
that we have CommSq f g h i.
Equations
Instances For
def
CategoryTheory.CommSq.coneOp
{C : Type u₁}
[Category.{v₁, u₁} C]
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
(p : CommSq f g h i)
:
The pushout cocone in the opposite category associated to the cone of a commutative square identifies to the cocone of the flipped commutative square in the opposite category
Equations
Instances For
def
CategoryTheory.CommSq.coconeOp
{C : Type u₁}
[Category.{v₁, u₁} C]
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
(p : CommSq f g h i)
:
The pullback cone in the opposite category associated to the cocone of a commutative square identifies to the cone of the flipped commutative square in the opposite category
Equations
Instances For
def
CategoryTheory.CommSq.coneUnop
{C : Type u₁}
[Category.{v₁, u₁} C]
{W X Y Z : Cᵒᵖ}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
(p : CommSq f g h i)
:
The pushout cocone obtained from the pullback cone associated to a commutative square in the opposite category identifies to the cocone associated to the flipped square.
Equations
Instances For
def
CategoryTheory.CommSq.coconeUnop
{C : Type u₁}
[Category.{v₁, u₁} C]
{W X Y Z : Cᵒᵖ}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
(p : CommSq f g h i)
:
The pullback cone obtained from the pushout cone associated to a commutative square in the opposite category identifies to the cone associated to the flipped square.
Equations
Instances For
structure
CategoryTheory.IsPullback
{C : Type u₁}
[Category.{v₁, u₁} C]
{P X Y Z : C}
(fst : P ⟶ X)
(snd : P ⟶ Y)
(f : X ⟶ Z)
(g : Y ⟶ Z)
extends CategoryTheory.CommSq fst snd f g :
The proposition that a square
P --fst--> X
| |
snd f
| |
v v
Y ---g---> Z
is a pullback square. (Also known as a fibered product or Cartesian square.)
- isLimit' : Nonempty (Limits.IsLimit (Limits.PullbackCone.mk fst snd ⋯))
the pullback cone is a limit
Instances For
structure
CategoryTheory.IsPushout
{C : Type u₁}
[Category.{v₁, u₁} C]
{Z X Y P : C}
(f : Z ⟶ X)
(g : Z ⟶ Y)
(inl : X ⟶ P)
(inr : Y ⟶ P)
extends CategoryTheory.CommSq f g inl inr :
The proposition that a square
Z ---f---> X
| |
g inl
| |
v v
Y --inr--> P
is a pushout square. (Also known as a fiber coproduct or co-Cartesian square.)
- isColimit' : Nonempty (Limits.IsColimit (Limits.PushoutCocone.mk inl inr ⋯))
the pushout cocone is a colimit
Instances For
structure
CategoryTheory.BicartesianSq
{C : Type u₁}
[Category.{v₁, u₁} C]
{W X Y Z : C}
(f : W ⟶ X)
(g : W ⟶ Y)
(h : X ⟶ Z)
(i : Y ⟶ Z)
extends CategoryTheory.IsPullback f g h i, CategoryTheory.IsPushout f g h i :
A bi-Cartesian square is a commutative square
W ---f---> X
| |
g h
| |
v v
Y ---i---> Z
that is both a pullback square and a pushout square.
- isLimit' : Nonempty (Limits.IsLimit (Limits.PullbackCone.mk f g ⋯))
- isColimit' : Nonempty (Limits.IsColimit (Limits.PushoutCocone.mk h i ⋯))
Instances For
We begin by providing some glue between IsPullback and the IsLimit and HasLimit APIs.
(And similarly for IsPushout.)
def
CategoryTheory.IsPullback.cone
{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)
:
The (limiting) PullbackCone f g implicit in the statement
that we have an IsPullback fst snd f g.
Instances For
@[simp]
theorem
CategoryTheory.IsPullback.cone_fst
{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)
:
@[simp]
theorem
CategoryTheory.IsPullback.cone_snd
{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)
:
noncomputable def
CategoryTheory.IsPullback.isLimit
{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)
:
The cone obtained from IsPullback fst snd f g is a limit cone.
Instances For
noncomputable def
CategoryTheory.IsPullback.lift
{C : Type u₁}
[Category.{v₁, u₁} C]
{P X Y Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(hP : IsPullback fst snd f g)
{W : C}
(h : W ⟶ X)
(k : W ⟶ Y)
(w : CategoryStruct.comp h f = CategoryStruct.comp k g)
:
API for PullbackCone.IsLimit.lift for IsPullback
Equations
- hP.lift h k w = CategoryTheory.Limits.PullbackCone.IsLimit.lift hP.isLimit h k w
Instances For
@[simp]
theorem
CategoryTheory.IsPullback.lift_fst
{C : Type u₁}
[Category.{v₁, u₁} C]
{P X Y Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(hP : IsPullback fst snd f g)
{W : C}
(h : W ⟶ X)
(k : W ⟶ Y)
(w : CategoryStruct.comp h f = CategoryStruct.comp k g)
:
@[simp]
theorem
CategoryTheory.IsPullback.lift_fst_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{P X Y Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(hP : IsPullback fst snd f g)
{W : C}
(h : W ⟶ X)
(k : W ⟶ Y)
(w : CategoryStruct.comp h f = CategoryStruct.comp k g)
{Z✝ : C}
(h✝ : X ⟶ Z✝)
:
@[simp]
theorem
CategoryTheory.IsPullback.lift_snd
{C : Type u₁}
[Category.{v₁, u₁} C]
{P X Y Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(hP : IsPullback fst snd f g)
{W : C}
(h : W ⟶ X)
(k : W ⟶ Y)
(w : CategoryStruct.comp h f = CategoryStruct.comp k g)
:
@[simp]
theorem
CategoryTheory.IsPullback.lift_snd_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{P X Y Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(hP : IsPullback fst snd f g)
{W : C}
(h : W ⟶ X)
(k : W ⟶ Y)
(w : CategoryStruct.comp h f = CategoryStruct.comp k g)
{Z✝ : C}
(h✝ : Y ⟶ Z✝)
:
theorem
CategoryTheory.IsPullback.hom_ext
{C : Type u₁}
[Category.{v₁, u₁} C]
{P X Y Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(hP : IsPullback fst snd f g)
{W : C}
{k l : W ⟶ P}
(h₀ : CategoryStruct.comp k fst = CategoryStruct.comp l fst)
(h₁ : CategoryStruct.comp k snd = CategoryStruct.comp l snd)
:
theorem
CategoryTheory.IsPullback.of_isLimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{c : Limits.PullbackCone f g}
(h : Limits.IsLimit c)
:
IsPullback c.fst c.snd f g
If c is a limiting pullback cone, then we have an IsPullback c.fst c.snd f g.
theorem
CategoryTheory.IsPullback.of_isLimit'
{C : Type u₁}
[Category.{v₁, u₁} C]
{P X Y Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(w : CommSq fst snd f g)
(h : Limits.IsLimit w.cone)
:
IsPullback fst snd f g
A variant of of_isLimit that is more useful with apply.
theorem
CategoryTheory.IsPullback.of_isLimit_cone
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Functor Limits.WalkingCospan C}
{c : Limits.Cone D}
(hc : Limits.IsLimit c)
:
Variant of of_isLimit for an arbitrary cone on a diagram WalkingCospan ⥤ C.
theorem
CategoryTheory.IsPullback.hasPullback
{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)
:
theorem
CategoryTheory.IsPullback.of_hasPullback
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[Limits.HasPullback f g]
:
IsPullback (Limits.pullback.fst f g) (Limits.pullback.snd f g) f g
The pullback provided by HasPullback f g fits into an IsPullback.
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_hasBinaryProduct
{C : Type u₁}
[Category.{v₁, u₁} C]
(X Y : C)
[Limits.HasBinaryProduct X Y]
[Limits.HasZeroObject C]
[Limits.HasZeroMorphisms C]
:
noncomputable def
CategoryTheory.IsPullback.isoIsPullback
{C : Type u₁}
[Category.{v₁, u₁} C]
{P : C}
(X Y : C)
{Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{P' : C}
{fst' : P' ⟶ X}
{snd' : P' ⟶ Y}
(h : IsPullback fst snd f g)
(h' : IsPullback fst' snd' f g)
:
Any object at the top left of a pullback square is isomorphic to the object at the top left of any other pullback square with the same cospan.
Equations
Instances For
@[simp]
theorem
CategoryTheory.IsPullback.isoIsPullback_hom_fst
{C : Type u₁}
[Category.{v₁, u₁} C]
{P : C}
(X Y : C)
{Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{P' : C}
{fst' : P' ⟶ X}
{snd' : P' ⟶ Y}
(h : IsPullback fst snd f g)
(h' : IsPullback fst' snd' f g)
:
@[simp]
theorem
CategoryTheory.IsPullback.isoIsPullback_hom_fst_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{P : C}
(X Y : C)
{Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{P' : C}
{fst' : P' ⟶ X}
{snd' : P' ⟶ Y}
(h : IsPullback fst snd f g)
(h' : IsPullback fst' snd' f g)
{Z✝ : C}
(h✝ : X ⟶ Z✝)
:
CategoryStruct.comp (isoIsPullback X Y h h').hom (CategoryStruct.comp fst' h✝) = CategoryStruct.comp fst h✝
@[simp]
theorem
CategoryTheory.IsPullback.isoIsPullback_hom_snd
{C : Type u₁}
[Category.{v₁, u₁} C]
{P : C}
(X Y : C)
{Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{P' : C}
{fst' : P' ⟶ X}
{snd' : P' ⟶ Y}
(h : IsPullback fst snd f g)
(h' : IsPullback fst' snd' f g)
:
@[simp]
theorem
CategoryTheory.IsPullback.isoIsPullback_hom_snd_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{P : C}
(X Y : C)
{Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{P' : C}
{fst' : P' ⟶ X}
{snd' : P' ⟶ Y}
(h : IsPullback fst snd f g)
(h' : IsPullback fst' snd' f g)
{Z✝ : C}
(h✝ : Y ⟶ Z✝)
:
CategoryStruct.comp (isoIsPullback X Y h h').hom (CategoryStruct.comp snd' h✝) = CategoryStruct.comp snd h✝
@[simp]
theorem
CategoryTheory.IsPullback.isoIsPullback_inv_fst
{C : Type u₁}
[Category.{v₁, u₁} C]
{P : C}
(X Y : C)
{Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{P' : C}
{fst' : P' ⟶ X}
{snd' : P' ⟶ Y}
(h : IsPullback fst snd f g)
(h' : IsPullback fst' snd' f g)
:
@[simp]
theorem
CategoryTheory.IsPullback.isoIsPullback_inv_fst_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{P : C}
(X Y : C)
{Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{P' : C}
{fst' : P' ⟶ X}
{snd' : P' ⟶ Y}
(h : IsPullback fst snd f g)
(h' : IsPullback fst' snd' f g)
{Z✝ : C}
(h✝ : X ⟶ Z✝)
:
CategoryStruct.comp (isoIsPullback X Y h h').inv (CategoryStruct.comp fst h✝) = CategoryStruct.comp fst' h✝
@[simp]
theorem
CategoryTheory.IsPullback.isoIsPullback_inv_snd
{C : Type u₁}
[Category.{v₁, u₁} C]
{P : C}
(X Y : C)
{Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{P' : C}
{fst' : P' ⟶ X}
{snd' : P' ⟶ Y}
(h : IsPullback fst snd f g)
(h' : IsPullback fst' snd' f g)
:
@[simp]
theorem
CategoryTheory.IsPullback.isoIsPullback_inv_snd_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{P : C}
(X Y : C)
{Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{P' : C}
{fst' : P' ⟶ X}
{snd' : P' ⟶ Y}
(h : IsPullback fst snd f g)
(h' : IsPullback fst' snd' f g)
{Z✝ : C}
(h✝ : Y ⟶ Z✝)
:
CategoryStruct.comp (isoIsPullback X Y h h').inv (CategoryStruct.comp snd h✝) = CategoryStruct.comp snd' h✝
noncomputable def
CategoryTheory.IsPullback.isoPullback
{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)
[Limits.HasPullback f g]
:
Any object at the top left of a pullback square is
isomorphic to the pullback provided by the HasLimit API.
Equations
- h.isoPullback = (CategoryTheory.Limits.limit.isoLimitCone { cone := h.cone, isLimit := h.isLimit }).symm
Instances For
@[simp]
theorem
CategoryTheory.IsPullback.isoPullback_hom_fst
{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)
[Limits.HasPullback f g]
:
@[simp]
theorem
CategoryTheory.IsPullback.isoPullback_hom_fst_assoc
{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)
[Limits.HasPullback f g]
{Z✝ : C}
(h✝ : X ⟶ Z✝)
:
CategoryStruct.comp h.isoPullback.hom (CategoryStruct.comp (Limits.pullback.fst f g) h✝) = CategoryStruct.comp fst h✝
@[simp]
theorem
CategoryTheory.IsPullback.isoPullback_hom_snd
{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)
[Limits.HasPullback f g]
:
@[simp]
theorem
CategoryTheory.IsPullback.isoPullback_hom_snd_assoc
{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)
[Limits.HasPullback f g]
{Z✝ : C}
(h✝ : Y ⟶ Z✝)
:
CategoryStruct.comp h.isoPullback.hom (CategoryStruct.comp (Limits.pullback.snd f g) h✝) = CategoryStruct.comp snd h✝
@[simp]
theorem
CategoryTheory.IsPullback.isoPullback_inv_fst
{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)
[Limits.HasPullback f g]
:
@[simp]
theorem
CategoryTheory.IsPullback.isoPullback_inv_fst_assoc
{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)
[Limits.HasPullback f g]
{Z✝ : C}
(h✝ : X ⟶ Z✝)
:
CategoryStruct.comp h.isoPullback.inv (CategoryStruct.comp fst h✝) = CategoryStruct.comp (Limits.pullback.fst f g) h✝
@[simp]
theorem
CategoryTheory.IsPullback.isoPullback_inv_snd
{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)
[Limits.HasPullback f g]
:
@[simp]
theorem
CategoryTheory.IsPullback.isoPullback_inv_snd_assoc
{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)
[Limits.HasPullback f g]
{Z✝ : C}
(h✝ : Y ⟶ Z✝)
:
CategoryStruct.comp h.isoPullback.inv (CategoryStruct.comp snd h✝) = CategoryStruct.comp (Limits.pullback.snd f g) h✝
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.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
def
CategoryTheory.IsPushout.cocone
{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)
:
The (colimiting) PushoutCocone f g implicit in the statement
that we have an IsPushout f g inl inr.
Instances For
noncomputable def
CategoryTheory.IsPushout.isColimit
{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)
:
The cocone obtained from IsPushout f g inl inr is a colimit cocone.
Instances For
noncomputable def
CategoryTheory.IsPushout.desc
{C : Type u₁}
[Category.{v₁, u₁} C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(hP : IsPushout f g inl inr)
{W : C}
(h : X ⟶ W)
(k : Y ⟶ W)
(w : CategoryStruct.comp f h = CategoryStruct.comp g k)
:
API for PushoutCocone.IsColimit.lift for IsPushout
Equations
- hP.desc h k w = CategoryTheory.Limits.PushoutCocone.IsColimit.desc hP.isColimit h k w
Instances For
@[simp]
theorem
CategoryTheory.IsPushout.inl_desc
{C : Type u₁}
[Category.{v₁, u₁} C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(hP : IsPushout f g inl inr)
{W : C}
(h : X ⟶ W)
(k : Y ⟶ W)
(w : CategoryStruct.comp f h = CategoryStruct.comp g k)
:
@[simp]
theorem
CategoryTheory.IsPushout.inl_desc_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(hP : IsPushout f g inl inr)
{W : C}
(h : X ⟶ W)
(k : Y ⟶ W)
(w : CategoryStruct.comp f h = CategoryStruct.comp g k)
{Z✝ : C}
(h✝ : W ⟶ Z✝)
:
@[simp]
theorem
CategoryTheory.IsPushout.inr_desc
{C : Type u₁}
[Category.{v₁, u₁} C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(hP : IsPushout f g inl inr)
{W : C}
(h : X ⟶ W)
(k : Y ⟶ W)
(w : CategoryStruct.comp f h = CategoryStruct.comp g k)
:
@[simp]
theorem
CategoryTheory.IsPushout.inr_desc_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(hP : IsPushout f g inl inr)
{W : C}
(h : X ⟶ W)
(k : Y ⟶ W)
(w : CategoryStruct.comp f h = CategoryStruct.comp g k)
{Z✝ : C}
(h✝ : W ⟶ Z✝)
:
theorem
CategoryTheory.IsPushout.hom_ext
{C : Type u₁}
[Category.{v₁, u₁} C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(hP : IsPushout f g inl inr)
{W : C}
{k l : P ⟶ W}
(h₀ : CategoryStruct.comp inl k = CategoryStruct.comp inl l)
(h₁ : CategoryStruct.comp inr k = CategoryStruct.comp inr l)
:
theorem
CategoryTheory.IsPushout.of_isColimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{Z X Y : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{c : Limits.PushoutCocone f g}
(h : Limits.IsColimit c)
:
If c is a colimiting pushout cocone, then we have an IsPushout f g c.inl c.inr.
theorem
CategoryTheory.IsPushout.of_isColimit'
{C : Type u₁}
[Category.{v₁, u₁} C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(w : CommSq f g inl inr)
(h : Limits.IsColimit w.cocone)
:
IsPushout f g inl inr
A variant of of_isColimit that is more useful with apply.
theorem
CategoryTheory.IsPushout.of_isColimit_cocone
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Functor Limits.WalkingSpan C}
{c : Limits.Cocone D}
(hc : Limits.IsColimit c)
:
Variant of of_isColimit for an arbitrary cocone on a diagram WalkingSpan ⥤ C.
theorem
CategoryTheory.IsPushout.hasPushout
{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)
:
theorem
CategoryTheory.IsPushout.of_hasPushout
{C : Type u₁}
[Category.{v₁, u₁} C]
{Z X Y : C}
(f : Z ⟶ X)
(g : Z ⟶ Y)
[Limits.HasPushout f g]
:
IsPushout f g (Limits.pushout.inl f g) (Limits.pushout.inr f g)
The pushout provided by HasPushout f g fits into an IsPushout.
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_hasBinaryCoproduct
{C : Type u₁}
[Category.{v₁, u₁} C]
(X Y : C)
[Limits.HasBinaryCoproduct X Y]
[Limits.HasZeroObject C]
[Limits.HasZeroMorphisms C]
:
noncomputable def
CategoryTheory.IsPushout.isoIsPushout
{C : Type u₁}
[Category.{v₁, u₁} C]
{Z : C}
(X Y : C)
{P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
{P' : C}
{inl' : X ⟶ P'}
{inr' : Y ⟶ P'}
(h : IsPushout f g inl inr)
(h' : IsPushout f g inl' inr')
:
Any object at the bottom right of a pushout square is isomorphic to the object at the bottom right of any other pushout square with the same span.
Equations
Instances For
@[simp]
theorem
CategoryTheory.IsPushout.inl_isoIsPushout_hom_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{Z : C}
(X Y : C)
{P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
{P' : C}
{inl' : X ⟶ P'}
{inr' : Y ⟶ P'}
(h : IsPushout f g inl inr)
(h' : IsPushout f g inl' inr')
{Z✝ : C}
(h✝ : P' ⟶ Z✝)
:
CategoryStruct.comp inl (CategoryStruct.comp (isoIsPushout X Y h h').hom h✝) = CategoryStruct.comp inl' h✝
@[simp]
theorem
CategoryTheory.IsPushout.inr_isoIsPushout_hom_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{Z : C}
(X Y : C)
{P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
{P' : C}
{inl' : X ⟶ P'}
{inr' : Y ⟶ P'}
(h : IsPushout f g inl inr)
(h' : IsPushout f g inl' inr')
{Z✝ : C}
(h✝ : P' ⟶ Z✝)
:
CategoryStruct.comp inr (CategoryStruct.comp (isoIsPushout X Y h h').hom h✝) = CategoryStruct.comp inr' h✝
@[simp]
theorem
CategoryTheory.IsPushout.inl_isoIsPushout_inv_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{Z : C}
(X Y : C)
{P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
{P' : C}
{inl' : X ⟶ P'}
{inr' : Y ⟶ P'}
(h : IsPushout f g inl inr)
(h' : IsPushout f g inl' inr')
{Z✝ : C}
(h✝ : P ⟶ Z✝)
:
CategoryStruct.comp inl' (CategoryStruct.comp (isoIsPushout X Y h h').inv h✝) = CategoryStruct.comp inl h✝
@[simp]
theorem
CategoryTheory.IsPushout.inr_isoIsPushout_inv_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{Z : C}
(X Y : C)
{P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
{P' : C}
{inl' : X ⟶ P'}
{inr' : Y ⟶ P'}
(h : IsPushout f g inl inr)
(h' : IsPushout f g inl' inr')
{Z✝ : C}
(h✝ : P ⟶ Z✝)
:
CategoryStruct.comp inr' (CategoryStruct.comp (isoIsPushout X Y h h').inv h✝) = CategoryStruct.comp inr h✝
noncomputable def
CategoryTheory.IsPushout.isoPushout
{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)
[Limits.HasPushout f g]
:
Any object at the top left of a pullback square is
isomorphic to the pullback provided by the HasLimit API.
Equations
- h.isoPushout = (CategoryTheory.Limits.colimit.isoColimitCocone { cocone := h.cocone, isColimit := h.isColimit }).symm
Instances For
@[simp]
theorem
CategoryTheory.IsPushout.inl_isoPushout_inv
{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)
[Limits.HasPushout f g]
:
@[simp]
theorem
CategoryTheory.IsPushout.inl_isoPushout_inv_assoc
{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)
[Limits.HasPushout f g]
{Z✝ : C}
(h✝ : P ⟶ Z✝)
:
CategoryStruct.comp (Limits.pushout.inl f g) (CategoryStruct.comp h.isoPushout.inv h✝) = CategoryStruct.comp inl h✝
@[simp]
theorem
CategoryTheory.IsPushout.inr_isoPushout_inv
{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)
[Limits.HasPushout f g]
:
@[simp]
theorem
CategoryTheory.IsPushout.inr_isoPushout_inv_assoc
{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)
[Limits.HasPushout f g]
{Z✝ : C}
(h✝ : P ⟶ Z✝)
:
CategoryStruct.comp (Limits.pushout.inr f g) (CategoryStruct.comp h.isoPushout.inv h✝) = CategoryStruct.comp inr h✝
@[simp]
theorem
CategoryTheory.IsPushout.inl_isoPushout_hom
{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)
[Limits.HasPushout f g]
:
@[simp]
theorem
CategoryTheory.IsPushout.inl_isoPushout_hom_assoc
{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)
[Limits.HasPushout f g]
{Z✝ : C}
(h✝ : Limits.pushout f g ⟶ Z✝)
:
CategoryStruct.comp inl (CategoryStruct.comp h.isoPushout.hom h✝) = CategoryStruct.comp (Limits.pushout.inl f g) h✝
@[simp]
theorem
CategoryTheory.IsPushout.inr_isoPushout_hom
{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)
[Limits.HasPushout f g]
:
@[simp]
theorem
CategoryTheory.IsPushout.inr_isoPushout_hom_assoc
{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)
[Limits.HasPushout f g]
{Z✝ : C}
(h✝ : Limits.pushout f g ⟶ Z✝)
:
CategoryStruct.comp inr (CategoryStruct.comp h.isoPushout.hom h✝) = CategoryStruct.comp (Limits.pushout.inr f g) h✝
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.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.IsPullback.flip
{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)
:
IsPullback snd fst g f
theorem
CategoryTheory.IsPullback.flip_iff
{C : Type u₁}
[Category.{v₁, u₁} C]
{P X Y Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
:
@[simp]
theorem
CategoryTheory.IsPullback.zero_left
{C : Type u₁}
[Category.{v₁, u₁} C]
[Limits.HasZeroObject C]
[Limits.HasZeroMorphisms C]
(X : C)
:
IsPullback 0 0 (CategoryStruct.id X) 0
The square with 0 : 0 ⟶ 0 on the left and 𝟙 X on the right is a pullback square.
@[simp]
theorem
CategoryTheory.IsPullback.zero_top
{C : Type u₁}
[Category.{v₁, u₁} C]
[Limits.HasZeroObject C]
[Limits.HasZeroMorphisms C]
(X : C)
:
IsPullback 0 0 0 (CategoryStruct.id X)
The square with 0 : 0 ⟶ 0 on the top and 𝟙 X on the bottom is a pullback square.
@[simp]
theorem
CategoryTheory.IsPullback.zero_right
{C : Type u₁}
[Category.{v₁, u₁} C]
[Limits.HasZeroObject C]
[Limits.HasZeroMorphisms C]
(X : C)
:
IsPullback 0 (CategoryStruct.id X) 0 0
The square with 0 : 0 ⟶ 0 on the right and 𝟙 X on the left is a pullback square.
@[simp]
theorem
CategoryTheory.IsPullback.zero_bot
{C : Type u₁}
[Category.{v₁, u₁} C]
[Limits.HasZeroObject C]
[Limits.HasZeroMorphisms C]
(X : C)
:
IsPullback (CategoryStruct.id X) 0 0 0
The square with 0 : 0 ⟶ 0 on the bottom and 𝟙 X on the top is a pullback square.
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_isBilimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y : C}
[Limits.HasZeroObject C]
[Limits.HasZeroMorphisms C]
{b : Limits.BinaryBicone X Y}
(h : b.IsBilimit)
:
IsPullback b.fst b.snd 0 0
@[simp]
theorem
CategoryTheory.IsPullback.of_has_biproduct
{C : Type u₁}
[Category.{v₁, u₁} C]
[Limits.HasZeroObject C]
[Limits.HasZeroMorphisms C]
(X Y : C)
[Limits.HasBinaryBiproduct X Y]
:
theorem
CategoryTheory.IsPullback.inl_snd'
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y : C}
[Limits.HasZeroObject C]
[Limits.HasZeroMorphisms C]
{b : Limits.BinaryBicone X Y}
(h : b.IsBilimit)
:
IsPullback b.inl 0 b.snd 0
@[simp]
theorem
CategoryTheory.IsPullback.inl_snd
{C : Type u₁}
[Category.{v₁, u₁} C]
[Limits.HasZeroObject C]
[Limits.HasZeroMorphisms C]
(X Y : C)
[Limits.HasBinaryBiproduct X Y]
:
The square
X --inl--> X ⊞ Y
| |
0 snd
| |
v v
0 ---0-----> Y
is a pullback square.
theorem
CategoryTheory.IsPullback.inr_fst'
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y : C}
[Limits.HasZeroObject C]
[Limits.HasZeroMorphisms C]
{b : Limits.BinaryBicone X Y}
(h : b.IsBilimit)
:
IsPullback b.inr 0 b.fst 0
@[simp]
theorem
CategoryTheory.IsPullback.inr_fst
{C : Type u₁}
[Category.{v₁, u₁} C]
[Limits.HasZeroObject C]
[Limits.HasZeroMorphisms C]
(X Y : C)
[Limits.HasBinaryBiproduct X Y]
:
The square
Y --inr--> X ⊞ Y
| |
0 fst
| |
v v
0 ---0-----> X
is a pullback square.
theorem
CategoryTheory.IsPullback.of_is_bilimit'
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y : C}
[Limits.HasZeroObject C]
[Limits.HasZeroMorphisms C]
{b : Limits.BinaryBicone X Y}
(h : b.IsBilimit)
:
IsPullback 0 0 b.inl b.inr
theorem
CategoryTheory.IsPullback.of_hasBinaryBiproduct
{C : Type u₁}
[Category.{v₁, u₁} C]
[Limits.HasZeroObject C]
[Limits.HasZeroMorphisms C]
(X Y : C)
[Limits.HasBinaryBiproduct X Y]
:
instance
CategoryTheory.IsPullback.hasPullback_biprod_fst_biprod_snd
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y : C}
[Limits.HasZeroObject C]
[Limits.HasZeroMorphisms C]
[Limits.HasBinaryBiproduct X Y]
:
def
CategoryTheory.IsPullback.pullbackBiprodInlBiprodInr
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y : C}
[Limits.HasZeroObject C]
[Limits.HasZeroMorphisms C]
[Limits.HasBinaryBiproduct X Y]
:
The pullback of biprod.inl and biprod.inr is the zero object.
Equations
- CategoryTheory.IsPullback.pullbackBiprodInlBiprodInr = CategoryTheory.Limits.limit.isoLimitCone { cone := ⋯.cone, isLimit := ⋯.isLimit }
Instances For
theorem
CategoryTheory.IsPullback.op
{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)
:
theorem
CategoryTheory.IsPullback.unop
{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)
:
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.flip
{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)
:
IsPushout g f inr inl
@[simp]
theorem
CategoryTheory.IsPushout.zero_right
{C : Type u₁}
[Category.{v₁, u₁} C]
[Limits.HasZeroObject C]
[Limits.HasZeroMorphisms C]
(X : C)
:
IsPushout 0 (CategoryStruct.id X) 0 0
The square with 0 : 0 ⟶ 0 on the right and 𝟙 X on the left is a pushout square.
@[simp]
theorem
CategoryTheory.IsPushout.zero_bot
{C : Type u₁}
[Category.{v₁, u₁} C]
[Limits.HasZeroObject C]
[Limits.HasZeroMorphisms C]
(X : C)
:
IsPushout (CategoryStruct.id X) 0 0 0
The square with 0 : 0 ⟶ 0 on the bottom and 𝟙 X on the top is a pushout square.
@[simp]
theorem
CategoryTheory.IsPushout.zero_left
{C : Type u₁}
[Category.{v₁, u₁} C]
[Limits.HasZeroObject C]
[Limits.HasZeroMorphisms C]
(X : C)
:
IsPushout 0 0 (CategoryStruct.id X) 0
The square with 0 : 0 ⟶ 0 on the right left 𝟙 X on the right is a pushout square.
@[simp]
theorem
CategoryTheory.IsPushout.zero_top
{C : Type u₁}
[Category.{v₁, u₁} C]
[Limits.HasZeroObject C]
[Limits.HasZeroMorphisms C]
(X : C)
:
IsPushout 0 0 0 (CategoryStruct.id X)
The square with 0 : 0 ⟶ 0 on the top and 𝟙 X on the bottom is a pushout square.
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_isBilimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y : C}
[Limits.HasZeroObject C]
[Limits.HasZeroMorphisms C]
{b : Limits.BinaryBicone X Y}
(h : b.IsBilimit)
:
@[simp]
theorem
CategoryTheory.IsPushout.of_has_biproduct
{C : Type u₁}
[Category.{v₁, u₁} C]
[Limits.HasZeroObject C]
[Limits.HasZeroMorphisms C]
(X Y : C)
[Limits.HasBinaryBiproduct X Y]
:
theorem
CategoryTheory.IsPushout.inl_snd'
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y : C}
[Limits.HasZeroObject C]
[Limits.HasZeroMorphisms C]
{b : Limits.BinaryBicone X Y}
(h : b.IsBilimit)
:
theorem
CategoryTheory.IsPushout.inl_snd
{C : Type u₁}
[Category.{v₁, u₁} C]
[Limits.HasZeroObject C]
[Limits.HasZeroMorphisms C]
(X Y : C)
[Limits.HasBinaryBiproduct X Y]
:
The square
X --inl--> X ⊞ Y
| |
0 snd
| |
v v
0 ---0-----> Y
is a pushout square.
theorem
CategoryTheory.IsPushout.inr_fst'
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y : C}
[Limits.HasZeroObject C]
[Limits.HasZeroMorphisms C]
{b : Limits.BinaryBicone X Y}
(h : b.IsBilimit)
:
theorem
CategoryTheory.IsPushout.inr_fst
{C : Type u₁}
[Category.{v₁, u₁} C]
[Limits.HasZeroObject C]
[Limits.HasZeroMorphisms C]
(X Y : C)
[Limits.HasBinaryBiproduct X Y]
:
The square
Y --inr--> X ⊞ Y
| |
0 fst
| |
v v
0 ---0-----> X
is a pushout square.
theorem
CategoryTheory.IsPushout.of_is_bilimit'
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y : C}
[Limits.HasZeroObject C]
[Limits.HasZeroMorphisms C]
{b : Limits.BinaryBicone X Y}
(h : b.IsBilimit)
:
theorem
CategoryTheory.IsPushout.of_hasBinaryBiproduct
{C : Type u₁}
[Category.{v₁, u₁} C]
[Limits.HasZeroObject C]
[Limits.HasZeroMorphisms C]
(X Y : C)
[Limits.HasBinaryBiproduct X Y]
:
instance
CategoryTheory.IsPushout.hasPushout_biprod_fst_biprod_snd
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y : C}
[Limits.HasZeroObject C]
[Limits.HasZeroMorphisms C]
[Limits.HasBinaryBiproduct X Y]
:
def
CategoryTheory.IsPushout.pushoutBiprodFstBiprodSnd
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y : C}
[Limits.HasZeroObject C]
[Limits.HasZeroMorphisms C]
[Limits.HasBinaryBiproduct X Y]
:
The pushout of biprod.fst and biprod.snd is the zero object.
Equations
- CategoryTheory.IsPushout.pushoutBiprodFstBiprodSnd = CategoryTheory.Limits.colimit.isoColimitCocone { cocone := ⋯.cocone, isColimit := ⋯.isColimit }
Instances For
theorem
CategoryTheory.IsPushout.op
{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)
:
IsPullback inr.op inl.op g.op f.op
theorem
CategoryTheory.IsPushout.unop
{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)
:
IsPullback inr.unop inl.unop g.unop f.unop
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.BicartesianSq.of_isPullback_isPushout
{C : Type u₁}
[Category.{v₁, u₁} C]
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
(p₁ : IsPullback f g h i)
(p₂ : IsPushout f g h i)
:
BicartesianSq f g h i
theorem
CategoryTheory.BicartesianSq.flip
{C : Type u₁}
[Category.{v₁, u₁} C]
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
(p : BicartesianSq f g h i)
:
BicartesianSq g f i h
theorem
CategoryTheory.BicartesianSq.of_is_biproduct₁
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y : C}
[Limits.HasZeroObject C]
[Limits.HasZeroMorphisms C]
{b : Limits.BinaryBicone X Y}
(h : b.IsBilimit)
:
BicartesianSq b.fst b.snd 0 0
X ⊞ Y --fst--> X
| |
snd 0
| |
v v
Y -----0---> 0
is a bi-Cartesian square.
theorem
CategoryTheory.BicartesianSq.of_is_biproduct₂
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y : C}
[Limits.HasZeroObject C]
[Limits.HasZeroMorphisms C]
{b : Limits.BinaryBicone X Y}
(h : b.IsBilimit)
:
BicartesianSq 0 0 b.inl b.inr
0 -----0---> X
| |
0 inl
| |
v v
Y --inr--> X ⊞ Y
is a bi-Cartesian square.
@[simp]
theorem
CategoryTheory.BicartesianSq.of_has_biproduct₁
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y : C}
[Limits.HasZeroObject C]
[Limits.HasZeroMorphisms C]
[Limits.HasBinaryBiproduct X Y]
:
X ⊞ Y --fst--> X
| |
snd 0
| |
v v
Y -----0---> 0
is a bi-Cartesian square.
@[simp]
theorem
CategoryTheory.BicartesianSq.of_has_biproduct₂
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y : C}
[Limits.HasZeroObject C]
[Limits.HasZeroMorphisms C]
[Limits.HasBinaryBiproduct X Y]
:
0 -----0---> X
| |
0 inl
| |
v v
Y --inr--> X ⊞ Y
is a bi-Cartesian square.
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.{u_2, 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.{u_2, 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)
: