Extending a valuation from a subring reached by the powers of an element

Let R be a subring of a ring A, and let s ∈ R be central in A, with some power of s carrying each element of A into R: for every a there is an n with sⁿ * a ∈ R. A valuation w of R that does not vanish at s then has only one possible extension to A,

v a = w (sⁿ * a) * (w s)⁻ⁿ,

and this file shows that the formula is well defined, is a valuation, and is the only valuation of A restricting to w.

No topology is involved. The hypothesis is met by a ring of definition of a Huber ring — it is open, so a topologically nilpotent s satisfies it — and TauCeti.RingTheory.Huber.ExtendValuation is that specialisation.

Why this is not Valuation.extendToLocalization

Mathlib extends a valuation along a localisation that inverts a set on which the valuation is nonzero. That does not apply here: the hypothesis does not make s invertible in A, so there need be no ring map R[1/s] → A at all. Take R = A = ℤ_[p] and s = p, where R[1/s] = ℚ_[p]. What is true, and is all the formula needs, is the one-sided statement that every element of A is carried into R by a power of s.

Well-definedness

Independence of n reduces to the case of comparing n with n + j, where s ^ (n + j) * a = s ^ j * (sⁿ * a) splits off a factor whose w-value is (w s) ^ j, exactly cancelling the extra (w s)⁻ʲ. Two arbitrary exponents are then compared through their sum.

The two valuation axioms reach a shared exponent differently. For a product, each argument keeps its own workable exponent — x at m and y at n — and only the product is evaluated at m + n, because s ^ (m + n) * (x * y) = (sᵐ * x) * (sⁿ * y) already splits that way. A sum has no such splitting, so there both terms are raised to the common exponent m + n. In each case the axiom is then inherited from w once the shared factor (w s)⁻⁽ᵐ⁺ⁿ⁾ is divided out.

Main definitions

• Valuation.extendOfPowMulMem : the extension of w to A.

Main results

• Valuation.extendOfPowMulMem_apply : the defining formula, at every exponent that works, not just the chosen one. This is the interface; the definition goes through Classical.choose and is not meant to be unfolded.
• Valuation.extendOfPowMulMem_coe : the extension restricts to w.
• Valuation.eq_extendOfPowMulMem : uniqueness — any valuation of A restricting to w is this one, so the extension is canonical.
• Valuation.extendOfPowMulMem_congr : consequently the extension does not depend on which s is used to build it.

References

• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Lemma 7.44(3), which uses this extension for a ring of definition of a Huber ring.

Provenance

Adapted from C. Birkbeck, AINTLIB, branch dev/adic-spaces, commit 37bbdaeb9, projects/AdicSpaces/Adic spaces/Lemma745.lean, declarations vExtFun_step, vExtFun_well_defined, vExtFun_map_mul, vExtFun_map_add_le_max and exists_valuation_extension. Adapted, not copied: that development states the result existentially, as ∃ v_ext, …, for a pair of definition of a Huber ring, and threads the value w s through five separate lemmas as an explicit parameter with its own defining equation. Here the extension is a def, so it can be named and rewritten at a call site, the arithmetic is one private lemma rather than four public ones, and the whole construction is carried out for a subring reached by the powers of s. The uniqueness theorem and the resulting independence of s have no counterpart there.

noncomputable def Valuation.extendOfPowMulMem {A : Type u_1} [Ring A] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {R : Subring A} (w : Valuation (↥R) Γ₀) {s : A} (hs : s ∈ R) (hcomm : ∀ (a : A), Commute s a) (hpow : ∀ (a : A), ∃ (n : ℕ), s ^ n * a ∈ R) (hw : w ⟨s, hs⟩ ≠ 0) : Valuation A Γ₀

The extension of w from R to A, when every element of A is carried into R by some power of a central element s. For any n with sⁿ * a ∈ R the value is w (sⁿ * a) * (w s)⁻ⁿ, and extendOfPowMulMem_apply says so at every such n.

Equations

• w.extendOfPowMulMem hs hcomm hpow hw = { toFun := fun (a : A) => w ⟨s ^ ⋯.choose * a, ⋯⟩ * (w ⟨s, hs⟩)⁻¹ ^ ⋯.choose, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯, map_add_le_max' := ⋯ }

theorem Valuation.extendOfPowMulMem_apply {A : Type u_1} [Ring A] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {R : Subring A} (w : Valuation (↥R) Γ₀) {s : A} (hs : s ∈ R) (hcomm : ∀ (a : A), Commute s a) (hpow : ∀ (a : A), ∃ (n : ℕ), s ^ n * a ∈ R) (hw : w ⟨s, hs⟩ ≠ 0) (a : A) {n : ℕ} (hn : s ^ n * a ∈ R) : (w.extendOfPowMulMem hs hcomm hpow hw) a = w ⟨s ^ n * a, hn⟩ * (w ⟨s, hs⟩)⁻¹ ^ n

The defining formula, at every exponent that carries a into the subring.

@[simp]

theorem Valuation.extendOfPowMulMem_coe {A : Type u_1} [Ring A] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {R : Subring A} (w : Valuation (↥R) Γ₀) {s : A} (hs : s ∈ R) (hcomm : ∀ (a : A), Commute s a) (hpow : ∀ (a : A), ∃ (n : ℕ), s ^ n * a ∈ R) (hw : w ⟨s, hs⟩ ≠ 0) (a : ↥R) : (w.extendOfPowMulMem hs hcomm hpow hw) ↑a = w a

The extension restricts to w.

theorem Valuation.eq_extendOfPowMulMem {A : Type u_1} [Ring A] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {R : Subring A} (w : Valuation (↥R) Γ₀) {s : A} (hs : s ∈ R) (hcomm : ∀ (a : A), Commute s a) (hpow : ∀ (a : A), ∃ (n : ℕ), s ^ n * a ∈ R) (hw : w ⟨s, hs⟩ ≠ 0) (v : Valuation A Γ₀) (hv : ∀ (a : ↥R), v ↑a = w a) : v = w.extendOfPowMulMem hs hcomm hpow hw

The extension is the only one: a valuation of A restricting to w on R is extendOfPowMulMem. In particular the extension is canonical.

theorem Valuation.extendOfPowMulMem_congr {A : Type u_1} [Ring A] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {R : Subring A} (w : Valuation (↥R) Γ₀) {s t : A} (hs : s ∈ R) (hcomms : ∀ (a : A), Commute s a) (hpows : ∀ (a : A), ∃ (n : ℕ), s ^ n * a ∈ R) (hws : w ⟨s, hs⟩ ≠ 0) (ht : t ∈ R) (hcommt : ∀ (a : A), Commute t a) (hpowt : ∀ (a : A), ∃ (n : ℕ), t ^ n * a ∈ R) (hwt : w ⟨t, ht⟩ ≠ 0) : w.extendOfPowMulMem hs hcomms hpows hws = w.extendOfPowMulMem ht hcommt hpowt hwt

The extension does not depend on s: two central elements of R whose powers carry A into R and at which w is nonzero give the same extension.