The m-division field of an elliptic curve

Let W be a Weierstrass curve over a field K, with separable closure Kˢ and absolute Galois group G_K. The m-division field K(E[m]) ⊆ Kˢ is the field generated over K by the coordinates of the points of E(Kˢ)[m] (Silverman VIII.1). An automorphism of Kˢ fixes it exactly when it fixes every point of E(Kˢ)[m], so its Galois group G_{K(E[m])} is the kernel of the action of G_K on the coefficient module E(Kˢ)[m] (WeierstrassCurve.TorsionCoeff). That kernel is normal, so K(E[m]) is Galois over K, and for W elliptic and m ≠ 0 the group E(Kˢ)[m] is finite, so K(E[m]) is a finite extension of K.

Over K(E[m]) the Galois module E[m] becomes trivial, and Galois cohomology with coefficients in E[m] is cohomology with constant coefficients. The inflation-restriction sequence

0 ⟶ H¹(Gal(K(E[m])/K), E[m]) ⟶ H¹(G_K, E[m]) ⟶ H¹(G_{K(E[m])}, E[m])

has a finite group on the left, so restriction to G_{K(E[m])} has finite kernel (WeierstrassCurve.finite_ker_explicitRes1_divisionField). This is how the finiteness of the m-Selmer group of an elliptic curve over a number field (Silverman X.4.2) is reduced to the finiteness of a group of homomorphisms out of G_{K(E[m])} unramified outside a finite set of places.

Main definitions

• WeierstrassCurve.divisionField: the m-division field K(E[m]) inside Kˢ.

Main results

• WeierstrassCurve.divisionField_le_iff: K(E[m]) is the smallest intermediate field containing the coordinates of every point of E(Kˢ)[m].
• WeierstrassCurve.divisionField_le_iff_forall_exists_map_eq: equivalently, the smallest intermediate field over which every point of E(Kˢ)[m] is defined.
• WeierstrassCurve.natCard_torsionBy_of_divisionField_le: for W elliptic and m invertible in K, the curve has m² points of order dividing m over every intermediate field containing K(E[m]).
• WeierstrassCurve.mem_fixingSubgroup_divisionField_iff: an element of G_K fixes K(E[m]) exactly when it fixes every point of E(Kˢ)[m].
• WeierstrassCurve.exists_map_separableClosure_eq_of_nsmul_eq_zero: for W elliptic and m invertible in K, every point of E(K^{alg})[m] is defined over Kˢ.
• WeierstrassCurve.forall_smul_torsionCoeff_eq_self_iff: for W elliptic and m invertible in K, an automorphism of K^{alg} fixes E(K^{alg})[m] exactly when its restriction to Kˢ fixes E(Kˢ)[m].
• WeierstrassCurve.isGalois_divisionField: K(E[m]) is Galois over K.
• WeierstrassCurve.finiteDimensional_divisionField: for W elliptic and m ≠ 0, K(E[m]) is finite over K.
• WeierstrassCurve.finite_ker_explicitRes1_divisionField: for W elliptic and m ≠ 0, the kernel of restriction H¹(G_K, E[m]) → H¹(G_{K(E[m])}, E[m]) is finite.

References

• J. Silverman, The Arithmetic of Elliptic Curves, VIII.1 and X.4.

noncomputable def WeierstrassCurve.divisionField {K : Type u_1} [Field K] (W : WeierstrassCurve K) (m : ℕ) : IntermediateField K (SeparableClosure K)

The m-division field K(E[m]) of W: the subfield of the separable closure Kˢ generated over K by the coordinates of the points of W over Kˢ killed by m.

theorem WeierstrassCurve.divisionField_def {K : Type u_1} [Field K] (W : WeierstrassCurve K) (m : ℕ) : W.divisionField m = IntermediateField.adjoin K (Affine.Point.xCoord '' ↑(AddSubgroup.torsionBy (W.baseChange (SeparableClosure K)).toAffine.Point ↑m) ∪ Affine.Point.yCoord '' ↑(AddSubgroup.torsionBy (W.baseChange (SeparableClosure K)).toAffine.Point ↑m))

K(E[m]) is generated over K by the coordinates of the points of E(Kˢ)[m].

theorem WeierstrassCurve.divisionField_le_iff {K : Type u_1} [Field K] {W : WeierstrassCurve K} {m : ℕ} {L : IntermediateField K (SeparableClosure K)} : W.divisionField m ≤ L ↔ ∀ P ∈ AddSubgroup.torsionBy (W.baseChange (SeparableClosure K)).toAffine.Point ↑m, P.xCoord ∈ L ∧ P.yCoord ∈ L

The universal property of K(E[m]): it lies in an intermediate field L exactly when L contains the coordinates of every point of E(Kˢ)[m].

theorem WeierstrassCurve.xCoord_mem_divisionField {K : Type u_1} [Field K] {W : WeierstrassCurve K} {m : ℕ} {P : (W.baseChange (SeparableClosure K)).toAffine.Point} (hP : P ∈ AddSubgroup.torsionBy (W.baseChange (SeparableClosure K)).toAffine.Point ↑m) : P.xCoord ∈ W.divisionField m

The x-coordinate of a point of E(Kˢ)[m] lies in K(E[m]).

theorem WeierstrassCurve.yCoord_mem_divisionField {K : Type u_1} [Field K] {W : WeierstrassCurve K} {m : ℕ} {P : (W.baseChange (SeparableClosure K)).toAffine.Point} (hP : P ∈ AddSubgroup.torsionBy (W.baseChange (SeparableClosure K)).toAffine.Point ↑m) : P.yCoord ∈ W.divisionField m

