The Galois coefficient modules of an elliptic curve

Let W be a Weierstrass curve over a field K, Kˢ a separable closure of K and G_K = AbsoluteGaloisGroup K. The Galois cohomology of an elliptic curve takes its coefficients in two discrete G_K-modules, fixed here once and for all:

W.PointCoeff = E(Kˢ),      W.TorsionCoeff m = E(Kˢ)[m],

with G_K acting on the coordinates of points. The first is a type synonym of TauCeti.ForcedDiscrete applied to the points of the base change W⁄Kˢ, so it carries the discrete topology imposed by that wrapper rather than by an instance on the point type itself. Both modules are discrete G_K-modules in the sense continuous cohomology asks for: the stabilizer of a point is open, because its coordinates lie in Kˢ, which is algebraic over K (WeierstrassCurve.PointCoeff.instContinuousSMul).

For m invertible in K, multiplication by m gives the Kummer sequence of W,

0 ⟶ E(Kˢ)[m] ⟶ E(Kˢ) ⟶ E(Kˢ) ⟶ 0,

as a TauCeti.ContCohomology.DiscreteShortExact (WeierstrassCurve.kummerShortExact), so that the long exact sequence of continuous cohomology applies to it verbatim. Exactness on the right is the divisibility of E(Kˢ) (WeierstrassCurve.Affine.nsmul_surjective), which is where invertibility of m enters.

Finally WeierstrassCurve.basePointEquivInvariants identifies H⁰(G_K, E(Kˢ)) with E(K). The two are different Lean types, so what is supplied is the canonical isomorphism, induced by the inclusion K → Kˢ. It rests on the fixed field of G_K being K, which is why the separable closure and not an algebraic closure is used: over an imperfect K the points of E fixed by the automorphisms of an algebraic closure are the points over the perfect closure of K.

Main definitions

• WeierstrassCurve.PointCoeff: the points of W over Kˢ, as a discrete G_K-module.
• WeierstrassCurve.pointCoeffEquiv: its identification with the points of W⁄Kˢ.
• WeierstrassCurve.TorsionCoeff: the m-torsion of W.PointCoeff, a discrete G_K-module.
• WeierstrassCurve.torsionCoeffIncl: the equivariant inclusion E(Kˢ)[m] → E(Kˢ).
• WeierstrassCurve.kummerShortExact: the Kummer sequence 0 → E[m] → E → E → 0 of W.
• WeierstrassCurve.basePointCoeff: the inclusion E(K) → E(Kˢ), the transport of points along K → Kˢ (WeierstrassCurve.basePointCoeff_eq_pointCoeffEquiv_mapAlong).
• WeierstrassCurve.basePointEquivInvariants: the isomorphism E(K) ≅ H⁰(G_K, E(Kˢ)).
• WeierstrassCurve.baseTorsionCoeff: the inclusion E(K)[m] → E(Kˢ)[m].

Main results

• WeierstrassCurve.PointCoeff.instContinuousSMul, WeierstrassCurve.TorsionCoeff.instContinuousSMul: the coefficients are discrete modules.
• WeierstrassCurve.finite_torsionCoeff: E(Kˢ)[m] is finite for W elliptic and m ≠ 0.
• WeierstrassCurve.pointGaloisAction_apply_eq_smul: the action is WeierstrassCurve.pointGaloisAction, and WeierstrassCurve.torsionByCongr_pointCoeffEquiv_symm_smul its torsion counterpart WeierstrassCurve.torsionGaloisAction.
• WeierstrassCurve.Affine.Point.map_map_separableClosure_val: an automorphism of K^{alg} acts on the points of E(Kˢ) through its restriction to Kˢ.
• WeierstrassCurve.natCard_torsionCoeff: E(Kˢ)[m] has m² points for m invertible in K.
• WeierstrassCurve.isAddKleinFour_torsionCoeff_two: E(Kˢ)[2] is a Klein four-group.
• WeierstrassCurve.cast_pointCoeff_smul, WeierstrassCurve.cast_torsionCoeff_smul: transport of the coefficients along an equality of curves, such as (W⁄L)⁄M = W⁄M, is G_K-equivariant.
• WeierstrassCurve.mem_H0_pointCoeff_iff: a point of E(Kˢ) fixed by G_K comes from E(K), and WeierstrassCurve.exists_baseTorsionCoeff_eq_of_forall_smul_eq its torsion counterpart.

