# mathlibdocumentation

category_theory.limits.shapes.comm_sq

# 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₁} {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (s : 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₁} {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (s : 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₁} {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (s : i) :
s.cone.fst = f
@[simp]
theorem category_theory.comm_sq.cone_snd {C : Type u₁} {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (s : i) :
s.cone.snd = g
@[simp]
theorem category_theory.comm_sq.cocone_inl {C : Type u₁} {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (s : i) :
@[simp]
theorem category_theory.comm_sq.cocone_inr {C : Type u₁} {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (s : i) :
def category_theory.comm_sq.cone_op {C : Type u₁} {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (p : 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₁} {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (p : 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₁} {W X Y Z : Cᵒᵖ} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (p : 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₁} {W X Y Z : Cᵒᵖ} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (p : 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₁} {P X Y Z : C} (fst : P X) (snd : P Y) (f : X Z) (g : Y Z) :
Prop
• to_comm_sq : snd f g
• is_limit' :

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₁} {Z X Y P : C} (f : Z X) (g : Z Y) (inl : X P) (inr : Y P) :
Prop
• to_comm_sq : inl inr
• is_colimit' :

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₁} {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (self : i) :
i
@[nolint]
def category_theory.bicartesian_sq.to_is_pushout {C : Type u₁} {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (self : i) :
i
inductive category_theory.bicartesian_sq {C : Type u₁} {W X Y Z : C} (f : W X) (g : W Y) (h : X Z) (i : Y Z) :
Prop
• mk : {C : Type u₁} [_inst_1 : {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (_to_comm_sq : 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₁} {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : snd f g) :

The (limiting) `pullback_cone f g` implicit in the statement that we have a `is_pullback fst snd f g`.

Equations
@[simp]
theorem category_theory.is_pullback.cone_fst {C : Type u₁} {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : snd f g) :
h.cone.fst = fst
@[simp]
theorem category_theory.is_pullback.cone_snd {C : Type u₁} {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : snd f g) :
h.cone.snd = snd
noncomputable def category_theory.is_pullback.is_limit {C : Type u₁} {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : snd f g) :

The cone obtained from `is_pullback fst snd f g` is a limit cone.

Equations
theorem category_theory.is_pullback.of_is_limit {C : Type u₁} {X Y Z : C} {f : X Z} {g : Y Z}  :
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₁} {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (w : snd f g)  :
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₁} {X Y Z : C} (f : X Z) (g : Y Z)  :

The pullback provided by `has_pullback f g` fits into a `is_pullback`.

theorem category_theory.is_pullback.of_is_product {C : Type u₁} {X Y Z : C}  :

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₁} {P X Y Z : C} {fst : P X} {snd : P Y}  :
snd (t.from X) (t.from Y)

A variant of `of_is_product` that is more useful with `apply`.

noncomputable def category_theory.is_pullback.iso_pullback {C : Type u₁} {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : snd 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_pullback.iso_pullback_hom_fst {C : Type u₁} {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : snd f g)  :
@[simp]
theorem category_theory.is_pullback.iso_pullback_hom_snd {C : Type u₁} {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : snd f g)  :
@[simp]
theorem category_theory.is_pullback.iso_pullback_inv_fst {C : Type u₁} {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : snd f g)  :
@[simp]
theorem category_theory.is_pullback.iso_pullback_inv_snd {C : Type u₁} {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : snd f g)  :
theorem category_theory.is_pullback.of_iso_pullback {C : Type u₁} {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : snd f g) (i : P ) (w₁ : = fst) (w₂ : = snd) :
snd f g
theorem category_theory.is_pullback.of_horiz_is_iso {C : Type u₁} {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (sq : snd f g) :
snd f g
def category_theory.is_pushout.cocone {C : Type u₁} {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : inl inr) :

The (colimiting) `pushout_cocone f g` implicit in the statement that we have a `is_pushout f g inl inr`.

Equations
@[simp]
theorem category_theory.is_pushout.cocone_inl {C : Type u₁} {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : inl inr) :
h.cocone.inl = inl
@[simp]
theorem category_theory.is_pushout.cocone_inr {C : Type u₁} {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : inl inr) :
h.cocone.inr = inr
noncomputable def category_theory.is_pushout.is_colimit {C : Type u₁} {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : inl inr) :

The cocone obtained from `is_pushout f g inl inr` is a colimit cocone.

Equations
theorem category_theory.is_pushout.of_is_colimit {C : Type u₁} {Z X Y : C} {f : Z X} {g : Z Y}  :
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₁} {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (w : inl inr)  :
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₁} {Z X Y : C} (f : Z X) (g : Z Y)  :

The pushout provided by `has_pushout f g` fits into a `is_pushout`.

theorem category_theory.is_pushout.of_is_coproduct {C : Type u₁} {Z X Y : C}  :
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₁} {Z X Y P : C} {inl : X P} {inr : Y P}  :
(t.to Y) inl inr

A variant of `of_is_coproduct` that is more useful with `apply`.

noncomputable def category_theory.is_pushout.iso_pushout {C : Type u₁} {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : inl inr)  :

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₁} {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : inl inr)  :
@[simp]
theorem category_theory.is_pushout.inr_iso_pushout_inv {C : Type u₁} {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : inl inr)  :
@[simp]
theorem category_theory.is_pushout.inl_iso_pushout_hom {C : Type u₁} {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : inl inr)  :
@[simp]
theorem category_theory.is_pushout.inr_iso_pushout_hom {C : Type u₁} {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : inl inr)  :
theorem category_theory.is_pushout.of_iso_pushout {C : Type u₁} {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : inl inr) (i : P ) (w₁ : inl i.hom = category_theory.limits.pushout.inl) (w₂ : inr i.hom = category_theory.limits.pushout.inr) :
inl inr
theorem category_theory.is_pullback.flip {C : Type u₁} {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : snd f g) :
fst g f
theorem category_theory.is_pullback.flip_iff {C : Type u₁} {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} :
snd f g fst g f
@[simp]
theorem category_theory.is_pullback.zero_left {C : Type u₁} (X : C) :
(𝟙 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₁} (X : C) :
(𝟙 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₁} (X : C) :
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₁} (X : C) :
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₁} {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 : v₁₁ v₁₂ h₂₁) (t : v₂₁ v₂₂ 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₁} {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 : v₁₁ v₁₂ h₂₁) (t : 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₁} {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 : (v₁₁ v₂₁) (v₁₂ v₂₂) h₃₁) (p : h₁₁ v₁₂ = v₁₁ h₂₁) (t : v₂₁ v₂₂ 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₁} {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 : v₁₂ v₁₃ 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₁} {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 : v₂₁ v₂₂ h₃₁) (e : h₁₁ v₁₂ = v₁₁ h₂₁) :
(v₁₁ v₂₁) (v₁₂ v₂₂) h₃₁ v₁₁ v₁₂ h₂₁
theorem category_theory.is_pullback.paste_horiz_iff {C : Type u₁} {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 : v₁₂ v₁₃ h₂₂) (e : h₁₁ v₁₂ = v₁₁ h₂₁) :
category_theory.is_pullback (h₁₁ h₁₂) v₁₁ v₁₃ (h₂₁ h₂₂) v₁₁ v₁₂ h₂₁
theorem category_theory.is_pullback.of_is_bilimit {C : Type u₁} {X Y : C} (h : b.is_bilimit) :
0
@[simp]
theorem category_theory.is_pullback.inl_snd' {C : Type u₁} {X Y : C} (h : b.is_bilimit) :
0
@[simp]

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₁} {X Y : C} (h : b.is_bilimit) :
0
@[simp]

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₁} {X Y : C} (h : b.is_bilimit) :
b.inr
@[protected, instance]

