Theorems · Inductive type · algebraic geometry

WeierstrassCurve.VariableChange

(R : Type u) → [CommRing R] → Type u

An admissible linear change of variables of Weierstrass curves defined over a ring R given by a tuple (u, r, s, t) for some u in Rˣ and some r, s, t in R. As a matrix, it is $$\begin{pmatrix} u^2 & 0 & r \cr u^2s & u^3 & t \cr 0 & 0 & 1 \end{pmatrix}.$$ In other words, this is the change of variables (X, Y) ↦ (u²X + r, u³Y + u²sX + t). When R is a field, any two isomorphic Weierstrass equations are related by this.

Defined in

Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Cited by

53 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

CommRing