English
Every morphism f in NonemptyFinLinOrd factors as an epi followed by a mono, with the epi split.
Русский
Каждый морфизм f в NonemptyFinLinOrd раскладывается как эпиморфизм за которым следует мономорфизм, причем эпиморфизм разщепим.
LaTeX
$$$\exists I\, (e:X\to I),\ (m:I\to Y)\; (\text{SplitEpi}(e))\land (\text{Mono}(m))\land f = m \circ e.$$$
Lean4
instance : SplitEpiCategory NonemptyFinLinOrd.{u} :=
⟨fun {X Y} f hf =>
by
have H : ∀ y : Y, Nonempty (f ⁻¹' { y }) :=
by
rw [epi_iff_surjective] at hf
intro y
exact Nonempty.intro ⟨(hf y).choose, (hf y).choose_spec⟩
let φ : Y → X := fun y => (H y).some.1
have hφ : ∀ y : Y, f (φ y) = y := fun y => (H y).some.2
refine IsSplitEpi.mk' ⟨ofHom ⟨φ, ?_⟩, ?_⟩
swap
· ext b
apply hφ
· intro a b
contrapose
intro h
simp only [not_le] at h ⊢
suffices b ≤ a by
apply lt_of_le_of_ne this
rintro rfl
exfalso
simp at h
have H : f (φ b) ≤ f (φ a) := f.hom.monotone (le_of_lt h)
simpa only [hφ] using H⟩