Implementation notes

The construction follows the multiplicative coefficient modules of TauCeti/FieldTheory/GaloisCohomology/Coefficients.lean: WeierstrassCurve.PointCoeff, WeierstrassCurve.kummerShortExact and WeierstrassCurve.basePointEquivInvariants play the roles of TauCeti.UnitsCoeff, TauCeti.kummerShortExact and TauCeti.baseUnitsEquivInvariants there.

References

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

The points over the separable closure

def WeierstrassCurve.PointCoeff {K : Type u_1} [Field K] (W : WeierstrassCurve K) : Type u_1

The points of W over a separable closure Kˢ of K, as the coefficient module of the Galois cohomology of W. It is a type synonym for ForcedDiscrete (W⁄Kˢ).toAffine.Point, so that the discrete topology is the one imposed by TauCeti.ForcedDiscrete, and the action of G_K lives on it and not on the point type.

@[instance_reducible]

noncomputable instance WeierstrassCurve.instAddCommGroupPointCoeff {K : Type u_1} [Field K] (W : WeierstrassCurve K) : AddCommGroup W.PointCoeff

@[instance_reducible]

noncomputable instance WeierstrassCurve.instTopologicalSpacePointCoeff {K : Type u_1} [Field K] (W : WeierstrassCurve K) : TopologicalSpace W.PointCoeff

instance WeierstrassCurve.instDiscreteTopologyPointCoeff {K : Type u_1} [Field K] (W : WeierstrassCurve K) : DiscreteTopology W.PointCoeff

noncomputable def WeierstrassCurve.pointCoeffEquiv {K : Type u_1} [Field K] (W : WeierstrassCurve K) : (W.baseChange (SeparableClosure K)).toAffine.Point ≃+ W.PointCoeff

The identification of W.PointCoeff with the points of W over Kˢ.

The Galois action

@[instance_reducible]

noncomputable instance WeierstrassCurve.instSMulAbsoluteGaloisGroupPointCoeff {K : Type u_1} [Field K] (W : WeierstrassCurve K) : SMul (TauCeti.AbsoluteGaloisGroup K) W.PointCoeff

G_K acts on E(Kˢ) through the coordinates, by Mathlib's point map along each automorphism.

@[simp]

theorem WeierstrassCurve.pointCoeffEquiv_symm_smul {K : Type u_1} [Field K] (W : WeierstrassCurve K) (σ : TauCeti.AbsoluteGaloisGroup K) (P : W.PointCoeff) : W.pointCoeffEquiv.symm (σ • P) = (Affine.Point.map ↑σ) (W.pointCoeffEquiv.symm P)

The Galois action on E(Kˢ) is the point map along the automorphism.

@[simp]

theorem WeierstrassCurve.smul_pointCoeffEquiv {K : Type u_1} [Field K] (W : WeierstrassCurve K) (σ : TauCeti.AbsoluteGaloisGroup K) (P : (W.baseChange (SeparableClosure K)).toAffine.Point) : σ • W.pointCoeffEquiv P = W.pointCoeffEquiv ((Affine.Point.map ↑σ) P)

The Galois action on a point of W⁄Kˢ, read in W.PointCoeff.

@[instance_reducible]

noncomputable instance WeierstrassCurve.instDistribMulActionAbsoluteGaloisGroupPointCoeff {K : Type u_1} [Field K] (W : WeierstrassCurve K) : DistribMulAction (TauCeti.AbsoluteGaloisGroup K) W.PointCoeff

