isoZeroOfMonoZero — Mathlib

English

A zero endomorphism 0: X → X is an isomorphism iff 𝟙_X = 0.

Русский

Нулевой эндоморфизм 0: X → X является изоморфизмом тогда и только тогда, когда 𝟙_X = 0.

LaTeX

$$$\text{IsIso}(0:\,X\to X)\iff 𝟙_X = 0$$$

Lean4

/-- If `0 : X ⟶ Y` is a monomorphism, then `X ≅ 0`. -/
@[simps]
def isoZeroOfMonoZero {X Y : C} (_ : Mono (0 : X ⟶ Y)) : X ≅ 0
    where
  hom := 0
  inv := 0
  hom_inv_id := (cancel_mono (0 : X ⟶ Y)).mp (by simp)

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