The fundamental exact sequence of the Selmer group, and its finiteness

Let R be a Dedekind domain with fraction field K, let S be a set of height-one primes of R and let n : ℕ. Mathlib defines the Selmer group K⟮S, n⟯ as the subgroup of Kˣ ⧸ (Kˣ)ⁿ of classes whose v-adic valuation is divisible by n for every v ∉ S, and its module docstring records as TODO both "maps in the sequence", "proofs of exactness of the sequence" and "proofs of finiteness for global fields". This file supplies all three, in the form

1 → 𝒪_S(K)ˣ / (𝒪_S(K)ˣ)ⁿ → K⟮S, n⟯ → Cl_S(R)[n] → 1

where 𝒪_S(K) = Set.integer S K is the ring of S-integers and the S-class group Cl_S(R) is ClassGroup (S.integer K).

The dictionary that makes it work

The S-integers are a Dedekind domain with fraction field K whose height-one primes are exactly the v ∉ S (IsDedekindDomain.integerHeightOneSpectrumEquiv), valuation-compatibly (IsDedekindDomain.valuation_integerHeightOneSpectrumEquiv). Under that dictionary the Selmer condition on a class u(Kˣ)ⁿ says exactly that the principal fractional ideal (u) of 𝒪_S has all of its multiplicities divisible by n — this is mk_mem_selmerGroup_iff_mem_unitsNDivisible — so the right-hand map is the n-th root class map TauCeti.AlgebraicGeometry.WeilDivisor.nthRootClass of the S-integers, descended along the surjection fromUnitsNDivisible.

Main definitions

Mathlib's Mathlib/RingTheory/DedekindDomain/SelmerGroup.lean already gives the S = ∅ case of the left-hand map, as IsDedekindDomain.selmerGroup.fromUnit and fromUnitLift. The general-S maps below therefore live in the same IsDedekindDomain.selmerGroup namespace and follow the same from…/to… scheme.

• IsDedekindDomain.selmerGroup.fromSUnit: the left-hand map, from the S-units to K⟮S, n⟯.
• IsDedekindDomain.selmerGroup.fromSUnitLift: the same map after dividing out n-th powers of S-units, which is the left-hand map of the exact sequence proper.
• IsDedekindDomain.selmerGroup.fromUnitsNDivisible: the surjection onto K⟮S, n⟯ from the units of K whose principal 𝒪_S-ideal is n-divisible.
• IsDedekindDomain.selmerGroup.toClassGroup: the right-hand map, to ClassGroup (S.integer K).

Main results

• IsDedekindDomain.mk_mem_selmerGroup_iff_mem_unitsNDivisible: the Selmer condition on a representative is n-divisibility of its principal 𝒪_S-ideal.
• IsDedekindDomain.selmerGroup.fromSUnitLift_injective: exactness on the left — the left-hand map is injective, because an n-th root in K of an S-unit is itself an S-unit.
• IsDedekindDomain.selmerGroup.ker_toClassGroup: exactness in the middle — a Selmer class has trivial n-th-root ideal class exactly when an S-unit represents it.
• IsDedekindDomain.selmerGroup.range_toClassGroup: exactness on the right — the image is the n-torsion of the S-class group. (Surjectivity onto the whole class group is false in general.) Of the three, only this one needs n ≠ 0.
• IsDedekindDomain.selmerGroup.finite: the Selmer group K⟮S, n⟯ is finite when the S-class group is finite, the S-units are finitely generated and n ≠ 0.

Finiteness is not automatic for a general Dedekind domain — it already fails for R = K a field whose unit group is not n-divisible of finite index — and the exact sequence isolates what is needed: [Group.FG (S.unit K)] and [Finite (ClassGroup (S.integer K))], which are exactly the hypotheses selmerGroup.finite takes. Both are on hand over the base ring, as the instances Set.unit_fg_of_units and IsDedekindDomain.finite_integer_classGroup, so a caller holding [Finite (ClassGroup R)], [Monoid.FG Rˣ] and [Finite S] gets the finiteness by instance resolution. For R the ring of integers of a number field those are the class number theorem and Dirichlet's unit theorem.

References

