Complements on the v-adic valuation of a unit

Mathlib's IsDedekindDomain.HeightOneSpectrum.valuationOfNeZero is the v-adic valuation restricted to Kˣ, valued in Multiplicative ℤ rather than ℤₘ₀, and Mathlib relates it to valuation only through the coercion valuationOfNeZero_eq. This file adds the triviality criterion in the uncoerced form, and the corresponding criterion one level up, on the quotient Kˣ ⧸ (Kˣ)ⁿ where the Selmer group K⟮S, n⟯ lives: there triviality of valuationOfNeZeroMod is divisibility by n of the valuation. That second criterion is what turns membership in IsDedekindDomain.selmerGroup from a statement about a quotient into an arithmetic condition on a representative.

Main results

• IsDedekindDomain.HeightOneSpectrum.valuationOfNeZeroMod_mk_eq_one_iff: the class of a unit has trivial v-adic valuationOfNeZeroMod n exactly when n divides its v-adic valuation.
• IsDedekindDomain.HeightOneSpectrum.dvd_toAdd_valuationOfNeZero: if the v-adic valuation of a unit is the n-th power of that of another unit, then n divides its v-adic order.
• IsDedekindDomain.HeightOneSpectrum.finite_setOfPred_valuation_ne_one: a nonzero element has trivial valuation at all but finitely many primes.

Michael Stoll's elliptic-curves formalisation (github.com/MichaelStollBayreuth/EllipticCurves, at the EllipticCurves roadmap's pin 66889eada51a, Apache 2.0, by Michael Stoll) reaches for a HeightOneSpectrum.valuationOfNeZero_eq_iff in this role; no such lemma exists at our Mathlib pin, so it and its m = 1 case valuationOfNeZero_eq_one_iff are supplied in TauCeti/RingTheory/DedekindDomain/ValuationOfNeZero.lean, which this file imports — they are generic, and the completion API needs them without needing the Selmer groups below. valuationOfNeZeroMod_mk_eq_one_iff, dvd_toAdd_valuationOfNeZero and finite_setOfPred_valuation_ne_one are adapted from that source's EllipticCurves/Mathlib/Basic.lean. Following this repository's convention for adapted material, the upstream authorship is credited here rather than in the copyright header.

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.valuationOfNeZeroMod_mk_eq_one_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (n : ℕ) (u : Kˣ) : (v.valuationOfNeZeroMod n) ↑u = 1 ↔ ↑n ∣ Multiplicative.toAdd (v.valuationOfNeZero u)

The class of a unit u in Kˣ ⧸ (Kˣ)ⁿ has trivial v-adic valuation mod n exactly when n divides the v-adic valuation of u. Membership in IsDedekindDomain.selmerGroup is the conjunction of these conditions over the primes away from S, so this is what expresses that membership as an arithmetic condition on a representative.

theorem IsDedekindDomain.HeightOneSpectrum.dvd_toAdd_valuationOfNeZero {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) {n : ℕ} {u z : Kˣ} (h : (valuation K v) ↑u = (valuation K v) ↑z ^ n) : ↑n ∣ Multiplicative.toAdd (v.valuationOfNeZero u)

If the valuation of a unit u is the n-th power of the valuation of a unit z, then the v-adic order of u is divisible by n.

theorem IsDedekindDomain.HeightOneSpectrum.finite_setOfPred_valuation_ne_one {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {x : K} (hx : x ≠ 0) : {v : HeightOneSpectrum R | (valuation K v) x ≠ 1}.Finite

A nonzero element of the fraction field of a Dedekind domain has trivial valuation at all but finitely many primes.