section_isSplitMono — Mathlib

English

The section of a split epimorphism is a split mono.

Русский

Секция разложимого эпиморфизма является разложимым моно.

LaTeX

$$$ \\text{section_}(f) \\text{ is a SplitMono when } f \\text{ is a SplitEpi}$$$

Lean4

/-- The section of a split epimorphism is itself a split monomorphism. -/
instance section_isSplitMono {X Y : C} (f : X ⟶ Y) [IsSplitEpi f] : IsSplitMono (section_ f) :=
  IsSplitMono.mk' (SplitEpi.splitMono _)

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