theorem WeierstrassCurve.pointGaloisAction_apply_eq_smul {K : Type u_1} [Field K] (W : WeierstrassCurve K) (σ : TauCeti.AbsoluteGaloisGroup K) (P : (W.baseChange (SeparableClosure K)).toAffine.Point) : (Multiplicative.toAdd (W.pointGaloisAction σ)) P = W.pointCoeffEquiv.symm (σ • W.pointCoeffEquiv P)

The action is WeierstrassCurve.pointGaloisAction, read in W.PointCoeff.

theorem WeierstrassCurve.Affine.Point.map_map_separableClosure_val {K : Type u_1} [Field K] {W : WeierstrassCurve K} (σ : Gal(AlgebraicClosure K/K)) (Q : (W.baseChange (SeparableClosure K)).toAffine.Point) : (map ↑σ) ((map (separableClosure K (AlgebraicClosure K)).val) Q) = (map (separableClosure K (AlgebraicClosure K)).val) ((map ↑((TauCeti.absoluteGaloisGroupRestrictEquiv K) σ)) Q)

Restriction to Kˢ commutes with the point map into K^{alg}. An automorphism σ of K^{alg} acts on the image in E(K^{alg}) of a point of E(Kˢ) as its restriction to Kˢ acts on that point.

instance WeierstrassCurve.PointCoeff.instContinuousSMul {K : Type u_1} [Field K] (W : WeierstrassCurve K) : ContinuousSMul (TauCeti.AbsoluteGaloisGroup K) W.PointCoeff

E(Kˢ) is a discrete G_K-module: the stabilizer of an affine point contains the stabilizers of its two coordinates, which are open because Kˢ is algebraic over K.

The m-torsion

@[reducible, inline]

abbrev WeierstrassCurve.TorsionCoeff {K : Type u_1} [Field K] (W : WeierstrassCurve K) (m : ℕ) : Type u_1

The m-torsion E(Kˢ)[m] of W, as a coefficient module of the Galois cohomology of W. Its topology is the subspace topology, which is discrete.

theorem WeierstrassCurve.smul_mem_torsionCoeff {K : Type u_1} [Field K] {W : WeierstrassCurve K} {m : ℕ} (σ : TauCeti.AbsoluteGaloisGroup K) {P : W.PointCoeff} (hP : P ∈ AddSubgroup.torsionBy W.PointCoeff ↑m) : σ • P ∈ AddSubgroup.torsionBy W.PointCoeff ↑m

The Galois action commutes with multiplication by m, so it preserves E(Kˢ)[m].

@[instance_reducible]

noncomputable instance WeierstrassCurve.instDistribMulActionAbsoluteGaloisGroupTorsionCoeff {K : Type u_1} [Field K] (W : WeierstrassCurve K) (m : ℕ) : DistribMulAction (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m)

@[simp]

theorem WeierstrassCurve.coe_smul_torsionCoeff {K : Type u_1} [Field K] (W : WeierstrassCurve K) {m : ℕ} (σ : TauCeti.AbsoluteGaloisGroup K) (P : W.TorsionCoeff m) : ↑(σ • P) = σ • ↑P

The Galois action on E(Kˢ)[m] is the action on E(Kˢ).

instance WeierstrassCurve.TorsionCoeff.instContinuousSMul {K : Type u_1} [Field K] (W : WeierstrassCurve K) (m : ℕ) : ContinuousSMul (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m)

E(Kˢ)[m] is a discrete G_K-module: the restriction of the continuous action on E(Kˢ) to a stable subgroup is continuous.

theorem WeierstrassCurve.torsionByCongr_pointCoeffEquiv_symm_smul {K : Type u_1} [Field K] (W : WeierstrassCurve K) {m : ℕ} (σ : TauCeti.AbsoluteGaloisGroup K) (P : W.TorsionCoeff m) : (W.pointCoeffEquiv.torsionByCongr ↑m).symm (σ • P) = (Multiplicative.toAdd ((W.torsionGaloisAction ↑m) σ)) ((W.pointCoeffEquiv.torsionByCongr ↑m).symm P)

