The basics of valuation theory.
The basic theory of valuations (non-archimedean norms) on a commutative ring, following T. Wedhorn's unpublished notes “Adic Spaces” ([wedhorn_adic]).
The definition of a valuation we use here is Definition 1.22 of [wedhorn_adic].
A valuation on a ring R is a monoid homomorphism v to a linearly ordered
commutative group with zero, that in addition satisfies the following two axioms:
v 0 = 0∀ x y, v (x + y) ≤ max (v x) (v y)
valuation R Γ₀is the type of valuations R → Γ₀, with a coercion to the underlying
function. If v is a valuation from R to Γ₀ then the induced group
homomorphism units(R) → Γ₀ is called unit_map v.
The equivalence "relation" is_equiv v₁ v₂ : Prop defined in 1.27 of [wedhorn_adic] is not strictly
speaking a relation, because v₁ : valuation R Γ₁ and v₂ : valuation R Γ₂ might
not have the same type. This corresponds in ZFC to the set-theoretic difficulty
that the class of all valuations (as Γ₀ varies) on a ring R is not a set.
The "relation" is however reflexive, symmetric and transitive in the obvious
sense. Note that we use 1.27(iii) of [wedhorn_adic] as the definition of equivalence.
The support of a valuation v : valuation R Γ₀ is supp v. If J is an ideal of R
with h : J ⊆ supp v then the induced valuation
on R / J = ideal.quotient J is on_quot v h.
Main definitions
valuation R Γ₀, the type of valuations onRwith values inΓ₀valuation.is_equiv, the heterogeneous equivalence relation on valuationsvaluation.supp, the support of a valuation
The monoid_hom underlying a valuation.
- to_fun : R → Γ₀
- map_one' : c.to_fun 1 = 1
- map_mul' : ∀ (x y : R), c.to_fun (x * y) = c.to_fun x * c.to_fun y
- map_zero' : c.to_fun 0 = 0
- map_add' : ∀ (x y : R), c.to_fun (x + y) ≤ max (c.to_fun x) (c.to_fun y)
The type of Γ₀-valued valuations on R.
A valuation is coerced to the underlying function R → Γ₀.
Equations
- valuation.has_coe_to_fun R Γ₀ = {F := λ (_x : valuation R Γ₀), R → Γ₀, coe := valuation.to_fun _inst_4}
A valuation is coerced to a monoid morphism R → Γ₀.
Equations
- valuation.has_coe R Γ₀ = {coe := valuation.to_monoid_hom _inst_4}
A valuation gives a preorder on the underlying ring.
Equations
If v is a valuation on a division ring then v(x) = 0 iff x = 0.
A ring homomorphism S → R induces a map valuation R Γ₀ → valuation S Γ₀
A ≤-preserving group homomorphism Γ₀ → Γ'₀ induces a map valuation R Γ₀ → valuation R Γ'₀.
Two valuations on R are defined to be equivalent if they induce the same preorder on R.
comap preserves equivalence.
The support of a valuation v : R → Γ₀ is the ideal of R where v vanishes.
The support of a valuation is a prime ideal.
Equations
- _ = _
If hJ : J ⊆ supp v then on_quot_val hJ is the induced function on R/J as a function.
Note: it's just the function; the valuation is on_quot hJ.
Equations
- v.on_quot_val hJ = λ (q : J.quotient), quotient.lift_on' q ⇑v _
The extension of valuation v on R to valuation on R/J if J ⊆ supp v
The quotient valuation on R/J has support supp(v)/J if J ⊆ supp v.