Adapted from Michael Stoll's elliptic-curves formalisation (github.com/MichaelStollBayreuth/EllipticCurves, EllipticCurves/Mathlib/SelmerGroup.lean at the EllipticCurves roadmap's pin 66889eada51a, Apache 2.0, by Michael Stoll), whose treatment this follows. The names differ: the substrate that source keeps in its own FractionalIdeal file is already here as TauCeti.AlgebraicGeometry.WeilDivisor.nthRootClass and its neighbours, and the S-integer dictionary is already here under IsDedekindDomain.integer*, so only the Selmer layer itself is adapted, and it is named after Mathlib's selmerGroup API rather than after the source. Following this repository's convention for adapted material, the upstream authorship is credited here rather than in the copyright header.

The Selmer condition as n-divisibility of an ideal

theorem IsDedekindDomain.mk_mem_selmerGroup_iff_mem_unitsNDivisible {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) (n : ℕ) (u : Kˣ) : ↑u ∈ selmerGroup ↔ u ∈ TauCeti.AlgebraicGeometry.WeilDivisor.unitsNDivisible (↥(S.integer K)) K n

The class of u lies in the Selmer group K⟮S, n⟯ exactly when the principal fractional ideal (u) of the S-integers has all of its multiplicities divisible by n. This is the dictionary that turns the Selmer condition into a statement about ideals of 𝒪_S, and hence lets the n-th root class map act as the right-hand map of the exact sequence.

The left-hand map: S-units into the Selmer group

noncomputable def IsDedekindDomain.selmerGroup.fromSUnit {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) (n : ℕ) : ↥(S.unit K) →* ↥selmerGroup

The class of an S-unit lies in the Selmer group K⟮S, n⟯: away from S an S-unit has trivial valuation, so in particular a valuation divisible by n.

Equations

