Documentation

TauCeti.RingTheory.DedekindDomain.AdicCompletionExtension

Extension of adic completions along an extension of Dedekind domains #

Let R be a Dedekind domain with fraction field K, let L/K be an extension and B a Dedekind domain with fraction field L extending R, and let w be a height-one prime of B lying over the height-one prime v of R. Completing at v and at w gives fields K_v and L_w, and the inclusion K β†’ L extends continuously to a ring homomorphism K_v β†’+* L_w.

This file constructs that homomorphism, adicCompletionExtension, records that the valuation of L_w restricted along it is the valuation of K_v raised to the ramification index, restricts it to the rings of integers as adicCompletionIntegersExtension, and shows that the maximal ideal contracts to the maximal ideal. It also provides the induced algebra structure in the AdicCompletionExtension scope, and identifies the valuation attached to the maximal ideal of π’ͺ_v β€” a discrete valuation ring β€” with the valuation of the completion itself, which is what lets a statement about height-one primes of π’ͺ_v be read as a statement about K_v.

This is the local-to-global bridge of the explicit 2-descent: comparing a square class of a global Γ©tale algebra with its images in the completions passes through exactly these maps.

Main definitions #

Main results #

Motivation #

Every result here is consumed by a semilocal comparison in explicit 2-descent: matching the unramifiedness of a square class at the primes of the field factors with unramifiedness over the valuation ring of K_v. Nothing in this file mentions a curve β€” each statement is about a Dedekind domain and one of its completions.

Provenance #

Adapted, with the authors' proofs, from Michael Stoll's EllipticCurves project (github.com/MichaelStollBayreuth/EllipticCurves, Apache-2.0, pinned by TauCetiRoadmap/EllipticCurves/README.md at 66889eada51a), EllipticCurves/Mathlib/AdicCompletionExtension.lean.

That file in turn credits the FLT project (github.com/ImperialCollegeLondon/FLT, FLT/DedekindDomain/Completion/BaseChange.lean, by Kevin Buzzard, Andrew Yang and Matthew Jasper) for the completion-extension material, rebased there onto Mathlib's valuation_liesOver and uniformContinuous_algebraMap_liesOver; the same rebasing is used here, so both are credited.

span_singleton_eq_maximalIdeal_pow comes from that same Stoll file, restated here against this repository's HeightOneSpectrum interface.

exists_unit_not_isSquare comes from the same source file (:183). Two deliberate departures from its proof: the source contracts the maximal ideal with its own comap_maximalIdeal_adicCompletionIntegers, which this repository states as under_maximalIdeal_adicCompletionIntegers (Ideal.under R I is by definition I.comap (algebraMap R S)); and where the source derives v d = 1 from a square by manipulating WithZero.log, this uses Mathlib's mul_self_le_one_iff and one_le_mul_self_iff, which say the same thing about the ordered value monoid in one line. The odd-residue-characteristic step is split out as ringChar_residueField_adicCompletionIntegers_ne_two, which the source keeps inline.

The Henselian and completeness chain from that same Stoll file lives in TauCeti.RingTheory.DedekindDomain.AdicValuation.Completion, with the single-completion valuation and residue-field results it rests on β€” among them residueFieldEquivAdicCompletionIntegers, which this file uses.

Implementation notes #

Every Mathlib module this file needs arrives through TauCeti.RingTheory.DedekindDomain.AdicValuation.Completion, which is imported for the single-completion results and publicly re-exports them.

source
theorem IsDedekindDomain.HeightOneSpectrum.valuation_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) (x : adicCompletion K v) :
(valuation (adicCompletion K v) (IsDiscreteValuationRing.maximalIdeal β†₯(adicCompletionIntegers K v))) x = Valued.v x

The valuation associated to the maximal ideal of the ring of integers of an adic completion is the valuation of the completion.

This is what lets a condition stated at the height-one primes of π’ͺ_v be read as a condition on K_v: π’ͺ_v is a discrete valuation ring, so it has exactly one, and it induces Valued.v.

Not @[simp]: this is the special case P = IsDiscreteValuationRing.maximalIdeal _ of valuation_adicCompletionIntegers, which carries the annotation instead. With both marked, the simpNF linter rejects this one β€” "simp can prove this" β€” because the general form subsumes it.

source
theorem IsDedekindDomain.HeightOneSpectrum.valuationOfNeZero_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) (u : KΛ£) :
(IsDiscreteValuationRing.maximalIdeal β†₯(adicCompletionIntegers K v)).valuationOfNeZero ((Units.map ↑(algebraMap K (adicCompletion K v))) u) = v.valuationOfNeZero u

