zero_left — Mathlib

English

The square with the left side equal to 0: 0 → X and the top-right morphism being the identity X → P is a pushout.

Русский

Квадрат, левый отрезок которого 0: 0 → X, а верхний правый отрезок — тождество X → P, образует пушаут.

LaTeX

$$$\operatorname{IsPushout}(0:X\leftarrow 0, 0:(0:C)\to 0, \mathrm{id}_X, 0:0\to X)$$$

Lean4

/-- The square with `0 : 0 ⟶ 0` on the right left `𝟙 X` on the right is a pushout square. -/
@[simp]
theorem zero_left (X : C) : IsPushout (0 : 0 ⟶ X) (0 : (0 : C) ⟶ 0) (𝟙 X) (0 : 0 ⟶ X) :=
  of_iso_pushout (by simp) ((coprodZeroIso X).symm ≪≫ (pushoutZeroZeroIso _ _).symm) (by simp)
    (by simp [eq_iff_true_of_subsingleton])

Похожие утверждения