Automorphisms of an elliptic curve with `j ∉ {0, 1728}` #

Let E be an elliptic curve over a field K. Over a field, isomorphisms of Weierstrass curves are exactly the admissible changes of variables WeierstrassCurve.VariableChange K, acting via •; the automorphisms of E are therefore the C : VariableChange K with C • E = E. This file proves the classical fact (Silverman, The Arithmetic of Elliptic Curves, III.10) that if j(E) ∉ {0, 1728} then the only automorphisms of E are ±1, uniformly in the characteristic.

Main definitions and statements #

WeierstrassCurve.eq_one_or_eq_negVariableChange_of_smul_eq: if j(E) ∉ {0, 1728} then any C : VariableChange K with C • E = E equals 1 or negVariableChange E.
WeierstrassCurve.eq_one_or_eq_negVariableChange_map: the same dichotomy for the image of E under any injective ring map, with the j-hypotheses still read on E itself.
WeierstrassCurve.autGroup E: the automorphism group of E, as the stabiliser of E under the action of VariableChange K. It is an abbrev, so Mathlib's MulAction.stabilizer API applies to it unchanged.
WeierstrassCurve.autGroupMulEquiv: for j(E) ∉ {0, 1728}, the isomorphism autGroup E ≃* Multiplicative (ZMod 2), obtained from Mathlib's zmodMulEquivOfGenerator with negVariableChange E as the generator.

Implementation notes #

The proof is broken into pieces. j ∉ {0, 1728} is equivalent to c₄ ≠ 0 and c₆ ≠ 0 (j_eq_zero_iff and j_eq_1728_iff). From the transformation laws of c₄ and c₆ one gets u² = 1 (u_eq_one_or_eq_neg_one), which reduces everything to the case u = 1. There r = 0 follows from the transformation laws of b₄, b₆, b₈ (r_eq_zero_of_u_eq_one), and then s, t are read off from those of a₁, a₂, a₃, a₄ (eq_one_or_eq_negVariableChange_of_u_eq_one, where the negVariableChange value can occur only in characteristic 2).

This is the Aut (E, O) milestone of TauCetiRoadmap/EllipticCurves/README.md §Layer 1 (in its equation-level form over the ground field), which §Layer 5's twist classification quantifies over: for j ∉ {0, 1728} the pointed twists are exactly the quadratic twists because this group is {±1}.

Adapted from the FLT project (ImperialCollegeLondon/FLT, FLT/Mathlib/AlgebraicGeometry/EllipticCurve/Aut.lean at the roadmap's pin bc2fe8ff7396, FLT PR #1088, Apache 2.0). That file's own header reads Authors: Michael Stoll, Claude, and it has not been touched in FLT since bc2fe8ff7396, so the pin and the working clone (d18b563029f3, a later Mathlib bump) agree on it verbatim. Following this repository's convention for adapted material, the upstream authorship is credited here rather than in the copyright header.

`Aut(E) = {±1}` for `j ∉ {0, 1728}` #

Throughout, C • E = E is an automorphism of E; the nonvanishing of c₄ and c₆ encodes j ∉ {0, 1728}.

source

theorem WeierstrassCurve.eq_one_or_eq_negVariableChange_of_c₄_ne_zero_of_c₆_ne_zero_of_smul_eq {A : Type u_1} [CommRing A] [IsDomain A] (E : WeierstrassCurve A) (hc4 : E.c₄ ≠ 0) (hc6 : E.c₆ ≠ 0) {C : VariableChange A} (hC : C • E = E) :

C = 1 ∨ C = E.negVariableChange

If c₄ ≠ 0 and c₆ ≠ 0 then the only admissible changes of variables fixing E are 1 and negVariableChange E.

The classification is a statement about an integral domain, not a field: the argument is cancellation and zero-product reasoning throughout. It is obtained here from the field case by base change to the fraction field, where every hypothesis and conclusion transfers along the injection — c₄, c₆ by map_c₄/map_c₆, the fixing equation by VariableChange.map_variableChange, and the conclusion back down by VariableChange.map_injective.

source

theorem WeierstrassCurve.eq_one_or_eq_negVariableChange_of_smul_eq {A : Type u_1} [CommRing A] [IsDomain A] (E : WeierstrassCurve A) [E.IsElliptic] (hj₀ : E.j ≠ 0) (hj₁₇₂₈ : E.j ≠ 1728) {C : VariableChange A} (hC : C • E = E) :

C = 1 ∨ C = E.negVariableChange

If j(E) ∉ {0, 1728} then the only admissible changes of variables fixing E are 1 and negVariableChange E; that is, Aut(E) = {±1}.

source

theorem WeierstrassCurve.eq_one_or_eq_negVariableChange_map {A : Type u_1} [CommRing A] (E : WeierstrassCurve A) {B : Type u_2} [CommRing B] [IsDomain B] [E.IsElliptic] {f : A →+* B} (hf : Function.Injective ⇑f) (hj₀ : E.j ≠ 0) (hj₁₇₂₈ : E.j ≠ 1728) {D : VariableChange B} (hD : D • E.map f = E.map f) :

D = 1 ∨ D = (E.map f).negVariableChange

Aut(E.map f) = {±1} when j(E) ∉ {0, 1728}: the dichotomy survives any injective change of base ring. The hypotheses stay on E over the source ring, since j of the image is the image of j (map_j), so an injective f carries both away from 0 and from 1728. Only the target has to be a domain; the source needs no more than a commutative ring. Applies to a base change through E.baseChange B = E.map (algebraMap A B).

The automorphism group #

source

@[reducible, inline]

abbrev WeierstrassCurve.autGroup {R : Type u_2} [CommRing R] (W : WeierstrassCurve R) :

Subgroup (VariableChange R)

The automorphism group of a Weierstrass curve W: the admissible changes of variables fixing W, i.e. the stabiliser of W under the action of VariableChange R. This is an abbrev rather than a def so that Mathlib's MulAction.stabilizer API applies to it unchanged — in particular the simp lemma MulAction.mem_stabilizer_iff, which is the membership normal form C ∈ W.autGroup ↔ C • W = W.

Equations

W.autGroup = MulAction.stabilizer (WeierstrassCurve.VariableChange R) W

Instances For

source

noncomputable def WeierstrassCurve.autGroupMulEquiv {A : Type u_1} [CommRing A] [IsDomain A] (E : WeierstrassCurve A) [E.IsElliptic] (hj₀ : E.j ≠ 0) (hj₁₇₂₈ : E.j ≠ 1728) :

↥E.autGroup ≃* Multiplicative (ZMod 2)

Aut(E) ≅ ℤ/2 for j(E) ∉ {0, 1728}. The automorphism group of E is {±1}, so it is isomorphic to Multiplicative (ZMod 2): it has exactly two elements — 1 and negVariableChange E (eq_one_or_eq_negVariableChange_of_smul_eq), distinct by negVariableChange_ne_one. The isomorphism sends negVariableChange E to Multiplicative.ofAdd 1 (autGroupMulEquiv_apply_negVariableChange), its inverse sending Multiplicative.ofAdd 1 back (autGroupMulEquiv_symm_apply_ofAdd_one).