The square and the inverse of the antipode of U_q(sl₂)

For a nonzero parameter q, the antipode S of UqSl2 q need not be involutive. Its square is the inner automorphism given by conjugation with the group-like element K⁻¹:

S² x = K⁻¹ x K, so that S² E = q⁻² E, S² F = q² F and S² K = K.

Since conjugation by a unit is bijective, so is S. Being antimultiplicative, S is therefore an algebra isomorphism from UqSl2 q onto its opposite algebra, whose inverse is

S⁻¹ x = K S(x) K⁻¹, so that S⁻¹ E = -E K⁻¹, S⁻¹ F = -K F and S⁻¹ K = K⁻¹.

Bijectivity of the antipode is what makes the left duals of finite-dimensional modules, built with S⁻¹, available alongside the right duals built with S.

Main results

• TauCeti.UqSl2.antipode_antipode: S (S x) = K⁻¹ x K.
• TauCeti.UqSl2.antipode_bijective: the antipode is bijective.
• TauCeti.UqSl2.antipodeEquiv: the antipode as an algebra isomorphism onto the opposite algebra.
• TauCeti.UqSl2.antipodeEquiv_symm_apply: its inverse is x ↦ K S(x) K⁻¹.

References

• A. Virelizier, Quantum groups, Section 2.3, for this rank-one Hopf convention.
• C. Kassel, Quantum Groups, Graduate Texts in Mathematics 155, Section VII.1, for the Hopf structure on U_q(sl₂) in the opposite coproduct convention.

theorem TauCeti.UqSl2.antipode_antipode (q : ℂ) [Fact (q ≠ 0)] (x : UqSl2 q) : (HopfAlgebraStruct.antipode ℂ) ((HopfAlgebraStruct.antipode ℂ) x) = kInv q * x * k q

The square of the antipode is conjugation by K⁻¹.

theorem TauCeti.UqSl2.antipode_antipode_e (q : ℂ) [Fact (q ≠ 0)] : (HopfAlgebraStruct.antipode ℂ) ((HopfAlgebraStruct.antipode ℂ) (e q)) = q⁻¹ ^ 2 • e q

The square of the antipode rescales the raising generator by q⁻².

theorem TauCeti.UqSl2.antipode_antipode_f (q : ℂ) [Fact (q ≠ 0)] : (HopfAlgebraStruct.antipode ℂ) ((HopfAlgebraStruct.antipode ℂ) (f q)) = q ^ 2 • f q

The square of the antipode rescales the lowering generator by q².

theorem TauCeti.UqSl2.antipode_bijective (q : ℂ) [Fact (q ≠ 0)] : Function.Bijective ⇑(HopfAlgebraStruct.antipode ℂ)

The antipode of UqSl2 q is bijective.

noncomputable def TauCeti.UqSl2.antipodeEquiv (q : ℂ) [Fact (q ≠ 0)] : UqSl2 q ≃ₐ[ℂ] (UqSl2 q)ᵐᵒᵖ

The antipode of UqSl2 q, as an algebra isomorphism onto the opposite algebra.

@[simp]

theorem TauCeti.UqSl2.antipodeEquiv_toAlgHom (q : ℂ) [Fact (q ≠ 0)] : ↑(antipodeEquiv q) = antipodeOp q

The algebra homomorphism underlying antipodeEquiv is antipodeOp.

@[simp]

theorem TauCeti.UqSl2.antipodeEquiv_apply (q : ℂ) [Fact (q ≠ 0)] (x : UqSl2 q) : (antipodeEquiv q) x = MulOpposite.op ((HopfAlgebraStruct.antipode ℂ) x)

The isomorphism antipodeEquiv acts by the antipode.

theorem TauCeti.UqSl2.antipodeEquiv_symm_apply (q : ℂ) [Fact (q ≠ 0)] (x : (UqSl2 q)ᵐᵒᵖ) : (antipodeEquiv q).symm x = k q * (HopfAlgebraStruct.antipode ℂ) (MulOpposite.unop x) * kInv q

The inverse of the antipode is x ↦ K S(x) K⁻¹.

@[simp]

theorem TauCeti.UqSl2.antipodeEquiv_symm_op_e (q : ℂ) [Fact (q ≠ 0)] : (antipodeEquiv q).symm (MulOpposite.op (e q)) = -(e q * kInv q)

The inverse of the antipode sends E to -E K⁻¹.

@[simp]

theorem TauCeti.UqSl2.antipodeEquiv_symm_op_f (q : ℂ) [Fact (q ≠ 0)] : (antipodeEquiv q).symm (MulOpposite.op (f q)) = -(k q * f q)

The inverse of the antipode sends F to -K F.

@[simp]

theorem TauCeti.UqSl2.antipodeEquiv_symm_op_k (q : ℂ) [Fact (q ≠ 0)] : (antipodeEquiv q).symm (MulOpposite.op (k q)) = kInv q

The inverse of the antipode sends K to K⁻¹.

@[simp]

theorem TauCeti.UqSl2.antipodeEquiv_symm_op_kInv (q : ℂ) [Fact (q ≠ 0)] : (antipodeEquiv q).symm (MulOpposite.op (kInv q)) = k q

The inverse of the antipode sends K⁻¹ to K.