skeletal — Mathlib

English

SimplexCategory is skeletal: every object is isomorphic to a unique representative in its skeleton via skeletalFunctor.

Русский

SimplexCategory является скелетальным: каждый объект изоморфен и представлен уникально в своем скелете через skeletalFunctor.

LaTeX

$$$\\text{Skeletal SimplexCategory}$$$

Lean4

theorem skeletal : Skeletal SimplexCategory := fun X Y ⟨I⟩ =>
  by
  suffices Fintype.card (Fin (X.len + 1)) = Fintype.card (Fin (Y.len + 1))
    by
    ext
    simpa
  apply Fintype.card_congr
  exact ((skeletalFunctor ⋙ forget NonemptyFinLinOrd).mapIso I).toEquiv

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