English
If the augmented initial images of two objects x,y in SimplexCategory agree, then the corresponding order-homomorphism obtained from their associated Down map is equal to the order-embedding obtained from a Fin-cast of a 1-shift, reflecting the shift in the augmented setting.
Русский
Если сопоставления WithInitial.of x и WithInitial.of y в SimplexCategory совпадают, то соответствующее отображение порядка, полученное из сопоставления Down, равно отображению порядка, приведённому к через Fin_cast после сдвига на единицу, отражая сдвиг в дополненном контексте.
LaTeX
$$$\\forall x,y:\\text{SimplexCategory},\\ h:\\mathrm{WithInitial.of}\,x=\\mathrm{WithInitial.of}\,y,\\\\\n\\mathrm{SimplexCategory.Hom.toOrderHom}(\\mathrm{WithInitial.down}(\\mathrm{eqToHom}\,h)) \;=\; (\\mathrm{Fin.castOrderIso}(\\mathrm{congrArg}(\\lambda t. t+1)(\\text{by injection } h))).\\mathrm{toOrderEmbedding}.\\mathrm{toOrderHom}.$$$
Lean4
@[simp]
theorem eqToHom_toOrderHom {x y : SimplexCategory} (h : WithInitial.of x = WithInitial.of y) :
SimplexCategory.Hom.toOrderHom (WithInitial.down <| eqToHom h) =
(Fin.castOrderIso (congrArg (fun t ↦ t + 1) (by injection h with h; rw [h]))).toOrderEmbedding.toOrderHom :=
SimplexCategory.eqToHom_toOrderHom (by injection h)
