Complements on admissible changes of variables

Material complementing Mathlib/AlgebraicGeometry/EllipticCurve/VariableChange.lean: the negation automorphism [-1] of a Weierstrass curve as an admissible change of variables, with its involution API, together with the compatibility of the action with base change (baseChange_smul_baseChange, and smul_baseChange_eq_baseChange_smul_map for a curve defined over a ring mapping into R; whence the instance isElliptic_baseChange_smul: the base change of C • V is elliptic along with that of V, and baseChange_smul_c₄ / baseChange_smul_c₆: a change of variables with u = 1 leaves the c-invariants of a base change alone) and the three base-change facts that Galois descent runs on: smul_eq_of_baseChange_smul_eq (a relation between base changes descends when the change of variables does), negVariableChange_baseChange_map ([-1] is defined over the base, so a base automorphism fixes it) and map_smul_baseChange_eq (the conjugate of an isomorphism of base changes is again one). Comparing an isomorphism with its conjugate via the last of these is what produces the Galois cocycle used by the twist classification. A change of variables over an extension descends to the base field exactly when its four coefficients do (VariableChange.mem_range_baseChange_iff). Conjugation by algebra automorphisms is an action (VariableChange.map_map_algEquiv).

That cocycle comparison lands on a product C * [-1], whose four components are read off here as mul_negVariableChange_u/_r/_s/_t rather than by unfolding VariableChange.mul_def against the components of [-1] at each use. The negation automorphism of C • E is that of E conjugated by C (negVariableChange_smul).

Similarly, the components of C * D⁻¹, the change of variables carrying D • W to C • W, are recorded as VariableChange.mul_inv_u/_r/_s/_t. A translation x ↦ x + r, y ↦ y + t leaves the discriminant and c₄ alone (variableChange_translate_Δ, variableChange_translate_c₄). Every change of variables multiplies c₄ and Δ by units, so it preserves the ideal (c₄, Δ) cutting out the cuspidal locus (span_variableChange_c₄_Δ).

The negation is the nontrivial automorphism in the Aut (E, O) milestone of TauCetiRoadmap/EllipticCurves/README.md §Layer 1, proved in TauCeti/AlgebraicGeometry/EllipticCurve/Aut.lean to exhaust Aut(E) with the identity when j(E) ∉ {0, 1728}.

