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.ofSurjective, which transfers the Hopf algebra axioms along a surjective bialgebra homomorphism intertwining the antipodes.

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)

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

@[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.

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) ⋯ ⋯

@[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)

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

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) ⋯ ⋯

@[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

@[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

@[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

@[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

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.

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.

@[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) ⋯ ⋯

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

@[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)) }

@[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.

@[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 := ⋯ }

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

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