The multiplicative group example #
This file records the functor-of-points calculation for the multiplicative group. Mathlib
already equips the Laurent polynomial algebra R[T;T⁻¹] with its Hopf algebra structure,
where T n is group-like and the antipode sends T n to T (-n). We package the resulting
R-points of Spec R[T;T⁻¹]: for every commutative R-algebra A, convolution points
R[T;T⁻¹] →ₐ[R] A are multiplicatively equivalent to units of A.
This is a worked-example check for the reductive-groups roadmap Layer 0 target "R-points as a
group" and the listed example 𝔾_m.
Main declarations #
TauCeti.MultiplicativeGroup.point: the point corresponding to a unit ofA.TauCeti.MultiplicativeGroup.pointEquiv: algebra maps fromR[T;T⁻¹]toAare equivalent to units ofA.TauCeti.MultiplicativeGroup.pointsMulEquiv: the same equivalence as a multiplicative equivalence from the convolution group toAˣ.TauCeti.MultiplicativeGroup.pointsMulEquiv_mapValue: the points equivalence is natural in the value algebra.TauCeti.MultiplicativeGroup.genericUnit: the tautological unitTof a Laurent polynomial ring.
References #
The Hopf algebra structure and Laurent polynomial evaluation API are from Mathlib's
Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra and Mathlib.Algebra.Polynomial.Laurent,
building on Amelia Livingston's monoid-algebra Hopf algebra formalization.
The R[T;T⁻¹]-point of the multiplicative group corresponding to a unit of the value
algebra. It sends T n to u ^ n.
Equations
- TauCeti.MultiplicativeGroup.point u = { toRingHom := LaurentPolynomial.eval₂ (algebraMap R A) u, commutes' := ⋯ }
Instances For
The point associated to a unit sends T n to u ^ n.
The point associated to a unit sends constants through the algebra map.
The unit of A obtained by evaluating an R[T;T⁻¹]-point at T.
Equations
- TauCeti.MultiplicativeGroup.unitOfPoint f = { val := f (LaurentPolynomial.T 1), inv := f (LaurentPolynomial.T (-1)), val_inv := ⋯, inv_val := ⋯ }
Instances For
Evaluating unitOfPoint f as an element of A gives the value of f on T.
The inverse of unitOfPoint f is the value of f on T⁻¹.
The point-to-unit construction inverts point.
The unit-to-point construction inverts unitOfPoint.
Algebra maps out of R[T;T⁻¹] are the same as units of the value algebra.
Equations
- TauCeti.MultiplicativeGroup.pointEquiv = { toFun := TauCeti.MultiplicativeGroup.unitOfPoint, invFun := TauCeti.MultiplicativeGroup.point, left_inv := ⋯, right_inv := ⋯ }
Instances For
The equivalence sends a point to its value on T.
The inverse equivalence sends a unit to the corresponding evaluation map.
The functor of points of the multiplicative group is the unit group of the value algebra.
The source is the convolution group of R-algebra maps out of R[T;T⁻¹]; the target is the
ordinary unit group of A.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The multiplicative equivalence sends a convolution point to its value on T.
The inverse multiplicative equivalence sends a unit to the corresponding point.
Reading a Laurent-polynomial point as a unit is natural under post-composition of algebra maps.
The plain Laurent-polynomial points equivalence is natural in the value algebra.
Naturality of the inverse plain points equivalence in the value algebra.
Reading a multiplicative-group point as a unit is natural in the value algebra:
post-composing the point with an R-algebra map applies the induced map on unit groups.
The 𝔾ₘ points equivalence is natural in the value algebra.
Naturality of the inverse 𝔾ₘ points equivalence in the value algebra.
The Laurent variable T, as a unit of A[T;T⁻¹]. It is the tautological
A[T;T⁻¹]-point of the multiplicative group.
Instances For
The generic unit is the Laurent variable T.
The inverse of the generic unit is the inverse Laurent variable.
An integer power of the generic unit is the corresponding Laurent monomial.
Mapping the generic unit along a Laurent-polynomial point gives the unit represented by that point.