The diagonalizable group and its character functor of points

For a commutative group G, the group algebra R[G] is a commutative Hopf algebra in which every group element g is group-like (Δ(single g 1) = single g 1 ⊗ single g 1, ε(single g 1) = 1, antipode single g 1 ↦ single g⁻¹ 1). The associated affine group scheme Spec R[G] is the diagonalizable group D(G) of the reductive-groups roadmap.

This file records the functor-of-points calculation for D(G): for every commutative R-algebra A, the convolution group of R-algebra homomorphisms R[G] →ₐ[R] A is the character group G →* Aˣ, with convolution corresponding to the pointwise product of characters. A point f is sent to the character g ↦ f (single g 1) (a unit of A with inverse f (single g⁻¹ 1)), and a character χ is sent to the algebra map extending it via MonoidAlgebra.lift.

Specializing to G = Multiplicative ℤ recovers the multiplicative group 𝔾ₘ on the group-algebra presentation R[Multiplicative ℤ]: the character read from a point is its value on the generator, and this agrees with the canonical Laurent-polynomial 𝔾ₘ of TauCeti.MultiplicativeGroup after precomposition by AddMonoidAlgebra.toMultiplicativeAlgEquiv.

This is a worked-example check for the reductive-groups roadmap (Layer 4, "diagonalizable groups and groups of multiplicative type: the anti-equivalence M ↦ D(M) = Spec k[M]", and the Layer 0 target "R-points as a group"), in the same spirit as the existing multiplicative group 𝔾ₘ.

Main definitions

• TauCeti.DiagonalizableGroup.point: the R[G]-point extending a character of G.
• TauCeti.DiagonalizableGroup.charOfPoint: the character of G read off from a point.
• TauCeti.DiagonalizableGroup.pointEquiv: algebra maps R[G] →ₐ[R] A are equivalent to characters G →* Aˣ.
• TauCeti.DiagonalizableGroup.pointsMulEquiv: the same equivalence as a multiplicative equivalence from the convolution group of points to the character group.
• TauCeti.DiagonalizableGroup.multiplicativeGroup_pointEquiv_apply: the bridge from the G = Multiplicative ℤ specialization to the canonical Laurent-polynomial 𝔾ₘ API of TauCeti.MultiplicativeGroup.

References

The Hopf algebra structure on a group algebra is Mathlib's Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra (with the bialgebra structure of Amelia Livingston's monoid-algebra formalization), and MonoidAlgebra.lift is its universal property. The convolution group of points and its antipode-driven inverse are Tau Ceti's TauCeti.Algebra.AlgebraicGroup.FunctorOfPoints, built on the Mathlib convolution monoid of Yaël Dillies, Michał Mrugała and Yunzhou Xie. This realizes the diagonalizable-group worked example of the Tau Ceti reductive-groups roadmap (Layer 4 and Layer 0).

noncomputable def TauCeti.DiagonalizableGroup.point {R : Type u} {A : Type v} {G : Type w} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommGroup G] (χ : G →* Aˣ) : MonoidAlgebra R G →ₐ[R] A

The R[G]-point of the diagonalizable group D(G) corresponding to a character of G. It is the algebra map extending χ via the universal property of the group algebra; it sends single g r to r • χ g.

Equations

• TauCeti.DiagonalizableGroup.point χ = (MonoidAlgebra.lift R A G) ((Units.coeHom A).comp χ)

@[simp]

theorem TauCeti.DiagonalizableGroup.point_single {R : Type u} {A : Type v} {G : Type w} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommGroup G] (χ : G →* Aˣ) (g : G) (r : R) : (point χ) (MonoidAlgebra.single g r) = r • ↑(χ g)

The point associated to a character sends single g r to r • χ g.

theorem TauCeti.DiagonalizableGroup.point_single_one {R : Type u} {A : Type v} {G : Type w} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommGroup G] (χ : G →* Aˣ) (g : G) : (point χ) (MonoidAlgebra.single g 1) = ↑(χ g)

The point associated to a character sends the group-like single g 1 to χ g.

noncomputable def TauCeti.DiagonalizableGroup.charOfPoint {R : Type u} {A : Type v} {G : Type w} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommGroup G] (f : MonoidAlgebra R G →ₐ[R] A) : G →* Aˣ

The character of G read off from an R[G]-point: it sends g to the unit f (single g 1) of A, whose inverse is f (single g⁻¹ 1). It is the monoid hom (MonoidAlgebra.lift R A G).symm f : G →* A made unit-valued through MonoidHom.toHomUnits, using that G is a group.

Equations

• TauCeti.DiagonalizableGroup.charOfPoint f = ((MonoidAlgebra.lift R A G).symm f).toHomUnits

@[simp]

theorem TauCeti.DiagonalizableGroup.charOfPoint_apply_coe {R : Type u} {A : Type v} {G : Type w} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommGroup G] (f : MonoidAlgebra R G →ₐ[R] A) (g : G) : ↑((charOfPoint f) g) = f (MonoidAlgebra.single g 1)

The character read off from a point sends g to the value of the point on single g 1.

@[simp]

theorem TauCeti.DiagonalizableGroup.charOfPoint_apply_inv_coe {R : Type u} {A : Type v} {G : Type w} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommGroup G] (f : MonoidAlgebra R G →ₐ[R] A) (g : G) : ↑((charOfPoint f) g)⁻¹ = f (MonoidAlgebra.single g⁻¹ 1)

The inverse of the unit charOfPoint f g is the value of the point on single g⁻¹ 1.

@[simp]

