Primes above a set of primes, and the Selmer group relative to them

For an injective algebra map of commutative rings R → B with B Dedekind, only finitely many nonzero prime ideals of B lie over a given nonzero prime v of R. This does not require integrality or a Dedekind hypothesis on R.

For domains R and B with B integral over R, contraction defines HeightOneSpectrum.under R. For a set S of primes of R, IsDedekindDomain.HeightOneSpectrum.primesAbove R B S is its preimage under contraction. When B is Dedekind and the algebra map is injective, this preimage is finite whenever S is. The Selmer group of the fraction field of B relative to these primes is IsDedekindDomain.selmerGroupAbove R B L S n, Mathlib's L⟮primesAbove R B S, n⟯.

Main definitions

• IsDedekindDomain.HeightOneSpectrum.primesAbove: the primes of B above a set of primes of R, as a preimage under HeightOneSpectrum.under.
• IsDedekindDomain.selmerGroupAbove: the n-Selmer group of L relative to the primes of B above S.

Main results

• IsDedekindDomain.HeightOneSpectrum.liesOver_under: the LiesOver instance relating a prime to its contraction, which the under-indexed results downstream need.
• IsDedekindDomain.HeightOneSpectrum.under_surjective: every height one prime of R lies under one of B.
• IsDedekindDomain.HeightOneSpectrum.under_under: contraction through a tower agrees with direct contraction.
• IsDedekindDomain.HeightOneSpectrum.liesOverTowerEquiv: primes over a fixed prime correspond to pairs of successive primes through an intermediate integral domain.
• IsDedekindDomain.HeightOneSpectrum.mem_primesAbove_iff: w lies above S iff HeightOneSpectrum.under R w ∈ S.
• IsDedekindDomain.HeightOneSpectrum.primesAbove_finite: finitely many primes lie above a finite set.
• IsDedekindDomain.HeightOneSpectrum.tendsto_under_cofinite: consequently, contraction tends to the cofinite filter along the cofinite filter; IsDedekindDomain.HeightOneSpectrum.tendsto_under_cofinite_of_isFractionRing is the variant for rings mapping compatibly to a common nontrivial algebra over a fraction field.
• IsDedekindDomain.HeightOneSpectrum.finite_liesOver: finitely many height one primes lie over a given one.

Provenance

Adapted from Michael Stoll's EllipticCurves project (github.com/MichaelStollBayreuth/EllipticCurves, Apache-2.0, at commit 66889eada51a), EllipticCurves/Mathlib/Basic.lean, section DedekindDomain. The source carries its own HeightOneSpectrum.below; at our Mathlib pin that map is HeightOneSpectrum.under, which is used here instead.

The source is written against Lean v4.32.0; this is a forward port.

instance IsDedekindDomain.HeightOneSpectrum.liesOver_under (R : Type u_1) [CommRing R] (B : Type u_2) [CommRing B] [Algebra R B] [IsDomain R] [IsDomain B] [Algebra.IsIntegral R B] (w : HeightOneSpectrum B) : w.asIdeal.LiesOver (under R w).asIdeal

A height one prime of B lies over its own contraction to R.

Mathlib's Ideal.over_under is this statement for Ideal.under, but instance search does not see through the HeightOneSpectrum.asIdeal projection to reach it, so it is registered here. Results stated at under R w and consuming a LiesOver hypothesis, such as HeightOneSpectrum.valuation_liesOver, do not fire without it.

theorem IsDedekindDomain.HeightOneSpectrum.under_surjective (R : Type u_1) [CommRing R] (B : Type u_2) [CommRing B] [Algebra R B] [IsDomain R] [IsDomain B] [Algebra.IsIntegral R B] [FaithfulSMul R B] : Function.Surjective (under R)

Every height one prime of R lies under one of B, for an integral extension of domains with injective algebra map: contraction HeightOneSpectrum B → HeightOneSpectrum R is surjective.

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.under_under (R : Type u_1) [CommRing R] [IsDomain R] {A : Type u_3} {C : Type u_4} [CommRing A] [IsDomain A] [CommRing C] [IsDomain C] [Algebra A R] [Algebra R C] [Algebra A C] [IsScalarTower A R C] [Algebra.IsIntegral A R] [Algebra.IsIntegral R C] (w : HeightOneSpectrum C) : under A (under R w) = under A w

Contracting a height-one prime through an intermediate integral domain agrees with direct contraction.

