zero_left — Mathlib

English

The square with left side 0:0→X and 0:0→0 and right side 𝟙X and 0 is a pullback.

Русский

Квадрат со стороны слева 0:0→X и 0:0→0 и справа 𝟙X и 0 является вытягиваемым.

LaTeX

$$$IsPullback(0:0\to X,\ 0:0\to 0,\ 𝟙X,\ 0:0\to X)$$$

Lean4

/-- The square with `0 : 0 ⟶ 0` on the left and `𝟙 X` on the right is a pullback square. -/
@[simp]
theorem zero_left (X : C) : IsPullback (0 : 0 ⟶ X) (0 : (0 : C) ⟶ 0) (𝟙 X) (0 : 0 ⟶ X) :=
  { w := by simp
    isLimit' :=
      ⟨{  lift := fun _ => 0
          fac := fun s => by
            simpa [eq_iff_true_of_subsingleton] using
              @PullbackCone.equalizer_ext _ _ _ _ _ _ _ s _ 0 (𝟙 _)
                (by simpa using (PullbackCone.condition s).symm) }⟩ }

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