Extending a valuation to a localisation away from one element

Mathlib's Valuation.extendToLocalization extends a valuation v : Valuation A Γ₀ to a localisation of A at a submonoid avoiding the support of v. This file specialises it to a localisation away from a single element s, which is the case rational localisation uses: the submonoid is Submonoid.powers s, the side condition is the single inequality v s ≠ 0, and the elements one wants to evaluate the extension on are the fractions t/s of TauCeti.Localization.divBy.

Nothing here is topological or Huber-specific. The topological content — that the extension is continuous for Wedhorn's localisation topology — is in TauCeti.RingTheory.Huber.LocalizationTopology.Valuation.

Main results

• Valuation.powers_le_supp_primeCompl: v s ≠ 0 discharges the side condition of Valuation.extendToLocalization at the submonoid generated by s.
• Valuation.extendToLocalization_divBy: the extension sends t/s to v t / v s.
• Valuation.extendToLocalization_divBy_le_one: that value is ≤ 1 as soon as v t ≤ v s.

theorem Valuation.powers_le_supp_primeCompl {A : Type u_1} [CommRing A] {Γ₀ : Type u_2} [LinearOrderedCommMonoidWithZero Γ₀] [Nontrivial Γ₀] {v : Valuation A Γ₀} {s : A} (hs : v s ≠ 0) : Submonoid.powers s ≤ v.supp.primeCompl

The powers of an element with nonzero valuation avoid the support. This holds for monoid-valued valuations; for group-valued valuations it supplies the side condition for Valuation.extendToLocalization away from that element.

The value-monoid generalization is due to Claude Opus 5, in commit 7d80f5396.

@[simp]

theorem Valuation.extendToLocalization_divBy {A : Type u_1} [CommRing A] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (S : Type u_3) [CommRing S] [Algebra A S] {v : Valuation A Γ₀} {s : A} (hs : v s ≠ 0) [IsLocalization.Away s S] (t : A) : (v.extendToLocalization ⋯ S) (TauCeti.Localization.divBy t s) = v t * (v s)⁻¹

The extension on a distinguished fraction: t/s goes to v t / v s.

theorem Valuation.extendToLocalization_divBy_le_one {A : Type u_1} [CommRing A] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (S : Type u_3) [CommRing S] [Algebra A S] {v : Valuation A Γ₀} {s : A} (hs : v s ≠ 0) [IsLocalization.Away s S] {t : A} (ht : v t ≤ v s) : (v.extendToLocalization ⋯ S) (TauCeti.Localization.divBy t s) ≤ 1

The fraction t/s is sub-unit for the extension as soon as v t ≤ v s — one of the two conditions cutting out a rational subset.