instConcreteCategoryOrderHomFinHAddNatLenOfNat

English

The category SimplexCategory is given a concrete structure via Hom := OrderHom.toOrderHom, i.e., morphisms correspond to order-preserving maps between finite ordinals.

Русский

У SimplexCategory есть конкретная структура: гомоморфизмом является отображение порядка между Fin-объектами.

LaTeX

$$$\\text{ConcreteCategory}(SimplexCategory, f \\mapsto f.toOrderHom)$$$

Lean4

instance : ConcreteCategory SimplexCategory (fun i j => Fin (i.len + 1) →o Fin (j.len + 1))
    where
  hom := Hom.toOrderHom
  ofHom f := Hom.mk f

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