Documentation

Mathlib.CategoryTheory.Limits.Shapes.CommSq

Pullback and pushout squares, and bicartesian 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 : pullback f g ⟶ X) (pullback.snd : pullback f g ⟶ Y) 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 bicartesian squares, and show that the pullback and pushout squares for a biproduct are bicartesian.

def CategoryTheory.CommSq.cone {C : Type u₁} [] {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (s : ) :

The (not necessarily limiting) PullbackCone h i implicit in the statement that we have CommSq f g h i.

Instances For
def CategoryTheory.CommSq.cocone {C : Type u₁} [] {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (s : ) :

The (not necessarily limiting) PushoutCocone f g implicit in the statement that we have CommSq f g h i.

Instances For
@[simp]
theorem CategoryTheory.CommSq.cone_fst {C : Type u₁} [] {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (s : ) :
@[simp]
theorem CategoryTheory.CommSq.cone_snd {C : Type u₁} [] {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (s : ) :
@[simp]
theorem CategoryTheory.CommSq.cocone_inl {C : Type u₁} [] {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (s : ) :
@[simp]
theorem CategoryTheory.CommSq.cocone_inr {C : Type u₁} [] {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (s : ) :
def CategoryTheory.CommSq.coneOp {C : Type u₁} [] {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (p : ) :

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

Instances For
def CategoryTheory.CommSq.coconeOp {C : Type u₁} [] {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (p : ) :

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

Instances For
def CategoryTheory.CommSq.coneUnop {C : Type u₁} [] {W : Cᵒᵖ} {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (p : ) :
CategoryTheory.CommSq.cocone (_ : CategoryTheory.CommSq h.unop i.unop f.unop g.unop)

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.

Instances For
def CategoryTheory.CommSq.coconeUnop {C : Type u₁} [] {W : Cᵒᵖ} {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (p : ) :
CategoryTheory.CommSq.cone (_ : CategoryTheory.CommSq h.unop i.unop f.unop g.unop)

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.

Instances For
structure CategoryTheory.IsPullback {C : Type u₁} [] {P : C} {X : C} {Y : C} {Z : C} (fst : P X) (snd : P Y) (f : X Z) (g : Y Z) extends :

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
structure CategoryTheory.IsPushout {C : Type u₁} [] {Z : C} {X : C} {Y : C} {P : C} (f : Z X) (g : Z Y) (inl : X P) (inr : Y P) extends :

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.)

Instances For
structure CategoryTheory.BicartesianSq {C : Type u₁} [] {W : C} {X : C} {Y : C} {Z : C} (f : W X) (g : W Y) (h : X Z) (i : Y Z) extends :
• isLimit' : Nonempty ()
• isColimit' :

the pushout cocone is a colimit

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.

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₁} [] {P : C} {X : C} {Y : C} {Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : CategoryTheory.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₁} [] {P : C} {X : C} {Y : C} {Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : CategoryTheory.IsPullback fst snd f g) :
@[simp]
theorem CategoryTheory.IsPullback.cone_snd {C : Type u₁} [] {P : C} {X : C} {Y : C} {Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : CategoryTheory.IsPullback fst snd f g) :
noncomputable def CategoryTheory.IsPullback.isLimit {C : Type u₁} [] {P : C} {X : C} {Y : C} {Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : CategoryTheory.IsPullback fst snd f g) :

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

Instances For
theorem CategoryTheory.IsPullback.of_isLimit {C : Type u₁} [] {X : C} {Y : C} {Z : C} {f : X Z} {g : Y Z} {c : } :

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₁} [] {P : C} {X : C} {Y : C} {Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (w : CategoryTheory.CommSq fst snd f g) :

A variant of of_isLimit that is more useful with apply.

theorem CategoryTheory.IsPullback.of_hasPullback {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X Z) (g : Y Z) :
CategoryTheory.IsPullback CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd f g

The pullback provided by HasPullback f g fits into an IsPullback.

theorem CategoryTheory.IsPullback.of_is_product {C : Type u₁} [] {X : C} {Y : C} {Z : C} {c : } :

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₁} [] {P : C} {X : C} {Y : C} {Z : C} {fst : P X} {snd : P Y} (h : ) :

A variant of of_is_product that is more useful with apply.

theorem CategoryTheory.IsPullback.of_hasBinaryProduct' {C : Type u₁} [] (X : C) (Y : C) :
CategoryTheory.IsPullback CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd () ()
theorem CategoryTheory.IsPullback.of_hasBinaryProduct {C : Type u₁} [] (X : C) (Y : C) :
CategoryTheory.IsPullback CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd 0 0
noncomputable def CategoryTheory.IsPullback.isoPullback {C : Type u₁} [] {P : C} {X : C} {Y : C} {Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : CategoryTheory.IsPullback fst snd f g) :

Any object at the top left of a pullback square is isomorphic to the pullback provided by the HasLimit API.

Instances For
@[simp]
theorem CategoryTheory.IsPullback.isoPullback_hom_fst {C : Type u₁} [] {P : C} {X : C} {Y : C} {Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : CategoryTheory.IsPullback fst snd f g) :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst = fst
@[simp]
theorem CategoryTheory.IsPullback.isoPullback_hom_snd {C : Type u₁} [] {P : C} {X : C} {Y : C} {Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : CategoryTheory.IsPullback fst snd f g) :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd = snd
@[simp]
theorem CategoryTheory.IsPullback.isoPullback_inv_fst {C : Type u₁} [] {P : C} {X : C} {Y : C} {Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : CategoryTheory.IsPullback fst snd f g) :
= CategoryTheory.Limits.pullback.fst
@[simp]
theorem CategoryTheory.IsPullback.isoPullback_inv_snd {C : Type u₁} [] {P : C} {X : C} {Y : C} {Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : CategoryTheory.IsPullback fst snd f g) :
= CategoryTheory.Limits.pullback.snd
theorem CategoryTheory.IsPullback.of_iso_pullback {C : Type u₁} [] {P : C} {X : C} {Y : C} {Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : CategoryTheory.CommSq fst snd f g) (i : ) (w₁ : CategoryTheory.CategoryStruct.comp i.hom CategoryTheory.Limits.pullback.fst = fst) (w₂ : CategoryTheory.CategoryStruct.comp i.hom CategoryTheory.Limits.pullback.snd = snd) :
theorem CategoryTheory.IsPullback.of_horiz_isIso {C : Type u₁} [] {P : C} {X : C} {Y : C} {Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} [] (sq : CategoryTheory.CommSq fst snd f g) :
def CategoryTheory.IsPushout.cocone {C : Type u₁} [] {Z : C} {X : C} {Y : C} {P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : CategoryTheory.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
@[simp]
theorem CategoryTheory.IsPushout.cocone_inl {C : Type u₁} [] {Z : C} {X : C} {Y : C} {P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : CategoryTheory.IsPushout f g inl inr) :
@[simp]
theorem CategoryTheory.IsPushout.cocone_inr {C : Type u₁} [] {Z : C} {X : C} {Y : C} {P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : CategoryTheory.IsPushout f g inl inr) :
noncomputable def CategoryTheory.IsPushout.isColimit {C : Type u₁} [] {Z : C} {X : C} {Y : C} {P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : CategoryTheory.IsPushout f g inl inr) :

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

Instances For
theorem CategoryTheory.IsPushout.of_isColimit {C : Type u₁} [] {Z : C} {X : C} {Y : C} {f : Z X} {g : Z Y} {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₁} [] {Z : C} {X : C} {Y : C} {P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (w : CategoryTheory.CommSq f g inl inr) :

A variant of of_isColimit that is more useful with apply.

theorem CategoryTheory.IsPushout.of_hasPushout {C : Type u₁} [] {Z : C} {X : C} {Y : C} (f : Z X) (g : Z Y) :
CategoryTheory.IsPushout f g CategoryTheory.Limits.pushout.inl CategoryTheory.Limits.pushout.inr

The pushout provided by HasPushout f g fits into an IsPushout.

theorem CategoryTheory.IsPushout.of_is_coproduct {C : Type u₁} [] {Z : C} {X : C} {Y : C} {c : } :

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₁} [] {Z : C} {X : C} {Y : C} {P : C} {inl : X P} {inr : Y P} :

A variant of of_is_coproduct that is more useful with apply.

theorem CategoryTheory.IsPushout.of_hasBinaryCoproduct' {C : Type u₁} [] (X : C) (Y : C) :
CategoryTheory.IsPushout () () CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr
theorem CategoryTheory.IsPushout.of_hasBinaryCoproduct {C : Type u₁} [] (X : C) (Y : C) :
CategoryTheory.IsPushout 0 0 CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr
noncomputable def CategoryTheory.IsPushout.isoPushout {C : Type u₁} [] {Z : C} {X : C} {Y : C} {P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : CategoryTheory.IsPushout f g inl inr) :

Any object at the top left of a pullback square is isomorphic to the pullback provided by the HasLimit API.

Instances For
@[simp]
theorem CategoryTheory.IsPushout.inl_isoPushout_inv {C : Type u₁} [] {Z : C} {X : C} {Y : C} {P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : CategoryTheory.IsPushout f g inl inr) :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl = inl
@[simp]
theorem CategoryTheory.IsPushout.inr_isoPushout_inv {C : Type u₁} [] {Z : C} {X : C} {Y : C} {P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : CategoryTheory.IsPushout f g inl inr) :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr = inr
@[simp]
theorem CategoryTheory.IsPushout.inl_isoPushout_hom {C : Type u₁} [] {Z : C} {X : C} {Y : C} {P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : CategoryTheory.IsPushout f g inl inr) :
= CategoryTheory.Limits.pushout.inl
@[simp]
theorem CategoryTheory.IsPushout.inr_isoPushout_hom {C : Type u₁} [] {Z : C} {X : C} {Y : C} {P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : CategoryTheory.IsPushout f g inl inr) :
= CategoryTheory.Limits.pushout.inr
theorem CategoryTheory.IsPushout.of_iso_pushout {C : Type u₁} [] {Z : C} {X : C} {Y : C} {P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : CategoryTheory.CommSq f g inl inr) (i : ) (w₁ : = CategoryTheory.Limits.pushout.inl) (w₂ : = CategoryTheory.Limits.pushout.inr) :
theorem CategoryTheory.IsPullback.flip {C : Type u₁} [] {P : C} {X : C} {Y : C} {Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : CategoryTheory.IsPullback fst snd f g) :
theorem CategoryTheory.IsPullback.flip_iff {C : Type u₁} [] {P : C} {X : C} {Y : C} {Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} :
@[simp]
theorem CategoryTheory.IsPullback.zero_left {C : Type u₁} [] (X : C) :

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₁} [] (X : C) :

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₁} [] (X : C) :

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₁} [] (X : C) :

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₁} [] {X₁₁ : C} {X₁₂ : C} {X₂₁ : C} {X₂₂ : C} {X₃₁ : C} {X₃₂ : C} {h₁₁ : X₁₁ X₁₂} {h₂₁ : X₂₁ X₂₂} {h₃₁ : X₃₁ X₃₂} {v₁₁ : X₁₁ X₂₁} {v₁₂ : X₁₂ X₂₂} {v₂₁ : X₂₁ X₃₁} {v₂₂ : X₂₂ X₃₂} (s : CategoryTheory.IsPullback h₁₁ v₁₁ v₁₂ h₂₁) (t : CategoryTheory.IsPullback h₂₁ v₂₁ v₂₂ h₃₁) :
CategoryTheory.IsPullback h₁₁ () () h₃₁

Paste two pullback squares "vertically" to obtain another pullback square.

theorem CategoryTheory.IsPullback.paste_horiz {C : Type u₁} [] {X₁₁ : C} {X₁₂ : C} {X₁₃ : C} {X₂₁ : C} {X₂₂ : C} {X₂₃ : C} {h₁₁ : X₁₁ X₁₂} {h₁₂ : X₁₂ X₁₃} {h₂₁ : X₂₁ X₂₂} {h₂₂ : X₂₂ X₂₃} {v₁₁ : X₁₁ X₂₁} {v₁₂ : X₁₂ X₂₂} {v₁₃ : X₁₃ X₂₃} (s : CategoryTheory.IsPullback h₁₁ v₁₁ v₁₂ h₂₁) (t : CategoryTheory.IsPullback h₁₂ v₁₂ v₁₃ h₂₂) :
CategoryTheory.IsPullback () v₁₁ v₁₃ ()

Paste two pullback squares "horizontally" to obtain another pullback square.

theorem CategoryTheory.IsPullback.of_bot {C : Type u₁} [] {X₁₁ : C} {X₁₂ : C} {X₂₁ : C} {X₂₂ : C} {X₃₁ : C} {X₃₂ : C} {h₁₁ : X₁₁ X₁₂} {h₂₁ : X₂₁ X₂₂} {h₃₁ : X₃₁ X₃₂} {v₁₁ : X₁₁ X₂₁} {v₁₂ : X₁₂ X₂₂} {v₂₁ : X₂₁ X₃₁} {v₂₂ : X₂₂ X₃₂} (s : CategoryTheory.IsPullback h₁₁ () () h₃₁) (p : ) (t : CategoryTheory.IsPullback h₂₁ v₂₁ v₂₂ h₃₁) :
CategoryTheory.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.

theorem CategoryTheory.IsPullback.of_right {C : Type u₁} [] {X₁₁ : C} {X₁₂ : C} {X₁₃ : C} {X₂₁ : C} {X₂₂ : C} {X₂₃ : C} {h₁₁ : X₁₁ X₁₂} {h₁₂ : X₁₂ X₁₃} {h₂₁ : X₂₁ X₂₂} {h₂₂ : X₂₂ X₂₃} {v₁₁ : X₁₁ X₂₁} {v₁₂ : X₁₂ X₂₂} {v₁₃ : X₁₃ X₂₃} (s : CategoryTheory.IsPullback () v₁₁ v₁₃ ()) (p : ) (t : CategoryTheory.IsPullback h₁₂ v₁₂ v₁₃ h₂₂) :
CategoryTheory.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.

theorem CategoryTheory.IsPullback.paste_vert_iff {C : Type u₁} [] {X₁₁ : C} {X₁₂ : C} {X₂₁ : C} {X₂₂ : C} {X₃₁ : C} {X₃₂ : C} {h₁₁ : X₁₁ X₁₂} {h₂₁ : X₂₁ X₂₂} {h₃₁ : X₃₁ X₃₂} {v₁₁ : X₁₁ X₂₁} {v₁₂ : X₁₂ X₂₂} {v₂₁ : X₂₁ X₃₁} {v₂₂ : X₂₂ X₃₂} (s : CategoryTheory.IsPullback h₂₁ v₂₁ v₂₂ h₃₁) (e : ) :
CategoryTheory.IsPullback h₁₁ () () h₃₁ CategoryTheory.IsPullback h₁₁ v₁₁ v₁₂ h₂₁
theorem CategoryTheory.IsPullback.paste_horiz_iff {C : Type u₁} [] {X₁₁ : C} {X₁₂ : C} {X₁₃ : C} {X₂₁ : C} {X₂₂ : C} {X₂₃ : C} {h₁₁ : X₁₁ X₁₂} {h₁₂ : X₁₂ X₁₃} {h₂₁ : X₂₁ X₂₂} {h₂₂ : X₂₂ X₂₃} {v₁₁ : X₁₁ X₂₁} {v₁₂ : X₁₂ X₂₂} {v₁₃ : X₁₃ X₂₃} (s : CategoryTheory.IsPullback h₁₂ v₁₂ v₁₃ h₂₂) (e : ) :
CategoryTheory.IsPullback () v₁₁ v₁₃ () CategoryTheory.IsPullback h₁₁ v₁₁ v₁₂ h₂₁
theorem CategoryTheory.IsPullback.of_isBilimit {C : Type u₁} [] {X : C} {Y : C} {b : } :
@[simp]
theorem CategoryTheory.IsPullback.of_has_biproduct {C : Type u₁} [] (X : C) (Y : C) :
CategoryTheory.IsPullback CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.snd 0 0
theorem CategoryTheory.IsPullback.inl_snd' {C : Type u₁} [] {X : C} {Y : C} {b : } :
@[simp]
theorem CategoryTheory.IsPullback.inl_snd {C : Type u₁} [] (X : C) (Y : C) :
CategoryTheory.IsPullback CategoryTheory.Limits.biprod.inl 0 CategoryTheory.Limits.biprod.snd 0

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₁} [] {X : C} {Y : C} {b : } :
@[simp]
theorem CategoryTheory.IsPullback.inr_fst {C : Type u₁} [] (X : C) (Y : C) :
CategoryTheory.IsPullback CategoryTheory.Limits.biprod.inr 0 CategoryTheory.Limits.biprod.fst 0

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₁} [] {X : C} {Y : C} {b : } :
theorem CategoryTheory.IsPullback.of_hasBinaryBiproduct {C : Type u₁} [] (X : C) (Y : C) :
CategoryTheory.IsPullback 0 0 CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.biprod.inr
instance CategoryTheory.IsPullback.hasPullback_biprod_fst_biprod_snd {C : Type u₁} [] {X : C} {Y : C} :
CategoryTheory.Limits.HasPullback CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.biprod.inr
def CategoryTheory.IsPullback.pullbackBiprodInlBiprodInr {C : Type u₁} [] {X : C} {Y : C} :
CategoryTheory.Limits.pullback CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.biprod.inr 0

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

Instances For
theorem CategoryTheory.IsPullback.op {C : Type u₁} [] {P : C} {X : C} {Y : C} {Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : CategoryTheory.IsPullback fst snd f g) :
CategoryTheory.IsPushout g.op f.op snd.op fst.op
theorem CategoryTheory.IsPullback.unop {C : Type u₁} [] {P : Cᵒᵖ} {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : CategoryTheory.IsPullback fst snd f g) :
CategoryTheory.IsPushout g.unop f.unop snd.unop fst.unop
theorem CategoryTheory.IsPullback.of_vert_isIso {C : Type u₁} [] {P : C} {X : C} {Y : C} {Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} [] (sq : CategoryTheory.CommSq fst snd f g) :
theorem CategoryTheory.IsPushout.flip {C : Type u₁} [] {Z : C} {X : C} {Y : C} {P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : CategoryTheory.IsPushout f g inl inr) :
theorem CategoryTheory.IsPushout.flip_iff {C : Type u₁} [] {Z : C} {X : C} {Y : C} {P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} :
@[simp]
theorem CategoryTheory.IsPushout.zero_right {C : Type u₁} [] (X : C) :

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₁} [] (X : C) :

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₁} [] (X : C) :

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₁} [] (X : C) :

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₁} [] {X₁₁ : C} {X₁₂ : C} {X₂₁ : C} {X₂₂ : C} {X₃₁ : C} {X₃₂ : C} {h₁₁ : X₁₁ X₁₂} {h₂₁ : X₂₁ X₂₂} {h₃₁ : X₃₁ X₃₂} {v₁₁ : X₁₁ X₂₁} {v₁₂ : X₁₂ X₂₂} {v₂₁ : X₂₁ X₃₁} {v₂₂ : X₂₂ X₃₂} (s : CategoryTheory.IsPushout h₁₁ v₁₁ v₁₂ h₂₁) (t : CategoryTheory.IsPushout h₂₁ v₂₁ v₂₂ h₃₁) :
CategoryTheory.IsPushout h₁₁ () () h₃₁

