Convolution groups of algebra homomorphisms out of a Hopf algebra

For an arbitrary Hopf algebra H over R and a commutative R-algebra A, the convolution monoid of R-algebra homomorphisms H →ₐ[R] A is a group, with inverse f ↦ f ∘ S, where S is the antipode of H. The source H need only be a Hopf algebra; it is not required to be commutative.

Mathlib already constructs the convolution Monoid on WithConv (H →ₐ[R] A) for H a bialgebra (Mathlib/RingTheory/Bialgebra/Convolution.lean): multiplication is the convolution product (f * g)(h) = ∑ f(h₍₁₎) * g(h₍₂₎) and the unit is algebraMap ∘ ε. What is added here is the inverse and hence the group structure, available exactly when H carries an antipode S: the inverse of f is f ∘ S.

The construction is functorial in the value algebra: post-composition with an R-algebra homomorphism φ : A →ₐ[R] B gives a monoid homomorphism mapValue φ between the convolution monoids, preserving identities and composition. This part needs only the bialgebra structure on H (the convolution monoid), so it lives in its own Bialgebra section.

Application: affine group schemes

When H is moreover commutative, Spec H is an affine group scheme, and the above is the group structure on its functor of points A ↦ (H →ₐ[R] A), with functoriality in A realizing the R-Alg ⥤ Grp structure, where the counit is the identity and f ∘ S is the inverse.

Main results

• AlgHom.convInv_apply: pointwise, the convolution inverse of f sends h to f (S h).
• AlgHom.instGroup, AlgHom.instCommGroup: for H a Hopf algebra over R and A a commutative R-algebra, WithConv (H →ₐ[R] A) is a group, commutative when H is cocommutative.
• AlgHom.mapValue: post-composition with φ : A →ₐ[R] B as a monoid homomorphism of convolution monoids, with AlgHom.mapValue_id, AlgHom.mapValue_comp recording its functoriality in the value algebra and AlgHom.mapValue_injective recording that it loses no information when φ does not.

References

The convolution monoid on algebra homomorphisms builds on Mathlib's convolution monoid of Yaël Dillies and Michał Mrugała, and the Hopf convolution algebra developed by Yaël Dillies, Michał Mrugała, and Yunzhou Xie.

noncomputable def TauCeti.AlgHom.antipodeComp {R : Type u_1} {H : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] (f : H →ₐ[R] A) : H →ₐ[R] A

Post-composition of an algebra homomorphism f : H →ₐ[R] A with the antipode S of H, as an R-algebra homomorphism H →ₐ[R] A. Its underlying linear map is f.toLinearMap ∘ₗ HopfAlgebra.antipode R. This is well-defined even when H is noncommutative: S is an antihomomorphism (HopfAlgebra.antipode_mul_antidistrib), and A is commutative, so f ∘ S is a homomorphism.

Equations

• TauCeti.AlgHom.antipodeComp f = AlgHom.ofLinearMap (f.toLinearMap ∘ₗ HopfAlgebraStruct.antipode R) ⋯ ⋯

@[simp]

theorem AlgHom.antipodeComp_apply {R : Type u_1} {H : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] (f : H →ₐ[R] A) (h : H) : (TauCeti.AlgHom.antipodeComp f) h = f ((HopfAlgebraStruct.antipode R) h)

Evaluation of antipodeComp f at an element h : H is f (S h).

@[simp]

theorem AlgHom.toLinearMap_antipodeComp {R : Type u_1} {H : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] (f : H →ₐ[R] A) : (TauCeti.AlgHom.antipodeComp f).toLinearMap = f.toLinearMap ∘ₗ HopfAlgebraStruct.antipode R

The underlying linear map of antipodeComp f is f.toLinearMap ∘ₗ antipode R.

@[instance_reducible]

noncomputable instance TauCeti.AlgHom.instInv {R : Type u_1} {H : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] : Inv (WithConv (H →ₐ[R] A))

The convolution inverse of an R-algebra homomorphism f : H →ₐ[R] A out of a Hopf algebra is f ∘ S, where S is the antipode.

Equations

• TauCeti.AlgHom.instInv = { inv := fun (f : WithConv (H →ₐ[R] A)) => WithConv.toConv (TauCeti.AlgHom.antipodeComp f.ofConv) }

theorem WithConv.convInv_def {R : Type u_1} {H : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] (f : WithConv (H →ₐ[R] A)) : f⁻¹ = toConv (TauCeti.AlgHom.antipodeComp f.ofConv)