The valuation of the height-one prime of π’ͺ_v at the image of a unit of K is the v-adic valuation of that unit. This is the form the square-class conditions of the 2-descent are stated in.

source
@[simp]
theorem IsDedekindDomain.HeightOneSpectrum.valuation_adicCompletionIntegers {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (P : HeightOneSpectrum β†₯(adicCompletionIntegers K v)) (x : adicCompletion K v) :
(valuation (adicCompletion K v) P) x = Valued.v x

Any height-one prime P of the valuation ring π’ͺ_v β€” necessarily its maximal ideal β€” induces on K_v the valuation of the completion.

source
theorem IsDedekindDomain.HeightOneSpectrum.valuation_adicCompletion_algebraMap {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (P : HeightOneSpectrum β†₯(adicCompletionIntegers K v)) (z : K) :
(valuation (adicCompletion K v) P) ((algebraMap K (adicCompletion K v)) z) = (valuation K v) z

Any height-one prime P of the valuation ring π’ͺ_v β€” necessarily its maximal ideal β€” induces on K the valuation v itself: the restriction to K of valuation_adicCompletionIntegers.

source
theorem IsDedekindDomain.HeightOneSpectrum.span_singleton_eq_maximalIdeal_pow {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)} {e : β„•} (hx : Valued.v ((algebraMap (β†₯(adicCompletionIntegers K v)) (adicCompletion K v)) x) = WithZero.exp (-↑e)) :
Ideal.span {x} = IsLocalRing.maximalIdeal β†₯(adicCompletionIntegers K v) ^ e

An element of the ring of integers of a completion of valuation exp (-e) generates the e-th power of the maximal ideal.

source
theorem IsDedekindDomain.HeightOneSpectrum.ringChar_residueField_adicCompletionIntegers_ne_two {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (hv2 : 2 βˆ‰ v.asIdeal) :
ringChar (IsLocalRing.ResidueField β†₯(adicCompletionIntegers K v)) β‰  2

At a place not dividing 2, the residue characteristic is odd. The residue field of π’ͺ_v is the residue field of v by residueFieldEquivAdicCompletionIntegers, so this is the hypothesis 2 βˆ‰ v transported along that equivalence β€” stated as a statement about ringChar because that is the form FiniteField.exists_nonsquare consumes.

source
theorem IsDedekindDomain.HeightOneSpectrum.exists_unit_not_isSquare {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)] (hv2 : 2 βˆ‰ v.asIdeal) :
βˆƒ (c : (β†₯(adicCompletionIntegers K v))Λ£), Β¬IsSquare ((algebraMap (β†₯(adicCompletionIntegers K v)) (adicCompletion K v)) ↑c)

At a place of odd residue characteristic and finite residue field, π’ͺ_v has a unit that is not a square in K_v. Any lift of a non-square of the residue field works: a square root in K_v would have valuation 1, hence lie in π’ͺ_v, and would reduce to a square root of the non-square.

source
noncomputable def IsDedekindDomain.HeightOneSpectrum.adicCompletionExtension {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] {B : Type u_3} [CommRing B] [IsDedekindDomain B] [Algebra R B] (L : Type u_4) [Field L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [Algebra B L] [IsFractionRing B L] [IsScalarTower R B L] (v : HeightOneSpectrum R) (w : HeightOneSpectrum B) [w.asIdeal.LiesOver v.asIdeal] :
adicCompletion K v β†’+* adicCompletion L w

The extension of adic completions along w ∣ v: the ring homomorphism K_v β†’+* L_w continuously extending K β†’ L.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[reducible]
    noncomputable def IsDedekindDomain.HeightOneSpectrum.adicCompletionExtensionAlgebra {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] {B : Type u_3} [CommRing B] [IsDedekindDomain B] [Algebra R B] (L : Type u_4) [Field L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [Algebra B L] [IsFractionRing B L] [IsScalarTower R B L] (v : HeightOneSpectrum R) (w : HeightOneSpectrum B) [w.asIdeal.LiesOver v.asIdeal] :
    Algebra (adicCompletion K v) (adicCompletion L w)

    The algebra structure on L_w over K_v induced by adicCompletionExtension, available in the AdicCompletionExtension scope.

    Equations
    Instances For
      source
      @[simp]
      theorem IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletionExtensionAlgebra {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] {B : Type u_3} [CommRing B] [IsDedekindDomain B] [Algebra R B] (L : Type u_4) [Field L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [Algebra B L] [IsFractionRing B L] [IsScalarTower R B L] (v : HeightOneSpectrum R) (w : HeightOneSpectrum B) [w.asIdeal.LiesOver v.asIdeal] :
      algebraMap (adicCompletion K v) (adicCompletion L w) = adicCompletionExtension K L v w

      The algebra map of adicCompletionExtensionAlgebra is adicCompletionExtension.

      source
      @[simp]
      theorem IsDedekindDomain.HeightOneSpectrum.toCompletion_adicCompletionExtension {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] {B : Type u_3} [CommRing B] [IsDedekindDomain B] [Algebra R B] (L : Type u_4) [Field L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [Algebra B L] [IsFractionRing B L] [IsScalarTower R B L] (v : HeightOneSpectrum R) (w : HeightOneSpectrum B) [w.asIdeal.LiesOver v.asIdeal] (x : adicCompletion K v) :
      ((adicCompletionExtension K L v w) x).toCompletion = UniformSpace.Completion.map (⇑(algebraMap (WithVal (valuation K v)) (WithVal (valuation L w)))) x.toCompletion

      Under toCompletion, the image of x is UniformSpace.Completion.map of the algebra map applied to x.toCompletion.

      source
      theorem IsDedekindDomain.HeightOneSpectrum.adicCompletionExtension_coe {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] {B : Type u_3} [CommRing B] [IsDedekindDomain B] [Algebra R B] (L : Type u_4) [Field L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [Algebra B L] [IsFractionRing B L] [IsScalarTower R B L] (v : HeightOneSpectrum R) (w : HeightOneSpectrum B) [w.asIdeal.LiesOver v.asIdeal] (x : K) :
      (adicCompletionExtension K L v w) (adicCompletion.ofCompletion ↑(WithVal.toVal (valuation K v) x)) = adicCompletion.ofCompletion ↑(WithVal.toVal (valuation L w) ((algebraMap K L) x))

      The square with sides K β†’ K_v β†’ L_w and K β†’ L β†’ L_w commutes.

      source
      @[simp]
      theorem IsDedekindDomain.HeightOneSpectrum.adicCompletionExtension_algebraMap {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] {B : Type u_3} [CommRing B] [IsDedekindDomain B] [Algebra R B] (L : Type u_4) [Field L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [Algebra B L] [IsFractionRing B L] [IsScalarTower R B L] (v : HeightOneSpectrum R) (w : HeightOneSpectrum B) [w.asIdeal.LiesOver v.asIdeal] (a : R) :
      (adicCompletionExtension K L v w) ((algebraMap R (adicCompletion K v)) a) = (algebraMap B (adicCompletion L w)) ((algebraMap R B) a)

      The square with sides R β†’ K_v β†’ L_w and R β†’ B β†’ L_w commutes.

      source
      theorem IsDedekindDomain.HeightOneSpectrum.continuous_adicCompletionExtension {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] {B : Type u_3} [CommRing B] [IsDedekindDomain B] [Algebra R B] (L : Type u_4) [Field L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [Algebra B L] [IsFractionRing B L] [IsScalarTower R B L] (v : HeightOneSpectrum R) (w : HeightOneSpectrum B) [w.asIdeal.LiesOver v.asIdeal] :
      Continuous ⇑(adicCompletionExtension K L v w)

      adicCompletionExtension is continuous.

      source
      theorem IsDedekindDomain.HeightOneSpectrum.eq_adicCompletionExtension_of_continuous {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] {B : Type u_3} [CommRing B] [IsDedekindDomain B] [Algebra R B] (L : Type u_4) [Field L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [Algebra B L] [IsFractionRing B L] [IsScalarTower R B L] (v : HeightOneSpectrum R) (w : HeightOneSpectrum B) [w.asIdeal.LiesOver v.asIdeal] {f : adicCompletion K v β†’+* adicCompletion L w} (hf : Continuous ⇑f) (hfK : βˆ€ (x : K), f (adicCompletion.ofCompletion ↑(WithVal.toVal (valuation K v) x)) = adicCompletion.ofCompletion ↑(WithVal.toVal (valuation L w) ((algebraMap K L) x))) :
      f = adicCompletionExtension K L v w

      adicCompletionExtension is the only continuous ring homomorphism K_v β†’+* L_w extending K β†’ L: K is dense in K_v, so a continuous map out of it is pinned by its values there.

      This is the universal property, available without unfolding the definition.

      source
      @[simp]
      theorem IsDedekindDomain.HeightOneSpectrum.valued_adicCompletionExtension {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] {B : Type u_3} [CommRing B] [IsDedekindDomain B] [Algebra R B] (L : Type u_4) [Field L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [Algebra B L] [IsFractionRing B L] [IsScalarTower R B L] (v : HeightOneSpectrum R) (w : HeightOneSpectrum B) [w.asIdeal.LiesOver v.asIdeal] (x : adicCompletion K v) :
      Valued.v ((adicCompletionExtension K L v w) x) = Valued.v x ^ v.asIdeal.ramificationIdx' w.asIdeal

      The valuation on L_w restricted along K_v β†’ L_w is the valuation on K_v raised to the ramification index of w over v.

      source
      @[simp]
      theorem IsDedekindDomain.HeightOneSpectrum.adicCompletionExtension_mem_adicCompletionIntegers {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] {B : Type u_3} [CommRing B] [IsDedekindDomain B] [Algebra R B] (L : Type u_4) [Field L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [Algebra B L] [IsFractionRing B L] [IsScalarTower R B L] (v : HeightOneSpectrum R) (w : HeightOneSpectrum B) [w.asIdeal.LiesOver v.asIdeal] (x : β†₯(adicCompletionIntegers K v)) :
      (adicCompletionExtension K L v w) ↑x ∈ adicCompletionIntegers L w

      The extension maps the ring of integers of K_v into the ring of integers of L_w.

      source
      noncomputable def IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegersExtension {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] {B : Type u_3} [CommRing B] [IsDedekindDomain B] [Algebra R B] (L : Type u_4) [Field L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [Algebra B L] [IsFractionRing B L] [IsScalarTower R B L] (v : HeightOneSpectrum R) (w : HeightOneSpectrum B) [w.asIdeal.LiesOver v.asIdeal] :
      β†₯(adicCompletionIntegers K v) β†’+* β†₯(adicCompletionIntegers L w)

      The restriction of adicCompletionExtension to the rings of integers.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem IsDedekindDomain.HeightOneSpectrum.coe_adicCompletionIntegersExtension {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] {B : Type u_3} [CommRing B] [IsDedekindDomain B] [Algebra R B] (L : Type u_4) [Field L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [Algebra B L] [IsFractionRing B L] [IsScalarTower R B L] (v : HeightOneSpectrum R) (w : HeightOneSpectrum B) [w.asIdeal.LiesOver v.asIdeal] (x : β†₯(adicCompletionIntegers K v)) :
        ↑((adicCompletionIntegersExtension K L v w) x) = (adicCompletionExtension K L v w) ↑x

        adicCompletionIntegersExtension agrees with adicCompletionExtension on the integers.

        source
        @[simp]
        theorem IsDedekindDomain.HeightOneSpectrum.comap_maximalIdeal_adicCompletionIntegersExtension {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] {B : Type u_3} [CommRing B] [IsDedekindDomain B] [Algebra R B] (L : Type u_4) [Field L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [Algebra B L] [IsFractionRing B L] [IsScalarTower R B L] (v : HeightOneSpectrum R) (w : HeightOneSpectrum B) [w.asIdeal.LiesOver v.asIdeal] :
        Ideal.comap (adicCompletionIntegersExtension K L v w) (IsLocalRing.maximalIdeal β†₯(adicCompletionIntegers L w)) = IsLocalRing.maximalIdeal β†₯(adicCompletionIntegers K v)

        The maximal ideal of the ring of integers of L_w contracts to the maximal ideal of the ring of integers of K_v.

        Stated with Ideal.comap of the explicit ring homomorphism, not Ideal.under: Ideal.under A is Ideal.comap (algebraMap A B) and so needs an Algebra (v.adicCompletionIntegers K) (w.adicCompletionIntegers L) instance, which is only installed in the AdicCompletionExtension scope. The Ideal.LiesOver form for that scoped algebra is maximalIdeal_adicCompletionIntegers_liesOver.

        source
        theorem AdjoinRoot.map_comp_algebraMap {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) {p : Polynomial K} {q : Polynomial (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} (hq : q ∣ Polynomial.map (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) p) :
        (map (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) p q hq).comp (algebraMap R (AdjoinRoot p)) = (algebraMap (β†₯(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (AdjoinRoot q)).comp (algebraMap R β†₯(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))

        The base-change map K[X] β§Έ (p) β†’+* K_v[X] β§Έ (q) of AdjoinRoots at a completion is compatible with the algebra maps from the underlying Dedekind domain R and from the ring of integers of the completion.