• IsDedekindDomain.selmerGroup.fromSUnit K S n = { toFun := fun (x : ↥(S.unit K)) => ⟨↑↑x, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem IsDedekindDomain.selmerGroup.coe_fromSUnit {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) (n : ℕ) (x : ↥(S.unit K)) : ↑((fromSUnit K S n) x) = ↑↑x

The Selmer class of an S-unit is, underneath the subtype, just its class in Kˣ ⧸ (Kˣ)ⁿ.

noncomputable def IsDedekindDomain.selmerGroup.fromSUnitLift {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) (n : ℕ) : ↥(S.unit K) ⧸ (powMonoidHom n).range →* ↥selmerGroup

The left-hand map of the fundamental exact sequence: an S-unit modulo n-th powers of S-units maps to the Selmer group K⟮S, n⟯.

Equations

• IsDedekindDomain.selmerGroup.fromSUnitLift K S n = QuotientGroup.lift (powMonoidHom n).range (IsDedekindDomain.selmerGroup.fromSUnit K S n) ⋯

@[simp]

theorem IsDedekindDomain.selmerGroup.fromSUnitLift_mk {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) (n : ℕ) (x : ↥(S.unit K)) : (fromSUnitLift K S n) ↑x = (fromSUnit K S n) x

The defining property of fromSUnitLift: on the class of an S-unit it agrees with the map fromSUnit it descends from.

@[simp]

theorem IsDedekindDomain.selmerGroup.range_fromSUnitLift {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) (n : ℕ) : (fromSUnitLift K S n).range = (fromSUnit K S n).range

Dividing out the n-th powers of S-units does not change the image: the two left-hand maps have the same range.

theorem IsDedekindDomain.selmerGroup.fromSUnitLift_injective {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) (n : ℕ) : Function.Injective ⇑(fromSUnitLift K S n)

Exactness on the left of the fundamental exact sequence. The left-hand map is injective: an S-unit that becomes an n-th power in K is already the n-th power of an S-unit. What makes this work is that an n-th root y of an S-unit is again an S-unit: away from S the relation n * ord_v(y) = ord_v(x) = 0 forces ord_v(y) = 0.

Like ker_toClassGroup, and unlike the exactness on the right, this needs no n ≠ 0: for n = 0 both sides divide out the trivial subgroup and the claim degenerates to the injectivity of S.unit K ≤ Kˣ.

The surjection from the n-divisible units

noncomputable def IsDedekindDomain.selmerGroup.fromUnitsNDivisible {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) (n : ℕ) : ↥(TauCeti.AlgebraicGeometry.WeilDivisor.unitsNDivisible (↥(S.integer K)) K n) →* ↥selmerGroup

The surjection from the units of K whose principal 𝒪_S-ideal is n-divisible onto the Selmer group K⟮S, n⟯, given by taking the class modulo n-th powers.

Equations

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

@[simp]

theorem IsDedekindDomain.selmerGroup.coe_fromUnitsNDivisible {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) (n : ℕ) (u : ↥(TauCeti.AlgebraicGeometry.WeilDivisor.unitsNDivisible (↥(S.integer K)) K n)) : ↑((fromUnitsNDivisible K S n) u) = ↑↑u

Underneath the codomain restriction, fromUnitsNDivisible is the quotient map.

theorem IsDedekindDomain.selmerGroup.fromUnitsNDivisible_surjective {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) (n : ℕ) : Function.Surjective ⇑(fromUnitsNDivisible K S n)

Every Selmer class is represented by an n-divisible unit. This is what lets the n-th root class map be transported from unitsNDivisible to the Selmer group.

The right-hand map, and exactness

noncomputable def IsDedekindDomain.selmerGroup.toClassGroup {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) (n : ℕ) : ↥selmerGroup →* ClassGroup ↥(S.integer K)

The right-hand map of the fundamental exact sequence: a Selmer class is sent to the ideal class of the n-th root of the principal ideal (u) of any representative u, in the class group of the S-integers. Obtained by descending the n-th root class map along fromUnitsNDivisible.

Equations

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

@[simp]

theorem IsDedekindDomain.selmerGroup.toClassGroup_fromUnitsNDivisible {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) (n : ℕ) (u : ↥(TauCeti.AlgebraicGeometry.WeilDivisor.unitsNDivisible (↥(S.integer K)) K n)) : (toClassGroup K S n) ((fromUnitsNDivisible K S n) u) = (TauCeti.AlgebraicGeometry.WeilDivisor.nthRootClass (↥(S.integer K)) K n) u

The defining property of toClassGroup: on the class of an n-divisible unit it agrees with the n-th root class map it descends from. Every computation with the right-hand map goes through this lemma, after fromUnitsNDivisible_surjective supplies a representative.

theorem IsDedekindDomain.selmerGroup.ker_toClassGroup {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) (n : ℕ) : (toClassGroup K S n).ker = (fromSUnit K S n).range

Exactness in the middle of the fundamental exact sequence. A Selmer class has trivial n-th-root ideal class exactly when it is represented by an S-unit.

No [NeZero n] is needed, unlike on the right-hand exactness below: nthRootClass_eq_one_iff is stated here for every n, degenerate n = 0 included.

theorem IsDedekindDomain.selmerGroup.range_toClassGroup {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) (n : ℕ) [NeZero n] : (toClassGroup K S n).range = (powMonoidHom n).ker

Exactness on the right of the fundamental exact sequence. The image of toClassGroup is the n-torsion of the class group of the S-integers; surjectivity onto the full class group fails in general.

Finiteness

theorem IsDedekindDomain.selmerGroup.finite_of_finite_ker_powMonoidHom {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) (n : ℕ) [Finite ↥(powMonoidHom n).ker] [Group.FG ↥(S.unit K)] [NeZero n] : Finite ↥selmerGroup

The Selmer group K⟮S, n⟯ is finite as soon as the n-torsion of the S-class group is, the S-units are finitely generated and n ≠ 0.

Both halves of MonoidHom.finite_iff_finite_ker_range for toClassGroup are in hand. The kernel is the image of fromSUnitLift by ker_toClassGroup, finite because its source is the quotient of the finitely generated group of S-units by its n-th powers. The range is the n-torsion of the class group by range_toClassGroup, which is exactly the hypothesis.

Only that n-torsion is needed, never the whole class group: range_toClassGroup says the image of toClassGroup never exceeds it. finite below is this theorem for a finite class group.

instance IsDedekindDomain.selmerGroup.finite {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) (n : ℕ) [Finite (ClassGroup ↥(S.integer K))] [Group.FG ↥(S.unit K)] [NeZero n] : Finite ↥selmerGroup

The Selmer group K⟮S, n⟯ is finite, provided that the S-class group is finite, that the S-units are finitely generated and that n ≠ 0. This discharges the TODO "proofs of finiteness for global fields" of Mathlib/RingTheory/DedekindDomain/SelmerGroup.lean.

This is finite_of_finite_ker_powMonoidHom for a finite class group, in which every subgroup — the n-torsion included — is finite.

The two hypotheses are exactly what the proof consumes. They are in turn supplied by the arithmetic over the base ring: IsDedekindDomain.finite_integer_classGroup and Set.unit_fg_of_units are instances, so a caller holding [Finite (ClassGroup R)], [Monoid.FG Rˣ] and [Finite S] — for R the ring of integers of a number field, the class number theorem and Dirichlet's unit theorem — still gets this by instance resolution.