Unramified Kummer classes at good reduction

For a Weierstrass curve over a nonarchimedean local field K, the unramified subgroup of H¹(K, E[m]) is the kernel of restriction to inertia. The coefficient module uses the separable closure, so inertia is transported from the algebraic closure through TauCeti.absoluteGaloisGroupRestrictEquiv.

At good reduction, if m is prime to the residue characteristic, every Kummer class is unramified. Indeed inertia fixes every m-division point of a rational point, so the cocycle σ ↦ σ Q - Q vanishes on inertia. This gives the containment of the local Kummer condition in the unramified local condition used to control ramification of Selmer classes. Consequently a Selmer class restricts to an unramified class at each nonarchimedean local field in its defining family where the equation has good reduction and m is a residue unit. Unramifiedness is also stable under restriction to any extension of nonarchimedean local fields, since the inertia subgroup of the larger field maps into that of the smaller one. This carries the local conditions at the places of a number field to the places of a finite extension, such as the m-division field, as the proof of the finiteness of Selmer groups requires (Silverman X.4.2).

References

• J. Silverman, The Arithmetic of Elliptic Curves, VII.4.1, VIII.1.5 and X.4.

noncomputable def WeierstrassCurve.unramifiedTorsionCohomology {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (W : WeierstrassCurve K) (m : ℕ) : AddSubgroup (TauCeti.ContCohomology.H1 (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m))

The unramified classes in H¹(K, E[m]): the kernel of restriction to inertia, transported to the automorphisms of the separable closure used by W.TorsionCoeff m.

@[simp]

theorem WeierstrassCurve.mem_unramifiedTorsionCohomology_iff {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (W : WeierstrassCurve K) (m : ℕ) {c : TauCeti.ContCohomology.H1 (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m)} : c ∈ W.unramifiedTorsionCohomology m ↔ (TauCeti.ContCohomology.explicitRes1 (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m) (Subgroup.map (TauCeti.absoluteGaloisGroupRestrictEquiv K).toMonoidHom (TauCeti.inertiaSubgroup K))) c = 0

A class is unramified exactly when its restriction to inertia is zero.

theorem WeierstrassCurve.torsionRes_mem_unramifiedTorsionCohomology {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (W : WeierstrassCurve K) (m : ℕ) {L : Type u_2} [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] (τ : SeparableClosure K →ₐ[K] SeparableClosure L) {c : TauCeti.ContCohomology.H1 (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m)} (hc : c ∈ W.unramifiedTorsionCohomology m) : (W.torsionRes τ m) c ∈ (W.baseChange L).unramifiedTorsionCohomology m

Unramified classes restrict to unramified classes. For an extension L/K of nonarchimedean local fields and a K-embedding τ : Kˢ → Lˢ of separable closures, restriction H¹(K, E[m]) → H¹(L, E[m]) along τ sends unramified classes to unramified classes, because the inertia subgroup of L maps into that of K. No reduction hypothesis on W is needed.

theorem WeierstrassCurve.instIsElliptic_tauCeti {K : Type u_1} [Field K] [ValuativeRel K] (W : WeierstrassCurve K) [IsIntegral (↥(ValuativeRel.valuation K).integer) W] [(integralModel (↥(ValuativeRel.valuation K).integer) W).IsElliptic] : W.IsElliptic

theorem WeierstrassCurve.smul_pointCoeff_eq_self_of_mem_inertiaSubgroup {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {W : WeierstrassCurve K} {m : ℕ} [IsIntegral (↥(ValuativeRel.valuation K).integer) W] [(integralModel (↥(ValuativeRel.valuation K).integer) W).IsElliptic] (hm : ↑m ≠ 0) {P : W.toAffine.Point} {Q : W.PointCoeff} (hQ : m • Q = W.basePointCoeff P) {σ : Gal(AlgebraicClosure K/K)} (hσ : σ ∈ TauCeti.inertiaSubgroup K) : (TauCeti.absoluteGaloisGroupRestrictEquiv K) σ • Q = Q

At good reduction, inertia fixes an m-division point of a K-rational point when m is prime to the residue characteristic. The action here is on the discrete coefficient module over the separable closure.

theorem WeierstrassCurve.kummerCocycle_eq_zero_of_mem_inertiaSubgroup {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {W : WeierstrassCurve K} {m : ℕ} [IsIntegral (↥(ValuativeRel.valuation K).integer) W] [(integralModel (↥(ValuativeRel.valuation K).integer) W).IsElliptic] (hm : ↑m ≠ 0) {P : W.toAffine.Point} {Q : W.PointCoeff} (hQ : m • Q = W.basePointCoeff P) {σ : Gal(AlgebraicClosure K/K)} (hσ : σ ∈ TauCeti.inertiaSubgroup K) : kummerCocycle hQ ((TauCeti.absoluteGaloisGroupRestrictEquiv K) σ) = 0

The Kummer cocycle of a division point of a rational point vanishes on inertia at good reduction, when its multiplier is prime to the residue characteristic.

theorem WeierstrassCurve.kummerMap_mem_unramifiedTorsionCohomology {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (W : WeierstrassCurve K) (m : ℕ) [IsIntegral (↥(ValuativeRel.valuation K).integer) W] [(integralModel (↥(ValuativeRel.valuation K).integer) W).IsElliptic] (hmres : ↑m ≠ 0) (P : W.toAffine.Point) : (W.kummerMap m ⋯) P ∈ W.unramifiedTorsionCohomology m

At good reduction, the Kummer class of a rational point is unramified when the multiplier is prime to the residue characteristic.

theorem WeierstrassCurve.range_kummerMap_le_unramifiedTorsionCohomology {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (W : WeierstrassCurve K) (m : ℕ) [IsIntegral (↥(ValuativeRel.valuation K).integer) W] [(integralModel (↥(ValuativeRel.valuation K).integer) W).IsElliptic] (hmres : ↑m ≠ 0) : (W.kummerMap m ⋯).range ≤ W.unramifiedTorsionCohomology m

At good reduction away from the multiplier, the local Kummer condition is contained in the unramified local condition.

theorem WeierstrassCurve.torsionRes_mem_unramifiedTorsionCohomology_of_mem_selmerGroup {K : Type u_1} [Field K] (W : WeierstrassCurve K) {ι : Type u_2} {L : ι → Type u_3} [(i : ι) → Field (L i)] [(i : ι) → Algebra K (L i)] (τ : (i : ι) → SeparableClosure K →ₐ[K] SeparableClosure (L i)) (i : ι) [ValuativeRel (L i)] [TopologicalSpace (L i)] [IsNonarchimedeanLocalField (L i)] [IsIntegral (↥(ValuativeRel.valuation (L i)).integer) (W.baseChange (L i))] [(integralModel (↥(ValuativeRel.valuation (L i)).integer) (W.baseChange (L i))).IsElliptic] {m : ℕ} (hmres : ↑m ≠ 0) {c : TauCeti.ContCohomology.H1 (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m)} (hc : c ∈ W.selmerGroup τ m) : (W.torsionRes (τ i) m) c ∈ (W.baseChange (L i)).unramifiedTorsionCohomology m

A Selmer class is unramified at each nonarchimedean local field in its defining family where the equation has good reduction and the multiplier is prime to the residue characteristic. No good-reduction assumption is made at the other fields in the family.

Classes unramified outside S

noncomputable def WeierstrassCurve.unramifiedOutsideTorsionCohomology {R : Type u_4} [CommRing R] [IsDedekindDomain R] [∀ (v : IsDedekindDomain.HeightOneSpectrum R), Finite (R ⧸ v.asIdeal)] {K : Type u_5} [Field K] [Algebra R K] [IsFractionRing R K] (W : WeierstrassCurve K) (τ : (v : IsDedekindDomain.HeightOneSpectrum R) → SeparableClosure K →ₐ[K] SeparableClosure (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) (S : Set (IsDedekindDomain.HeightOneSpectrum R)) (m : ℕ) : AddSubgroup (TauCeti.ContCohomology.H1 (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m))

The classes of H¹(G_K, E[m]) unramified outside S: those whose restriction to the completion K_v along τ v, for every prime v ∉ S, is unramified, that is, vanishes on the inertia subgroup of K_v.

@[simp]

theorem WeierstrassCurve.mem_unramifiedOutsideTorsionCohomology_iff {R : Type u_4} [CommRing R] [IsDedekindDomain R] [∀ (v : IsDedekindDomain.HeightOneSpectrum R), Finite (R ⧸ v.asIdeal)] {K : Type u_5} [Field K] [Algebra R K] [IsFractionRing R K] {W : WeierstrassCurve K} {τ : (v : IsDedekindDomain.HeightOneSpectrum R) → SeparableClosure K →ₐ[K] SeparableClosure (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {S : Set (IsDedekindDomain.HeightOneSpectrum R)} {m : ℕ} {c : TauCeti.ContCohomology.H1 (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m)} : c ∈ W.unramifiedOutsideTorsionCohomology τ S m ↔ ∀ v ∉ S, (W.torsionRes (τ v) m) c ∈ (W.baseChange (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)).unramifiedTorsionCohomology m

A class is unramified outside S exactly when its restriction to every K_v with v ∉ S is unramified.

theorem WeierstrassCurve.selmerGroup_le_unramifiedOutsideTorsionCohomology {R : Type u_4} [CommRing R] [IsDedekindDomain R] [∀ (v : IsDedekindDomain.HeightOneSpectrum R), Finite (R ⧸ v.asIdeal)] {K : Type u_5} [Field K] [Algebra R K] [IsFractionRing R K] {W : WeierstrassCurve K} {τ : (v : IsDedekindDomain.HeightOneSpectrum R) → SeparableClosure K →ₐ[K] SeparableClosure (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {S : Set (IsDedekindDomain.HeightOneSpectrum R)} {m : ℕ} (hgood : ∀ v ∉ S, ∃ (x : IsIntegral (↥(ValuativeRel.valuation (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)).integer) (W.baseChange (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v))), (integralModel (↥(ValuativeRel.valuation (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)).integer) (W.baseChange (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v))).IsElliptic) (hS : ∀ v ∉ S, ↑m ∉ v.asIdeal) : W.selmerGroup τ m ≤ W.unramifiedOutsideTorsionCohomology τ S m

Selmer classes are unramified outside the bad primes. If W has good reduction at every prime v ∉ S and no prime outside S divides m, then every class of the m-Selmer group relative to the completions K_v is unramified outside S.