English
In a braided Hopf setting, if a certain braiding condition holds, the antipode squares to the identity.
Русский
В braided Hopf системе, при выполнении условия braiding, антиподака квадрат равен единице.
LaTeX
$$$ 𝒮_A^2 = id_A \quad\text{under suitable braiding condition} $$$
Lean4
/-- In a commutative Hopf algebra, the antipode squares to the identity.
-/
theorem antipode_antipode (A : C) [HopfObj A] (comm : (β_ _ _).hom ≫ μ[A] = μ[A]) : 𝒮[A] ≫ 𝒮[A] = 𝟙 A := by
-- Again, it is a "left inverse equals right inverse" argument in the convolution monoid.
apply left_inv_eq_right_inv (M := Conv A A) (a := 𝒮[A])
· -- Unfold the algebra structure in the convolution monoid,
-- then `simp?`.
rw [Conv.mul_eq, Conv.one_eq]
simp only [comp_whiskerRight, Category.assoc]
rw [← comm, ← tensorHom_def_assoc, ← mul_antipode]
simp
· rw [Conv.mul_eq, Conv.one_eq]
simp