Paste two pushout squares "vertically" to obtain another pushout square.

theorem CategoryTheory.IsPushout.paste_horiz {C : Type u₁} [] {X₁₁ : C} {X₁₂ : C} {X₁₃ : C} {X₂₁ : C} {X₂₂ : C} {X₂₃ : C} {h₁₁ : X₁₁ X₁₂} {h₁₂ : X₁₂ X₁₃} {h₂₁ : X₂₁ X₂₂} {h₂₂ : X₂₂ X₂₃} {v₁₁ : X₁₁ X₂₁} {v₁₂ : X₁₂ X₂₂} {v₁₃ : X₁₃ X₂₃} (s : CategoryTheory.IsPushout h₁₁ v₁₁ v₁₂ h₂₁) (t : CategoryTheory.IsPushout h₁₂ v₁₂ v₁₃ h₂₂) :
CategoryTheory.IsPushout () v₁₁ v₁₃ ()

Paste two pushout squares "horizontally" to obtain another pushout square.

theorem CategoryTheory.IsPushout.of_bot {C : Type u₁} [] {X₁₁ : C} {X₁₂ : C} {X₂₁ : C} {X₂₂ : C} {X₃₁ : C} {X₃₂ : C} {h₁₁ : X₁₁ X₁₂} {h₂₁ : X₂₁ X₂₂} {h₃₁ : X₃₁ X₃₂} {v₁₁ : X₁₁ X₂₁} {v₁₂ : X₁₂ X₂₂} {v₂₁ : X₂₁ X₃₁} {v₂₂ : X₂₂ X₃₂} (s : CategoryTheory.IsPushout h₁₁ () () h₃₁) (p : ) (t : CategoryTheory.IsPushout h₁₁ v₁₁ v₁₂ h₂₁) :
CategoryTheory.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.

