English
The SimplexCategory is balanced: any morphism that is both mono and epi is an isomorphism.
Русский
Категория SimplexCategory сбалансирована: любая морфизма, которая и моно, и эпиморфизм, является изоморфизмом.
LaTeX
$$$\\\\forall X,Y \\\\in \\\\text{SimplexCategory}, \\\\forall f: X \\\\to Y, \\\\big([\\\\text{Mono}(f)] \\\and [\\\\text{Epi}(f)]\\\\big) \\\Rightarrow \\text{IsIso}(f)$$$
Lean4
instance : (forget SimplexCategory).ReflectsIsomorphisms :=
⟨fun f hf =>
Iso.isIso_hom
{ hom := f
inv :=
Hom.mk
{ toFun := inv ((forget SimplexCategory).map f)
monotone' := fun y₁ y₂ h => by
by_cases h' : y₁ < y₂
· by_contra h''
apply not_le.mpr h'
convert f.toOrderHom.monotone (le_of_not_ge h'')
all_goals exact (congr_hom (Iso.inv_hom_id (asIso ((forget SimplexCategory).map f))) _).symm
· rw [eq_of_le_of_not_lt h h'] }
hom_inv_id := by
ext1
ext1
exact Iso.hom_inv_id (asIso ((forget _).map f))
inv_hom_id := by
ext1
ext1
exact Iso.inv_hom_id (asIso ((forget _).map f)) }⟩