A change of variables that fixes three affine points (x₁, y₁), (x₁, y₁') and (x₂, y₂), with x₁ - x₂ and y₁ - y₁' units, is the identity (VariableChange.eq_one_of_isUnit_sub): the two x-coordinates force u² = 1 and r = 0, the two y-coordinates over x₁ force u = 1, and then s = t = 0. Read on the points of E[N] for N ≥ 3, this is the rigidity of full level structures.

Everything here is stated over a commutative ring: ⟨-1, 0, -a₁, -a₃⟩ is an admissible change of variables for a Weierstrass curve over any commutative ring, and the two identities it satisfies are polynomial. Only the nontriviality negVariableChange_ne_one needs the curve to be elliptic over a nontrivial ring.

Adapted from the FLT project (ImperialCollegeLondon/FLT, FLT/Mathlib/AlgebraicGeometry/EllipticCurve/VariableChange.lean at the roadmap's pin bc2fe8ff7396 (FLT PR #1088), Apache 2.0, by Kevin Buzzard and Claude), generalised here from FLT's field-level statements to a commutative ring.

theorem WeierstrassCurve.VariableChange.map_map_algEquiv {R : Type u_1} {L : Type u_2} [CommSemiring R] [CommRing L] [Algebra R L] (C : VariableChange L) (σ τ : L ≃ₐ[R] L) : (C.map ↑σ).map ↑τ = C.map ↑(τ * σ)

Conjugating a change of variables by σ and then by τ is conjugating by τ * σ.

def WeierstrassCurve.negVariableChange {R : Type u_1} [CommRing R] (E : WeierstrassCurve R) : VariableChange R

The automorphism [-1] : (x, y) ↦ (x, -y - a₁x - a₃) of a Weierstrass curve, as an admissible change of variables ⟨-1, 0, -a₁, -a₃⟩. It fixes E (negVariableChange_smul_self) and is an involution (negVariableChange_mul_self).

@[simp]

theorem WeierstrassCurve.negVariableChange_u {R : Type u_1} [CommRing R] (E : WeierstrassCurve R) : E.negVariableChange.u = -1

@[simp]

theorem WeierstrassCurve.negVariableChange_r {R : Type u_1} [CommRing R] (E : WeierstrassCurve R) : E.negVariableChange.r = 0

@[simp]

theorem WeierstrassCurve.negVariableChange_s {R : Type u_1} [CommRing R] (E : WeierstrassCurve R) : E.negVariableChange.s = -E.a₁

@[simp]

theorem WeierstrassCurve.negVariableChange_t {R : Type u_1} [CommRing R] (E : WeierstrassCurve R) : E.negVariableChange.t = -E.a₃

@[simp]

theorem WeierstrassCurve.negVariableChange_smul_self {R : Type u_1} [CommRing R] (E : WeierstrassCurve R) : E.negVariableChange • E = E

The negation automorphism fixes the curve.

@[simp]

theorem WeierstrassCurve.negVariableChange_map {R : Type u_1} [CommRing R] (E : WeierstrassCurve R) {A : Type u_2} [CommRing A] (φ : R →+* A) : (E.map φ).negVariableChange = E.negVariableChange.map φ

The negation automorphism commutes with base change along a ring homomorphism.

theorem WeierstrassCurve.negVariableChange_ne_one {R : Type u_1} [CommRing R] (E : WeierstrassCurve R) [Nontrivial R] [E.IsElliptic] : E.negVariableChange ≠ 1

The negation automorphism is nontrivial for an elliptic curve: where 2 ≠ 0 it has u = -1 ≠ 1, and where 2 = 0 it has (s, t) = (-a₁, -a₃) ≠ (0, 0), since an elliptic curve over a ring in which 2 = 0 cannot have a₁ = a₃ = 0.

@[simp]

theorem WeierstrassCurve.VariableChange.map_inv {R : Type u_1} [CommRing R] {A : Type u_2} [CommRing A] (φ : R →+* A) (C : VariableChange R) : C⁻¹.map φ = (C.map φ)⁻¹

A change of variables maps its inverse to the inverse of its image. Mathlib has this as map_inv for the bundled VariableChange.mapHom; this is the same fact in the .map spelling, which is the one goals are phrased in — rw does not see through mapHom φ C ≡ C.map φ.

@[simp]

theorem WeierstrassCurve.VariableChange.map_one {R : Type u_1} [CommRing R] {A : Type u_2} [CommRing A] (φ : R →+* A) : map 1 φ = 1

A change of variables maps the identity to the identity, in the .map spelling. The companion of VariableChange.map_inv; see there for why the bundled mapHom form is not enough.

@[simp]

theorem WeierstrassCurve.VariableChange.map_mul {R : Type u_1} [CommRing R] {A : Type u_2} [CommRing A] (φ : R →+* A) (C D : VariableChange R) : (C * D).map φ = C.map φ * D.map φ

A change of variables maps a product to the product of the images, in the .map spelling. The companion of VariableChange.map_inv; see there for why the bundled mapHom form is not enough.

Components of C * D⁻¹

C * D⁻¹ is the change of variables carrying D • W to C • W. Its components are the differences of those of C and D, rescaled by powers of D.u⁻¹.

@[simp]

theorem WeierstrassCurve.VariableChange.mul_inv_u {R : Type u_1} [CommRing R] (C D : VariableChange R) : (C * D⁻¹).u = C.u * D.u⁻¹

The scaling factor of C * D⁻¹ is C.u * D.u⁻¹.

@[simp]

theorem WeierstrassCurve.VariableChange.mul_inv_r {R : Type u_1} [CommRing R] (C D : VariableChange R) : (C * D⁻¹).r = (C.r - D.r) * ↑D.u⁻¹ ^ 2

The translation r of C * D⁻¹ is (C.r - D.r) * D.u⁻¹ ^ 2.

@[simp]

theorem WeierstrassCurve.VariableChange.mul_inv_s {R : Type u_1} [CommRing R] (C D : VariableChange R) : (C * D⁻¹).s = (C.s - D.s) * ↑D.u⁻¹

The shear s of C * D⁻¹ is (C.s - D.s) * D.u⁻¹.

@[simp]

theorem WeierstrassCurve.VariableChange.mul_inv_t {R : Type u_1} [CommRing R] (C D : VariableChange R) : (C * D⁻¹).t = (C.t - D.t - D.s * (C.r - D.r)) * ↑D.u⁻¹ ^ 3

The translation t of C * D⁻¹ is (C.t - D.t - D.s * (C.r - D.r)) * D.u⁻¹ ^ 3.

Components of a change of variables composed with [-1]

[-1] has u = -1 and r = 0, so composing with it negates u, fixes r, and shifts s and t by the curve's a₁ and a₃. These four are @[simp]: their right-hand sides are the normal form wanted downstream, since the cocycle comparisons of the twist classification land on exactly this product.

@[simp]

theorem WeierstrassCurve.mul_negVariableChange_u {R : Type u_1} [CommRing R] (E : WeierstrassCurve R) (C : VariableChange R) : (C * E.negVariableChange).u = -C.u

Composing with [-1] negates the scaling factor u.

@[simp]

theorem WeierstrassCurve.mul_negVariableChange_r {R : Type u_1} [CommRing R] (E : WeierstrassCurve R) (C : VariableChange R) : (C * E.negVariableChange).r = C.r

Composing with [-1] leaves the translation r unchanged, [-1] having r = 0 and u = -1 entering squared.

@[simp]

theorem WeierstrassCurve.mul_negVariableChange_s {R : Type u_1} [CommRing R] (E : WeierstrassCurve R) (C : VariableChange R) : (C * E.negVariableChange).s = -C.s - E.a₁

Composing with [-1] negates the shear s and shifts it by the curve's a₁.

@[simp]

theorem WeierstrassCurve.mul_negVariableChange_t {R : Type u_1} [CommRing R] (E : WeierstrassCurve R) (C : VariableChange R) : (C * E.negVariableChange).t = -C.t - C.r * E.a₁ - E.a₃

Composing with [-1] negates the translation t and shifts it by r * a₁ and the curve's a₃.

@[simp]

theorem WeierstrassCurve.negVariableChange_mul_self {R : Type u_1} [CommRing R] (E : WeierstrassCurve R) : E.negVariableChange * E.negVariableChange = 1

The negation automorphism is an involution.

@[simp]

theorem WeierstrassCurve.negVariableChange_inv {R : Type u_1} [CommRing R] (E : WeierstrassCurve R) : E.negVariableChange⁻¹ = E.negVariableChange

The negation automorphism is its own inverse, being an involution.

theorem WeierstrassCurve.negVariableChange_smul {R : Type u_1} [CommRing R] (E : WeierstrassCurve R) (C : VariableChange R) : (C • E).negVariableChange = C * E.negVariableChange * C⁻¹

The negation automorphism of C • E is that of E conjugated by C: negating a point of C • E is carrying it to E by C, negating there, and carrying the result back by C⁻¹.

@[simp]

theorem WeierstrassCurve.variableChange_translate_Δ {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (x y : R) : ({ u := 1, r := x, s := 0, t := y } • W).Δ = W.Δ

A translation does not change the discriminant.

@[simp]

theorem WeierstrassCurve.variableChange_translate_c₄ {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (x y : R) : ({ u := 1, r := x, s := 0, t := y } • W).c₄ = W.c₄

A translation does not change c₄.

theorem WeierstrassCurve.span_variableChange_c₄_Δ {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (C : VariableChange R) : Ideal.span {(C • W).c₄, (C • W).Δ} = Ideal.span {W.c₄, W.Δ}

A change of variables multiplies c₄ and Δ by units, so it preserves the ideal they generate: the cuspidal locus V(c₄, Δ) is stable under the coordinate-change group.

@[simp]

theorem WeierstrassCurve.baseChange_smul_baseChange {R : Type u_1} [CommRing R] (L : Type u_2) [CommRing L] [Algebra R L] (C : VariableChange R) (V : WeierstrassCurve R) : C.baseChange L • V.baseChange L = (C • V).baseChange L

Base change commutes with the action of a change of variables. Base changing a curve and then acting by the base-changed variable change gives the same model as acting first and base changing the result, so a VariableChange-invariant statement over R transports to L. Stated in the baseChange spelling, so it rewrites directly in goals phrased that way.

theorem WeierstrassCurve.smul_baseChange_eq_baseChange_smul_map {R : Type u_1} [CommRing R] {L : Type u_2} [CommRing L] [Algebra R L] {A : Type u_3} [CommRing A] [Algebra A L] {φ : A →+* R} (hφ : (algebraMap R L).comp φ = algebraMap A L) (C : VariableChange R) (W₀ : WeierstrassCurve A) : C.baseChange L • W₀.baseChange L = (C • W₀.map φ).baseChange L

Base change commutes with the action of a change of variables, through an intermediate ring. Let φ : A →+* R be compatible with the structure maps to L. For a change of variables C over R and a curve W₀ over A, acting by Cᴸ on W₀ᴸ gives the base change of C applied to the image of W₀ in R. This extends baseChange_smul_baseChange to an equation over a ring mapping into R, such as an equation over ℤ.

instance WeierstrassCurve.isElliptic_baseChange_smul {R : Type u_1} [CommRing R] {L : Type u_2} [CommRing L] [Algebra R L] (V : WeierstrassCurve R) (C : VariableChange R) [(V.baseChange L).IsElliptic] : ((C • V).baseChange L).IsElliptic

The base change of C • V to L is elliptic whenever that of V is, since it is Cᴸ • Vᴸ.

@[simp]

theorem WeierstrassCurve.baseChange_smul_c₄ {R : Type u_1} [CommRing R] (L : Type u_2) [CommRing L] [Algebra R L] {C : VariableChange R} (hu : C.u = 1) (V : WeierstrassCurve R) : ((C • V).baseChange L).c₄ = (V.baseChange L).c₄

A change of variables with u = 1 leaves c₄ alone, and base change carries that along: the scaling factor u⁻¹ ^ 4 of WeierstrassCurve.variableChange_c₄ is 1.

@[simp]

theorem WeierstrassCurve.baseChange_smul_c₆ {R : Type u_1} [CommRing R] (L : Type u_2) [CommRing L] [Algebra R L] {C : VariableChange R} (hu : C.u = 1) (V : WeierstrassCurve R) : ((C • V).baseChange L).c₆ = (V.baseChange L).c₆

A change of variables with u = 1 leaves c₆ alone, and base change carries that along: the scaling factor u⁻¹ ^ 6 of WeierstrassCurve.variableChange_c₆ is 1.

theorem WeierstrassCurve.smul_eq_of_baseChange_smul_eq {R : Type u_1} [CommRing R] (L : Type u_2) [CommRing L] [Algebra R L] (hRL : Function.Injective ⇑(algebraMap R L)) (C : VariableChange R) {V W : WeierstrassCurve R} (h : C.baseChange L • V.baseChange L = W.baseChange L) : C • V = W

A relation between base changes descends, provided the change of variables does. If C is defined over R and Cᴸ carries Vᴸ to Wᴸ, then C already carries V to W over R. The content is that base change is injective on models when R → L is.

@[simp]

theorem WeierstrassCurve.negVariableChange_baseChange_map {R : Type u_1} [CommRing R] (E : WeierstrassCurve R) (L : Type u_2) [CommRing L] [Algebra R L] (σ : L →ₐ[R] L) : (E.baseChange L).negVariableChange.map ↑σ = (E.baseChange L).negVariableChange

The automorphism [-1] of a base-changed curve is defined over the base, hence fixed by every R-algebra map L → L: its four components -1, 0, -a₁, -a₃ all come from R.

theorem WeierstrassCurve.map_smul_baseChange_eq {R : Type u_1} [CommRing R] (L : Type u_2) [CommRing L] [Algebra R L] (σ : L →ₐ[R] L) {V W : WeierstrassCurve R} {ρ : VariableChange L} (hρ : ρ • V.baseChange L = W.baseChange L) : ρ.map ↑σ • V.baseChange L = W.baseChange L

The conjugate of an isomorphism between base-changed curves is again one. If ρ : Vᴸ ≅ Wᴸ and V, W are defined over R, then σρ is also an isomorphism Vᴸ ≅ Wᴸ, because σ fixes both curves. Only that σ is an R-algebra map is used, not that it is invertible; the Galois case is the instance the twist classification takes. Comparing ρ with σρ is what produces the Galois cocycle.

theorem WeierstrassCurve.VariableChange.mem_range_baseChange_iff {K : Type u_2} {L : Type u_3} [Field K] [CommRing L] [Nontrivial L] [Algebra K L] (C : VariableChange L) : (C ∈ Set.range fun (D : VariableChange K) => D.baseChange L) ↔ ↑C.u ∈ Set.range ⇑(algebraMap K L) ∧ C.r ∈ Set.range ⇑(algebraMap K L) ∧ C.s ∈ Set.range ⇑(algebraMap K L) ∧ C.t ∈ Set.range ⇑(algebraMap K L)

A change of variables descends exactly when its coefficients do. A change of variables over a nontrivial K-algebra L is the base change of one over the field K if and only if its four coefficients u, r, s, t lie in the image of K.

theorem WeierstrassCurve.VariableChange.eq_one_of_isUnit_sub {R : Type u_1} [CommRing R] (C : VariableChange R) {x₁ x₂ y₁ y₁' y₂ : R} (hx : IsUnit (x₁ - x₂)) (hy : IsUnit (y₁ - y₁')) (hx₁ : ↑C.u ^ 2 * x₁ + C.r = x₁) (hx₂ : ↑C.u ^ 2 * x₂ + C.r = x₂) (hy₁ : ↑C.u ^ 3 * y₁ + ↑C.u ^ 2 * C.s * x₁ + C.t = y₁) (hy₁' : ↑C.u ^ 3 * y₁' + ↑C.u ^ 2 * C.s * x₁ + C.t = y₁') (hy₂ : ↑C.u ^ 3 * y₂ + ↑C.u ^ 2 * C.s * x₂ + C.t = y₂) : C = 1

A change of variables fixing three suitable points is the identity. Let C = (u, r, s, t) fix the affine points (x₁, y₁), (x₁, y₁') and (x₂, y₂) under (x, y) ↦ (u²x + r, u³y + u²sx + t). If x₁ - x₂ and y₁ - y₁' are units, then C = 1. For points of a Weierstrass curve, (x₁, y₁') is typically the negative of (x₁, y₁), and the hypotheses then say that the three points have distinct images in every residue field.