zero_right — Mathlib

English

The square with the right-hand side being the zero morphism 0: X → 0 and the left-hand side being the identity on X forms a pushout.

Русский

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

LaTeX

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

Lean4

/-- The square with `0 : 0 ⟶ 0` on the right and `𝟙 X` on the left is a pushout square. -/
@[simp]
theorem zero_right (X : C) : IsPushout (0 : X ⟶ 0) (𝟙 X) (0 : (0 : C) ⟶ 0) (0 : X ⟶ 0) :=
  { w := by simp
    isColimit' :=
      ⟨{  desc := fun _ => 0
          fac := fun s =>
            by
            have c :=
              @PushoutCocone.coequalizer_ext _ _ _ _ _ _ _ s _ 0 (𝟙 _) (by simp [eq_iff_true_of_subsingleton])
                (by simpa using PushoutCocone.condition s)
            dsimp at c
            simpa using c }⟩ }

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