Compatibility of global and localized Dedekind orders

The height-one valuation of a Dedekind domain and the maximal-ideal valuation of its localization at that height-one prime have the same normalization. This file proves equality, rather than equivalence up to an unspecified rescaling, and transfers the associated principal-ideal orders.

theorem BGS.CorvajaZannier.valuation_eq_of_isEquiv_of_surjective {F : Type u_1} [Field F] {v w : Valuation F (WithZero (Multiplicative ℤ))} (h : v.IsEquiv w) (hv : Function.Surjective ⇑v) (hw : Function.Surjective ⇑w) : v = w

Equivalent surjective valuations with value group ℤᵐ⁰ have the same normalization. Surjectivity rules out a nontrivial integral rescaling.

theorem BGS.CorvajaZannier.fractionRingAlgEquiv_valuation {R : Type u_1} {L : Type u_2} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] (q : IsDedekindDomain.HeightOneSpectrum R) (x : FractionRing R) : (IsDedekindDomain.HeightOneSpectrum.valuation L q) ((FractionRing.algEquiv R L) x) = (IsDedekindDomain.HeightOneSpectrum.valuation (FractionRing R) q) x

The canonical equivalence from the chosen fraction-ring model preserves every normalized height-one valuation.

theorem BGS.CorvajaZannier.fractionRingAlgEquiv_finitePlaceOrder_eq {R : Type u_1} {L : Type u_2} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] (q : IsDedekindDomain.HeightOneSpectrum R) (x : FractionRing R) : finitePlaceOrder q ((FractionRing.algEquiv R L) x) = finitePlaceOrder q x

The canonical fraction-ring equivalence preserves the additive order at every height-one prime, including Mathlib's zero-order convention.

theorem BGS.CorvajaZannier.localizationAtPrime_valuation_eq {R : Type u_1} {S : Type u_2} {L : Type u_3} [CommRing R] [IsDedekindDomain R] [CommRing S] [IsDomain S] [IsDiscreteValuationRing S] [Field L] [Algebra R S] [Algebra R L] [Algebra S L] [IsScalarTower R S L] [IsFractionRing R L] [IsFractionRing S L] (q : IsDedekindDomain.HeightOneSpectrum R) [IsLocalization q.asIdeal.primeCompl S] : IsDedekindDomain.HeightOneSpectrum.valuation L (IsDiscreteValuationRing.maximalIdeal S) = IsDedekindDomain.HeightOneSpectrum.valuation L q

The normalized valuation of the maximal ideal of R_q is the normalized height-one valuation attached to q.

theorem BGS.CorvajaZannier.localizationAtPrime_finitePlaceOrder_eq {R : Type u_1} {S : Type u_2} {L : Type u_3} [CommRing R] [IsDedekindDomain R] [CommRing S] [IsDomain S] [IsDiscreteValuationRing S] [Field L] [Algebra R S] [Algebra R L] [Algebra S L] [IsScalarTower R S L] [IsFractionRing R L] [IsFractionRing S L] (q : IsDedekindDomain.HeightOneSpectrum R) [IsLocalization q.asIdeal.primeCompl S] (x : L) : finitePlaceOrder (IsDiscreteValuationRing.maximalIdeal S) x = finitePlaceOrder q x

Principal-ideal orders computed globally and in the localized DVR agree.

theorem BGS.CorvajaZannier.localizationAtPrime_finitePlaceOrderTop_eq {R : Type u_1} {S : Type u_2} {L : Type u_3} [CommRing R] [IsDedekindDomain R] [CommRing S] [IsDomain S] [IsDiscreteValuationRing S] [Field L] [Algebra R S] [Algebra R L] [Algebra S L] [IsScalarTower R S L] [IsFractionRing R L] [IsFractionRing S L] (q : IsDedekindDomain.HeightOneSpectrum R) [IsLocalization q.asIdeal.primeCompl S] (x : L) : finitePlaceOrderTop (IsDiscreteValuationRing.maximalIdeal S) x = finitePlaceOrderTop q x

WithTop-valued orders computed globally and in the localized DVR agree, including the zero element.