of_iso — Mathlib

English

If Y is zero and X ≅ Y, then X is zero.

Русский

Если Y нулевой и существует изоморфизм X ≅ Y, то X также нулевой.

LaTeX

$$$\\\\text{IsZero}(Y) \\\\Longrightarrow \\\\text{IsZero}(X) \text{ when } X \\cong Y$$$

Lean4

theorem of_iso (hY : IsZero Y) (e : X ≅ Y) : IsZero X :=
  by
  refine ⟨fun Z => ⟨⟨⟨e.hom ≫ hY.to_ Z⟩, fun f => ?_⟩⟩, fun Z => ⟨⟨⟨hY.from_ Z ≫ e.inv⟩, fun f => ?_⟩⟩⟩
  · rw [← cancel_epi e.inv]
    apply hY.eq_of_src
  · rw [← cancel_mono e.hom]
    apply hY.eq_of_tgt

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