isIsoZeroEquivIsoZero — Mathlib

English

There is a canonical equivalence between the property IsIso 0 and the pair of isomorphisms X ≅ 0, Y ≅ 0.

Русский

Существует каноническая эквивалентность между IsIso 0 и парой изоморфизмов X ≅ 0 и Y ≅ 0.

LaTeX

$$$IsIso(0) \iff (X\cong 0) \times (Y\cong 0)$$$

Lean4

/-- A zero morphism `0 : X ⟶ Y` is an isomorphism if and only if
`X` and `Y` are isomorphic to the zero object.
-/
def isIsoZeroEquivIsoZero (X Y : C) : IsIso (0 : X ⟶ Y) ≃ (X ≅ 0) × (Y ≅ 0) := by
  -- This is lame, because `Prod` can't cope with `Prop`, so we can't use `Equiv.prodCongr`.

  refine (isIsoZeroEquiv X Y).trans ?_
  symm
  fconstructor
  · rintro ⟨eX, eY⟩
    fconstructor
    · exact (idZeroEquivIsoZero X).symm eX
    · exact (idZeroEquivIsoZero Y).symm eY
  · rintro ⟨hX, hY⟩
    fconstructor
    · exact (idZeroEquivIsoZero X) hX
    · exact (idZeroEquivIsoZero Y) hY
  · cat_disch
  · cat_disch

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