theorem TauCeti.DiagonalizableGroup.charOfPoint_point {R : Type u} {A : Type v} {G : Type w} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommGroup G] (χ : G →* Aˣ) : charOfPoint (point χ) = χ

Reading off the character of the point of χ recovers χ.

@[simp]

theorem TauCeti.DiagonalizableGroup.point_charOfPoint {R : Type u} {A : Type v} {G : Type w} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommGroup G] (f : MonoidAlgebra R G →ₐ[R] A) : point (charOfPoint f) = f

The point of the character read off from f recovers f.

noncomputable def TauCeti.DiagonalizableGroup.pointEquiv {R : Type u} {A : Type v} {G : Type w} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommGroup G] : (MonoidAlgebra R G →ₐ[R] A) ≃ (G →* Aˣ)

Algebra maps out of R[G] are the same as characters G →* Aˣ of G.

Equations

• TauCeti.DiagonalizableGroup.pointEquiv = (MonoidAlgebra.lift R A G).symm.trans MonoidHom.toHomUnitsMulEquiv.toEquiv

@[simp]

theorem TauCeti.DiagonalizableGroup.pointEquiv_apply {R : Type u} {A : Type v} {G : Type w} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommGroup G] (f : MonoidAlgebra R G →ₐ[R] A) : pointEquiv f = charOfPoint f

The equivalence sends a point to the character read off from it.

@[simp]

theorem TauCeti.DiagonalizableGroup.pointEquiv_symm_apply {R : Type u} {A : Type v} {G : Type w} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommGroup G] (χ : G →* Aˣ) : pointEquiv.symm χ = point χ

The inverse equivalence sends a character to the point extending it.

@[simp]

theorem TauCeti.DiagonalizableGroup.charOfPoint_convMul {R : Type u} {A : Type v} {G : Type w} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommGroup G] (f g : WithConv (MonoidAlgebra R G →ₐ[R] A)) : charOfPoint (f * g).ofConv = charOfPoint f.ofConv * charOfPoint g.ofConv

Reading off characters turns the convolution product of points into the pointwise product of characters.

theorem TauCeti.DiagonalizableGroup.charOfPoint_mapValue {R : Type u} {A : Type v} {G : Type w} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommGroup G] {B : Type u_1} [CommSemiring B] [Algebra R B] (φ : A →ₐ[R] B) (f : WithConv (MonoidAlgebra R G →ₐ[R] A)) : charOfPoint ((AlgHom.mapValue φ) f).ofConv = (Units.map ↑φ.toRingHom).comp (charOfPoint f.ofConv)

Reading off characters is natural in the value algebra: post-composing a point with an R-algebra map sends the associated character through the induced map on units.

noncomputable def TauCeti.DiagonalizableGroup.pointsMulEquiv {R : Type u} {A : Type v} {G : Type w} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommGroup G] : WithConv (MonoidAlgebra R G →ₐ[R] A) ≃* (G →* Aˣ)

The functor of points of the diagonalizable group D(G) is the character group G →* Aˣ.

The source is the convolution group of R-algebra maps out of R[G]; the target is the group of characters of G valued in the units of A, under pointwise multiplication.

Equations

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

@[simp]

theorem TauCeti.DiagonalizableGroup.pointsMulEquiv_apply {R : Type u} {A : Type v} {G : Type w} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommGroup G] (f : WithConv (MonoidAlgebra R G →ₐ[R] A)) : pointsMulEquiv f = charOfPoint f.ofConv

The multiplicative equivalence sends a convolution point to the character read off from it.

theorem TauCeti.DiagonalizableGroup.pointsMulEquiv_mapValue {R : Type u} {A : Type v} {G : Type w} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommGroup G] {B : Type u_1} [CommSemiring B] [Algebra R B] (φ : A →ₐ[R] B) (f : WithConv (MonoidAlgebra R G →ₐ[R] A)) : pointsMulEquiv ((AlgHom.mapValue φ) f) = (Units.map ↑φ.toRingHom).comp (pointsMulEquiv f)

The multiplicative point equivalence is natural in the value algebra.

@[simp]

theorem TauCeti.DiagonalizableGroup.pointsMulEquiv_symm_apply {R : Type u} {A : Type v} {G : Type w} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommGroup G] (χ : G →* Aˣ) : pointsMulEquiv.symm χ = WithConv.toConv (point χ)

The inverse multiplicative equivalence sends a character to the point extending it.

The multiplicative group 𝔾ₘ as D(Multiplicative ℤ)

Specializing to G = Multiplicative ℤ recovers the multiplicative group on the group-algebra presentation R[Multiplicative ℤ]. The canonical 𝔾ₘ points API remains TauCeti.MultiplicativeGroup.pointEquiv for Laurent polynomials; the theorem below records how the group-algebra presentation compares to it through AddMonoidAlgebra.toMultiplicativeAlgEquiv.

theorem TauCeti.DiagonalizableGroup.multiplicativeGroup_pointEquiv_apply {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] (f : MonoidAlgebra R (Multiplicative ℤ) →ₐ[R] A) : (charOfPoint f) (Multiplicative.ofAdd 1) = MultiplicativeGroup.pointEquiv (f.comp ↑(AddMonoidAlgebra.toMultiplicativeAlgEquiv R R ℤ))

The group-algebra presentation of D(Multiplicative ℤ) agrees with the Laurent-polynomial multiplicative group 𝔾ₘ of TauCeti.MultiplicativeGroup: reading a point on the generator single (ofAdd 1) 1 gives the same unit as first precomposing it with AddMonoidAlgebra.toMultiplicativeAlgEquiv and then using the canonical TauCeti.MultiplicativeGroup.pointEquiv.