instReflectsIsomorphismsForget — Mathlib

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)) }⟩

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