English
The associator interacts with inr in a standard way: the two ways of regrouping the tensor with inr agree via the associator.
Русский
Ассоциатор взаимодействует с inr обычным образом: два способа перестройки тензора с inr совпадают через ассоциатор.
LaTeX
$$$\\forall x,y,z:\\; inr_{x,y}\\; ≫ (\\alpha_{x,y,z})^{\\mathrm{hom}} = inr_{x,y} \\; ≫ inr_{y,z}.$$$
Lean4
@[reassoc (attr := simp)]
theorem inr_comp_associator (x y z : AugmentedSimplexCategory) : inr _ _ ≫ (α_ x y z).hom = inr _ _ ≫ inr _ _ :=
match x, y, z with
| .of x, .of y, .of z => by
change inr' _ _ ≫ WithInitial.down _ = inr' _ _ ≫ inr' _ _
ext i : 3
dsimp [MonoidalCategoryStruct.associator, associator]
simp only [eqToHom_toOrderHom, SimplexCategory.len_mk, OrderEmbedding.toOrderHom_coe, OrderIso.coe_toOrderEmbedding,
Fin.castOrderIso_apply]
have e₁ := inr'_eval (tensorObjOf x y) z i
have e₂ := inr'_eval y z i
have e₃ := inr'_eval x (tensorObjOf y z) <| Fin.cast (by simp +arith) <| i.natAdd (y.len + 1)
simp only [SimplexCategory.len_mk] at e₁ e₂ e₃
rw [e₁, e₂, e₃]
ext; simp +arith
| .star, _, _ => by cat_disch
| _, .star, _ => by cat_disch
| _, _, .star => by cat_disch