The action on E(Kˢ)[m] is WeierstrassCurve.torsionGaloisAction, read through the identification WeierstrassCurve.pointCoeffEquiv of E(Kˢ) with the points of W⁄Kˢ.

instance WeierstrassCurve.finite_torsionCoeff {K : Type u_1} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] (m : ℕ) [NeZero m] : Finite (W.TorsionCoeff m)

For W elliptic and m ≠ 0, the m-torsion E(Kˢ)[m] of W over the separable closure is finite.

noncomputable def WeierstrassCurve.torsionCoeffIncl {K : Type u_1} [Field K] (W : WeierstrassCurve K) (m : ℕ) : W.TorsionCoeff m →+[TauCeti.AbsoluteGaloisGroup K] W.PointCoeff

The inclusion E(Kˢ)[m] → E(Kˢ), as a G_K-equivariant homomorphism.

@[simp]

theorem WeierstrassCurve.torsionCoeffIncl_apply {K : Type u_1} [Field K] (W : WeierstrassCurve K) {m : ℕ} (P : W.TorsionCoeff m) : (W.torsionCoeffIncl m) P = ↑P

theorem WeierstrassCurve.natCard_torsionCoeff {K : Type u_1} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] {m : ℕ} (hm : IsUnit ↑m) : Nat.card (W.TorsionCoeff m) = m ^ 2

E(Kˢ)[m] has m² points when m is invertible in K.

theorem WeierstrassCurve.isAddKleinFour_torsionCoeff_two {K : Type u_1} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] (h2 : IsUnit ↑2) : IsAddKleinFour (W.TorsionCoeff 2)

E(Kˢ)[2] is a Klein four-group when 2 is invertible in K: it has 2² = 4 points, each killed by 2.

Transport along an equality of curves

theorem WeierstrassCurve.cast_pointCoeff_smul {K : Type u_1} [Field K] {V V' : WeierstrassCurve K} (h : V = V') (σ : TauCeti.AbsoluteGaloisGroup K) (P : V.PointCoeff) : (AddEquiv.cast h) (σ • P) = σ • (AddEquiv.cast h) P

Transport of E(Kˢ) along an equality of Weierstrass curves is G_K-equivariant.

theorem WeierstrassCurve.cast_pointCoeffEquiv_some {K : Type u_1} [Field K] {V V' : WeierstrassCurve K} (h : V = V') {x y : SeparableClosure K} (hns : (V.baseChange (SeparableClosure K)).toAffine.Nonsingular x y) : (AddEquiv.cast h) (V.pointCoeffEquiv (Affine.Point.some x y hns)) = V'.pointCoeffEquiv (Affine.Point.some x y ⋯)

Transport of E(Kˢ) along an equality of Weierstrass curves keeps the coordinates of an affine point.

theorem WeierstrassCurve.coe_cast_torsionCoeff {K : Type u_1} [Field K] {V V' : WeierstrassCurve K} (h : V = V') {m : ℕ} (P : V.TorsionCoeff m) : ↑((AddEquiv.cast h) P) = (AddEquiv.cast h) ↑P

Transport of E(Kˢ)[m] along an equality of Weierstrass curves is the transport of the underlying point of E(Kˢ).

theorem WeierstrassCurve.cast_torsionCoeff_smul {K : Type u_1} [Field K] {V V' : WeierstrassCurve K} (h : V = V') {m : ℕ} (σ : TauCeti.AbsoluteGaloisGroup K) (P : V.TorsionCoeff m) : (AddEquiv.cast h) (σ • P) = σ • (AddEquiv.cast h) P

Transport of E(Kˢ)[m] along an equality of Weierstrass curves is G_K-equivariant.

The Kummer sequence

