Documentation

TauCeti.RingTheory.DedekindDomain.SInteger.Spectrum

The height one spectrum of a ring of S-integers #

Let R be a Dedekind domain with fraction field K and S a set of height-one primes of R. TauCeti/RingTheory/DedekindDomain/SInteger/Basic.lean shows that the ring of S-integers is again a Dedekind domain, so it has a height one spectrum of its own. This file identifies that spectrum: the height-one primes of π’ͺ_S are exactly the height-one primes of R not in S, via v ↦ v Β· π’ͺ_S (integerHeightOneSpectrumEquiv), and the correspondence carries the valuations across unchanged (valuation_integerHeightOneSpectrumEquiv).

Two companion facts record what extension does to prime powers for v βˆ‰ S: integer_comap_map_pow, that contracting the extension of v ^ n returns v ^ n, and integer_map_le_map_pow_iff, that containment in a prime power transfers along the extension in both directions. Multiplicities are turned into such containments by le_count_associates_iff_le_pow in TauCeti/RingTheory/DedekindDomain/Factorization.lean; integer_map_le_map_pow_iff is what then carries them across the extension.

The two directions are integerPrimeOverOfNotMem, extending v βˆ‰ S to π’ͺ_S, and integerPrimeUnder, contracting a prime of π’ͺ_S back to R. That they are mutually inverse is Mathlib's Ideal.comap_map_eq_self_of_isMaximal in one direction β€” the extension of a maximal v βˆ‰ S stays proper, so contracting it returns v β€” and integer_map_comap_eq β€” every ideal of π’ͺ_S is extended β€” in the other.

The valuations transfer through Mathlib's HeightOneSpectrum.valuation_liesOver, which relates the valuation at a prime to the valuation at the prime below it by the ramification index. Here that index is 1 by Mathlib's Ideal.ramificationIdx'_map_self_eq_one, the extended ideal being the prime above. Both readings of the transfer are supplied β€” valuation_integerPrimeOverOfNotMem for a prime of R avoiding S, and valuation_integerPrimeUnder for an arbitrary prime of π’ͺ_S.

Inverting S therefore removes exactly the primes of S from the spectrum and changes nothing else, which is why the Selmer group of π’ͺ_S relative to βˆ… is the Selmer group of R relative to S. That identification is what TauCetiRoadmap/EllipticCurves/README.md Β§Layer 6 needs for weak Mordell–Weil: the finiteness of A(S, 2) is the finiteness of a Selmer group over π’ͺ_S.

Adapted from Michael Stoll's elliptic-curves formalisation (github.com/MichaelStollBayreuth/EllipticCurves, EllipticCurves/Mathlib/SIntegers.lean at the roadmap's pin 66889eada51a, Apache 2.0, by Michael Stoll), the source the roadmap's Β§Provenance names for the Layer 6 Mordell–Weil lane. Following this repository's convention for adapted material, the upstream authorship is credited here rather than in the copyright header. This is the height-one-spectrum half of that file; the Dedekind property came first, and the class-group computation Cl(π’ͺ_S) ≃* Cl(R) β§Έ ⟨[v] : v ∈ S⟩ is IsDedekindDomain.integerClassGroupEquiv in TauCeti/RingTheory/DedekindDomain/SInteger/ClassGroup.lean, which consumes this file.

source
theorem IsDedekindDomain.integer_map_asIdeal_ne_top {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) {v : HeightOneSpectrum R} (hv : v βˆ‰ S) :
Ideal.map (algebraMap R β†₯(S.integer K)) v.asIdeal β‰  ⊀

For v βˆ‰ S, the extension of v to π’ͺ_S is a proper ideal.

source
theorem IsDedekindDomain.isMaximal_integer_map_asIdeal {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) {v : HeightOneSpectrum R} (hv : v βˆ‰ S) :
(Ideal.map (algebraMap R β†₯(S.integer K)) v.asIdeal).IsMaximal

