idZeroEquivIsoZero — Mathlib

English

There is a one-to-one correspondence between 𝟙_X = 0 and X ≅ 0.

Русский

Существует биекция между равенством 𝟙_X = 0 и тем, что X изоморфен нулевому объекту.

LaTeX

$$$𝟙_X = 0 \quad\leftrightarrow\quad X \cong 0$$$

Lean4

/-- An object `X` has `𝟙 X = 0` if and only if it is isomorphic to the zero object.

Because `X ≅ 0` contains data (even if a subsingleton), we express this `↔` as an `≃`.
-/
def idZeroEquivIsoZero (X : C) : 𝟙 X = 0 ≃ (X ≅ 0)
    where
  toFun
    h :=
    { hom := 0
      inv := 0 }
  invFun i := zero_of_target_iso_zero (𝟙 X) i
  left_inv := by cat_disch
  right_inv := by cat_disch

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