English
A core identity expressing compatibility of μ and 𝒮 under braiding and associativity.
Русский
Является базовой идентичностью совместимости μ и 𝒮 подBraiding и ассоциатором.
LaTeX
$$$ μ_A \circ 𝒮_A = (𝒮_A \otimes 𝒮_A) \circ (β_{A,A})^{hom} \circ μ_A $$$
Lean4
theorem mul_antipode₁ (A : C) [HopfObj A] :
(Δ[A] ⊗ₘ Δ[A]) ≫
(α_ A A (A ⊗ A)).hom ≫
A ◁ (α_ A A A).inv ≫
A ◁ (β_ A A).hom ▷ A ≫
(α_ A (A ⊗ A) A).inv ≫
(α_ A A A).inv ▷ A ≫ μ[A] ▷ A ▷ A ≫ 𝒮[A] ▷ A ▷ A ≫ (α_ A A A).hom ≫ A ◁ μ[A] ≫ μ[A] =
(ε[A] ⊗ₘ ε[A]) ≫ (λ_ (𝟙_ C)).hom ≫ η[A] :=
by
slice_lhs 8 9 => rw [associator_naturality_left]
slice_lhs 9 10 => rw [← whisker_exchange]
slice_lhs 7 8 => rw [associator_naturality_left]
slice_lhs 8 9 => rw [← tensorHom_def]
simp
