isIsoZeroEquiv — Mathlib

English

If f: X → Y and Y ≅ 0, then f is an epimorphism.

Русский

Если f: X → Y и Y изоморфен нулевому объекту, то f эпиморфизм.

LaTeX

$$$\forall X,Y:\, C,\ \forall f:X\to Y,\forall i:Y\cong 0,\ Epi\ f$$$

Lean4

/-- A zero morphism `0 : X ⟶ Y` is an isomorphism if and only if
the identities on both `X` and `Y` are zero.
-/
def isIsoZeroEquiv (X Y : C) : IsIso (0 : X ⟶ Y) ≃ 𝟙 X = 0 ∧ 𝟙 Y = 0
    where
  toFun := by
    intro i
    rw [← IsIso.hom_inv_id (0 : X ⟶ Y)]
    rw [← IsIso.inv_hom_id (0 : X ⟶ Y)]
    simp only [comp_zero, and_self, zero_comp]
  invFun h := ⟨⟨(0 : Y ⟶ X), by cat_disch⟩⟩
  left_inv := by cat_disch
  right_inv := by cat_disch

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