The coordinate algebra of Weierstrass changes of variables #
Over an arbitrary commutative coefficient ring B, the ring ChangeRing B = B[u, u⁻¹, r, s, t]
is the coordinate ring of Spec B × G for the group scheme G of changes of variables: its
homomorphisms classify pairs of a homomorphism out of B and a change of variables
(ChangeRing.lift, with universal change ChangeRing.universalChange B). The coefficient
extension ChangeRing.map is functorial (ChangeRing.map_id, ChangeRing.map_comp), and
ChangeRing.pushoutLift is the universal property of
B'[u, u⁻¹, r, s, t] = B' ⊗_B B[u, u⁻¹, r, s, t] as a pushout. For B = ℤ[a₁, ⋯, a₆] it is the
ring of arrows of the Weierstrass Hopf algebroid.
For B = ℤ it is the coordinate algebra Universal.CoordinateRing = ℤ[u,r,s,t][u⁻¹], which
corepresents the group-valued functor R ↦ WeierstrassCurve.VariableChange R. The equivalence
here uses the native change of variables, including over rings with nilpotents and the zero ring;
it is not a classification on field points. This supplies the coordinate algebra for the group
acting on Weierstrass equations.
WeierstrassCurve.VariableChange.specialize classifies a change of variables, and
ChangeRing.universalChange ℤ is the universal one. Their two inverse laws, together with
naturality, give pointsCorepresentableBy.
The functor takes values in groups using Mathlib's VariableChange.mapHom, so its product
is the native, noncommutative product, not addition on three translation coordinates.
References #
- T. Bauer, Computation of the homotopy of the spectrum tmf, §3, for the Weierstrass coordinate-change group. The native multiplication convention is retained here.
The ring B[u, u⁻¹, r, s, t] #
The ring B[u, u⁻¹, r, s, t], the localization of B[u, r, s, t] away from u, with indices
0, 1, 2, 3 for u, r, s, t. It is the coordinate ring of Spec B × G, for the group scheme G
of admissible changes of variables of Weierstrass curves.
Instances For
The universal change of variables (u, r, s, t) over B[u, u⁻¹, r, s, t].
Instances For
Ring homomorphisms out of B[u, u⁻¹, r, s, t] classify pairs of a ring homomorphism out
of B and a change of variables: a homomorphism k corresponds to its restriction to B and
to the base change of universalChange B along k.
Instances For
lift p restricts to p.1 on B.
lift p agrees with p.1 on B.
lift p carries the universal change of variables to p.2.
lift p sends the coordinates u, r, s, t to the coefficients of p.2.
lift p sends the inverse of the scaling coordinate u to the inverse of p.2.u.
A ring homomorphism out of B[u, u⁻¹, r, s, t] is determined by its restriction to B and
the change of variables it classifies.
Coefficient extension and the pushout B' ⊗_B B[u, u⁻¹, r, s, t] #
Coefficient extension fixes the coordinates u, r, s, t.
Coefficient extension along the identity is the identity.
The universal property of B'[u, u⁻¹, r, s, t] as the pushout B' ⊗_B B[u, u⁻¹, r, s, t]
of f : B →+* B' and the inclusion algebraMap: ring homomorphisms out of it correspond to
pairs (g, h) of ring homomorphisms out of B' and out of B[u, u⁻¹, r, s, t] with
g ∘ f = h ∘ algebraMap, by restriction along algebraMap and along map f.
Instances For
The first component of the pair classified by k : B'[u, u⁻¹, r, s, t] →+* R is its
restriction along algebraMap.
The second component of the pair classified by k : B'[u, u⁻¹, r, s, t] →+* R is its
restriction along map f.
pushoutLift f (g, h) restricts to g along algebraMap.
pushoutLift f (g, h) restricts to h along map f.
pushoutLift f (g, h) carries the universal change of variables over B' to the change
classified by h.
The coefficient-extension square is a pushout in the category of commutative rings.
This is the categorical form of pushoutLift, with no flatness assumption.
The coordinate algebra ℤ[u, r, s, t][u⁻¹] #
The coordinate algebra ℤ[u,r,s,t][u⁻¹] of the changes of variables, the case B = ℤ of
ChangeRing B.
Instances For
A map from the coordinate algebra is determined by the change of variables it classifies.
The classifying homomorphism of a change of variables: send u,r,s,t to its coefficients.
Instances For
Every change of variables is the image of the universal one under its classifying map.
Classifying maps commute with coefficient extension.
The universal change is classified by the identity on its coordinate algebra.
Ring homomorphisms from the coordinate algebra classify native changes of variables.
Instances For
The represented point associated to a composite is obtained by mapping the original point along the second ring homomorphism.
Changes of variables, with their native noncommutative group law, form a group-valued
functor of the coefficient ring. Its body is exposed so that its value types are the native
groups VariableChange R, without transporting points across object equalities.
Instances For
The points functor acts by the native coefficient map.
The underlying type-valued functor of Weierstrass changes of variables is corepresented
by ℤ[u,r,s,t][u⁻¹]. The group-scheme structure is not constructed here.
Instances For
The representing equivalence evaluates the universal change along the given ring map.
The inverse representing equivalence is the classifying homomorphism.
The underlying functor of changes of variables is corepresentable by its coordinate
algebra; the representing equivalence is pointsCorepresentableBy.