theorem CategoryTheory.IsPushout.of_right {C : Type u₁} [] {X₁₁ : C} {X₁₂ : C} {X₁₃ : C} {X₂₁ : C} {X₂₂ : C} {X₂₃ : C} {h₁₁ : X₁₁ X₁₂} {h₁₂ : X₁₂ X₁₃} {h₂₁ : X₂₁ X₂₂} {h₂₂ : X₂₂ X₂₃} {v₁₁ : X₁₁ X₂₁} {v₁₂ : X₁₂ X₂₂} {v₁₃ : X₁₃ X₂₃} (s : CategoryTheory.IsPushout () v₁₁ v₁₃ ()) (p : ) (t : CategoryTheory.IsPushout h₁₁ v₁₁ v₁₂ h₂₁) :
CategoryTheory.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.

theorem CategoryTheory.IsPushout.paste_vert_iff {C : Type u₁} [] {X₁₁ : C} {X₁₂ : C} {X₂₁ : C} {X₂₂ : C} {X₃₁ : C} {X₃₂ : C} {h₁₁ : X₁₁ X₁₂} {h₂₁ : X₂₁ X₂₂} {h₃₁ : X₃₁ X₃₂} {v₁₁ : X₁₁ X₂₁} {v₁₂ : X₁₂ X₂₂} {v₂₁ : X₂₁ X₃₁} {v₂₂ : X₂₂ X₃₂} (s : CategoryTheory.IsPushout h₁₁ v₁₁ v₁₂ h₂₁) (e : ) :
CategoryTheory.IsPushout h₁₁ () () h₃₁ CategoryTheory.IsPushout h₂₁ v₂₁ v₂₂ h₃₁
theorem CategoryTheory.IsPushout.paste_horiz_iff {C : Type u₁} [] {X₁₁ : C} {X₁₂ : C} {X₁₃ : C} {X₂₁ : C} {X₂₂ : C} {X₂₃ : C} {h₁₁ : X₁₁ X₁₂} {h₁₂ : X₁₂ X₁₃} {h₂₁ : X₂₁ X₂₂} {h₂₂ : X₂₂ X₂₃} {v₁₁ : X₁₁ X₂₁} {v₁₂ : X₁₂ X₂₂} {v₁₃ : X₁₃ X₂₃} (s : CategoryTheory.IsPushout h₁₁ v₁₁ v₁₂ h₂₁) (e : ) :
CategoryTheory.IsPushout () v₁₁ v₁₃ () CategoryTheory.IsPushout h₁₂ v₁₂ v₁₃ h₂₂
theorem CategoryTheory.IsPushout.of_isBilimit {C : Type u₁} [] {X : C} {Y : C} {b : } :
CategoryTheory.IsPushout 0 0 b.inl b.inr
@[simp]
theorem CategoryTheory.IsPushout.of_has_biproduct {C : Type u₁} [] (X : C) (Y : C) :
CategoryTheory.IsPushout 0 0 CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.biprod.inr
theorem CategoryTheory.IsPushout.inl_snd' {C : Type u₁} [] {X : C} {Y : C} {b : } :
CategoryTheory.IsPushout b.inl 0 b.snd 0
theorem CategoryTheory.IsPushout.inl_snd {C : Type u₁} [] (X : C) (Y : C) :
CategoryTheory.IsPushout CategoryTheory.Limits.biprod.inl 0 CategoryTheory.Limits.biprod.snd 0

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₁} [] {X : C} {Y : C} {b : } :
CategoryTheory.IsPushout b.inr 0 b.fst 0
theorem CategoryTheory.IsPushout.inr_fst {C : Type u₁} [] (X : C) (Y : C) :
CategoryTheory.IsPushout CategoryTheory.Limits.biprod.inr 0 CategoryTheory.Limits.biprod.fst 0

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₁} [] {X : C} {Y : C} {b : } :
CategoryTheory.IsPushout b.fst b.snd 0 0
theorem CategoryTheory.IsPushout.of_hasBinaryBiproduct {C : Type u₁} [] (X : C) (Y : C) :
CategoryTheory.IsPushout CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.snd 0 0
instance CategoryTheory.IsPushout.hasPushout_biprod_fst_biprod_snd {C : Type u₁} [] {X : C} {Y : C} :
CategoryTheory.Limits.HasPushout CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.snd
def CategoryTheory.IsPushout.pushoutBiprodFstBiprodSnd {C : Type u₁} [] {X : C} {Y : C} :
CategoryTheory.Limits.pushout CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.snd 0

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