noncomputable def WeierstrassCurve.kummerShortExact {K : Type u_1} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] (m : ℕ) (hm : IsUnit ↑m) : TauCeti.ContCohomology.DiscreteShortExact (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m) W.PointCoeff W.PointCoeff

The Kummer sequence 0 → E(Kˢ)[m] → E(Kˢ) → E(Kˢ) → 0 of W, for m invertible in K. Exactness on the right is the divisibility of E(Kˢ) by m.

@[simp]

theorem WeierstrassCurve.kummerShortExact_incl {K : Type u_1} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] (m : ℕ) (hm : IsUnit ↑m) : (W.kummerShortExact m hm).incl = (AddSubgroup.torsionBy W.PointCoeff ↑m).subtype

@[simp]

theorem WeierstrassCurve.kummerShortExact_proj {K : Type u_1} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] (m : ℕ) (hm : IsUnit ↑m) : (W.kummerShortExact m hm).proj = nsmulAddMonoidHom m

@[simp]

theorem WeierstrassCurve.kummerShortExact_inclDistribMulActionHom {K : Type u_1} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] (m : ℕ) (hm : IsUnit ↑m) : (W.kummerShortExact m hm).inclDistribMulActionHom = W.torsionCoeffIncl m

The equivariant inclusion of the Kummer sequence is WeierstrassCurve.torsionCoeffIncl.

The invariants of E(Kˢ)

noncomputable def WeierstrassCurve.basePointCoeff {K : Type u_1} [Field K] (W : WeierstrassCurve K) [DecidableEq K] : W.toAffine.Point →+ W.PointCoeff

The inclusion E(K) → E(Kˢ), induced by the inclusion of K into Kˢ.

@[simp]

theorem WeierstrassCurve.basePointCoeff_some {K : Type u_1} [Field K] (W : WeierstrassCurve K) [DecidableEq K] {x y : K} (h : W.toAffine.Nonsingular x y) : W.basePointCoeff (Affine.Point.some x y h) = W.pointCoeffEquiv (Affine.Point.some ((algebraMap K (SeparableClosure K)) x) ((algebraMap K (SeparableClosure K)) y) ⋯)

The inclusion E(K) → E(Kˢ) keeps the coordinates of an affine point.

theorem WeierstrassCurve.basePointCoeff_eq_pointCoeffEquiv_mapAlong {K : Type u_1} [Field K] (W : WeierstrassCurve K) [DecidableEq K] (P : W.toAffine.Point) : W.basePointCoeff P = W.pointCoeffEquiv (Affine.Point.mapAlong (algebraMap K (SeparableClosure K)) ⋯ P)

The inclusion E(K) → E(Kˢ) is the transport of points along algebraMap K Kˢ (WeierstrassCurve.Affine.Point.mapAlong), read in W.PointCoeff.

theorem WeierstrassCurve.basePointCoeff_injective {K : Type u_1} [Field K] (W : WeierstrassCurve K) [DecidableEq K] : Function.Injective ⇑W.basePointCoeff

The inclusion E(K) → E(Kˢ) is injective.

theorem WeierstrassCurve.smul_basePointCoeff {K : Type u_1} [Field K] (W : WeierstrassCurve K) [DecidableEq K] (σ : TauCeti.AbsoluteGaloisGroup K) (P : W.toAffine.Point) : σ • W.basePointCoeff P = W.basePointCoeff P

A point of E(K) is fixed by G_K after mapping into E(Kˢ).

noncomputable def WeierstrassCurve.baseTorsionCoeff {K : Type u_1} [Field K] (W : WeierstrassCurve K) [DecidableEq K] (m : ℕ) : ↥(AddSubgroup.torsionBy W.toAffine.Point ↑m) →+ W.TorsionCoeff m

The inclusion E(K)[m] → E(Kˢ)[m], the restriction of WeierstrassCurve.basePointCoeff to the m-torsion.

@[simp]

