Pullback and pushout squares, and bicartesian squares #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We provide another API for pullbacks and pushouts.
is_pullback 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 is_pushout.)
We provide the glue to go back and forth to the usual is_limit API for pullbacks, and prove
is_pullback (pullback.fst : pullback f g ⟶ X) (pullback.snd : pullback f g ⟶ Y) f g
for the usual pullback f g provided by the has_limit API.
We don't attempt to restate everything we know about pullbacks in this language, but do restate the pasting lemmas.
We define bicartesian squares, and show that the pullback and pushout squares for a biproduct are bicartesian.
def
category_theory.comm_sq.cone
{C : Type u₁}
[category_theory.category C]
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
(s : category_theory.comm_sq f g h i) :
The (not necessarily limiting) pullback_cone h i implicit in the statement
that we have comm_sq f g h i.
Equations
def
category_theory.comm_sq.cocone
{C : Type u₁}
[category_theory.category C]
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
(s : category_theory.comm_sq f g h i) :
The (not necessarily limiting) pushout_cocone f g implicit in the statement
that we have comm_sq f g h i.
Equations
@[simp]
theorem
category_theory.comm_sq.cone_fst
{C : Type u₁}
[category_theory.category C]
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
(s : category_theory.comm_sq f g h i) :
@[simp]
theorem
category_theory.comm_sq.cone_snd
{C : Type u₁}
[category_theory.category C]
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
(s : category_theory.comm_sq f g h i) :
@[simp]
theorem
category_theory.comm_sq.cocone_inl
{C : Type u₁}
[category_theory.category C]
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
(s : category_theory.comm_sq f g h i) :
@[simp]
theorem
category_theory.comm_sq.cocone_inr
{C : Type u₁}
[category_theory.category C]
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
(s : category_theory.comm_sq f g h i) :
def
category_theory.comm_sq.cone_op
{C : Type u₁}
[category_theory.category C]
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
(p : category_theory.comm_sq 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
def
category_theory.comm_sq.cocone_op
{C : Type u₁}
[category_theory.category C]
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
(p : category_theory.comm_sq 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
def
category_theory.comm_sq.cone_unop
{C : Type u₁}
[category_theory.category C]
{W X Y Z : Cᵒᵖ}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
(p : category_theory.comm_sq 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
def
category_theory.comm_sq.cocone_unop
{C : Type u₁}
[category_theory.category C]
{W X Y Z : Cᵒᵖ}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
(p : category_theory.comm_sq 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
structure
category_theory.is_pullback
{C : Type u₁}
[category_theory.category C]
{P X Y Z : C}
(fst : P ⟶ X)
(snd : P ⟶ Y)
(f : X ⟶ Z)
(g : Y ⟶ Z) :
Prop
- to_comm_sq : category_theory.comm_sq fst snd f g
- is_limit' : nonempty (category_theory.limits.is_limit (category_theory.limits.pullback_cone.mk fst snd _))
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.)
Instances for category_theory.is_pullback
structure
category_theory.is_pushout
{C : Type u₁}
[category_theory.category C]
{Z X Y P : C}
(f : Z ⟶ X)
(g : Z ⟶ Y)
(inl : X ⟶ P)
(inr : Y ⟶ P) :
Prop
- to_comm_sq : category_theory.comm_sq f g inl inr
- is_colimit' : nonempty (category_theory.limits.is_colimit (category_theory.limits.pushout_cocone.mk 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 cocartesian square.)
@[nolint]
def
category_theory.bicartesian_sq.to_is_pullback
{C : Type u₁}
[category_theory.category C]
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
(self : category_theory.bicartesian_sq f g h i) :
category_theory.is_pullback f g h i
@[nolint]
def
category_theory.bicartesian_sq.to_is_pushout
{C : Type u₁}
[category_theory.category C]
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
(self : category_theory.bicartesian_sq f g h i) :
category_theory.is_pushout f g h i
inductive
category_theory.bicartesian_sq
{C : Type u₁}
[category_theory.category C]
{W X Y Z : C}
(f : W ⟶ X)
(g : W ⟶ Y)
(h : X ⟶ Z)
(i : Y ⟶ Z) :
Prop
- mk : ∀ {C : Type u₁} [_inst_1 : category_theory.category C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} (_to_comm_sq : category_theory.comm_sq f g h i), nonempty (category_theory.limits.is_limit (category_theory.limits.pullback_cone.mk f g _)) → nonempty (category_theory.limits.is_colimit (category_theory.limits.pushout_cocone.mk h i _)) → category_theory.bicartesian_sq f g h i
A bicartesian 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.
We begin by providing some glue between is_pullback and the is_limit and has_limit APIs.
(And similarly for is_pushout.)
def
category_theory.is_pullback.cone
{C : Type u₁}
[category_theory.category C]
{P X Y Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(h : category_theory.is_pullback fst snd f g) :
The (limiting) pullback_cone f g implicit in the statement
that we have a is_pullback fst snd f g.
@[simp]
theorem
category_theory.is_pullback.cone_fst
{C : Type u₁}
[category_theory.category C]
{P X Y Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(h : category_theory.is_pullback fst snd f g) :
@[simp]
theorem
category_theory.is_pullback.cone_snd
{C : Type u₁}
[category_theory.category C]
{P X Y Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(h : category_theory.is_pullback fst snd f g) :
noncomputable
def
category_theory.is_pullback.is_limit
{C : Type u₁}
[category_theory.category C]
{P X Y Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(h : category_theory.is_pullback fst snd f g) :
The cone obtained from is_pullback fst snd f g is a limit cone.
theorem
category_theory.is_pullback.of_is_limit
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{c : category_theory.limits.pullback_cone f g}
(h : category_theory.limits.is_limit c) :
category_theory.is_pullback c.fst c.snd f g
If c is a limiting pullback cone, then we have a is_pullback c.fst c.snd f g.
theorem
category_theory.is_pullback.of_is_limit'
{C : Type u₁}
[category_theory.category C]
{P X Y Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(w : category_theory.comm_sq fst snd f g)
(h : category_theory.limits.is_limit w.cone) :
category_theory.is_pullback fst snd f g
A variant of of_is_limit that is more useful with apply.
theorem
category_theory.is_pullback.of_has_pullback
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.limits.has_pullback f g] :
The pullback provided by has_pullback f g fits into a is_pullback.
theorem
category_theory.is_pullback.of_is_product
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
{c : category_theory.limits.binary_fan X Y}
(h : category_theory.limits.is_limit c)
(t : category_theory.limits.is_terminal Z) :
category_theory.is_pullback c.fst c.snd (t.from ((category_theory.limits.pair X Y).obj {as := category_theory.limits.walking_pair.left})) (t.from ((category_theory.limits.pair X Y).obj {as := category_theory.limits.walking_pair.right}))
If c is a limiting binary product cone, and we have a terminal object,
then we have is_pullback c.fst c.snd 0 0
(where each 0 is the unique morphism to the terminal object).
theorem
category_theory.is_pullback.of_is_product'
{C : Type u₁}
[category_theory.category C]
{P X Y Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
(h : category_theory.limits.is_limit (category_theory.limits.binary_fan.mk fst snd))
(t : category_theory.limits.is_terminal Z) :
category_theory.is_pullback fst snd (t.from X) (t.from Y)
A variant of of_is_product that is more useful with apply.
theorem
category_theory.is_pullback.of_has_binary_product'
{C : Type u₁}
[category_theory.category C]
(X Y : C)
[category_theory.limits.has_binary_product X Y]
[category_theory.limits.has_terminal C] :
theorem
category_theory.is_pullback.of_has_binary_product
{C : Type u₁}
[category_theory.category C]
(X Y : C)
[category_theory.limits.has_binary_product X Y]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C] :
noncomputable
def
category_theory.is_pullback.iso_pullback
{C : Type u₁}
[category_theory.category C]
{P X Y Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(h : category_theory.is_pullback fst snd f g)
[category_theory.limits.has_pullback f g] :
Any object at the top left of a pullback square is
isomorphic to the pullback provided by the has_limit API.
Equations
- h.iso_pullback = (category_theory.limits.limit.iso_limit_cone {cone := h.cone, is_limit := h.is_limit}).symm
@[simp]
theorem
category_theory.is_pullback.iso_pullback_hom_fst
{C : Type u₁}
[category_theory.category C]
{P X Y Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(h : category_theory.is_pullback fst snd f g)
[category_theory.limits.has_pullback f g] :
@[simp]
theorem
category_theory.is_pullback.iso_pullback_hom_snd
{C : Type u₁}
[category_theory.category C]
{P X Y Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(h : category_theory.is_pullback fst snd f g)
[category_theory.limits.has_pullback f g] :
@[simp]
theorem
category_theory.is_pullback.iso_pullback_inv_fst
{C : Type u₁}
[category_theory.category C]
{P X Y Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(h : category_theory.is_pullback fst snd f g)
[category_theory.limits.has_pullback f g] :
@[simp]
theorem
category_theory.is_pullback.iso_pullback_inv_snd
{C : Type u₁}
[category_theory.category C]
{P X Y Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(h : category_theory.is_pullback fst snd f g)
[category_theory.limits.has_pullback f g] :
theorem
category_theory.is_pullback.of_iso_pullback
{C : Type u₁}
[category_theory.category C]
{P X Y Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(h : category_theory.comm_sq fst snd f g)
[category_theory.limits.has_pullback f g]
(i : P ≅ category_theory.limits.pullback f g)
(w₁ : i.hom ≫ category_theory.limits.pullback.fst = fst)
(w₂ : i.hom ≫ category_theory.limits.pullback.snd = snd) :
category_theory.is_pullback fst snd f g
theorem
category_theory.is_pullback.of_horiz_is_iso
{C : Type u₁}
[category_theory.category C]
{P X Y Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[category_theory.is_iso fst]
[category_theory.is_iso g]
(sq : category_theory.comm_sq fst snd f g) :
category_theory.is_pullback fst snd f g
def
category_theory.is_pushout.cocone
{C : Type u₁}
[category_theory.category C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(h : category_theory.is_pushout f g inl inr) :
The (colimiting) pushout_cocone f g implicit in the statement
that we have a is_pushout f g inl inr.
@[simp]
theorem
category_theory.is_pushout.cocone_inl
{C : Type u₁}
[category_theory.category C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(h : category_theory.is_pushout f g inl inr) :
@[simp]
theorem
category_theory.is_pushout.cocone_inr
{C : Type u₁}
[category_theory.category C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(h : category_theory.is_pushout f g inl inr) :
noncomputable
def
category_theory.is_pushout.is_colimit
{C : Type u₁}
[category_theory.category C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(h : category_theory.is_pushout f g inl inr) :
The cocone obtained from is_pushout f g inl inr is a colimit cocone.
Equations
- h.is_colimit = _.some
theorem
category_theory.is_pushout.of_is_colimit
{C : Type u₁}
[category_theory.category C]
{Z X Y : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{c : category_theory.limits.pushout_cocone f g}
(h : category_theory.limits.is_colimit c) :
category_theory.is_pushout f g c.inl c.inr
If c is a colimiting pushout cocone, then we have a is_pushout f g c.inl c.inr.
theorem
category_theory.is_pushout.of_is_colimit'
{C : Type u₁}
[category_theory.category C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(w : category_theory.comm_sq f g inl inr)
(h : category_theory.limits.is_colimit w.cocone) :
category_theory.is_pushout f g inl inr
A variant of of_is_colimit that is more useful with apply.
theorem
category_theory.is_pushout.of_has_pushout
{C : Type u₁}
[category_theory.category C]
{Z X Y : C}
(f : Z ⟶ X)
(g : Z ⟶ Y)
[category_theory.limits.has_pushout f g] :
The pushout provided by has_pushout f g fits into a is_pushout.
theorem
category_theory.is_pushout.of_is_coproduct
{C : Type u₁}
[category_theory.category C]
{Z X Y : C}
{c : category_theory.limits.binary_cofan X Y}
(h : category_theory.limits.is_colimit c)
(t : category_theory.limits.is_initial Z) :
category_theory.is_pushout (t.to ((category_theory.limits.pair X Y).obj {as := category_theory.limits.walking_pair.left})) (t.to ((category_theory.limits.pair X Y).obj {as := category_theory.limits.walking_pair.right})) c.inl c.inr
If c is a colimiting binary coproduct cocone, and we have an initial object,
then we have is_pushout 0 0 c.inl c.inr
(where each 0 is the unique morphism from the initial object).
theorem
category_theory.is_pushout.of_is_coproduct'
{C : Type u₁}
[category_theory.category C]
{Z X Y P : C}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(h : category_theory.limits.is_colimit (category_theory.limits.binary_cofan.mk inl inr))
(t : category_theory.limits.is_initial Z) :
category_theory.is_pushout (t.to X) (t.to Y) inl inr
A variant of of_is_coproduct that is more useful with apply.
theorem
category_theory.is_pushout.of_has_binary_coproduct'
{C : Type u₁}
[category_theory.category C]
(X Y : C)
[category_theory.limits.has_binary_coproduct X Y]
[category_theory.limits.has_initial C] :
theorem
category_theory.is_pushout.of_has_binary_coproduct
{C : Type u₁}
[category_theory.category C]
(X Y : C)
[category_theory.limits.has_binary_coproduct X Y]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C] :
noncomputable
def
category_theory.is_pushout.iso_pushout
{C : Type u₁}
[category_theory.category C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(h : category_theory.is_pushout f g inl inr)
[category_theory.limits.has_pushout f g] :
Any object at the top left of a pullback square is
isomorphic to the pullback provided by the has_limit API.
Equations
@[simp]
theorem
category_theory.is_pushout.inl_iso_pushout_inv
{C : Type u₁}
[category_theory.category C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(h : category_theory.is_pushout f g inl inr)
[category_theory.limits.has_pushout f g] :
@[simp]
theorem
category_theory.is_pushout.inr_iso_pushout_inv
{C : Type u₁}
[category_theory.category C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(h : category_theory.is_pushout f g inl inr)
[category_theory.limits.has_pushout f g] :
@[simp]
theorem
category_theory.is_pushout.inl_iso_pushout_hom
{C : Type u₁}
[category_theory.category C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(h : category_theory.is_pushout f g inl inr)
[category_theory.limits.has_pushout f g] :
@[simp]
theorem
category_theory.is_pushout.inr_iso_pushout_hom
{C : Type u₁}
[category_theory.category C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(h : category_theory.is_pushout f g inl inr)
[category_theory.limits.has_pushout f g] :
theorem
category_theory.is_pushout.of_iso_pushout
{C : Type u₁}
[category_theory.category C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(h : category_theory.comm_sq f g inl inr)
[category_theory.limits.has_pushout f g]
(i : P ≅ category_theory.limits.pushout f g)
(w₁ : inl ≫ i.hom = category_theory.limits.pushout.inl)
(w₂ : inr ≫ i.hom = category_theory.limits.pushout.inr) :
category_theory.is_pushout f g inl inr
theorem
category_theory.is_pullback.flip
{C : Type u₁}
[category_theory.category C]
{P X Y Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(h : category_theory.is_pullback fst snd f g) :
category_theory.is_pullback snd fst g f
theorem
category_theory.is_pullback.flip_iff
{C : Type u₁}
[category_theory.category C]
{P X Y Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z} :
category_theory.is_pullback fst snd f g ↔ category_theory.is_pullback snd fst g f
@[simp]
theorem
category_theory.is_pullback.zero_left
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
(X : C) :
category_theory.is_pullback 0 0 (𝟙 X) 0
The square with 0 : 0 ⟶ 0 on the left and 𝟙 X on the right is a pullback square.
@[simp]
theorem
category_theory.is_pullback.zero_top
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
(X : C) :
category_theory.is_pullback 0 0 0 (𝟙 X)
The square with 0 : 0 ⟶ 0 on the top and 𝟙 X on the bottom is a pullback square.
@[simp]
theorem
category_theory.is_pullback.zero_right
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
(X : C) :
category_theory.is_pullback 0 (𝟙 X) 0 0
The square with 0 : 0 ⟶ 0 on the right and 𝟙 X on the left is a pullback square.
@[simp]
theorem
category_theory.is_pullback.zero_bot
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
(X : C) :
category_theory.is_pullback (𝟙 X) 0 0 0
The square with 0 : 0 ⟶ 0 on the bottom and 𝟙 X on the top is a pullback square.
theorem
category_theory.is_pullback.paste_vert
{C : Type u₁}
[category_theory.category 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 : category_theory.is_pullback h₁₁ v₁₁ v₁₂ h₂₁)
(t : category_theory.is_pullback h₂₁ v₂₁ v₂₂ h₃₁) :
category_theory.is_pullback h₁₁ (v₁₁ ≫ v₂₁) (v₁₂ ≫ v₂₂) h₃₁
Paste two pullback squares "vertically" to obtain another pullback square.
theorem
category_theory.is_pullback.paste_horiz
{C : Type u₁}
[category_theory.category 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 : category_theory.is_pullback h₁₁ v₁₁ v₁₂ h₂₁)
(t : category_theory.is_pullback h₁₂ v₁₂ v₁₃ h₂₂) :
category_theory.is_pullback (h₁₁ ≫ h₁₂) v₁₁ v₁₃ (h₂₁ ≫ h₂₂)
Paste two pullback squares "horizontally" to obtain another pullback square.
theorem
category_theory.is_pullback.of_bot
{C : Type u₁}
[category_theory.category 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 : category_theory.is_pullback h₁₁ (v₁₁ ≫ v₂₁) (v₁₂ ≫ v₂₂) h₃₁)
(p : h₁₁ ≫ v₁₂ = v₁₁ ≫ h₂₁)
(t : category_theory.is_pullback h₂₁ v₂₁ v₂₂ h₃₁) :
category_theory.is_pullback 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.
theorem
category_theory.is_pullback.of_right
{C : Type u₁}
[category_theory.category 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 : category_theory.is_pullback (h₁₁ ≫ h₁₂) v₁₁ v₁₃ (h₂₁ ≫ h₂₂))
(p : h₁₁ ≫ v₁₂ = v₁₁ ≫ h₂₁)
(t : category_theory.is_pullback h₁₂ v₁₂ v₁₃ h₂₂) :
category_theory.is_pullback 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.
theorem
category_theory.is_pullback.paste_vert_iff
{C : Type u₁}
[category_theory.category 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 : category_theory.is_pullback h₂₁ v₂₁ v₂₂ h₃₁)
(e : h₁₁ ≫ v₁₂ = v₁₁ ≫ h₂₁) :
category_theory.is_pullback h₁₁ (v₁₁ ≫ v₂₁) (v₁₂ ≫ v₂₂) h₃₁ ↔ category_theory.is_pullback h₁₁ v₁₁ v₁₂ h₂₁
theorem
category_theory.is_pullback.paste_horiz_iff
{C : Type u₁}
[category_theory.category 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 : category_theory.is_pullback h₁₂ v₁₂ v₁₃ h₂₂)
(e : h₁₁ ≫ v₁₂ = v₁₁ ≫ h₂₁) :
category_theory.is_pullback (h₁₁ ≫ h₁₂) v₁₁ v₁₃ (h₂₁ ≫ h₂₂) ↔ category_theory.is_pullback h₁₁ v₁₁ v₁₂ h₂₁
theorem
category_theory.is_pullback.of_is_bilimit
{C : Type u₁}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
{b : category_theory.limits.binary_bicone X Y}
(h : b.is_bilimit) :
category_theory.is_pullback b.fst b.snd 0 0
@[simp]
theorem
category_theory.is_pullback.of_has_biproduct
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y] :
theorem
category_theory.is_pullback.inl_snd'
{C : Type u₁}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
{b : category_theory.limits.binary_bicone X Y}
(h : b.is_bilimit) :
category_theory.is_pullback b.inl 0 b.snd 0
@[simp]
theorem
category_theory.is_pullback.inl_snd
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y] :
The square
X --inl--> X ⊞ Y
| |
0 snd
| |
v v
0 ---0-----> Y
is a pullback square.
theorem
category_theory.is_pullback.inr_fst'
{C : Type u₁}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
{b : category_theory.limits.binary_bicone X Y}
(h : b.is_bilimit) :
category_theory.is_pullback b.inr 0 b.fst 0
@[simp]
theorem
category_theory.is_pullback.inr_fst
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y] :
The square
Y --inr--> X ⊞ Y
| |
0 fst
| |
v v
0 ---0-----> X
is a pullback square.
theorem
category_theory.is_pullback.of_is_bilimit'
{C : Type u₁}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
{b : category_theory.limits.binary_bicone X Y}
(h : b.is_bilimit) :
category_theory.is_pullback 0 0 b.inl b.inr
theorem
category_theory.is_pullback.of_has_binary_biproduct
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y] :
@[protected, instance]
noncomputable
def
category_theory.is_pullback.pullback_biprod_inl_biprod_inr
{C : Type u₁}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_binary_biproduct X Y] :
The pullback of biprod.inl and biprod.inr is the zero object.
theorem
category_theory.is_pullback.op
{C : Type u₁}
[category_theory.category C]
{P X Y Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(h : category_theory.is_pullback fst snd f g) :
category_theory.is_pushout g.op f.op snd.op fst.op
theorem
category_theory.is_pullback.unop
{C : Type u₁}
[category_theory.category C]
{P X Y Z : Cᵒᵖ}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(h : category_theory.is_pullback fst snd f g) :
category_theory.is_pushout g.unop f.unop snd.unop fst.unop
theorem
category_theory.is_pullback.of_vert_is_iso
{C : Type u₁}
[category_theory.category C]
{P X Y Z : C}
{fst : P ⟶ X}
{snd : P ⟶ Y}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[category_theory.is_iso snd]
[category_theory.is_iso f]
(sq : category_theory.comm_sq fst snd f g) :
category_theory.is_pullback fst snd f g
theorem
category_theory.is_pushout.flip
{C : Type u₁}
[category_theory.category C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(h : category_theory.is_pushout f g inl inr) :
category_theory.is_pushout g f inr inl
theorem
category_theory.is_pushout.flip_iff
{C : Type u₁}
[category_theory.category C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P} :
category_theory.is_pushout f g inl inr ↔ category_theory.is_pushout g f inr inl
@[simp]
theorem
category_theory.is_pushout.zero_right
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
(X : C) :
category_theory.is_pushout 0 (𝟙 X) 0 0
The square with 0 : 0 ⟶ 0 on the right and 𝟙 X on the left is a pushout square.
@[simp]
theorem
category_theory.is_pushout.zero_bot
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
(X : C) :
category_theory.is_pushout (𝟙 X) 0 0 0
The square with 0 : 0 ⟶ 0 on the bottom and 𝟙 X on the top is a pushout square.
@[simp]
theorem
category_theory.is_pushout.zero_left
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
(X : C) :
category_theory.is_pushout 0 0 (𝟙 X) 0
The square with 0 : 0 ⟶ 0 on the right left 𝟙 X on the right is a pushout square.
@[simp]
theorem
category_theory.is_pushout.zero_top
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
(X : C) :
category_theory.is_pushout 0 0 0 (𝟙 X)
The square with 0 : 0 ⟶ 0 on the top and 𝟙 X on the bottom is a pushout square.
theorem
category_theory.is_pushout.paste_vert
{C : Type u₁}
[category_theory.category 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 : category_theory.is_pushout h₁₁ v₁₁ v₁₂ h₂₁)
(t : category_theory.is_pushout h₂₁ v₂₁ v₂₂ h₃₁) :
category_theory.is_pushout h₁₁ (v₁₁ ≫ v₂₁) (v₁₂ ≫ v₂₂) h₃₁
Paste two pushout squares "vertically" to obtain another pushout square.
theorem
category_theory.is_pushout.paste_horiz
{C : Type u₁}
[category_theory.category 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 : category_theory.is_pushout h₁₁ v₁₁ v₁₂ h₂₁)
(t : category_theory.is_pushout h₁₂ v₁₂ v₁₃ h₂₂) :
category_theory.is_pushout (h₁₁ ≫ h₁₂) v₁₁ v₁₃ (h₂₁ ≫ h₂₂)
Paste two pushout squares "horizontally" to obtain another pushout square.
theorem
category_theory.is_pushout.of_bot
{C : Type u₁}
[category_theory.category 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 : category_theory.is_pushout h₁₁ (v₁₁ ≫ v₂₁) (v₁₂ ≫ v₂₂) h₃₁)
(p : h₂₁ ≫ v₂₂ = v₂₁ ≫ h₃₁)
(t : category_theory.is_pushout h₁₁ v₁₁ v₁₂ h₂₁) :
category_theory.is_pushout 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.
theorem
category_theory.is_pushout.of_right
{C : Type u₁}
[category_theory.category 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 : category_theory.is_pushout (h₁₁ ≫ h₁₂) v₁₁ v₁₃ (h₂₁ ≫ h₂₂))
(p : h₁₂ ≫ v₁₃ = v₁₂ ≫ h₂₂)
(t : category_theory.is_pushout h₁₁ v₁₁ v₁₂ h₂₁) :
category_theory.is_pushout 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.
theorem
category_theory.is_pushout.paste_vert_iff
{C : Type u₁}
[category_theory.category 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 : category_theory.is_pushout h₁₁ v₁₁ v₁₂ h₂₁)
(e : h₂₁ ≫ v₂₂ = v₂₁ ≫ h₃₁) :
category_theory.is_pushout h₁₁ (v₁₁ ≫ v₂₁) (v₁₂ ≫ v₂₂) h₃₁ ↔ category_theory.is_pushout h₂₁ v₂₁ v₂₂ h₃₁
theorem
category_theory.is_pushout.paste_horiz_iff
{C : Type u₁}
[category_theory.category 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 : category_theory.is_pushout h₁₁ v₁₁ v₁₂ h₂₁)
(e : h₁₂ ≫ v₁₃ = v₁₂ ≫ h₂₂) :
category_theory.is_pushout (h₁₁ ≫ h₁₂) v₁₁ v₁₃ (h₂₁ ≫ h₂₂) ↔ category_theory.is_pushout h₁₂ v₁₂ v₁₃ h₂₂
theorem
category_theory.is_pushout.of_is_bilimit
{C : Type u₁}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
{b : category_theory.limits.binary_bicone X Y}
(h : b.is_bilimit) :
category_theory.is_pushout 0 0 b.inl b.inr
@[simp]
theorem
category_theory.is_pushout.of_has_biproduct
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y] :
theorem
category_theory.is_pushout.inl_snd'
{C : Type u₁}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
{b : category_theory.limits.binary_bicone X Y}
(h : b.is_bilimit) :
category_theory.is_pushout b.inl 0 b.snd 0
theorem
category_theory.is_pushout.inl_snd
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y] :
The square
X --inl--> X ⊞ Y
| |
0 snd
| |
v v
0 ---0-----> Y
is a pushout square.
theorem
category_theory.is_pushout.inr_fst'
{C : Type u₁}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
{b : category_theory.limits.binary_bicone X Y}
(h : b.is_bilimit) :
category_theory.is_pushout b.inr 0 b.fst 0
theorem
category_theory.is_pushout.inr_fst
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y] :
The square
Y --inr--> X ⊞ Y
| |
0 fst
| |
v v
0 ---0-----> X
is a pushout square.
theorem
category_theory.is_pushout.of_is_bilimit'
{C : Type u₁}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
{b : category_theory.limits.binary_bicone X Y}
(h : b.is_bilimit) :
category_theory.is_pushout b.fst b.snd 0 0
theorem
category_theory.is_pushout.of_has_binary_biproduct
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y] :
@[protected, instance]
noncomputable
def
category_theory.is_pushout.pushout_biprod_fst_biprod_snd
{C : Type u₁}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_binary_biproduct X Y] :
The pushout of biprod.fst and biprod.snd is the zero object.
theorem
category_theory.is_pushout.op
{C : Type u₁}
[category_theory.category C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(h : category_theory.is_pushout f g inl inr) :
category_theory.is_pullback inr.op inl.op g.op f.op
theorem
category_theory.is_pushout.unop
{C : Type u₁}
[category_theory.category C]
{Z X Y P : Cᵒᵖ}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
(h : category_theory.is_pushout f g inl inr) :
category_theory.is_pullback inr.unop inl.unop g.unop f.unop
theorem
category_theory.is_pushout.of_horiz_is_iso
{C : Type u₁}
[category_theory.category C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
[category_theory.is_iso f]
[category_theory.is_iso inr]
(sq : category_theory.comm_sq f g inl inr) :
category_theory.is_pushout f g inl inr
theorem
category_theory.is_pushout.of_vert_is_iso
{C : Type u₁}
[category_theory.category C]
{Z X Y P : C}
{f : Z ⟶ X}
{g : Z ⟶ Y}
{inl : X ⟶ P}
{inr : Y ⟶ P}
[category_theory.is_iso g]
[category_theory.is_iso inl]
(sq : category_theory.comm_sq f g inl inr) :
category_theory.is_pushout f g inl inr
noncomputable
def
category_theory.is_pullback.is_limit_fork
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Y}
{g g' : Y ⟶ Z}
(H : category_theory.is_pullback 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
- H.is_limit_fork = category_theory.limits.fork.is_limit.mk (category_theory.limits.fork.of_ι f _) (λ (s : category_theory.limits.fork g g'), H.is_limit.lift (category_theory.limits.pullback_cone.mk s.ι s.ι _)) _ _
noncomputable
def
category_theory.is_pushout.is_limit_fork
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
{f f' : X ⟶ Y}
{g : Y ⟶ Z}
(H : category_theory.is_pushout 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
- H.is_limit_fork = category_theory.limits.cofork.is_colimit.mk (category_theory.limits.cofork.of_π g _) (λ (s : category_theory.limits.cofork f f'), H.is_colimit.desc (category_theory.limits.pushout_cocone.mk s.π s.π _)) _ _
theorem
category_theory.bicartesian_sq.of_is_pullback_is_pushout
{C : Type u₁}
[category_theory.category C]
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
(p₁ : category_theory.is_pullback f g h i)
(p₂ : category_theory.is_pushout f g h i) :
category_theory.bicartesian_sq f g h i
theorem
category_theory.bicartesian_sq.flip
{C : Type u₁}
[category_theory.category C]
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
(p : category_theory.bicartesian_sq f g h i) :
category_theory.bicartesian_sq g f i h
theorem
category_theory.bicartesian_sq.of_is_biproduct₁
{C : Type u₁}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
{b : category_theory.limits.binary_bicone X Y}
(h : b.is_bilimit) :
category_theory.bicartesian_sq b.fst b.snd 0 0
X ⊞ Y --fst--> X
| |
snd 0
| |
v v
Y -----0---> 0
is a bicartesian square.
theorem
category_theory.bicartesian_sq.of_is_biproduct₂
{C : Type u₁}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
{b : category_theory.limits.binary_bicone X Y}
(h : b.is_bilimit) :
category_theory.bicartesian_sq 0 0 b.inl b.inr
0 -----0---> X
| |
0 inl
| |
v v
Y --inr--> X ⊞ Y
is a bicartesian square.
@[simp]
theorem
category_theory.bicartesian_sq.of_has_biproduct₁
{C : Type u₁}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_binary_biproduct X Y] :
X ⊞ Y --fst--> X
| |
snd 0
| |
v v
Y -----0---> 0
is a bicartesian square.
@[simp]
theorem
category_theory.bicartesian_sq.of_has_biproduct₂
{C : Type u₁}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_binary_biproduct X Y] :
0 -----0---> X
| |
0 inl
| |
v v
Y --inr--> X ⊞ Y
is a bicartesian square.
theorem
category_theory.functor.map_is_pullback
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
[category_theory.limits.preserves_limit (category_theory.limits.cospan h i) F]
(s : category_theory.is_pullback f g h i) :
category_theory.is_pullback (F.map f) (F.map g) (F.map h) (F.map i)
theorem
category_theory.functor.map_is_pushout
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
[category_theory.limits.preserves_colimit (category_theory.limits.span f g) F]
(s : category_theory.is_pushout f g h i) :
category_theory.is_pushout (F.map f) (F.map g) (F.map h) (F.map i)
theorem
category_theory.is_pullback.map
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
[category_theory.limits.preserves_limit (category_theory.limits.cospan h i) F]
(s : category_theory.is_pullback f g h i) :
category_theory.is_pullback (F.map f) (F.map g) (F.map h) (F.map i)
Alias of category_theory.functor.map_is_pullback.
theorem
category_theory.is_pushout.map
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
[category_theory.limits.preserves_colimit (category_theory.limits.span f g) F]
(s : category_theory.is_pushout f g h i) :
category_theory.is_pushout (F.map f) (F.map g) (F.map h) (F.map i)
Alias of category_theory.functor.map_is_pushout.
theorem
category_theory.is_pullback.of_map
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
[category_theory.limits.reflects_limit (category_theory.limits.cospan h i) F]
(e : f ≫ h = g ≫ i)
(H : category_theory.is_pullback (F.map f) (F.map g) (F.map h) (F.map i)) :
category_theory.is_pullback f g h i
theorem
category_theory.is_pullback.of_map_of_faithful
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
[category_theory.limits.reflects_limit (category_theory.limits.cospan h i) F]
[category_theory.faithful F]
(H : category_theory.is_pullback (F.map f) (F.map g) (F.map h) (F.map i)) :
category_theory.is_pullback f g h i
theorem
category_theory.is_pullback.map_iff
{C : Type u₁}
[category_theory.category C]
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
{D : Type u_1}
[category_theory.category D]
(F : C ⥤ D)
[category_theory.limits.preserves_limit (category_theory.limits.cospan h i) F]
[category_theory.limits.reflects_limit (category_theory.limits.cospan h i) F]
(e : f ≫ h = g ≫ i) :
category_theory.is_pullback (F.map f) (F.map g) (F.map h) (F.map i) ↔ category_theory.is_pullback f g h i
theorem
category_theory.is_pushout.of_map
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
[category_theory.limits.reflects_colimit (category_theory.limits.span f g) F]
(e : f ≫ h = g ≫ i)
(H : category_theory.is_pushout (F.map f) (F.map g) (F.map h) (F.map i)) :
category_theory.is_pushout f g h i
theorem
category_theory.is_pushout.of_map_of_faithful
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
[category_theory.limits.reflects_colimit (category_theory.limits.span f g) F]
[category_theory.faithful F]
(H : category_theory.is_pushout (F.map f) (F.map g) (F.map h) (F.map i)) :
category_theory.is_pushout f g h i
theorem
category_theory.is_pushout.map_iff
{C : Type u₁}
[category_theory.category C]
{W X Y Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
{D : Type u_1}
[category_theory.category D]
(F : C ⥤ D)
[category_theory.limits.preserves_colimit (category_theory.limits.span f g) F]
[category_theory.limits.reflects_colimit (category_theory.limits.span f g) F]
(e : f ≫ h = g ≫ i) :
category_theory.is_pushout (F.map f) (F.map g) (F.map h) (F.map i) ↔ category_theory.is_pushout f g h i