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.

References

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

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

class HopfAlgebra (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] extends Bialgebra : 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
• toFun : R → A
• map_one' : (↑↑Algebra.toRingHom).toFun 1 = 1
• map_mul' : ∀ (x y : R), (↑↑Algebra.toRingHom).toFun (x * y) = (↑↑Algebra.toRingHom).toFun x * (↑↑Algebra.toRingHom).toFun y
• map_zero' : (↑↑Algebra.toRingHom).toFun 0 = 0
• map_add' : ∀ (x y : R), (↑↑Algebra.toRingHom).toFun (x + y) = (↑↑Algebra.toRingHom).toFun x + (↑↑Algebra.toRingHom).toFun y
• commutes' : ∀ (r : R) (x : A), Algebra.toRingHom r * x = x * Algebra.toRingHom r
• smul_def' : ∀ (r : R) (x : A), r • x = Algebra.toRingHom r * x
• comul : A →ₗ[R] TensorProduct R A A
• counit : A →ₗ[R] R
• coassoc : ↑(TensorProduct.assoc R A A A) ∘ₗ LinearMap.rTensor A Coalgebra.comul ∘ₗ Coalgebra.comul = LinearMap.lTensor A Coalgebra.comul ∘ₗ Coalgebra.comul
• rTensor_counit_comp_comul : LinearMap.rTensor A Coalgebra.counit ∘ₗ Coalgebra.comul = (TensorProduct.mk R R A) 1
• lTensor_counit_comp_comul : LinearMap.lTensor A Coalgebra.counit ∘ₗ Coalgebra.comul = (TensorProduct.mk R A R).flip 1
• counit_one : Coalgebra.counit 1 = 1
• mul_compr₂_counit : (LinearMap.mul R A).compr₂ Coalgebra.counit = (LinearMap.mul R R).compl₁₂ Coalgebra.counit Coalgebra.counit
• comul_one : Coalgebra.comul 1 = 1
• mul_compr₂_comul : (LinearMap.mul R A).compr₂ Coalgebra.comul = (LinearMap.mul R (TensorProduct R A A)).compl₁₂ Coalgebra.comul Coalgebra.comul
• antipode : A →ₗ[R] A

  The antipode of the Hopf algebra.

• mul_antipode_rTensor_comul : LinearMap.mul' R A ∘ₗ LinearMap.rTensor A HopfAlgebra.antipode ∘ₗ Coalgebra.comul = Algebra.linearMap R A ∘ₗ Coalgebra.counit

  One of the antipode axioms for a Hopf algebra.

• mul_antipode_lTensor_comul : LinearMap.mul' R A ∘ₗ LinearMap.lTensor A HopfAlgebra.antipode ∘ₗ Coalgebra.comul = Algebra.linearMap R A ∘ₗ Coalgebra.counit

  One of the antipode axioms for a Hopf algebra.

theorem HopfAlgebra.mul_antipode_rTensor_comul {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [self : HopfAlgebra R A] : LinearMap.mul' R A ∘ₗ LinearMap.rTensor A HopfAlgebra.antipode ∘ₗ Coalgebra.comul = Algebra.linearMap R A ∘ₗ Coalgebra.counit

One of the antipode axioms for a Hopf algebra.

theorem HopfAlgebra.mul_antipode_lTensor_comul {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [self : HopfAlgebra R A] : LinearMap.mul' R A ∘ₗ LinearMap.lTensor A HopfAlgebra.antipode ∘ₗ Coalgebra.comul = Algebra.linearMap R A ∘ₗ Coalgebra.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 HopfAlgebra.antipode) (Coalgebra.comul a)) = (algebraMap R A) (Coalgebra.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 HopfAlgebra.antipode) (Coalgebra.comul a)) = (algebraMap R A) (Coalgebra.counit a)

noncomputable 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 = HopfAlgebra.mk LinearMap.id ⋯ ⋯

@[simp]

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