English
Coherence of composing tensor-structure maps with associator; the diagram relating tensorμ, μ, and α commutes in a braided monoidal setting.
Русский
Согласованность композиции тензорных структур и ассоциатора; диаграмма, соединяющая tensorμ, μ и α, коммутирует в braided моноидальном контексте.
LaTeX
$$$$ (tensorμ (M \otimes N) P (M \otimes N) P \; \rhd) \; $$$$
Lean4
theorem mul_associator {M N P : C} [MonObj M] [MonObj N] [MonObj P] :
(tensorμ (M ⊗ N) P (M ⊗ N) P ≫ (tensorμ M N M N ≫ (μ ⊗ₘ μ) ⊗ₘ μ)) ≫ (α_ M N P).hom =
((α_ M N P).hom ⊗ₘ (α_ M N P).hom) ≫ tensorμ M (N ⊗ P) M (N ⊗ P) ≫ (μ ⊗ₘ tensorμ N P N P ≫ (μ ⊗ₘ μ)) :=
by
simp only [Category.assoc]
slice_lhs 2 3 => rw [← Category.id_comp μ[P], ← tensorHom_comp_tensorHom]
slice_lhs 3 4 => rw [associator_naturality]
slice_rhs 3 4 => rw [← Category.id_comp μ, ← tensorHom_comp_tensorHom]
simp only [tensorHom_id, id_tensorHom]
slice_lhs 1 3 => rw [associator_monoidal]
simp only [Category.assoc]