The pullback of `biprod.inl` and `biprod.inr` is the zero object.

Equations
theorem category_theory.is_pullback.op {C : Type u₁} {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : snd f g) :
snd.op fst.op
theorem category_theory.is_pullback.unop {C : Type u₁} {P X Y Z : Cᵒᵖ} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : snd f g) :
snd.unop fst.unop
theorem category_theory.is_pullback.of_vert_is_iso {C : Type u₁} {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (sq : snd f g) :
snd f g
theorem category_theory.is_pushout.flip {C : Type u₁} {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : inl inr) :
inr inl
theorem category_theory.is_pushout.flip_iff {C : Type u₁} {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} :
inl inr inr inl
@[simp]
theorem category_theory.is_pushout.zero_right {C : Type u₁} (X : C) :
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₁} (X : C) :
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₁} (X : C) :
(𝟙 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₁} (X : C) :
(𝟙 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₁} {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 : v₁₁ v₁₂ h₂₁) (t : v₂₁ v₂₂ 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₁} {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 : v₁₁ v₁₂ h₂₁) (t : 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₁} {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 : (v₁₁ v₂₁) (v₁₂ v₂₂) h₃₁) (p : h₂₁ v₂₂ = v₂₁ h₃₁) (t : v₁₁ v₁₂ 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₁} {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 : v₁₁ v₁₂ 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₁} {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 : v₁₁ v₁₂ h₂₁) (e : h₂₁ v₂₂ = v₂₁ h₃₁) :
(v₁₁ v₂₁) (v₁₂ v₂₂) h₃₁ v₂₁ v₂₂ h₃₁
theorem category_theory.is_pushout.paste_horiz_iff {C : Type u₁} {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 : v₁₁ v₁₂ h₂₁) (e : h₁₂ v₁₃ = v₁₂ h₂₂) :
category_theory.is_pushout (h₁₁ h₁₂) v₁₁ v₁₃ (h₂₁ h₂₂) v₁₂ v₁₃ h₂₂
theorem category_theory.is_pushout.of_is_bilimit {C : Type u₁} {X Y : C} (h : b.is_bilimit) :
b.inr
@[simp]
theorem category_theory.is_pushout.inl_snd' {C : Type u₁} {X Y : C} (h : b.is_bilimit) :
0

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₁} {X Y : C} (h : b.is_bilimit) :
0

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₁} {X Y : C} (h : b.is_bilimit) :
0
@[protected, instance]

