The diagonalizable group of a product #
This file records the functor-of-points consequence of
TauCeti.MonoidAlgebra.prodTensorBialgEquiv: for commutative monoids G and H, points of
Spec R[G × H] split as pairs of points of Spec R[G] and Spec R[H]. For commutative groups,
this specializes to the diagonalizable group statement
D(G × H)(A) ≃* D(G)(A) × D(H)(A).
On points this composes with TauCeti.AffineGroup.Product.pointsMulEquiv, the tensor-product
points calculation, through the equiv-version AlgHom.mapDomainMulEquiv of the contravariant
functoriality AlgHom.mapDomain. When G and H are commutative groups the group algebras
are Hopf algebras and these convolution monoids are the convolution groups of points
(TauCeti.AlgHom.instGroup), so the points equivalence is automatically an isomorphism of
groups: D(G × H)(A) ≅ D(G)(A) × D(H)(A).
This advances the reductive-groups roadmap (ReductiveGroups/README.md in TauCetiRoadmap,
Layer 4 "Diagonalizable groups" and the "Worked examples / products" theme, together with the
Layer 0 functor-of-points dictionary): this supplies the binary product step used in the
calculation of split tori as iterated products of 𝔾ₘ.
Main definitions #
TauCeti.MonoidAlgebra.prodPointsMulEquiv: on convolution points,Spec R[G × H](A) ≃* Spec R[G](A) × Spec R[H](A).TauCeti.DiagonalizableGroup.prodPointsMulEquiv: for commutative groups, on points,D(G × H)(A) ≃* D(G)(A) × D(H)(A).
References #
The tensor-product points calculation TauCeti.AffineGroup.Product.pointsMulEquiv, the generic
monoid-algebra bialgebra product TauCeti.MonoidAlgebra.prodTensorBialgEquiv, and the
contravariant functoriality TauCeti.AlgHom.mapDomain are Tau Ceti's existing
functor-of-points infrastructure, built on Mathlib's tensor-product and monoid-algebra
bialgebra structures and the Mathlib convolution monoid of Yaël Dillies, Michał Mrugała and
Yunzhou Xie.
The monoid algebra of a product gives the product functor on convolution points.
For commutative monoids G and H and every commutative R-algebra A, the convolution
monoid of A-points of Spec R[G × H] is the product of the convolution monoids of
A-points of Spec R[G] and Spec R[H].
Equations
Instances For
The first component of prodPointsMulEquiv restricts an A-point of Spec R[G × H] to
the factor Spec R[G]: on the generator single g 1 it evaluates the original point at
single (g, 1) 1, the image of g under G → G × H.
The second component of prodPointsMulEquiv restricts an A-point of Spec R[G × H] to
the factor Spec R[H]: on the generator single h 1 it evaluates the original point at
single (1, h) 1, the image of h under H → G × H.
The inverse of prodPointsMulEquiv assembles an A-point of Spec R[G × H] from a pair of
points of Spec R[G] and Spec R[H]: on the generator single (g, h) 1 it multiplies the
value of the first point at single g 1 and the value of the second at single h 1.
The product-points equivalence is natural in the value algebra.
The diagonalizable group of a product is the product of diagonalizable groups, on points.
For commutative groups G and H and every commutative R-algebra A, the convolution group
of A-points of D(G × H) is the product of the convolution groups of A-points of D(G) and
D(H).
Instances For
On generators, the first component of the diagonalizable product-points equivalence restricts
along g ↦ (g, 1).
On generators, the second component of the diagonalizable product-points equivalence restricts
along h ↦ (1, h).
On generators, the inverse diagonalizable product-points equivalence multiplies the two factor-point values.
The diagonalizable product-points equivalence is natural in the value algebra.
The diagonalizable product-points equivalence agrees with the existing character description of diagonalizable-group points: reading the character of a product point is the coproduct of the characters read from its two restrictions.