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.

TODO

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

• antipode 1 = 1 and antipode (a * b) = antipode b * antipode a, so in particular 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 : ↑(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 : ↑(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)

@[deprecated HopfAlgebra.sum_antipode_mul_eq_algebraMap_counit (since := "2025-05-29")]

theorem HopfAlgebra.sum_antipode_mul_eq {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)

Alias of HopfAlgebra.sum_antipode_mul_eq_algebraMap_counit.

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)

@[deprecated HopfAlgebra.sum_mul_antipode_eq_algebraMap_counit (since := "2025-05-29")]

theorem HopfAlgebra.sum_mul_antipode_eq {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)

Alias of HopfAlgebra.sum_mul_antipode_eq_algebraMap_counit.

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

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