English
Auxiliary calculation for antipode_comul with ASCII-art intuition; expresses a complex interaction identity.
Русский
Вспомогательное вычисление antipode_comul₂ с символическим рисунком; выражает сложную идентичность взаимодействия.
LaTeX
$$$ Δ_A ≫ Δ_A \triangleright A ≫ (α_{A A A})^{hom} ≫ A ◁ A ◁ Δ_A ≫ A ◁ A ◁ (β_{A A})^{hom} ≫ A ◁ A ◁ (𝒮_A ⊗ 𝒮_A) ≫ A ◁ (α_{A A A})^{inv} ≫ A ◁ (β_{A A})^{hom} ▷ A ≫ A ◁ (α_{A A A})^{hom} ≫ (α_{A A (A⊗A)})^{inv} ≫ (μ_A ⊗ μ_A) = ε_A ≫ λ_{I}^{-1} ≫ (η_A ⊗ η_A) $$$
Lean4
theorem antipode_comul₁ (A : C) [HopfObj A] :
Δ[A] ≫
𝒮[A] ▷ A ≫
Δ[A] ▷ A ≫
(α_ A A A).hom ≫
A ◁ A ◁ Δ[A] ≫
A ◁ (α_ A A A).inv ≫ A ◁ (β_ A A).hom ▷ A ≫ A ◁ (α_ A A A).hom ≫ (α_ A A (A ⊗ A)).inv ≫ (μ[A] ⊗ₘ μ[A]) =
ε[A] ≫ (λ_ (𝟙_ C)).inv ≫ (η[A] ⊗ₘ η[A]) :=
by
slice_lhs 3 5 => rw [← associator_naturality_right, ← Category.assoc, ← tensorHom_def]
slice_lhs 3 9 => rw [Bimon.compatibility]
slice_lhs 1 3 => rw [antipode_left]
simp [MonObj.tensorObj.one_def]
