Documentation

TauCeti.RingTheory.DedekindDomain.AdicValuation.Completion

The ring of integers of a single adic completion #

The ring of integers π’ͺ_v of the completion K_v of the fraction field of a Dedekind domain R at a height-one prime v is a local ring, and this file collects what it is: its maximal ideal contracts to v itself, its ideal filtration is the valuation filtration K_v induces on it, and in the subspace topology it is a complete π”ͺ-adic β€” hence Henselian β€” local ring. The scope AdicCompletionIntegers lets an algebra action on R act on this valuation ring through its canonical R-algebra action, without changing ambient actions elsewhere.

Everything here concerns one completion. The comparison of two completions along an extension w ∣ v is TauCeti.RingTheory.DedekindDomain.AdicCompletionExtension.

Main results #

Implementation notes #

Mathlib.NumberTheory.NumberField.Completion.FinitePlace supplies two instances used throughout β€” IsDiscreteValuationRing (v.adicCompletionIntegers K) and (Valued.v : Valuation (v.adicCompletion K) ℀ᡐ⁰).IsRankOneDiscrete. Both are stated there for an arbitrary Dedekind domain and its fraction field, not for number fields, so nothing here depends on number-field theory; they simply live in that module upstream. This note records the reason so the placement of a NumberTheory import inside RingTheory is not mistaken for a layering slip.

Motivation #

These results are consumed by a semilocal comparison in explicit 2-descent, which matches a square class of a global Γ©tale algebra with its images in the completions, and by the local valuation conditions that cut out congruence subgroups of the ideles. Nothing here mentions a curve β€” each statement is about a Dedekind domain and one of its completions.

Provenance #

Adapted, with the author's proof, from Michael Stoll's EllipticCurves project (github.com/MichaelStollBayreuth/EllipticCurves, Apache-2.0, pinned by TauCetiRoadmap/EllipticCurves/README.md at 66889eada51a), EllipticCurves/Mathlib/Basic.lean line 594, and EllipticCurves/Mathlib/AdicCompletionExtension.lean for the filtration and Henselian results, and for residueFieldEquivAdicCompletionIntegers and the approximation modulo the maximal ideal behind it, which exists_valued_sub_le generalizes to every power of the maximal ideal. The source states the contraction with Ideal.comap of an algebraMap; Mathlib spells that Ideal.under, which is used here.

source
@[reducible]
noncomputable def TauCeti.adicCompletionIntegersAlgebra {R : Type u_1} {K : Type u_2} {S : Type u_3} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] [CommSemiring S] [Algebra S R] {v : IsDedekindDomain.HeightOneSpectrum R} :
Algebra S β†₯(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)

An algebra action on the affine model acts on the integers of its adic completion. Available as an instance in the scope AdicCompletionIntegers.

