Hopf algebras

In this file we define HopfAlgebra, and provide instances for:

• Commutative semirings: CommSemiring.toHopfAlgebra

Main definitions

• HopfAlgebra R A : the Hopf algebra structure on an R-bialgebra A.
• HopfAlgebra.antipode : the R-linear map A →ₗ[R] A.

Main results

• HopfAlgebra.antipode_one : the antipode of the unit is the unit.
• HopfAlgebra.antipode_mul : the antipode is an antihomomorphism: S(ab) = S(b)S(a).

TODO

• Uniqueness of Hopf algebra structure on a bialgebra (i.e. if the algebra and coalgebra structures agree then the antipodes must also agree).

• If A is commutative then antipode is an algebra homomorphism.

• If A is commutative then antipode is necessarily a bijection and its square is the identity.

(Note that all three facts have been proved for Hopf bimonoids in an arbitrary braided category, so we could deduce the facts here from an equivalence HopfAlgCat R ≌ Hopf (ModuleCat R).)

References

• https://en.wikipedia.org/wiki/Hopf_algebra

• C. Kassel, Quantum Groups (§III.3)

class HopfAlgebraStruct (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] extends Bialgebra R A : Type (max u v)

Isolates the antipode of a Hopf algebra, to allow API to be constructed before proving the Hopf algebra axioms. See HopfAlgebra for documentation.

• smul : R → A → A
• algebraMap : R →+* A
• commutes' (r : R) (x : A) : Algebra.algebraMap r * x = x * Algebra.algebraMap r
• smul_def' (r : R) (x : A) : r • x = Algebra.algebraMap r * x
• comul : A →ₗ[R] TensorProduct R A A
• counit : A →ₗ[R] R
• coassoc : ↑(_root_.TensorProduct.assoc R A A A) ∘ₗ LinearMap.rTensor A comul ∘ₗ comul = LinearMap.lTensor A comul ∘ₗ comul
• rTensor_counit_comp_comul : LinearMap.rTensor A counit ∘ₗ comul = (TensorProduct.mk R R A) 1
• lTensor_counit_comp_comul : LinearMap.lTensor A counit ∘ₗ comul = (TensorProduct.mk R A R).flip 1
• counit_one : CoalgebraStruct.counit 1 = 1
• mul_compr₂_counit : (LinearMap.mul R A).compr₂ CoalgebraStruct.counit = (LinearMap.mul R R).compl₁₂ CoalgebraStruct.counit CoalgebraStruct.counit
• comul_one : CoalgebraStruct.comul 1 = 1
• mul_compr₂_comul : (LinearMap.mul R A).compr₂ CoalgebraStruct.comul = (LinearMap.mul R (TensorProduct R A A)).compl₁₂ CoalgebraStruct.comul CoalgebraStruct.comul
• antipode : A →ₗ[R] A

  The antipode of the Hopf algebra.

class HopfAlgebra (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] extends HopfAlgebraStruct R A : Type (max u v)

A Hopf algebra over a commutative (semi)ring R is a bialgebra over R equipped with an R-linear endomorphism antipode satisfying the antipode axioms.

• smul : R → A → A
• algebraMap : R →+* A
• commutes' (r : R) (x : A) : Algebra.algebraMap r * x = x * Algebra.algebraMap r
• smul_def' (r : R) (x : A) : r • x = Algebra.algebraMap r * x
• comul : A →ₗ[R] TensorProduct R A A
• counit : A →ₗ[R] R
• coassoc : ↑(_root_.TensorProduct.assoc R A A A) ∘ₗ LinearMap.rTensor A comul ∘ₗ comul = LinearMap.lTensor A comul ∘ₗ comul
• rTensor_counit_comp_comul : LinearMap.rTensor A counit ∘ₗ comul = (TensorProduct.mk R R A) 1
• lTensor_counit_comp_comul : LinearMap.lTensor A counit ∘ₗ comul = (TensorProduct.mk R A R).flip 1
• counit_one : CoalgebraStruct.counit 1 = 1
• mul_compr₂_counit : (LinearMap.mul R A).compr₂ CoalgebraStruct.counit = (LinearMap.mul R R).compl₁₂ CoalgebraStruct.counit CoalgebraStruct.counit
• comul_one : CoalgebraStruct.comul 1 = 1
• mul_compr₂_comul : (LinearMap.mul R A).compr₂ CoalgebraStruct.comul = (LinearMap.mul R (TensorProduct R A A)).compl₁₂ CoalgebraStruct.comul CoalgebraStruct.comul
• antipode : A →ₗ[R] A
• mul_antipode_rTensor_comul : LinearMap.mul' R A ∘ₗ LinearMap.rTensor A (antipode R) ∘ₗ CoalgebraStruct.comul = Algebra.linearMap R A ∘ₗ CoalgebraStruct.counit

  One of the antipode axioms for a Hopf algebra.