theorem WeierstrassCurve.coe_baseTorsionCoeff {K : Type u_1} [Field K] (W : WeierstrassCurve K) [DecidableEq K] {m : ℕ} (T : ↥(AddSubgroup.torsionBy W.toAffine.Point ↑m)) : ↑((W.baseTorsionCoeff m) T) = W.basePointCoeff ↑T

theorem WeierstrassCurve.torsionByCongr_symm_baseTorsionCoeff {K : Type u_1} [Field K] (W : WeierstrassCurve K) [DecidableEq K] (m : ℕ) (P : ↥(AddSubgroup.torsionBy W.toAffine.Point ↑m)) : (W.pointCoeffEquiv.torsionByCongr ↑m).symm ((W.baseTorsionCoeff m) P) = (W.torsionMapAlong (algebraMap K (SeparableClosure K)) ↑m) P

The inclusion of rational torsion agrees with transport along the base-field embedding.

@[simp]

theorem WeierstrassCurve.smul_baseTorsionCoeff {K : Type u_1} [Field K] (W : WeierstrassCurve K) [DecidableEq K] {m : ℕ} (σ : TauCeti.AbsoluteGaloisGroup K) (T : ↥(AddSubgroup.torsionBy W.toAffine.Point ↑m)) : σ • (W.baseTorsionCoeff m) T = (W.baseTorsionCoeff m) T

A point of E(K)[m] is fixed by G_K after mapping into E(Kˢ)[m].

theorem WeierstrassCurve.baseTorsionCoeff_injective {K : Type u_1} [Field K] (W : WeierstrassCurve K) [DecidableEq K] (m : ℕ) : Function.Injective ⇑(W.baseTorsionCoeff m)

The inclusion E(K)[m] → E(Kˢ)[m] is injective.

theorem WeierstrassCurve.mem_H0_pointCoeff_iff {K : Type u_1} [Field K] (W : WeierstrassCurve K) [DecidableEq K] {P : W.PointCoeff} : P ∈ TauCeti.ContCohomology.H0 (TauCeti.AbsoluteGaloisGroup K) W.PointCoeff ↔ ∃ (Q : W.toAffine.Point), W.basePointCoeff Q = P

A point of E(Kˢ) fixed by the whole Galois group comes from E(K). This is the fixed-field theorem InfiniteGalois.mem_range_algebraMap_iff_fixed for the separable closure, applied to the two coordinates of the point.

theorem WeierstrassCurve.exists_baseTorsionCoeff_eq_of_forall_smul_eq {K : Type u_1} [Field K] (W : WeierstrassCurve K) [DecidableEq K] {m : ℕ} {Q : W.TorsionCoeff m} (h : ∀ (σ : TauCeti.AbsoluteGaloisGroup K), σ • Q = Q) : ∃ (T : ↥(AddSubgroup.torsionBy W.toAffine.Point ↑m)), (W.baseTorsionCoeff m) T = Q

A point of E(Kˢ)[m] fixed by the whole Galois group comes from E(K)[m], the torsion counterpart of WeierstrassCurve.mem_H0_pointCoeff_iff.

noncomputable def WeierstrassCurve.basePointEquivInvariants {K : Type u_1} [Field K] (W : WeierstrassCurve K) [DecidableEq K] : W.toAffine.Point ≃+ ↥(TauCeti.ContCohomology.H0 (TauCeti.AbsoluteGaloisGroup K) W.PointCoeff)

The invariants of E(Kˢ) are the points of E(K), that is H⁰(G_K, E(Kˢ)) ≅ E(K). The two sides are different Lean types, so this canonical isomorphism, and not an equality, is what a cohomological construction starting from E(K) goes through, the Kummer map among them.

@[simp]

theorem WeierstrassCurve.coe_basePointEquivInvariants {K : Type u_1} [Field K] (W : WeierstrassCurve K) [DecidableEq K] (P : W.toAffine.Point) : ↑(W.basePointEquivInvariants P) = W.basePointCoeff P