iff_isSplitEpi_eq_zero — Mathlib

English

If f is a split epi, then IsZero Y iff f = 0.

Русский

Если f является разложимым эпиморфизмом, то IsZero Y эквивалентно f = 0.

LaTeX

$$IsSplitEpi f \Rightarrow (IsZero Y \iff f = 0)$$

Lean4

theorem iff_isSplitEpi_eq_zero {X Y : C} (f : X ⟶ Y) [IsSplitEpi f] : IsZero Y ↔ f = 0 :=
  by
  rw [iff_id_eq_zero]
  constructor
  · intro h
    rw [← Category.comp_id f, h, comp_zero]
  · intro h
    rw [← IsSplitEpi.id f]
    simp [h]

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