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)
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.
- 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 → Γ₀.
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
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
The extension of valuation v on R to valuation on R/J if J ⊆ supp v