eqToHom_toOrderHom — Mathlib

English

If x = y in the simplex category, then the order-hom induced by the equality is exactly the corresponding cast of the equality on the length, i.e., the order-hom is the same as the natural embedding coming from len+1.

Русский

Пусть x = y в симплексной категории. Тогда отображение порядка, полученное из равенства, совпадает с соответствующим вложением по длине len+1.

LaTeX

$$$\mathrm{Hom}.toOrderHom (\mathrm{eqToHom}\, h) = (\mathrm{Fin.castOrderIso} (\mathrm{congrArg} (\lambda t \; t.len + 1) h)).toOrderEmbedding.toOrderHom$$$

Lean4

@[simp]
theorem eqToHom_toOrderHom {x y : SimplexCategory} (h : x = y) :
    SimplexCategory.Hom.toOrderHom (eqToHom h) =
      (Fin.castOrderIso (congrArg (fun t ↦ t.len + 1) h)).toOrderEmbedding.toOrderHom :=
  by
  subst h
  rfl

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