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 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.

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 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}.

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.

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).

Equations

• E.negVariableChange = { u := -1, r := 0, s := -E.a₁, t := -E.a₃ }

@[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 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.

@[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_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.