The convolution inverse of f is f ∘ S, where S is the antipode: f⁻¹ = toConv (antipodeComp f.ofConv).

@[simp]

theorem TauCeti.AlgHom.convInv_apply {R : Type u_1} {H : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] (f : WithConv (H →ₐ[R] A)) (h : H) : f⁻¹.ofConv h = f.ofConv ((HopfAlgebraStruct.antipode R) h)

Pointwise, the convolution inverse of f sends h to f (S h), where S is the antipode.

@[instance_reducible]

noncomputable instance TauCeti.AlgHom.instGroup {R : Type u_1} {H : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] : Group (WithConv (H →ₐ[R] A))

For a Hopf algebra H over R and a commutative R-algebra A, the convolution monoid of R-algebra homomorphisms H →ₐ[R] A is a group, with inverse f ↦ f ∘ S. When H is moreover commutative, Spec H is an affine group scheme and this is the group structure on its functor of points evaluated at A.

Equations

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

noncomputable def TauCeti.AlgHom.mapValue {R : Type u_1} {H : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring H] [Bialgebra R H] [CommSemiring A] [Algebra R A] {B : Type u_4} [CommSemiring B] [Algebra R B] (φ : A →ₐ[R] B) : WithConv (H →ₐ[R] A) →* WithConv (H →ₐ[R] B)

Functoriality of A ↦ (H →ₐ[R] A) in the value algebra: an R-algebra homomorphism φ : A →ₐ[R] B induces, by post-composition, a monoid homomorphism between the convolution monoids. This needs only the bialgebra structure on H. When H is moreover a Hopf algebra, these convolution monoids are the convolution groups (instGroup); a MonoidHom between groups is automatically a group homomorphism, so no separate construction is needed there.

Equations

• TauCeti.AlgHom.mapValue φ = { toFun := fun (f : WithConv (H →ₐ[R] A)) => WithConv.toConv (φ.comp f.ofConv), map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.AlgHom.mapValue_apply {R : Type u_1} {H : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring H] [Bialgebra R H] [CommSemiring A] [Algebra R A] {B : Type u_4} [CommSemiring B] [Algebra R B] (φ : A →ₐ[R] B) (f : WithConv (H →ₐ[R] A)) : (mapValue φ) f = WithConv.toConv (φ.comp f.ofConv)

mapValue φ acts pointwise by post-composition: (mapValue φ f) = φ ∘ f.

@[simp]

theorem TauCeti.AlgHom.mapValue_id {R : Type u_1} {H : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring H] [Bialgebra R H] [CommSemiring A] [Algebra R A] : mapValue (AlgHom.id R A) = MonoidHom.id (WithConv (H →ₐ[R] A))

mapValue preserves the identity: mapValue (𝟙 A) is the identity monoid homomorphism.

theorem TauCeti.AlgHom.mapValue_injective {R : Type u_1} {H : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring H] [Bialgebra R H] [CommSemiring A] [Algebra R A] {B : Type u_4} [CommSemiring B] [Algebra R B] {φ : A →ₐ[R] B} (hφ : Function.Injective ⇑φ) : Function.Injective ⇑(mapValue φ)

An injective homomorphism of value algebras induces an injective map on points: a point is determined by its values.

theorem TauCeti.AlgHom.mapValue_comp {R : Type u_1} {H : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring H] [Bialgebra R H] [CommSemiring A] [Algebra R A] {B : Type u_4} [CommSemiring B] [Algebra R B] {C : Type u_5} [CommSemiring C] [Algebra R C] (ψ : B →ₐ[R] C) (φ : A →ₐ[R] B) : mapValue (ψ.comp φ) = (mapValue ψ).comp (mapValue φ)

mapValue preserves composition: mapValue (ψ ∘ φ) = mapValue ψ ∘ mapValue φ.

@[instance_reducible]

noncomputable instance TauCeti.AlgHom.instCommGroup {R : Type u_1} {H : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [Coalgebra.IsCocomm R H] [CommSemiring A] [Algebra R A] : CommGroup (WithConv (H →ₐ[R] A))

When H is moreover cocommutative, the convolution group of R-algebra homomorphisms H →ₐ[R] A is abelian.

Equations

• TauCeti.AlgHom.instCommGroup = { toGroup := TauCeti.AlgHom.instGroup, mul_comm := ⋯ }