isoOfIsIsomorphicZero — Mathlib

English

There is an equivalence between the proposition 𝟙_X = 0 and the isomorphism X ≅ 0.

Русский

Существует эквивалентность между равенством 𝟙_X = 0 и изоморфизмом X с нулевым объектом.

LaTeX

$$$𝟙_X = 0 \iff X \cong 0$$$

Lean4

/-- If an object `X` is isomorphic to 0, there's no need to use choice to construct
an explicit isomorphism: the zero morphism suffices. -/
def isoOfIsIsomorphicZero {X : C} (P : IsIsomorphic X 0) : X ≅ 0
    where
  hom := 0
  inv := 0
  hom_inv_id := by
    have P := P.some
    rw [← P.hom_inv_id, ← Category.id_comp P.inv]
    apply Eq.symm
    simp only [id_comp, Iso.hom_inv_id, comp_zero]
    apply (idZeroEquivIsoZero X).invFun P
  inv_hom_id := by simp

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