zero_of_source_iso_zero — Mathlib

English

If a morphism f: X → Y has X isomorphic to the zero object, then f is the zero morphism.

Русский

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

LaTeX

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

Lean4

theorem zero_of_source_iso_zero {X Y : C} (f : X ⟶ Y) (i : X ≅ 0) : f = 0 :=
  by
  have h : f = i.hom ≫ 𝟙 0 ≫ i.inv ≫ f := by simp only [Iso.hom_inv_id_assoc, id_comp]
  simpa using h

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