The antipode of a Hopf star algebra

A Hopf star algebra is a Hopf algebra A over a commutative star ring R with a compatible star algebra structure (StarRing A, StarModule R A) whose comultiplication is a star map (TauCeti.StarCoalgebra R A). In such an algebra the antipode is always bijective, with inverse a ↦ S(a*)*:

S(S(a*)*) = a and S(S(a)*)* = a.

The first identity says that S ∘ T is the identity for T(a) = S(a*)*. Writing Δ a = ∑ xᵢ ⊗ yᵢ, the star of the antipode law ∑ xᵢ* S(yᵢ*) = ε(a*) together with ε(a*) = conj (ε a) gives ∑ T(yᵢ) xᵢ = ε(a). Applying the antimultiplicative S shows that S ∘ T is a right convolution inverse of S, and id is a left convolution inverse of S, so S ∘ T = id. The second identity is the first one conjugated by star.

No positivity is involved: these are the purely algebraic consequences of the axioms, used before any Haar state or completion is constructed.

Main declarations

• TauCeti.HopfAlgebra.antipode_star_antipode_star: S(S(a*)*) = a.
• TauCeti.HopfAlgebra.star_antipode_star_antipode: S(S(a)*)* = a.
• TauCeti.HopfAlgebra.antipode_bijective: the antipode of a Hopf star algebra is bijective.
• TauCeti.HopfAlgebra.antipodeAlgEquivOp: the antipode as an algebra isomorphism A ≃ Aᵐᵒᵖ, whose inverse is a ↦ S(a*)* (TauCeti.HopfAlgebra.antipodeAlgEquivOp_symm_apply).

References

• A. Klimyk and K. Schmüdgen, Quantum Groups and Their Representations, Springer, 1997, Section 1.2.7.

@[simp]

theorem TauCeti.HopfAlgebra.antipode_star_antipode_star {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [HopfAlgebra R A] [StarModule R A] [StarCoalgebra R A] (a : A) : (HopfAlgebraStruct.antipode R) (star ((HopfAlgebraStruct.antipode R) (star a))) = a

In a Hopf star algebra, S(S(a*)*) = a.

@[simp]

theorem TauCeti.HopfAlgebra.star_antipode_star_antipode {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [HopfAlgebra R A] [StarModule R A] [StarCoalgebra R A] (a : A) : star ((HopfAlgebraStruct.antipode R) (star ((HopfAlgebraStruct.antipode R) a))) = a

In a Hopf star algebra, S(S(a)*)* = a.

theorem TauCeti.HopfAlgebra.antipode_bijective {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [HopfAlgebra R A] [StarModule R A] [StarCoalgebra R A] : Function.Bijective ⇑(HopfAlgebraStruct.antipode R)

The antipode of a Hopf star algebra is bijective.

noncomputable def TauCeti.HopfAlgebra.antipodeAlgEquivOp (R : Type u_1) (A : Type u_2) [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [HopfAlgebra R A] [StarModule R A] [StarCoalgebra R A] : A ≃ₐ[R] Aᵐᵒᵖ

The antipode of a Hopf star algebra as an algebra isomorphism onto the opposite algebra. Its inverse is a ↦ S(a*)*.

@[simp]

theorem TauCeti.HopfAlgebra.antipodeAlgEquivOp_toAlgHom {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [HopfAlgebra R A] [StarModule R A] [StarCoalgebra R A] : ↑(antipodeAlgEquivOp R A) = HopfAlgebra.antipodeAlgHomOp R A

@[simp]

theorem TauCeti.HopfAlgebra.antipodeAlgEquivOp_apply {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [HopfAlgebra R A] [StarModule R A] [StarCoalgebra R A] (a : A) : (antipodeAlgEquivOp R A) a = MulOpposite.op ((HopfAlgebraStruct.antipode R) a)

@[simp]

theorem TauCeti.HopfAlgebra.antipodeAlgEquivOp_symm_apply {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [HopfAlgebra R A] [StarModule R A] [StarCoalgebra R A] (a : Aᵐᵒᵖ) : (antipodeAlgEquivOp R A).symm a = star ((HopfAlgebraStruct.antipode R) (star (MulOpposite.unop a)))

The inverse of the antipode of a Hopf star algebra is a ↦ S(a*)*.