Definitions/Def_Mathlib_RingTheory_DedekindDomain_AdicValuation.lean
Adic valuation as ideal multiplicity; separable adic completions
Two supplements to Mathlib's theory of valuations attached to height-one primes of a Dedekind domain are made here, both in the namespace IsDedekindDomain.HeightOneSpectrum.
The first is an instance recording separability of adic completions. For a Dedekind domain R with fraction field K and a height-one prime v of R, if K is countable as a type then the completion v.\mathrm{adicCompletion}\ K of K at v is a separable topological space: the countable set obtained as the image of K under the canonical map into the completion is dense, by denseRange_algebraMap. Thus the topological space underlying the v-adic completion of a countable fraction field admits a countable dense subset.
The second is the lemma IsDedekindDomain.HeightOneSpectrum.intValuation_eq_coe_neg_multiplicity: for a Dedekind domain A, a height-one prime v of A with underlying prime ideal v.asIdeal, and a nonzero a \in A, the integral valuation v.\mathrm{intValuation}\ a equals \mathrm{WithZero.exp}\bigl(-m\bigr), where m \in \mathbb{Z} is the multiplicity of v.asIdeal in the principal ideal \langle a\rangle = Ideal.span {a}, that is, the largest n with v^{n} \mid \langle a\rangle, coerced from \mathbb{N} to \mathbb{Z}; here \mathrm{WithZero.exp} is the embedding of \mathbb{Z} into the multiplicative group with zero in which the valuation takes its values. The proof rewrites Mathlib's definition of intValuation for nonzero arguments, which is phrased through the count of v.asIdeal among the normalised factors of \langle a\rangle in the monoid of associated ideals, and identifies that count with the multiplicity.
Relation to Mathlib
intValuation, adicCompletion and multiplicity are Mathlib notions; this module adds to Mathlib's namespace a reformulation of intValuation in terms of multiplicity (Mathlib's own definition proceeds via counts of normalised factors) together with a separability instance for adic completions of a countable fraction field.
Where it is used
These facts serve the handling of v-adic valuations and their completions in the number-theoretic parts of the development, where valuations of elements of a Dedekind domain must be computed ideal-theoretically and where topological properties of local fields are needed.
References
- J. Neukirch, Algebraic Number Theory, Grundlehren der mathematischen Wissenschaften 322, Springer, 1999, Ch. I–II
References are suggested automatically and have not been individually verified.
English text generated automatically from the Lean source; the Lean statement is authoritative.
- 32 lines
- 2 declarations
- used in the statements of 0 theorems and imported by 2 proofs
- imports 0 definition modules
Source file: Definitions/Def_Mathlib_RingTheory_DedekindDomain_AdicValuation.lean
Declarations
Source
import Mathlib section namespace IsDedekindDomain.HeightOneSpectrum open IsDedekindDomain instance {R : Type*} [CommRing R] [IsDedekindDomain R] (K : Type*) [Field K] [Countable K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : TopologicalSpace.SeparableSpace (v.adicCompletion K) where exists_countable_dense := ⟨_, Set.countable_range _, denseRange_algebraMap (K := K) (v := v)⟩ lemma intValuation_eq_coe_neg_multiplicity {A : Type*} [CommRing A] [IsDedekindDomain A] (v : HeightOneSpectrum A) {a : A} (hnz : a ≠ 0) : v.intValuation a = WithZero.exp (-(multiplicity v.asIdeal (Ideal.span {a}) : ℤ)) := by classical have hnb : Ideal.span {a} ≠ ⊥ := by rwa [ne_eq, Ideal.span_singleton_eq_bot] rw [intValuation_if_neg _ hnz, count_associates_factors_eq hnb v.isPrime v.ne_bot] nth_rw 1 [← normalize_eq v.asIdeal] congr symm apply multiplicity_eq_of_emultiplicity_eq_some rw [← UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors v.irreducible hnb] end IsDedekindDomain.HeightOneSpectrum end
Statements phrased using this module (0)
No statement module imports it directly (it is used through other definition modules or by proofs).