English
In a braided category, the multiplication followed by the unit morphism relates to the braiding: μ ∘ ι equals the braiding with ι’s and μ.
Русский
В связной категории композиция умножения и единичного морфизма связана с перекрещиванием: μ ∘ ι равняется перекрещиванию с единицами и μ.
LaTeX
$$$\mu \circ \iota = (\beta_{A,A})^{\mathrm{hom}} \circ (\iota \otimes \iota) \circ \mu$$$
Lean4
@[reassoc]
theorem mul_inv [BraidedCategory C] (A : C) [GrpObj A] : μ ≫ ι = (β_ A A).hom ≫ (ι ⊗ₘ ι) ≫ μ :=
by
apply lift_left_mul_ext μ
nth_rw 2 [← Category.comp_id μ]
rw [← comp_lift, Category.assoc, left_inv, ← Category.assoc (β_ A A).hom, ← lift_snd_fst, lift_map, lift_lift_assoc]
nth_rw 2 [← Category.id_comp μ]
rw [← lift_fst_snd, ← lift_lift_assoc (fst A A ≫ _), lift_comp_inv_left, lift_comp_one_left, lift_comp_inv_left,
comp_toUnit_assoc]