def IsDedekindDomain.HeightOneSpectrum.liesOverTowerEquiv (R : Type u_1) [CommRing R] [IsDomain R] {A : Type u_3} {C : Type u_4} [CommRing A] [CommRing C] [IsDomain C] [Algebra A R] [Algebra R C] [Algebra A C] [IsScalarTower A R C] [Algebra.IsIntegral R C] (v : HeightOneSpectrum A) : (w : { w : HeightOneSpectrum R // w.asIdeal.LiesOver v.asIdeal }) × { u : HeightOneSpectrum C // u.asIdeal.LiesOver (↑w).asIdeal } ≃ { u : HeightOneSpectrum C // u.asIdeal.LiesOver v.asIdeal }

Height-one primes over v correspond to pairs of successive height-one primes through an intermediate integral domain.

Equations

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

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.liesOverTowerEquiv_apply (R : Type u_1) [CommRing R] [IsDomain R] {A : Type u_3} {C : Type u_4} [CommRing A] [CommRing C] [IsDomain C] [Algebra A R] [Algebra R C] [Algebra A C] [IsScalarTower A R C] [Algebra.IsIntegral R C] (v : HeightOneSpectrum A) (p : (w : { w : HeightOneSpectrum R // w.asIdeal.LiesOver v.asIdeal }) × { u : HeightOneSpectrum C // u.asIdeal.LiesOver (↑w).asIdeal }) : ↑((liesOverTowerEquiv R v) p) = ↑p.snd

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.liesOverTowerEquiv_symm_apply_fst (R : Type u_1) [CommRing R] [IsDomain R] {A : Type u_3} {C : Type u_4} [CommRing A] [CommRing C] [IsDomain C] [Algebra A R] [Algebra R C] [Algebra A C] [IsScalarTower A R C] [Algebra.IsIntegral R C] (v : HeightOneSpectrum A) (u : { u : HeightOneSpectrum C // u.asIdeal.LiesOver v.asIdeal }) : ↑((liesOverTowerEquiv R v).symm u).fst = under R ↑u

The inverse of liesOverTowerEquiv passes through the contraction of u to R.

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.liesOverTowerEquiv_symm_apply_snd (R : Type u_1) [CommRing R] [IsDomain R] {A : Type u_3} {C : Type u_4} [CommRing A] [CommRing C] [IsDomain C] [Algebra A R] [Algebra R C] [Algebra A C] [IsScalarTower A R C] [Algebra.IsIntegral R C] (v : HeightOneSpectrum A) (u : { u : HeightOneSpectrum C // u.asIdeal.LiesOver v.asIdeal }) : ↑((liesOverTowerEquiv R v).symm u).snd = ↑u

The inverse of liesOverTowerEquiv keeps u as the top prime.

def IsDedekindDomain.HeightOneSpectrum.primesAbove (R : Type u_1) [CommRing R] (B : Type u_2) [CommRing B] [Algebra R B] [IsDomain R] [IsDomain B] [Algebra.IsIntegral R B] (S : Set (HeightOneSpectrum R)) : Set (HeightOneSpectrum B)

The primes of B lying above a set S of primes of R: the preimage of S under the contraction HeightOneSpectrum.under R.

Equations

• IsDedekindDomain.HeightOneSpectrum.primesAbove R B S = IsDedekindDomain.HeightOneSpectrum.under R ⁻¹' S

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.mem_primesAbove_iff (R : Type u_1) [CommRing R] (B : Type u_2) [CommRing B] [Algebra R B] [IsDomain R] [IsDomain B] [Algebra.IsIntegral R B] (S : Set (HeightOneSpectrum R)) (w : HeightOneSpectrum B) : w ∈ primesAbove R B S ↔ under R w ∈ S

A prime of B lies above S exactly when its contraction to R lies in S.

theorem IsDedekindDomain.HeightOneSpectrum.primesAbove_mono (R : Type u_1) [CommRing R] (B : Type u_2) [CommRing B] [Algebra R B] [IsDomain R] [IsDomain B] [Algebra.IsIntegral R B] {S T : Set (HeightOneSpectrum R)} (hST : S ⊆ T) : primesAbove R B S ⊆ primesAbove R B T

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.primesAbove_empty (R : Type u_1) [CommRing R] (B : Type u_2) [CommRing B] [Algebra R B] [IsDomain R] [IsDomain B] [Algebra.IsIntegral R B] : primesAbove R B ∅ = ∅

instance IsDedekindDomain.HeightOneSpectrum.finite_liesOver {R : Type u_1} [CommRing R] (B : Type u_2) [CommRing B] [Algebra R B] [FaithfulSMul R B] [IsDedekindDomain B] (v : HeightOneSpectrum R) : Finite { w : HeightOneSpectrum B // w.asIdeal.LiesOver v.asIdeal }

Only finitely many nonzero primes of a Dedekind domain B lie over a given nonzero prime of R. The extension need not be integral, and R need not be Dedekind.

theorem IsDedekindDomain.HeightOneSpectrum.primesAbove_finite (R : Type u_1) [CommRing R] (B : Type u_2) [CommRing B] [Algebra R B] [IsDomain R] [IsDedekindDomain B] [Algebra.IsIntegral R B] [FaithfulSMul R B] {S : Set (HeightOneSpectrum R)} (hS : S.Finite) : (primesAbove R B S).Finite

Only finitely many primes of B lie above a finite set of primes of R.

theorem IsDedekindDomain.HeightOneSpectrum.tendsto_under_cofinite (R : Type u_1) [CommRing R] (B : Type u_2) [CommRing B] [Algebra R B] [IsDomain R] [IsDedekindDomain B] [Algebra.IsIntegral R B] [FaithfulSMul R B] : Filter.Tendsto (under R) Filter.cofinite Filter.cofinite

Only finitely many primes of B contract to each prime of R, so contraction tends to the cofinite filter along the cofinite filter.

theorem IsDedekindDomain.HeightOneSpectrum.tendsto_under_cofinite_of_isFractionRing (R : Type u_1) [CommRing R] (B : Type u_2) [CommRing B] [Algebra R B] [IsDomain R] [IsDedekindDomain B] [Algebra.IsIntegral R B] (K : Type u_3) (L : Type u_4) [Field K] [Algebra R K] [IsFractionRing R K] [Semiring L] [Nontrivial L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [Algebra B L] [IsScalarTower R B L] : Filter.Tendsto (under R) Filter.cofinite Filter.cofinite

tendsto_under_cofinite when R and B map compatibly to a nontrivial algebra L over the fraction field K of R: the tower R → K → L makes the algebra map R → B injective.

def IsDedekindDomain.selmerGroupAbove (R : Type u_1) [CommRing R] (B : Type u_2) [CommRing B] [Algebra R B] [IsDomain R] [IsDedekindDomain B] [Algebra.IsIntegral R B] (L : Type u_3) [Field L] [Algebra B L] [IsFractionRing B L] (S : Set (HeightOneSpectrum R)) (n : ℕ) : Subgroup (Lˣ ⧸ (powMonoidHom n).range)

The S-Selmer group of L, where B is a Dedekind domain with fraction field L and S is a set of primes of R: the classes of Lˣ modulo n-th powers whose valuation is divisible by n at every prime of B not lying above S.

Equations

• IsDedekindDomain.selmerGroupAbove R B L S n = IsDedekindDomain.selmerGroup

theorem IsDedekindDomain.selmerGroupAbove_def (R : Type u_1) [CommRing R] (B : Type u_2) [CommRing B] [Algebra R B] [IsDomain R] [IsDedekindDomain B] [Algebra.IsIntegral R B] (L : Type u_3) [Field L] [Algebra B L] [IsFractionRing B L] (S : Set (HeightOneSpectrum R)) (n : ℕ) : selmerGroupAbove R B L S n = selmerGroup

selmerGroupAbove is the ordinary Selmer group taken over the primes above S. This is the form in which IsDedekindDomain.selmerGroupPi and selmerGroupOfEquiv, stated in terms of selmerGroup, apply to it.

@[simp]

theorem IsDedekindDomain.mem_selmerGroupAbove_iff (R : Type u_1) [CommRing R] (B : Type u_2) [CommRing B] [Algebra R B] [IsDomain R] [IsDedekindDomain B] [Algebra.IsIntegral R B] (L : Type u_3) [Field L] [Algebra B L] [IsFractionRing B L] (S : Set (HeightOneSpectrum R)) (n : ℕ) (x : Lˣ ⧸ (powMonoidHom n).range) : x ∈ selmerGroupAbove R B L S n ↔ ∀ w ∉ HeightOneSpectrum.primesAbove R B S, (w.valuationOfNeZeroMod n) x = 1

A class of units lies in the Selmer group relative to S exactly when its valuationOfNeZeroMod n is trivial at every prime of B not lying above S, i.e. n divides the w-adic valuation there.