The y-coordinate of a point of E(Kˢ)[m] lies in K(E[m]).

theorem WeierstrassCurve.divisionField_le_iff_forall_exists_map_eq {K : Type u_1} [Field K] {W : WeierstrassCurve K} {m : ℕ} {L : IntermediateField K (SeparableClosure K)} : W.divisionField m ≤ L ↔ ∀ P ∈ AddSubgroup.torsionBy (W.baseChange (SeparableClosure K)).toAffine.Point ↑m, ∃ (Q : (W.baseChange ↥L).toAffine.Point), (Affine.Point.map L.val) Q = P

E[m] is defined over L exactly when L contains K(E[m]): an intermediate field L of Kˢ/K contains K(E[m]) exactly when every point of E(Kˢ)[m] comes from a point of W over L.

theorem WeierstrassCurve.natCard_torsionBy_of_divisionField_le {K : Type u_1} [Field K] {W : WeierstrassCurve K} {m : ℕ} [W.IsElliptic] (hm : ↑m ≠ 0) {L : IntermediateField K (SeparableClosure K)} (hL : W.divisionField m ≤ L) : Nat.card ↥(AddSubgroup.torsionBy (W.baseChange ↥L).toAffine.Point ↑m) = m ^ 2

An elliptic curve has full m-torsion over every field containing K(E[m]). For m invertible in K and an intermediate field L of Kˢ/K containing K(E[m]), the group E(L)[m] has m² elements: it maps bijectively onto E(Kˢ)[m].

The Galois group of K(E[m])

theorem WeierstrassCurve.mem_fixingSubgroup_divisionField_iff {K : Type u_1} [Field K] {W : WeierstrassCurve K} {m : ℕ} {σ : TauCeti.AbsoluteGaloisGroup K} : σ ∈ (W.divisionField m).fixingSubgroup ↔ ∀ (P : W.TorsionCoeff m), σ • P = P

The Galois group of K(E[m]) is the kernel of the action on E[m]: an element of G_K fixes K(E[m]) pointwise exactly when it fixes every point of E(Kˢ)[m].

theorem WeierstrassCurve.exists_map_separableClosure_eq_of_nsmul_eq_zero {K : Type u_1} [Field K] {W : WeierstrassCurve K} {m : ℕ} [W.IsElliptic] (hm : ↑m ≠ 0) {P : (W.baseChange (AlgebraicClosure K)).toAffine.Point} (hP : m • P = 0) : ∃ (Q : (W.baseChange (SeparableClosure K)).toAffine.Point), (Affine.Point.map (separableClosure K (AlgebraicClosure K)).val) Q = P

Every point of E(K^{alg})[m] is defined over Kˢ for W elliptic and m invertible in K: it is the image of a point of E(Kˢ) under the inclusion Kˢ → K^{alg}.

theorem WeierstrassCurve.forall_smul_torsionCoeff_eq_self_iff {K : Type u_1} [Field K] {W : WeierstrassCurve K} {m : ℕ} [W.IsElliptic] (hm : ↑m ≠ 0) (σ : Gal(AlgebraicClosure K/K)) : (∀ (P : W.TorsionCoeff m), (TauCeti.absoluteGaloisGroupRestrictEquiv K) σ • P = P) ↔ ∀ (P : (W.baseChange (AlgebraicClosure K)).toAffine.Point), m • P = 0 → (Affine.Point.map ↑σ) P = P

The action on E[m] over Kˢ and over K^{alg}. For W elliptic and m invertible in K, an automorphism σ of K^{alg} fixes every point of E(K^{alg})[m] exactly when its restriction to Kˢ fixes every point of E(Kˢ)[m], since every point of E(K^{alg})[m] is already defined over Kˢ.

instance WeierstrassCurve.fixingSubgroup_divisionField_normal {K : Type u_1} [Field K] (W : WeierstrassCurve K) (m : ℕ) : (W.divisionField m).fixingSubgroup.Normal

The Galois group of K(E[m]) is normal in G_K, being the kernel of the action of G_K on E(Kˢ)[m].

instance WeierstrassCurve.isGalois_divisionField {K : Type u_1} [Field K] (W : WeierstrassCurve K) (m : ℕ) : IsGalois K ↥(W.divisionField m)

K(E[m]) is Galois over K.

instance WeierstrassCurve.finiteDimensional_divisionField {K : Type u_1} [Field K] (W : WeierstrassCurve K) (m : ℕ) [W.IsElliptic] [NeZero m] : FiniteDimensional K ↥(W.divisionField m)

K(E[m]) is a finite extension of K for W elliptic and m ≠ 0: it is generated by the coordinates of the finitely many points of E(Kˢ)[m], each algebraic over K.

Restriction to the Galois group of K(E[m])

theorem WeierstrassCurve.finite_ker_explicitRes1_divisionField {K : Type u_1} [Field K] (W : WeierstrassCurve K) (m : ℕ) [W.IsElliptic] [NeZero m] : Finite ↥(TauCeti.ContCohomology.explicitRes1 (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m) (W.divisionField m).fixingSubgroup).ker

Restriction of H¹(G_K, E[m]) to G_{K(E[m])} has finite kernel, for W elliptic and m ≠ 0. By inflation-restriction the kernel is the image of H¹(Gal(K(E[m])/K), E[m]), and both the Galois group of the finite extension K(E[m]) / K and E(Kˢ)[m] are finite.