isoNerve — Mathlib

English

Components of the nerve isomorphism are compatible with face/edge identifications.

Русский

Компоненты нерва-изоморфизма совместимы с идентификациями граней/ребер.

LaTeX

$$isoNerve_hom_app_apply {n d} (s) (i) : ((isoNerve n).hom.app _ s).obj i = ULift.up (s i)$$

Lean4

/-- The standard simplex identifies to the nerve to the preordered type
`ULift (Fin (n + 1))`. -/
@[pp_with_univ]
def isoNerve (n : ℕ) : (Δ[n] : SSet.{u}) ≅ nerve (ULift.{u} (Fin (n + 1))) :=
  NatIso.ofComponents
    (fun d ↦
      Equiv.toIso
        (objEquiv.trans
          { toFun f := (ULift.orderIso.symm.monotone.comp f.toOrderHom.monotone).functor
            invFun f := SimplexCategory.Hom.mk (ULift.orderIso.toOrderEmbedding.toOrderHom.comp f.toOrderHom)
            left_inv _ := by aesop }))

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