mathlib documentation

category_theory.limits.shapes.comm_sq

Pullback and pushout 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.

Future work #

Bicartesian squares, and show that the pullback and pushout squares for a biproduct are bicartesian.

structure category_theory.comm_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

The proposition that a square

  W ---f---> X
  |          |
  g          h
  |          |
  v          v
  Y ---i---> Z

is a commuting square.

theorem category_theory.comm_sq.w_assoc {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.comm_sq f g h i) {X' : C} (f' : Z X') :
f h f' = g i f'
theorem category_theory.comm_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.comm_sq f g h i) :
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
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.

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.

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

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

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

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

The square with 0 : 0 ⟶ 0 on the top and 𝟙 X on the bottom 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_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) :

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

The square with 0 : 0 ⟶ 0 on the bottom and 𝟙 X on the top 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.functor.map_comm_sq {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} (s : category_theory.comm_sq f g h i) :
category_theory.comm_sq (F.map f) (F.map g) (F.map h) (F.map 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.comm_sq.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} (s : category_theory.comm_sq f g h i) :
category_theory.comm_sq (F.map f) (F.map g) (F.map h) (F.map i)

Alias of category_theory.functor.map_comm_sq.

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.