isSplitMono_of_mono — Mathlib

English

In a category where every mono splits, every mono is split.

Русский

В категории, где каждый моно-разложим, каждый моно-морфизм является разделимым.

LaTeX

$$$ [\text{SplitMonoCategory } C] \Rightarrow \forall X,Y\,(f: X \to Y),\; \mathrm{Mono}(f) \Rightarrow \mathrm{IsSplitMono}(f).$$$

Lean4

/-- In a category in which every monomorphism is split, every monomorphism splits. This is not an
    instance because it would create an instance loop. -/
theorem isSplitMono_of_mono [SplitMonoCategory C] {X Y : C} (f : X ⟶ Y) [Mono f] : IsSplitMono f :=
  SplitMonoCategory.isSplitMono_of_mono _

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