isoOfRepresentableBy — Mathlib

English

If X is representable by ⦋m⦌, there is an isomorphism Δ[m] ≅ X.

Русский

Если X представимо ⦋m⦌, существует изоморфизм Δ[m] ≅ X.

LaTeX

$$isoOfRepresentableBy {X} {m} (h : X.RepresentableBy ⦋m⦌) : Δ[m] ≅ X$$

Lean4

/-- If a simplicial set `X` is representable by `⦋m⦌` for some `m : ℕ`, then this is the
corresponding isomorphism `Δ[m] ≅ X`. -/
def isoOfRepresentableBy {X : SSet.{u}} {m : ℕ} (h : X.RepresentableBy ⦋m⦌) : Δ[m] ≅ X :=
  NatIso.ofComponents (fun n ↦ Equiv.toIso (objEquiv.trans h.homEquiv))
    (by
      intros
      ext
      apply h.homEquiv_comp)

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