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 HopfAlgebraCat R ≌ Hopf_ (ModuleCat R).)

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} : ∀ {inst : CommSemiring R} {inst_1 : 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} : ∀ {inst : CommSemiring R} {inst_1 : 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)

@[simp]

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, HopfAlgebra.antipode (repr.left i) * repr.right i = (algebraMap R A) (Coalgebra.counit a)

@[simp]

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 * HopfAlgebra.antipode (repr.right i) = (algebraMap R A) (Coalgebra.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, HopfAlgebra.antipode (repr.left i) * repr.right i = Coalgebra.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 * HopfAlgebra.antipode (repr.right i) = Coalgebra.counit a • 1

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