The pushout of `biprod.fst` and `biprod.snd` is the zero object.

Equations
theorem category_theory.is_pushout.op {C : Type u₁} {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : inl inr) :
inl.op g.op f.op
theorem category_theory.is_pushout.unop {C : Type u₁} {Z X Y P : Cᵒᵖ} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : inl inr) :
inl.unop g.unop f.unop
theorem category_theory.is_pushout.of_horiz_is_iso {C : Type u₁} {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (sq : inl inr) :
inl inr
theorem category_theory.is_pushout.of_vert_is_iso {C : Type u₁} {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (sq : inl inr) :
inl inr
noncomputable def category_theory.is_pullback.is_limit_fork {C : Type u₁} {X Y Z : C} {f : X Y} {g g' : Y Z} (H : g') :

If `f : X ⟶ Y`, `g g' : Y ⟶ Z` forms a pullback square, then `f` is the equalizer of `g` and `g'`.

Equations
noncomputable def category_theory.is_pushout.is_limit_fork {C : Type u₁} {X Y Z : C} {f f' : X Y} {g : Y Z} (H : g) :

If `f f' : X ⟶ Y`, `g : Y ⟶ Z` forms a pushout square, then `g` is the coequalizer of `f` and `f'`.

Equations
theorem category_theory.bicartesian_sq.of_is_pullback_is_pushout {C : Type u₁} {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (p₁ : i) (p₂ : i) :
theorem category_theory.bicartesian_sq.flip {C : Type u₁} {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (p : i) :
theorem category_theory.bicartesian_sq.of_is_biproduct₁ {C : Type u₁} {X Y : C} (h : b.is_bilimit) :
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₁} {X Y : C} (h : b.is_bilimit) :
b.inr
``````   0 -----0---> X
|            |
0           inl
|            |
v            v
Y --inr--> X ⊞ Y
``````

is a bicartesian square.

@[simp]
`````` X ⊞ Y --fst--> X
|            |
snd           0
|            |
v            v
Y -----0---> 0
``````

is a bicartesian square.

@[simp]
``````   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₁} {D : Type u₂} (F : C D) {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (s : i) :
(F.map g) (F.map h) (F.map i)
theorem category_theory.functor.map_is_pushout {C : Type u₁} {D : Type u₂} (F : C D) {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (s : i) :
(F.map g) (F.map h) (F.map i)
theorem category_theory.is_pullback.map {C : Type u₁} {D : Type u₂} (F : C D) {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (s : i) :
(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₁} {D : Type u₂} (F : C D) {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (s : i) :
(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₁} {D : Type u₂} (F : C D) {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (e : f h = g i) (H : (F.map g) (F.map h) (F.map i)) :
i
theorem category_theory.is_pullback.of_map_of_faithful {C : Type u₁} {D : Type u₂} (F : C D) {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (H : (F.map g) (F.map h) (F.map i)) :
i
theorem category_theory.is_pullback.map_iff {C : Type u₁} {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} {D : Type u_1} (F : C D) (e : f h = g i) :
(F.map g) (F.map h) (F.map i) i
theorem category_theory.is_pushout.of_map {C : Type u₁} {D : Type u₂} (F : C D) {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (e : f h = g i) (H : (F.map g) (F.map h) (F.map i)) :
i
theorem category_theory.is_pushout.of_map_of_faithful {C : Type u₁} {D : Type u₂} (F : C D) {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (H : (F.map g) (F.map h) (F.map i)) :
i
theorem category_theory.is_pushout.map_iff {C : Type u₁} {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} {D : Type u_1} (F : C D) (e : f h = g i) :
(F.map g) (F.map h) (F.map i) i