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.
• HopfAlgebra.ofConvInverse : construct a Hopf algebra from a two-sided convolution inverse of the identity.
• HopfAlgebra.ofAlgHom : the same for commutative A, with AlgHom hypotheses.

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)][Kassel1995]

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) : (algebraMap R A) r * x = x * (algebraMap R A) r
• smul_def' (r : R) (x : A) : r • x = (algebraMap R A) 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) : (algebraMap R A) r * x = x * (algebraMap R A) r
• smul_def' (r : R) (x : A) : r • x = (algebraMap R A) 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} {ι : Type u_1} [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} {ι : Type u_1} [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} {ι : Type u_1} [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} {ι : Type u_1} [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

@[reducible, inline]

noncomputable abbrev HopfAlgebra.ofConvInverse {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Bialgebra R A] (antipode : A →ₗ[R] A) (antipode_convMul_id : WithConv.toConv antipode * WithConv.toConv LinearMap.id = 1) (id_convMul_antipode : WithConv.toConv LinearMap.id * WithConv.toConv antipode = 1) : HopfAlgebra R A

Upgrade a bialgebra to a Hopf algebra by specifying a convolution inverse of the identity.

Equations

• HopfAlgebra.ofConvInverse antipode antipode_convMul_id id_convMul_antipode = { toBialgebra := inst✝, antipode := antipode, mul_antipode_rTensor_comul := ⋯, mul_antipode_lTensor_comul := ⋯ }

@[reducible, inline]

noncomputable abbrev HopfAlgebra.ofAlgHom {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Bialgebra R A] (antipode : A →ₐ[R] A) (mul_antipode_rTensor_comul : (Algebra.TensorProduct.lift antipode (AlgHom.id R A) ⋯).comp (Bialgebra.comulAlgHom R A) = (Algebra.ofId R A).comp (Bialgebra.counitAlgHom R A)) (mul_antipode_lTensor_comul : (Algebra.TensorProduct.lift (AlgHom.id R A) antipode ⋯).comp (Bialgebra.comulAlgHom R A) = (Algebra.ofId R A).comp (Bialgebra.counitAlgHom R A)) : HopfAlgebra R A

Upgrade a commutative bialgebra to a Hopf algebra by specifying the antipode A →ₐ[R] A with appropriate conditions.

Equations

• HopfAlgebra.ofAlgHom antipode mul_antipode_rTensor_comul mul_antipode_lTensor_comul = HopfAlgebra.ofConvInverse antipode.toLinearMap ⋯ ⋯