Equations
Instances For
    source
    theorem TauCeti.adicCompletionIntegersIsScalarTower {R : Type u_1} {K : Type u_2} {S : Type u_3} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] [CommSemiring S] [Algebra S R] {v : IsDedekindDomain.HeightOneSpectrum R} :
    IsScalarTower S R β†₯(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)

    The inherited algebra action on the adic valuation ring factors through the affine model. Available as an instance in the scope AdicCompletionIntegers.

    source
    theorem TauCeti.isUniformizer_adicCompletion_iff {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} {x : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v} :
    Valued.v.IsUniformizer x ↔ Valued.v x = WithZero.exp (-1)

    A uniformizer in an adic completion has normalized valuation exp (-1).

    source
    instance IsDedekindDomain.HeightOneSpectrum.adicCompletion_charZero {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] [CharZero K] (v : HeightOneSpectrum R) :
    CharZero (adicCompletion K v)

    The completion of a field of characteristic zero at a height-one prime has characteristic zero, since the field embeds into it.

    source
    @[simp]
    theorem IsDedekindDomain.HeightOneSpectrum.under_maximalIdeal_adicCompletionIntegers {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) :
    Ideal.under R (IsLocalRing.maximalIdeal β†₯(adicCompletionIntegers K v)) = v.asIdeal

    The prime of R lying under the maximal ideal of the ring of integers of the completion of K at v is v itself.

    source
    @[simp]
    theorem IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletion_eq_algebraMap_adicCompletionIntegers {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (r : R) :
    (algebraMap K (adicCompletion K v)) ((algebraMap R K) r) = (algebraMap (β†₯(adicCompletionIntegers K v)) (adicCompletion K v)) ((algebraMap R β†₯(adicCompletionIntegers K v)) r)

    An element of R, mapped to K_v through K, is the image of its image in π’ͺ_v.

    source
    theorem IsDedekindDomain.HeightOneSpectrum.exists_isUnit_adicCompletionIntegers_of_valuation_eq_one {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) {c : K} (hc : (valuation K v) c = 1) :
    βˆƒ (u : β†₯(adicCompletionIntegers K v)), IsUnit u ∧ ↑u = (algebraMap K (adicCompletion K v)) c

    An element of K with valuation one is the image of a unit in the ring of integers of its completion at v.

    source
    theorem IsDedekindDomain.HeightOneSpectrum.valued_algebraMap_eq_exp_neg_one_of_irreducible {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) {Ο€ : β†₯(adicCompletionIntegers K v)} (hΟ€ : Irreducible Ο€) :
    Valued.v ((algebraMap (β†₯(adicCompletionIntegers K v)) (adicCompletion K v)) Ο€) = WithZero.exp (-1)

    An irreducible element of the ring of integers of a completion has valuation exp (-1).

    source
    @[simp]
    theorem IsDedekindDomain.HeightOneSpectrum.map_asIdeal_adicCompletionIntegers {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) :
    Ideal.map (algebraMap R β†₯(adicCompletionIntegers K v)) v.asIdeal = IsLocalRing.maximalIdeal β†₯(adicCompletionIntegers K v)

    The height-one prime v generates the maximal ideal of the ring of integers of the completion at v.

    source
    @[simp]
    theorem IsDedekindDomain.HeightOneSpectrum.mem_maximalIdeal_pow_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) {x : β†₯(adicCompletionIntegers K v)} {n : β„•} :
    x ∈ IsLocalRing.maximalIdeal β†₯(adicCompletionIntegers K v) ^ n ↔ Valued.v ↑x ≀ WithZero.exp (-↑n)

    An element of π’ͺ_v lies in the n-th power of the maximal ideal exactly when its valuation is at most exp (-n).

    This identifies the ideal filtration of π’ͺ_v with the valuation filtration it inherits from K_v, which is what makes the subspace topology visibly π”ͺ-adic below.

    source
    theorem IsDedekindDomain.HeightOneSpectrum.mem_asIdeal_pow_iff_valued_algebraMap_le {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) {r : R} {n : β„•} :
    r ∈ v.asIdeal ^ n ↔ Valued.v ((algebraMap R (adicCompletion K v)) r) ≀ WithZero.exp (-↑n)

    An element of R lies in v ^ n exactly when its image in K_v has valuation at most exp (-n): the ideal filtration of R at v is the valuation filtration K_v induces on it.

    source
    theorem IsDedekindDomain.HeightOneSpectrum.exists_ne_zero_mem_maximalIdeal_valued_lt {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) {a b : β†₯(adicCompletionIntegers K v)} (ha0 : a β‰  0) (hb0 : b β‰  0) :
    βˆƒ s ∈ IsLocalRing.maximalIdeal β†₯(adicCompletionIntegers K v), s β‰  0 ∧ Valued.v ↑s < Valued.v ↑a ∧ Valued.v ↑s < Valued.v ↑b ∧ Valued.v ↑s < 1

    The maximal ideal of the ring of integers of an adic completion contains a nonzero element whose valuation is below the valuations of a and b, and below 1.

    π’ͺ_v is a complete adic Henselian local ring #

    The subspace topology π’ͺ_v inherits from K_v is the π”ͺ-adic one, and π’ͺ_v is closed in the complete field K_v, hence complete. Being complete for the π”ͺ-adic topology it is π”ͺ-adically complete, and a local ring that is complete with respect to its maximal ideal is Henselian.

    source
    instance IsDedekindDomain.HeightOneSpectrum.isTopologicalRing_adicCompletionIntegers {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) :
    IsTopologicalRing β†₯(adicCompletionIntegers K v)

    The ring of integers of an adic completion is a topological ring, as a subring of K_v.

    source
    theorem IsDedekindDomain.HeightOneSpectrum.isOpen_setOf_valued_le {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) {Ξ³ : WithZero (Multiplicative β„€)} (hΞ³ : Ξ³ β‰  0) :
    IsOpen {z : adicCompletion K v | Valued.v z ≀ Ξ³}

    A closed valuation ball of K_v around the origin is open. The valuation of K_v is surjective onto ℀ᡐ⁰, so every nonzero bound is attained and the ball is the closed ball around a point, which Valued.isOpen_closedBall shows is open.

    source
    theorem IsDedekindDomain.HeightOneSpectrum.isOpen_maximalIdeal_pow_adicCompletionIntegers {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (n : β„•) :
    IsOpen ↑(IsLocalRing.maximalIdeal β†₯(adicCompletionIntegers K v) ^ n)

    Each power of the maximal ideal of π’ͺ_v is open: π”ͺ ^ n is the preimage under the inclusion π’ͺ_v β†’ K_v of a closed valuation ball, and those are open.

    source
    theorem IsDedekindDomain.HeightOneSpectrum.exists_maximalIdeal_pow_subset_of_mem_nhds {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) {s : Set β†₯(adicCompletionIntegers K v)} (hs : s ∈ nhds 0) :
    βˆƒ (n : β„•), ↑(IsLocalRing.maximalIdeal β†₯(adicCompletionIntegers K v) ^ n) βŠ† s

    Every neighbourhood of 0 in π’ͺ_v contains a power of the maximal ideal. A neighbourhood is cut out by a valuation bound, and exp takes some integer below that bound; the corresponding π”ͺ ^ n is then undercut by it.

    source
    theorem IsDedekindDomain.HeightOneSpectrum.isAdic_maximalIdeal_adicCompletionIntegers {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) :
    IsAdic (IsLocalRing.maximalIdeal β†₯(adicCompletionIntegers K v))

    The subspace topology on the ring of integers π’ͺ_v of an adic completion is the π”ͺ-adic topology of its maximal ideal.

    source
    instance IsDedekindDomain.HeightOneSpectrum.completeSpace_adicCompletionIntegers {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) :
    CompleteSpace β†₯(adicCompletionIntegers K v)

    π’ͺ_v is complete: it is a closed subset of the complete field K_v.

    source
    instance IsDedekindDomain.HeightOneSpectrum.isUniformAddGroup_adicCompletionIntegers {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) :
    IsUniformAddGroup β†₯(adicCompletionIntegers K v)

    π’ͺ_v is a uniform additive group, as an additive subgroup of K_v.

    source
    instance IsDedekindDomain.HeightOneSpectrum.isAdicComplete_adicCompletionIntegers {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) :
    IsAdicComplete (IsLocalRing.maximalIdeal β†₯(adicCompletionIntegers K v)) β†₯(adicCompletionIntegers K v)

    π’ͺ_v is π”ͺ-adically complete: its topology is the π”ͺ-adic one and it is complete.

    source
    theorem IsDedekindDomain.HeightOneSpectrum.exists_valued_sub_le {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (x : β†₯(adicCompletionIntegers K v)) (n : β„•) :
    βˆƒ (a : R), Valued.v (↑x - (algebraMap R (adicCompletion K v)) a) ≀ WithZero.exp (-↑n)

    R is dense in π’ͺ_v: every element of the ring of integers of the completion is congruent to an element of R modulo any power π”ͺ ^ n of the maximal ideal.

    source
    theorem IsDedekindDomain.HeightOneSpectrum.denseRange_algebraMap_adicCompletionIntegers {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) :
    DenseRange ⇑(algebraMap R β†₯(adicCompletionIntegers K v))

    R is dense in the ring of integers of its completion at v. Equivalently, every neighbourhood of an element of π’ͺ_v contains the image of an element of R.

    source
    noncomputable def IsDedekindDomain.HeightOneSpectrum.residueFieldEquivAdicCompletionIntegers {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) :
    R β§Έ v.asIdeal ≃+* β†₯(adicCompletionIntegers K v) β§Έ IsLocalRing.maximalIdeal β†₯(adicCompletionIntegers K v)

    The residue field of v maps isomorphically onto the residue field of the ring of integers of the completion at v.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      instance IsDedekindDomain.HeightOneSpectrum.finite_residueField_adicCompletionIntegers {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) [Finite (R β§Έ v.asIdeal)] :
      Finite (IsLocalRing.ResidueField β†₯(adicCompletionIntegers K v))

      The residue field of an adic completion is finite when the residue field at v is finite.

      source
      @[simp]
      theorem IsDedekindDomain.HeightOneSpectrum.residueFieldEquivAdicCompletionIntegers_apply_mk {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (a : R) :
      v.residueFieldEquivAdicCompletionIntegers ((Ideal.Quotient.mk v.asIdeal) a) = (Ideal.Quotient.mk (IsLocalRing.maximalIdeal β†₯(adicCompletionIntegers K v))) ((algebraMap R β†₯(adicCompletionIntegers K v)) a)

      The residue-field equivalence on a quotient representative. This is the characterization consumers should use; the equivalence's construction as an Ideal.quotientMap is an implementation detail and should not be unfolded.

      source
      noncomputable def TauCeti.residueFieldAlgEquivAdicCompletionIntegers {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (S : Type u_3) [CommRing S] [Algebra S R] {v : IsDedekindDomain.HeightOneSpectrum R} :
      (R β§Έ v.asIdeal) ≃ₐ[S] IsLocalRing.ResidueField β†₯(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)

      The affine-model residue comparison as an equivalence over any scalars acting on the model. Use the scope AdicCompletionIntegers for the inherited action on completed integers.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.residueFieldAlgEquivAdicCompletionIntegers_apply {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (S : Type u_3) [CommRing S] [Algebra S R] {v : IsDedekindDomain.HeightOneSpectrum R} (x : R β§Έ v.asIdeal) :
        (residueFieldAlgEquivAdicCompletionIntegers S) x = v.residueFieldEquivAdicCompletionIntegers x

        The scalar-preserving residue comparison has Mathlib's underlying ring comparison.