The direct product of affine group schemes on points #
For two commutative bialgebras H₁ and H₂ over R, the tensor product H₁ ⊗[R] H₂ is the
coordinate bialgebra of the direct product of the affine group schemes Spec H₁ and
Spec H₂. This file proves that this is reflected on the functor of points: for every
commutative R-algebra A, the convolution monoid of R-algebra homomorphisms
(H₁ ⊗[R] H₂) →ₐ[R] A is multiplicatively equivalent to the product of the convolution
monoids H₁ →ₐ[R] A and H₂ →ₐ[R] A (pointsMulEquiv). When H₁ and H₂ are Hopf
algebras these convolution monoids are the convolution groups of points, so this is
automatically an isomorphism of groups: the points of the product group scheme are the
product of the points.
The equivalence sends a point f : (H₁ ⊗[R] H₂) →ₐ[R] A to its two restrictions
f ∘ (· ⊗ₜ 1) and f ∘ (1 ⊗ₜ ·); its inverse is Mathlib's tensor-product product map,
Algebra.TensorProduct.productMap f₁ f₂ : x ⊗ₜ y ↦ f₁ x * f₂ y. Both restrictions are
instances of pre-composition with the bialgebra morphisms from
TauCeti.Algebra.Bialgebra.TensorProduct, so the restriction map is a monoid homomorphism by
TauCeti.AlgHom.mapDomain; Mathlib's product map is its inverse by the universal property.
Main definitions #
TauCeti.Bialgebra.TensorProduct.includeLeftandTauCeti.Bialgebra.TensorProduct.includeRight: the inclusionsx ↦ x ⊗ₜ 1andy ↦ 1 ⊗ₜ ypackaged as bialgebra morphisms.TauCeti.AffineGroup.Product.pointsMulEquiv: the convolution monoid isomorphism between(H₁ ⊗[R] H₂) →ₐ[R] Aand the product(H₁ →ₐ[R] A) × (H₂ →ₐ[R] A). WhenH₁andH₂are Hopf algebras these are convolution groups, so this is automatically a group isomorphism.TauCeti.AffineGroup.Product.mapDomain_projectLeftandmapDomain_projectRight: precomposition with a tensor-product projection inserts a point into the corresponding product factor.TauCeti.AffineGroup.Product.pointsMulEquiv_mapValue: the product-points equivalence is natural in the value algebra.
References #
This realizes the "products of affine group schemes" computation on the functor of points, in
the spirit of the worked examples of the Tau Ceti ReductiveGroups roadmap
(ReductiveGroups/README.md in TauCetiRoadmap, Layer 0 "R-points as a group" and the three
synchronized models). The tensor-product bialgebra structure and its unit and identity
isomorphisms are from Mathlib's Mathlib.RingTheory.Bialgebra.TensorProduct; the universal
property Algebra.TensorProduct.lift is from Mathlib's
Mathlib.RingTheory.TensorProduct.Maps. The convolution monoid and its contravariant
functoriality TauCeti.AlgHom.mapDomain are Tau Ceti's existing functor-of-points
infrastructure, built on the Mathlib convolution monoid of Yaël Dillies, Michał Mrugała and
Yunzhou Xie.
Post-composition distributes over the tensor-product map induced by a pair of algebra maps.
A point of Spec (H₁ ⊗[R] H₂) is recovered from its two restrictions by Mathlib's
Algebra.TensorProduct.productMap.
Restriction of a point of Spec (H₁ ⊗[R] H₂) to its two factors, as a monoid homomorphism
of convolution monoids: it pre-composes with the two inclusions includeLeft and
includeRight. Each component is TauCeti.AlgHom.mapDomain of a bialgebra morphism, hence a
monoid homomorphism, so their pairing is too.
Equations
Instances For
The convolution monoid of R-algebra homomorphisms out of a tensor product of commutative
bialgebras H₁ ⊗[R] H₂ is the product of the convolution monoids out of H₁ and H₂.
On the functor of points this is the direct product of the affine group schemes Spec H₁ and
Spec H₂: Mathlib's product map sends x ⊗ₜ y to f₁ x * f₂ y, and convolution is computed
componentwise. When H₁ and H₂ are Hopf algebras these convolution monoids are groups
(TauCeti.AlgHom.instGroup), so this is automatically an isomorphism of groups.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Precomposition with the left tensor-product projection inserts a point as the left factor of the product, with the identity in the right factor.
Precomposition with the right tensor-product projection inserts a point as the right factor of the product, with the identity in the left factor.
Restricting a product point to the two factors commutes with post-composition in the value
algebra. This is the naturality square for the restriction homomorphism underlying
pointsMulEquiv.
The product-points equivalence is natural in the value algebra.
Post-composing an A-valued point of Spec (H₁ ⊗[R] H₂) by φ : A →ₐ[R] B, then splitting
it into its two factor points, gives the same pair as first splitting and then post-composing
each factor point by φ.
First-component form of pointsMulEquiv_mapValue.
Second-component form of pointsMulEquiv_mapValue.
The inverse product-points map is natural in the value algebra.
Assembling an A-valued product point from a pair of factor points and then post-composing by
φ : A →ₐ[R] B is the same as post-composing both factor points by φ and then assembling the
resulting B-valued product point.
On pure tensors, naturality of the inverse product-points map says that post-composition
by φ evaluates as applying φ to the product of the two factor values.
On pure tensors, assembling after post-composing both factor points multiplies the two post-composed factor values.