Selmer groups of a finite etale algebra

The finiteness of the Selmer group proved in TauCeti.RingTheory.DedekindDomain.SInteger.SelmerGroup.Basic is stated for a Dedekind domain with a fraction field. The arithmetic application needs it for a finite etale algebra A over a number field, which is not a field but a product of them. This file makes that step: it forms the product of the Selmer groups of the factors and transports it along a decomposition of A into fields. The number-field case, where both finiteness hypotheses are theorems of Mathlib, is TauCeti.RingTheory.DedekindDomain.SInteger.SelmerGroup.NumberField.

Main definitions

• IsDedekindDomain.selmerGroupPi: the product of the Selmer groups of the factors.
• IsDedekindDomain.selmerGroupOfEquiv: the Selmer group of A, defined by pulling selmerGroupPi back along a decomposition of A into a product of fields.

Main results

• IsDedekindDomain.finite_selmerGroupPi and IsDedekindDomain.finite_selmerGroupOfEquiv: both are finite, for finitely many factors each with finite class group and finitely generated units.

Implementation notes

The decomposition e is an input rather than something extracted from an Algebra.IsEtale hypothesis: Mathlib does not provide the splitting of an etale algebra into fields, and at the application site the decomposition is already in hand.

Where the source this follows takes the finiteness of each factor's Selmer group as an explicit argument, here it is found by instance resolution: IsDedekindDomain.selmerGroup.finite is an instance whose two hypotheses are supplied by IsDedekindDomain.finite_integer_classGroup and Set.unit_fg_of_units, which are themselves instances. So a caller holding [Finite (ClassGroup (B i))], [Monoid.FG (B i)ˣ] and the finiteness of S i gets it unaided; the Set.Finite hypotheses are converted to Finite instances with Set.Finite.to_subtype.

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: that source abbreviates the quotient Kˣ ⧸ (Kˣ)ⁿ as Units.modPow and states the per-factor finiteness as an explicit finite_selmerGroup, whereas here the quotient is spelled out as Mathlib does and the finiteness is the instance IsDedekindDomain.selmerGroup.finite.

noncomputable def IsDedekindDomain.selmerGroupPi {ι : Type u_1} (L : ι → Type u_2) [(i : ι) → Field (L i)] (B : ι → Type u_3) [(i : ι) → CommRing (B i)] [∀ (i : ι), IsDedekindDomain (B i)] [(i : ι) → Algebra (B i) (L i)] [∀ (i : ι), IsFractionRing (B i) (L i)] (S : (i : ι) → Set (HeightOneSpectrum (B i))) (n : ℕ) : Subgroup ((i : ι) → (L i)ˣ ⧸ (powMonoidHom n).range)

The product of the Selmer groups of the field factors.

Equations

• IsDedekindDomain.selmerGroupPi L B S n = Subgroup.pi Set.univ fun (i : ι) => IsDedekindDomain.selmerGroup

@[simp]

theorem IsDedekindDomain.mem_selmerGroupPi_iff {ι : Type u_1} (L : ι → Type u_2) [(i : ι) → Field (L i)] (B : ι → Type u_3) [(i : ι) → CommRing (B i)] [∀ (i : ι), IsDedekindDomain (B i)] [(i : ι) → Algebra (B i) (L i)] [∀ (i : ι), IsFractionRing (B i) (L i)] (S : (i : ι) → Set (HeightOneSpectrum (B i))) (n : ℕ) (x : (i : ι) → (L i)ˣ ⧸ (powMonoidHom n).range) : x ∈ selmerGroupPi L B S n ↔ ∀ (i : ι), x i ∈ selmerGroup

Membership in the product is membership in each factor.

theorem IsDedekindDomain.finite_selmerGroupPi {ι : Type u_1} (L : ι → Type u_2) [(i : ι) → Field (L i)] (B : ι → Type u_3) [(i : ι) → CommRing (B i)] [∀ (i : ι), IsDedekindDomain (B i)] [(i : ι) → Algebra (B i) (L i)] [∀ (i : ι), IsFractionRing (B i) (L i)] (S : (i : ι) → Set (HeightOneSpectrum (B i))) (n : ℕ) [Finite ι] [∀ (i : ι), Finite (ClassGroup (B i))] [∀ (i : ι), Monoid.FG (B i)ˣ] (hS : ∀ (i : ι), (S i).Finite) [NeZero n] : Finite ↥(selmerGroupPi L B S n)

A finite product of Selmer groups is finite.

noncomputable def IsDedekindDomain.selmerGroupOfEquiv {ι : Type u_1} (L : ι → Type u_2) [(i : ι) → Field (L i)] (B : ι → Type u_3) [(i : ι) → CommRing (B i)] [∀ (i : ι), IsDedekindDomain (B i)] [(i : ι) → Algebra (B i) (L i)] [∀ (i : ι), IsFractionRing (B i) (L i)] (S : (i : ι) → Set (HeightOneSpectrum (B i))) (n : ℕ) {A : Type u_4} [CommRing A] (e : Aˣ ⧸ (powMonoidHom n).range ≃* ((i : ι) → (L i)ˣ ⧸ (powMonoidHom n).range)) : Subgroup (Aˣ ⧸ (powMonoidHom n).range)

The Selmer group of the etale algebra A, transported along a decomposition of A into a product of fields.

Equations

• IsDedekindDomain.selmerGroupOfEquiv L B S n e = Subgroup.comap e.toMonoidHom (IsDedekindDomain.selmerGroupPi L B S n)

@[simp]

theorem IsDedekindDomain.mem_selmerGroupOfEquiv_iff {ι : Type u_1} (L : ι → Type u_2) [(i : ι) → Field (L i)] (B : ι → Type u_3) [(i : ι) → CommRing (B i)] [∀ (i : ι), IsDedekindDomain (B i)] [(i : ι) → Algebra (B i) (L i)] [∀ (i : ι), IsFractionRing (B i) (L i)] (S : (i : ι) → Set (HeightOneSpectrum (B i))) (n : ℕ) {A : Type u_4} [CommRing A] (e : Aˣ ⧸ (powMonoidHom n).range ≃* ((i : ι) → (L i)ˣ ⧸ (powMonoidHom n).range)) (x : Aˣ ⧸ (powMonoidHom n).range) : x ∈ selmerGroupOfEquiv L B S n e ↔ ∀ (i : ι), e x i ∈ selmerGroup

Membership in the transported Selmer group is the Selmer condition on each factor.

theorem IsDedekindDomain.finite_selmerGroupOfEquiv {ι : Type u_1} (L : ι → Type u_2) [(i : ι) → Field (L i)] (B : ι → Type u_3) [(i : ι) → CommRing (B i)] [∀ (i : ι), IsDedekindDomain (B i)] [(i : ι) → Algebra (B i) (L i)] [∀ (i : ι), IsFractionRing (B i) (L i)] (S : (i : ι) → Set (HeightOneSpectrum (B i))) (n : ℕ) {A : Type u_4} [CommRing A] [Finite ι] [∀ (i : ι), Finite (ClassGroup (B i))] [∀ (i : ι), Monoid.FG (B i)ˣ] (hS : ∀ (i : ι), (S i).Finite) [NeZero n] (e : Aˣ ⧸ (powMonoidHom n).range ≃* ((i : ι) → (L i)ˣ ⧸ (powMonoidHom n).range)) : Finite ↥(selmerGroupOfEquiv L B S n e)

The Selmer group of a finite etale algebra is finite.