instBalanced — Mathlib

English

The category of simplicial sets is balanced: a morphism that is both mono and epi is an isomorphism.

Русский

Категория симплициальных множеств сбалансирована: морфизм, являющийся и моно, и эпим, является изоморфизмом.

LaTeX

$$$$ \text{SSet is Balanced} $$$$

Lean4

instance : Balanced SSet.{u} where
  isIso_of_mono_of_epi f _
    _ := by
    rw [NatTrans.isIso_iff_isIso_app]
    intro
    rw [isIso_iff_bijective]
    constructor
    · rw [← mono_iff_injective]
      infer_instance
    · rw [← epi_iff_surjective]
      infer_instance

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