isoZeroOfEpiZero — Mathlib

English

The isIso equivalence is given by mapping 0-endomorphism to the pair of isomorphisms to zero object for both source and target.

Русский

Эквивалентность изоморфизма задаётся отображением нулевого морфизма в пару изоморфизмов к нулевому объекту на источнике и цели.

LaTeX

$$$IsIso(0:X\to Y) \equiv (X\cong 0) \times (Y\cong 0)$$$

Lean4

/-- If `0 : X ⟶ Y` is an epimorphism, then `Y ≅ 0`. -/
@[simps]
def isoZeroOfEpiZero {X Y : C} (_ : Epi (0 : X ⟶ Y)) : Y ≅ 0
    where
  hom := 0
  inv := 0
  hom_inv_id := (cancel_epi (0 : X ⟶ Y)).mp (by simp)

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