For v βˆ‰ S, the extension of v to π’ͺ_S is maximal.

source
noncomputable def IsDedekindDomain.integerPrimeOverOfNotMem {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) {v : HeightOneSpectrum R} (hv : v βˆ‰ S) :
HeightOneSpectrum β†₯(S.integer K)

The prime of π’ͺ_S above a prime v βˆ‰ S of R: the extension of v.

Equations
Instances For
    source
    @[simp]
    theorem IsDedekindDomain.integerPrimeOverOfNotMem_asIdeal {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) {v : HeightOneSpectrum R} (hv : v βˆ‰ S) :
    (integerPrimeOverOfNotMem K S hv).asIdeal = Ideal.map (algebraMap R β†₯(S.integer K)) v.asIdeal
    source
    @[simp]
    theorem IsDedekindDomain.integer_comap_map_pow {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) {v : HeightOneSpectrum R} (hv : v βˆ‰ S) (n : β„•) :
    Ideal.comap (algebraMap R β†₯(S.integer K)) (Ideal.map (algebraMap R β†₯(S.integer K)) (v.asIdeal ^ n)) = v.asIdeal ^ n

    For v βˆ‰ S, the contraction of the extension of v ^ n is v ^ n again. Mathlib's Ideal.comap_map_eq_self_of_isMaximal gives this only for n = 1.

    source
    theorem IsDedekindDomain.integer_map_le_map_pow_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) {v : HeightOneSpectrum R} (hv : v βˆ‰ S) (J : Ideal R) (k : β„•) :
    Ideal.map (algebraMap R β†₯(S.integer K)) J ≀ (integerPrimeOverOfNotMem K S hv).asIdeal ^ k ↔ J ≀ v.asIdeal ^ k

    For v βˆ‰ S, an ideal J of R is contained in v ^ k exactly when its extension to π’ͺ_S is contained in the k-th power of the prime above v.

    source
    noncomputable def IsDedekindDomain.integerPrimeUnder {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) (P : HeightOneSpectrum β†₯(S.integer K)) :
    HeightOneSpectrum R

    The prime of R below a prime P of π’ͺ_S: its contraction.

    Equations
    Instances For
      source
      @[simp]
      theorem IsDedekindDomain.integerPrimeUnder_asIdeal {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) (P : HeightOneSpectrum β†₯(S.integer K)) :
      (integerPrimeUnder K S P).asIdeal = Ideal.comap (algebraMap R β†₯(S.integer K)) P.asIdeal
      source
      theorem IsDedekindDomain.integerPrimeUnder_notMem {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) (P : HeightOneSpectrum β†₯(S.integer K)) :
      integerPrimeUnder K S P βˆ‰ S

      A prime under a prime of π’ͺ_S never lies in S.

      source
      @[simp]
      theorem IsDedekindDomain.integerPrimeUnder_integerPrimeOverOfNotMem {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) {v : HeightOneSpectrum R} (hv : v βˆ‰ S) :
      integerPrimeUnder K S (integerPrimeOverOfNotMem K S hv) = v

      Extending v βˆ‰ S to π’ͺ_S and contracting back returns v.

      source
      @[simp]
      theorem IsDedekindDomain.integerPrimeOverOfNotMem_integerPrimeUnder {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) (P : HeightOneSpectrum β†₯(S.integer K)) :
      integerPrimeOverOfNotMem K S β‹― = P

      Contracting a prime of π’ͺ_S and extending back returns it.

      source
      noncomputable def IsDedekindDomain.integerHeightOneSpectrumEquiv {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) :
      { v : HeightOneSpectrum R // v βˆ‰ S } ≃ HeightOneSpectrum β†₯(S.integer K)

      The height-one primes of π’ͺ_S are exactly the height-one primes of R not in S.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem IsDedekindDomain.integerHeightOneSpectrumEquiv_apply {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) (v : { v : HeightOneSpectrum R // v βˆ‰ S }) :
        (integerHeightOneSpectrumEquiv K S) v = integerPrimeOverOfNotMem K S β‹―
        source
        @[simp]
        theorem IsDedekindDomain.integerHeightOneSpectrumEquiv_symm_apply_coe {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) (P : HeightOneSpectrum β†₯(S.integer K)) :
        ↑((integerHeightOneSpectrumEquiv K S).symm P) = integerPrimeUnder K S P
        source
        instance IsDedekindDomain.liesOver_integerPrimeOverOfNotMem {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) {v : HeightOneSpectrum R} (hv : v βˆ‰ S) :
        (integerPrimeOverOfNotMem K S hv).asIdeal.LiesOver v.asIdeal

        For v βˆ‰ S, the prime of π’ͺ_S above v lies over v.

        source
        @[simp]
        theorem IsDedekindDomain.valuation_integerPrimeOverOfNotMem {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) {v : HeightOneSpectrum R} (hv : v βˆ‰ S) (x : K) :
        (HeightOneSpectrum.valuation K (integerPrimeOverOfNotMem K S hv)) x = (HeightOneSpectrum.valuation K v) x

        The correspondence preserves valuations: the valuation of π’ͺ_S at the prime above v is the valuation of R at v. Mathlib's valuation_liesOver relates the two by the ramification index, which is 1 here.

        source
        theorem IsDedekindDomain.valuation_integerHeightOneSpectrumEquiv {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) (v : { v : HeightOneSpectrum R // v βˆ‰ S }) (x : K) :
        (HeightOneSpectrum.valuation K ((integerHeightOneSpectrumEquiv K S) v)) x = (HeightOneSpectrum.valuation K ↑v) x

        The correspondence preserves valuations, phrased through the equivalence. Not a simp lemma: integerHeightOneSpectrumEquiv_apply rewrites the left-hand side to integerPrimeOverOfNotMem first, so this form is never in normal form β€” the simp lemma is valuation_integerPrimeOverOfNotMem above.

        source
        @[simp]
        theorem IsDedekindDomain.valuationOfNeZero_integerPrimeOverOfNotMem {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) {v : HeightOneSpectrum R} (hv : v βˆ‰ S) (u : KΛ£) :
        (integerPrimeOverOfNotMem K S hv).valuationOfNeZero u = v.valuationOfNeZero u

        The correspondence preserves the integer-valued valuation: the Multiplicative β„€-valued valuation of the S-integers at the prime above v is the one of R at v. This is the KΛ£ companion of valuation_integerPrimeOverOfNotMem.

        source
        theorem IsDedekindDomain.valuationOfNeZero_integerHeightOneSpectrumEquiv {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) (v : { v : HeightOneSpectrum R // v βˆ‰ S }) (u : KΛ£) :
        ((integerHeightOneSpectrumEquiv K S) v).valuationOfNeZero u = (↑v).valuationOfNeZero u

        Transport of the integer-valued valuation, phrased through the equivalence. Not a simp lemma: integerHeightOneSpectrumEquiv_apply rewrites the left-hand side to integerPrimeOverOfNotMem first, so this form is never in normal form β€” the simp lemma is valuationOfNeZero_integerPrimeOverOfNotMem above.

        source
        theorem IsDedekindDomain.valuation_integerPrimeUnder {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Set (HeightOneSpectrum R)) (P : HeightOneSpectrum β†₯(S.integer K)) (x : K) :
        (HeightOneSpectrum.valuation K P) x = (HeightOneSpectrum.valuation K (integerPrimeUnder K S P)) x

        The correspondence preserves valuations, read downwards: the valuation of π’ͺ_S at an arbitrary prime P is the valuation of R at the prime under P. This is the form a consumer holding a prime of π’ͺ_S β€” rather than one of R avoiding S β€” can apply directly.

        Not a simp lemma: its left-hand side is an unrestricted P.valuation K x, so tagging it would rewrite every valuation on π’ͺ_S, including the one valuation_integerPrimeOverOfNotMem is the normal form for.