mathlib documentation

category_theory.limits.shapes.comm_sq

Pullback and pushout squares, and bicartesian squares #

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) :
s.cone.fst = f
@[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) :
s.cone.snd = g
@[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

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

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) :
@[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) :
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

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.

Equations
@[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) :
h.cone.fst = fst
@[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) :
h.cone.snd = snd
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.

Equations

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

A variant of of_is_limit that is more useful with apply.

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

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

A variant of of_is_product that is more useful with apply.

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

Equations
@[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) :
h.cocone.inl = inl
@[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) :
h.cocone.inr = 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

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

A variant of of_is_colimit that is more useful with apply.

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

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

A variant of of_is_coproduct that is more useful with apply.

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]
@[simp]
@[simp]
@[simp]
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) :
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} :
@[simp]

The square with 0 : 0 ⟶ 0 on the left and 𝟙 X on the right is a pullback square.

@[simp]

The square with 0 : 0 ⟶ 0 on the top and 𝟙 X on the bottom is a pullback square.

@[simp]

The square with 0 : 0 ⟶ 0 on the right and 𝟙 X on the left is a pullback square.

@[simp]

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.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) :
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) :
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) :
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) :
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} :
@[simp]

The square with 0 : 0 ⟶ 0 on the right and 𝟙 X on the left is a pushout square.

@[simp]

The square with 0 : 0 ⟶ 0 on the bottom and 𝟙 X on the top is a pushout square.

@[simp]

The square with 0 : 0 ⟶ 0 on the right left 𝟙 X on the right is a pushout square.

@[simp]

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

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

Equations

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₁} [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) :
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) :
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_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)) :
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)) :