• mul_antipode_lTensor_comul : LinearMap.mul' R A ∘ₗ LinearMap.lTensor A (antipode R) ∘ₗ CoalgebraStruct.comul = Algebra.linearMap R A ∘ₗ CoalgebraStruct.counit

  One of the antipode axioms for a Hopf algebra.

@[simp]

theorem HopfAlgebra.mul_antipode_rTensor_comul_apply {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [HopfAlgebra R A] (a : A) : (LinearMap.mul' R A) ((LinearMap.rTensor A (antipode R)) (CoalgebraStruct.comul a)) = (algebraMap R A) (CoalgebraStruct.counit a)

@[simp]

theorem HopfAlgebra.mul_antipode_lTensor_comul_apply {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [HopfAlgebra R A] (a : A) : (LinearMap.mul' R A) ((LinearMap.lTensor A (antipode R)) (CoalgebraStruct.comul a)) = (algebraMap R A) (CoalgebraStruct.counit a)

@[simp]

theorem HopfAlgebra.antipode_one {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [HopfAlgebra R A] : (antipode R) 1 = 1

theorem HopfAlgebra.sum_antipode_mul_eq_algebraMap_counit {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [HopfAlgebra R A] {a : A} (repr : Coalgebra.Repr R a) : ∑ i ∈ repr.index, (antipode R) (repr.left i) * repr.right i = (algebraMap R A) (CoalgebraStruct.counit a)

theorem HopfAlgebra.sum_mul_antipode_eq_algebraMap_counit {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [HopfAlgebra R A] {a : A} (repr : Coalgebra.Repr R a) : ∑ i ∈ repr.index, repr.left i * (antipode R) (repr.right i) = (algebraMap R A) (CoalgebraStruct.counit a)

theorem HopfAlgebra.sum_antipode_mul_eq_smul {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [HopfAlgebra R A] {a : A} (repr : Coalgebra.Repr R a) : ∑ i ∈ repr.index, (antipode R) (repr.left i) * repr.right i = CoalgebraStruct.counit a • 1

theorem HopfAlgebra.sum_mul_antipode_eq_smul {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [HopfAlgebra R A] {a : A} (repr : Coalgebra.Repr R a) : ∑ i ∈ repr.index, repr.left i * (antipode R) (repr.right i) = CoalgebraStruct.counit a • 1

@[simp]

theorem HopfAlgebra.counit_antipode {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [HopfAlgebra R A] (a : A) : CoalgebraStruct.counit ((antipode R) a) = CoalgebraStruct.counit a

@[simp]

theorem HopfAlgebra.counit_comp_antipode {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [HopfAlgebra R A] : CoalgebraStruct.counit ∘ₗ antipode R = CoalgebraStruct.counit

The antipode is an antihomomorphism

We prove that antipode (a * b) = antipode b * antipode a. The proof uses the "left inverse equals right inverse" trick in the convolution algebra (A ⊗ A) →ₗ[R] A.

theorem HopfAlgebra.antipode_mul {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [HopfAlgebra R A] (a b : A) : (antipode R) (a * b) = (antipode R) b * (antipode R) a

The antipode reverses multiplication: S(ab) = S(b)S(a).

@[implicit_reducible]

instance CommSemiring.toHopfAlgebra (R : Type u) [CommSemiring R] : HopfAlgebra R R

Every commutative (semi)ring is a Hopf algebra over itself

Equations

• CommSemiring.toHopfAlgebra R = { toBialgebra := CommSemiring.toBialgebra R, antipode := LinearMap.id, mul_antipode_rTensor_comul := ⋯, mul_antipode_lTensor_comul := ⋯ }

@[simp]

theorem CommSemiring.antipode_eq_id (R : Type u) [CommSemiring R] : HopfAlgebraStruct.antipode R = LinearMap.id