Convolution product on Hopf algebra maps #

This file constructs the ring structure on bialgebra homs C → A where C and A are Hopf algebras and multiplication is given by

         |
         μ
|   |   / \
f * g = f g
|   |   \ /
         δ
         |

diagrammatically, where μ stands for multiplication and δ for comultiplication.

It also provides:

HopfAlgebra.ofAntipodeOfAdjoin, which upgrades a bialgebra A to a Hopf algebra given an algebra hom S : A →ₐ[R] Aᵐᵒᵖ satisfying the antipode identities on a generating set. HopfAlgebra.ofSurjective, which transfers the Hopf algebra axioms along a surjective bialgebra homomorphism intertwining the antipodes.

source

theorem HopfAlgebra.antipode_comp_mul_comp_comm {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [HopfAlgebra R A] :

antipode R ∘ₗ LinearMap.mul' R A ∘ₗ ↑(TensorProduct.comm R A A) = LinearMap.mul' R A ∘ₗ TensorProduct.map (antipode R) (antipode R)

source

theorem HopfAlgebra.antipode_mul_antidistrib {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [HopfAlgebra R A] (a b : A) :

(antipode R) (a * b) = (antipode R) b * (antipode R) a

source

@[deprecated HopfAlgebra.antipode_mul_antidistrib (since := "2026-06-05")]

theorem HopfAlgebra.antipode_mul {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [HopfAlgebra R A] (a b : A) :

(antipode R) (a * b) = (antipode R) b * (antipode R) a

Alias of HopfAlgebra.antipode_mul_antidistrib.

source

noncomputable def HopfAlgebra.antipodeAlgHomOp (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [HopfAlgebra R A] :

A →ₐ[R] Aᵐᵒᵖ

The antipode of a commutative Hopf algebra as an anti-algebra hom.

Equations

HopfAlgebra.antipodeAlgHomOp R A = AlgHom.ofLinearMap (↑(MulOpposite.opLinearEquiv R) ∘ₗ HopfAlgebraStruct.antipode R) ⋯ ⋯

Instances For

source

@[simp]

theorem HopfAlgebra.antipodeAlgHomOp_apply (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [HopfAlgebra R A] (a : A) :

(antipodeAlgHomOp R A) a = MulOpposite.op ((antipode R) a)

source

theorem HopfAlgebra.antipode_mul_distrib {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] (a b : A) :

(antipode R) (a * b) = (antipode R) a * (antipode R) b

source

noncomputable def HopfAlgebra.antipodeAlgHom (R : Type u_1) (A : Type u_2) [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] :

A →ₐ[R] A

The antipode of a commutative Hopf algebra as an algebra hom.

Equations

HopfAlgebra.antipodeAlgHom R A = AlgHom.ofLinearMap (HopfAlgebraStruct.antipode R) ⋯ ⋯

Instances For

source

@[simp]

theorem HopfAlgebra.antipodeAlgHom_apply (R : Type u_1) (A : Type u_2) [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] (a : A) :

(antipodeAlgHom R A) a = (antipode R) a

source

@[simp]

theorem HopfAlgebra.toLinearMap_antipodeAlgHom {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] :

(antipodeAlgHom R A).toLinearMap = antipode R

source

@[simp]

theorem LinearMap.antipode_mul_id {R : Type u_1} {C : Type u_3} [CommSemiring R] [Semiring C] [HopfAlgebra R C] :

WithConv.toConv (HopfAlgebraStruct.antipode R) * WithConv.toConv id = 1

source

@[simp]

theorem LinearMap.id_mul_antipode {R : Type u_1} {C : Type u_3} [CommSemiring R] [Semiring C] [HopfAlgebra R C] :

WithConv.toConv id * WithConv.toConv (HopfAlgebraStruct.antipode R) = 1

source

theorem HopfAlgebra.eq_antipode_of_convMul_id_eq_one {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [HopfAlgebra R A] {f : A →ₗ[R] A} (h : WithConv.toConv f * WithConv.toConv LinearMap.id = 1) :

f = antipode R

The antipode is the unique left convolution inverse of the identity: any R-linear map f with f * id = 1 in the convolution monoid equals the antipode.

source

theorem HopfAlgebra.eq_antipode_of_id_convMul_eq_one {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [HopfAlgebra R A] {f : A →ₗ[R] A} (h : WithConv.toConv LinearMap.id * WithConv.toConv f = 1) :

f = antipode R

The antipode is the unique right convolution inverse of the identity: any R-linear map f with id * f = 1 in the convolution monoid equals the antipode.

source

@[reducible, inline]

noncomputable abbrev HopfAlgebra.ofSurjective {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [HopfAlgebra R A] {B : Type u_4} [Semiring B] [HopfAlgebraStruct R B] (f : A →ₐc[R] B) (hf : Function.Surjective ⇑f) (map_antipode : ∀ (a : A), f ((antipode R) a) = (antipode R) (f a)) :

HopfAlgebra R B

Transfer the Hopf algebra axioms along a surjective bialgebra homomorphism intertwining the antipodes.

Equations

HopfAlgebra.ofSurjective f hf map_antipode = HopfAlgebra.ofConvInverse (HopfAlgebraStruct.antipode R) ⋯ ⋯

Instances For

source

theorem LinearMap.comul_right_inv {R : Type u_1} {C : Type u_3} [CommSemiring R] [Semiring C] [HopfAlgebra R C] :

WithConv.toConv CoalgebraStruct.comul * WithConv.toConv (CoalgebraStruct.comul ∘ₗ HopfAlgebraStruct.antipode R) = 1

source

@[instance_reducible]

noncomputable instance AlgHom.convInv {R : Type u_1} {A : Type u_2} {C : Type u_3} [CommSemiring R] [CommSemiring A] [CommSemiring C] [Bialgebra R C] [HopfAlgebra R A] :

Inv (WithConv (A →ₐ[R] C))

Equations

AlgHom.convInv = { inv := fun (f : WithConv (A →ₐ[R] C)) => WithConv.toConv (f.ofConv.comp (HopfAlgebra.antipodeAlgHom R A)) }

source

@[instance_reducible]

noncomputable instance AlgHom.convGroup {R : Type u_1} {A : Type u_2} {C : Type u_3} [CommSemiring R] [CommSemiring A] [CommSemiring C] [Bialgebra R C] [HopfAlgebra R A] :

Group (WithConv (A →ₐ[R] C))

Equations

One or more equations did not get rendered due to their size.

source

@[instance_reducible]

noncomputable instance AlgHom.instCommGroupWithConvOfIsCocomm {R : Type u_1} {A : Type u_2} {C : Type u_3} [CommSemiring R] [CommSemiring A] [CommSemiring C] [Bialgebra R C] [HopfAlgebra R A] [Coalgebra.IsCocomm R A] :

CommGroup (WithConv (A →ₐ[R] C))

Equations

AlgHom.instCommGroupWithConvOfIsCocomm = { toGroup := AlgHom.convGroup, mul_comm := ⋯ }

source

theorem AlgHom.antipode_id_cancel {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] :

WithConv.toConv (HopfAlgebra.antipodeAlgHom R A) * WithConv.toConv (AlgHom.id R A) = 1

source

theorem AlgHom.id_antipode_cancel {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] :

WithConv.toConv (AlgHom.id R A) * WithConv.toConv (HopfAlgebra.antipodeAlgHom R A) = 1

source

theorem AlgHom.counitAlgHom_comp_antipodeAlgHom {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] :

(Bialgebra.counitAlgHom R A).comp (HopfAlgebra.antipodeAlgHom R A) = Bialgebra.counitAlgHom R A

source

theorem HopfAlgebra.convMul_id_eq_one_of_adjoin_eq_top {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Bialgebra R A] {X : Set A} (S : A →ₐ[R] Aᵐᵒᵖ) (hX : Algebra.adjoin R X = ⊤) (h : ∀ x ∈ X, (LinearMap.mul' R A) ((LinearMap.rTensor A (↑(MulOpposite.opLinearEquiv R).symm ∘ₗ S.toLinearMap)) (CoalgebraStruct.comul x)) = (Algebra.linearMap R A) (CoalgebraStruct.counit x)) :

WithConv.toConv (↑(MulOpposite.opLinearEquiv R).symm ∘ₗ S.toLinearMap) * WithConv.toConv LinearMap.id = 1

source

theorem HopfAlgebra.id_convMul_eq_one_of_adjoin_eq_top {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Bialgebra R A] {X : Set A} (S : A →ₐ[R] Aᵐᵒᵖ) (hX : Algebra.adjoin R X = ⊤) (h : ∀ x ∈ X, (LinearMap.mul' R A) ((LinearMap.lTensor A (↑(MulOpposite.opLinearEquiv R).symm ∘ₗ S.toLinearMap)) (CoalgebraStruct.comul x)) = (Algebra.linearMap R A) (CoalgebraStruct.counit x)) :

WithConv.toConv LinearMap.id * WithConv.toConv (↑(MulOpposite.opLinearEquiv R).symm ∘ₗ S.toLinearMap) = 1

source

@[reducible, inline]

noncomputable abbrev HopfAlgebra.ofAntipodeOfAdjoin {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Bialgebra R A] {X : Set A} (S : A →ₐ[R] Aᵐᵒᵖ) (hX : Algebra.adjoin R X = ⊤) (hxr : ∀ x ∈ X, (LinearMap.mul' R A) ((LinearMap.rTensor A (↑(MulOpposite.opLinearEquiv R).symm ∘ₗ S.toLinearMap)) (CoalgebraStruct.comul x)) = (Algebra.linearMap R A) (CoalgebraStruct.counit x)) (hxl : ∀ x ∈ X, (LinearMap.mul' R A) ((LinearMap.lTensor A (↑(MulOpposite.opLinearEquiv R).symm ∘ₗ S.toLinearMap)) (CoalgebraStruct.comul x)) = (Algebra.linearMap R A) (CoalgebraStruct.counit x)) :

HopfAlgebra R A

If A is generated as an R-algebra by X, and S : A →ₐ[R] Aᵐᵒᵖ satisfies the two antipode identities on X, then the underlying linear map gives a Hopf algebra structure on A.

Equations

HopfAlgebra.ofAntipodeOfAdjoin S hX hxr hxl = HopfAlgebra.ofConvInverse (↑(MulOpposite.opLinearEquiv R).symm ∘ₗ S.toLinearMap) ⋯ ⋯

Instances For

Documentation

Mathlib.RingTheory.HopfAlgebra.Convolution

Convolution product on Hopf algebra maps #