Instances For
theorem CategoryTheory.IsPushout.op {C : Type u₁} [] {Z : C} {X : C} {Y : C} {P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : CategoryTheory.IsPushout f g inl inr) :
CategoryTheory.IsPullback inr.op inl.op g.op f.op
theorem CategoryTheory.IsPushout.unop {C : Type u₁} [] {Z : Cᵒᵖ} {X : Cᵒᵖ} {Y : Cᵒᵖ} {P : Cᵒᵖ} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : CategoryTheory.IsPushout f g inl inr) :
CategoryTheory.IsPullback inr.unop inl.unop g.unop f.unop
theorem CategoryTheory.IsPushout.of_horiz_isIso {C : Type u₁} [] {Z : C} {X : C} {Y : C} {P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} [] (sq : CategoryTheory.CommSq f g inl inr) :
theorem CategoryTheory.IsPushout.of_vert_isIso {C : Type u₁} [] {Z : C} {X : C} {Y : C} {P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} [] (sq : CategoryTheory.CommSq f g inl inr) :
noncomputable def CategoryTheory.IsPullback.isLimitFork {C : Type u₁} [] {X : C} {Y : C} {Z : C} {f : X Y} {g : Y Z} {g' : Y Z} (H : ) :

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

Instances For
noncomputable def CategoryTheory.IsPushout.isLimitFork {C : Type u₁} [] {X : C} {Y : C} {Z : C} {f : X Y} {f' : X Y} {g : Y Z} (H : ) :

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

Instances For
theorem CategoryTheory.BicartesianSq.of_isPullback_isPushout {C : Type u₁} [] {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (p₁ : ) (p₂ : ) :
theorem CategoryTheory.BicartesianSq.flip {C : Type u₁} [] {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (p : ) :
theorem CategoryTheory.BicartesianSq.of_is_biproduct₁ {C : Type u₁} [] {X : C} {Y : C} {b : } :
 X ⊞ Y --fst--> X
|            |
snd           0
|            |
v            v
Y -----0---> 0


is a bicartesian square.

theorem CategoryTheory.BicartesianSq.of_is_biproduct₂ {C : Type u₁} [] {X : C} {Y : C} {b : } :
   0 -----0---> X
|            |
0           inl
|            |
v            v
Y --inr--> X ⊞ Y


is a bicartesian square.

@[simp]
theorem CategoryTheory.BicartesianSq.of_has_biproduct₁ {C : Type u₁} [] {X : C} {Y : C} :
CategoryTheory.BicartesianSq CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.snd 0 0
 X ⊞ Y --fst--> X
|            |
snd           0
|            |
v            v
Y -----0---> 0


is a bicartesian square.

@[simp]
theorem CategoryTheory.BicartesianSq.of_has_biproduct₂ {C : Type u₁} [] {X : C} {Y : C} :
CategoryTheory.BicartesianSq 0 0 CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.biprod.inr
   0 -----0---> X
|            |
0           inl
|            |
v            v
Y --inr--> X ⊞ Y


is a bicartesian square.

theorem CategoryTheory.Functor.map_isPullback {C : Type u₁} [] {D : Type u₂} [] (F : ) {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (s : ) :
CategoryTheory.IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
theorem CategoryTheory.Functor.map_isPushout {C : Type u₁} [] {D : Type u₂} [] (F : ) {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (s : ) :
CategoryTheory.IsPushout (F.map f) (F.map g) (F.map h) (F.map i)
theorem CategoryTheory.IsPullback.map {C : Type u₁} [] {D : Type u₂} [] (F : ) {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (s : ) :
CategoryTheory.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₁} [] {D : Type u₂} [] (F : ) {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (s : ) :
CategoryTheory.IsPushout (F.map f) (F.map g) (F.map h) (F.map i)

Alias of CategoryTheory.Functor.map_isPushout.

theorem CategoryTheory.IsPullback.of_map {C : Type u₁} [] {D : Type u₂} [] (F : ) {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (H : CategoryTheory.IsPullback (F.map f) (F.map g) (F.map h) (F.map i)) :
theorem CategoryTheory.IsPullback.of_map_of_faithful {C : Type u₁} [] {D : Type u₂} [] (F : ) {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (H : CategoryTheory.IsPullback (F.map f) (F.map g) (F.map h) (F.map i)) :
theorem CategoryTheory.IsPullback.map_iff {C : Type u₁} [] {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} {D : Type u_1} [] (F : ) :
CategoryTheory.IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
theorem CategoryTheory.IsPushout.of_map {C : Type u₁} [] {D : Type u₂} [] (F : ) {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (H : CategoryTheory.IsPushout (F.map f) (F.map g) (F.map h) (F.map i)) :
theorem CategoryTheory.IsPushout.of_map_of_faithful {C : Type u₁} [] {D : Type u₂} [] (F : ) {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (H : CategoryTheory.IsPushout (F.map f) (F.map g) (F.map h) (F.map i)) :
theorem CategoryTheory.IsPushout.map_iff {C : Type u₁} [] {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} {D : Type u_1} [] (F : ) :
CategoryTheory.IsPushout (F.map f) (F.map g) (F.map h) (F.map i)