epiWithInjectiveKernel_of_iso — Mathlib

English

If f is an isomorphism, then f has the property epiWithInjectiveKernel.

Русский

Если морфизм f является изоморфизмом, то он имеет свойство epiWithInjectiveKernel.

LaTeX

$$$\\text{IsIso}(f) \\Rightarrow \\mathrm{epiWithInjectiveKernel}(f)$$$

Lean4

theorem epiWithInjectiveKernel_of_iso {X Y : C} (f : X ⟶ Y) [IsIso f] : epiWithInjectiveKernel f :=
  by
  rw [epiWithInjectiveKernel_iff]
  exact ⟨0, inferInstance, 0, by simp, ⟨ShortComplex.Splitting.ofIsZeroOfIsIso _ (isZero_zero C) (by assumption)⟩⟩

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