of_epi_section' — Mathlib

English

Every split epi whose section is epi is an iso.

Русский

Каждый раздельный эпиморфизм, у которого секция является эпи, является изоморфизмом.

LaTeX

$$$ \forall X,Y\;(f: X \to Y),\; \mathrm{SplitEpi}(f) \Rightarrow [\mathrm{Epi}(\mathrm{section_}(f))] \Rightarrow \mathrm{IsIso}(f).$$$

Lean4

/-- Every split epi whose section is epi is an iso. -/
theorem of_epi_section' {X Y : C} {f : X ⟶ Y} (hf : SplitEpi f) [Epi <| hf.section_] : IsIso f :=
  ⟨⟨hf.section_, ⟨(cancel_epi_id <| hf.section_).mp (by simp), by simp⟩⟩⟩

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