English
The right and left inclusions interact via the associator to give a balanced rearrangement of tensor factors.
Русский
Правое и левое включения взаимодействуют через ассоциатор, обеспечивая сбалансированное перераспределение тензорных факторов.
LaTeX
$$$\\forall x,y,z:\\; inr_{x,y} \\; ≫ inl_{y,z} \\; ≫ (\\alpha_{x,y,z})^{\\mathrm{hom}} = inl_{x,y} \\; ≫ inr_{y,z}.$$$
Lean4
@[reassoc (attr := simp)]
theorem inr_comp_inl_comp_associator (x y z : AugmentedSimplexCategory) :
inr _ _ ≫ inl _ _ ≫ (α_ x y z).hom = inl _ _ ≫ inr _ _ :=
match x, y, z with
| .of x, .of y, .of z =>
by
change inr' _ _ ≫ inl' _ _ ≫ WithInitial.down _ = inl' _ _ ≫ inr' _ _
ext i : 3
dsimp [MonoidalCategoryStruct.associator, associator]
have e₁ := inl'_eval y z i
have e₂ := inr'_eval x y i
have e₃ := inl'_eval (tensorObjOf x y) z <| Fin.cast (by simp +arith) <| i.natAdd (x.len + 1)
have e₄ := inr'_eval x (tensorObjOf y z) <| Fin.cast (by simp +arith) <| i.castAdd (z.len + 1)
simp only [SimplexCategory.len_mk] at e₁ e₂ e₃ e₄
rw [e₁, e₂, e₃, e₄]
ext; simp +arith
| .star, _, _ => by cat_disch
| _, .star, _ => by cat_disch
| _, _, .star => by cat_disch
