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 onR
with 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.