Selmer groups of fraction fields of Dedekind domains

Let $K$ be the field of fractions of a Dedekind domain $R$. For any set $S$ of prime ideals in the height one spectrum of $R$, and for any natural number $n$, the Selmer group $K(S,n)$ is defined to be the subgroup of the unit group $K^{\times }$ modulo $n$-th powers where each element has $v$-adic valuation divisible by $n$ for all prime ideals $v$ away from $S$. In other words, this is precisely $$K(S,n):=\{x(K^{\times }{)}^n\in K^{\times }/(K^{\times }{)}^n\mid \mathrm{\forall }v\notin S,{\mathrm{ord}}_v(x)\equiv 0(\mathrm{mod}n)\}.$$

There is a fundamental short exact sequence $$1\to R_S^{\times }/(R_S^{\times }{)}^n\to K(S,n)\to {\mathrm{Cl}}_S(R)[n]\to 0,$$ where $R_S^{\times }$ is the $S$-unit group of $R$ and ${\mathrm{Cl}}_S(R)$ is the $S$-class group of $R$. If the flanking groups are both finite, then $K(S,n)$ is finite by the first isomorphism theorem. Such is the case when $R$ is the ring of integers of a number field $K$, $S$ is finite, and $n$ is positive, in which case $R_S^{\times }$ is finitely generated by Dirichlet's unit theorem and ${\mathrm{Cl}}_S(R)$ is finite by the class number theorem.

This file defines the Selmer group $K(S,n)$ and some basic facts.

Main definitions

• IsDedekindDomain.selmerGroup: the Selmer group.
• TODO: maps in the sequence.

Main statements

• TODO: proofs of exactness of the sequence.
• TODO: proofs of finiteness for global fields.

Notations

• K⟮S, n⟯: the Selmer group with parameters K, S, and n.

Implementation notes

The Selmer group is typically defined as a subgroup of the Galois cohomology group $H^1(K,{\mu }_n)$ with certain local conditions defined by $v$-adic valuations, where ${\mu }_n$ is the group of $n$-th roots of unity over a separable closure of $K$. Here $H^1(K,{\mu }_n)$ is identified with $K^{\times }/(K^{\times }{)}^n$ by the long exact sequence from Kummer theory and Hilbert's theorem 90, and the fundamental short exact sequence becomes an easy consequence of the snake lemma. This file will define all the maps explicitly for computational purposes, but isomorphisms to the Galois cohomological definition will be provided when possible.

References

https://doc.sagemath.org/html/en/reference/number_fields/sage/rings/number_field/selmer_group.html

Tags

class group, selmer group, unit group

Valuations of non-zero elements

