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 exactly the group structure on its functor of points A ↦ (H →ₐ[R] A), with functoriality in A realizing the R-Alg ⥤ Grp structure. This is the first concrete target of the Tau Ceti reductive-groups roadmap (Layer 0, "R-points as a group"), which records that the group structure on the functor of points is by convolution, with the counit as identity and f ∘ S as 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.

References

This realizes the "R-points as a group via convolution" milestone of the Tau Ceti reductive-groups roadmap (Layer 0). The convolution monoid it builds on is the work of Yaël Dillies, Michał Mrugała and Yunzhou Xie in Mathlib.

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

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

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