of_epi_section — Mathlib

English

If a split epi has a section that is epi, then the morphism is an iso.

Русский

Если раздельный эпиморфизм имеет секцию, которая является эпиморфизмом, то сам morphism является изоморфизмом.

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 : IsSplitEpi f] [hf' : Epi <| section_ f] : IsIso f :=
  @IsIso.of_epi_section' _ _ _ _ _ hf.exists_splitEpi.some hf'

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