English
In a symmetric braided monoidal category, the multiplication μ commutes with braiding: μ ≫ β = (β ⊗ β) ≫ μ.
Русский
В симметричной braided моноидальной категории умножение μ commuting с braiding: μ ≫ β = (β ⊗ β) ≫ μ.
LaTeX
$$$μ \\; \\; ≫ \\; (β_{X,Y}).hom = ((β_{X,Y}).hom ⊗ (β_{X,Y}).hom) ≫ μ$$$
Lean4
theorem mul_braiding (X Y : C) [MonObj X] [MonObj Y] : μ ≫ (β_ X Y).hom = ((β_ X Y).hom ⊗ₘ (β_ X Y).hom) ≫ μ :=
by
dsimp [tensorObj.mul_def]
simp only [tensorμ, Category.assoc, BraidedCategory.braiding_naturality, BraidedCategory.braiding_tensor_right_hom,
BraidedCategory.braiding_tensor_left_hom, comp_whiskerRight, whisker_assoc, whiskerLeft_comp, pentagon_assoc,
pentagon_inv_hom_hom_hom_inv_assoc, Iso.inv_hom_id_assoc, whiskerLeft_hom_inv_assoc]
slice_lhs 3 4 =>
-- We use symmetry here:
rw [← whiskerLeft_comp, ← comp_whiskerRight, SymmetricCategory.symmetry]
simp only [id_whiskerRight, whiskerLeft_id, Category.id_comp, Category.assoc, pentagon_inv_assoc,
Iso.hom_inv_id_assoc]
slice_lhs 1 2 => rw [← associator_inv_naturality_left]
slice_lhs 2 3 => rw [Iso.inv_hom_id]
rw [Category.id_comp]
slice_lhs 2 3 => rw [← associator_naturality_right]
slice_lhs 1 2 => rw [← tensorHom_def]
simp only [Category.assoc]