def IsDedekindDomain.HeightOneSpectrum.valuationOfNeZeroToFun {R : Type u} [CommRing R] [IsDedekindDomain R] {K : Type v} [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (x : Kˣ) : Multiplicative ℤ

The multiplicative v-adic valuation on Kˣ.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.valuationOfNeZeroToFun_eq {R : Type u} [CommRing R] [IsDedekindDomain R] {K : Type v} [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (x : Kˣ) : ↑(v.valuationOfNeZeroToFun x) = v.valuation ↑x

def IsDedekindDomain.HeightOneSpectrum.valuationOfNeZero {R : Type u} [CommRing R] [IsDedekindDomain R] {K : Type v} [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) : Kˣ →* Multiplicative ℤ

The multiplicative v-adic valuation on Kˣ.

Equations

• v.valuationOfNeZero = { toFun := v.valuationOfNeZeroToFun, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.valuationOfNeZero_eq {R : Type u} [CommRing R] [IsDedekindDomain R] {K : Type v} [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (x : Kˣ) : ↑(v.valuationOfNeZero x) = v.valuation ↑x

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.valuation_of_unit_eq {R : Type u} [CommRing R] [IsDedekindDomain R] {K : Type v} [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (x : Rˣ) : v.valuationOfNeZero ((Units.map ↑(algebraMap R K)) x) = 1

def IsDedekindDomain.HeightOneSpectrum.valuationOfNeZeroMod {R : Type u} [CommRing R] [IsDedekindDomain R] {K : Type v} [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (n : ℕ) : Kˣ ⧸ (powMonoidHom n).range →* Multiplicative (ZMod n)

The multiplicative v-adic valuation on Kˣ modulo n-th powers.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.valuation_of_unit_mod_eq {R : Type u} [CommRing R] [IsDedekindDomain R] {K : Type v} [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (n : ℕ) (x : Rˣ) : (v.valuationOfNeZeroMod n) ↑((Units.map ↑(algebraMap R K)) x) = 1

Selmer groups

def IsDedekindDomain.selmerGroup {R : Type u} [CommRing R] [IsDedekindDomain R] {K : Type v} [Field K] [Algebra R K] [IsFractionRing R K] {S : Set (IsDedekindDomain.HeightOneSpectrum R)} {n : ℕ} : Subgroup (Kˣ ⧸ (powMonoidHom n).range)

The Selmer group K⟮S, n⟯.

Equations

• IsDedekindDomain.selmerGroup = { carrier := {x : Kˣ ⧸ (powMonoidHom n).range | ∀ v ∉ S, (v.valuationOfNeZeroMod n) x = 1}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

theorem IsDedekindDomain.selmerGroup.monotone {R : Type u} [CommRing R] [IsDedekindDomain R] {K : Type v} [Field K] [Algebra R K] [IsFractionRing R K] {S : Set (IsDedekindDomain.HeightOneSpectrum R)} {S' : Set (IsDedekindDomain.HeightOneSpectrum R)} {n : ℕ} (hS : S ≤ S') : IsDedekindDomain.selmerGroup ≤ IsDedekindDomain.selmerGroup

def IsDedekindDomain.selmerGroup.valuation {R : Type u} [CommRing R] [IsDedekindDomain R] {K : Type v} [Field K] [Algebra R K] [IsFractionRing R K] {S : Set (IsDedekindDomain.HeightOneSpectrum R)} {n : ℕ} : { x : Kˣ ⧸ (powMonoidHom n).range // x ∈ IsDedekindDomain.selmerGroup } →* ↑S → Multiplicative (ZMod n)

The multiplicative v-adic valuations on K⟮S, n⟯ for all v ∈ S.

Equations

• One or more equations did not get rendered due to their size.

theorem IsDedekindDomain.selmerGroup.valuation_ker_eq {R : Type u} [CommRing R] [IsDedekindDomain R] {K : Type v} [Field K] [Algebra R K] [IsFractionRing R K] {S : Set (IsDedekindDomain.HeightOneSpectrum R)} {n : ℕ} : IsDedekindDomain.selmerGroup.valuation.ker = IsDedekindDomain.selmerGroup.subgroupOf IsDedekindDomain.selmerGroup

def IsDedekindDomain.selmerGroup.fromUnit {R : Type u} [CommRing R] [IsDedekindDomain R] {K : Type v} [Field K] [Algebra R K] [IsFractionRing R K] {n : ℕ} : Rˣ →* { x : Kˣ ⧸ (powMonoidHom n).range // x ∈ IsDedekindDomain.selmerGroup }

The natural homomorphism from Rˣ to K⟮∅, n⟯.

Equations

• IsDedekindDomain.selmerGroup.fromUnit = { toFun := fun (x : Rˣ) => ⟨↑((Units.map ↑(algebraMap R K)) x), ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

theorem IsDedekindDomain.selmerGroup.fromUnit_ker {R : Type u} [CommRing R] [IsDedekindDomain R] {K : Type v} [Field K] [Algebra R K] [IsFractionRing R K] {n : ℕ} [hn : Fact (0 < n)] : IsDedekindDomain.selmerGroup.fromUnit.ker = (powMonoidHom n).range

def IsDedekindDomain.selmerGroup.fromUnitLift {R : Type u} [CommRing R] [IsDedekindDomain R] {K : Type v} [Field K] [Algebra R K] [IsFractionRing R K] {n : ℕ} [Fact (0 < n)] : Rˣ ⧸ (powMonoidHom n).range →* { x : Kˣ ⧸ (powMonoidHom n).range // x ∈ IsDedekindDomain.selmerGroup }

The injection induced by the natural homomorphism from Rˣ to K⟮∅, n⟯.

Equations

• IsDedekindDomain.selmerGroup.fromUnitLift = (QuotientGroup.kerLift IsDedekindDomain.selmerGroup.fromUnit).comp (QuotientGroup.quotientMulEquivOfEq ⋯).symm.toMonoidHom

theorem IsDedekindDomain.selmerGroup.fromUnitLift_injective {R : Type u} [CommRing R] [IsDedekindDomain R] {K : Type v} [Field K] [Algebra R K] [IsFractionRing R K] {n : ℕ} [Fact (0 < n)] : Function.Injective ⇑IsDedekindDomain.selmerGroup.fromUnitLift