retraction_isSplitEpi — Mathlib

English

The retraction of a split mono is a split epi.

Русский

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

LaTeX

$$$ \\text{retraction}(f) \\text{ isSplitEpi}$ for any splitMono f$$

Lean4

/-- The retraction of a split monomorphism is itself a split epimorphism. -/
instance retraction_isSplitEpi {X Y : C} (f : X ⟶ Y) [IsSplitMono f] : IsSplitEpi (retraction f) :=
  IsSplitEpi.mk' (SplitMono.splitEpi _)

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