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 monoid 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" IsEquiv 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.
Main definitions #
-
Valuation R Γ₀
, the type of valuations onR
with values inΓ₀
-
Valuation.IsEquiv
, the heterogeneous equivalence relation on valuations -
Valuation.supp
, the support of a valuation -
AddValuation R Γ₀
, the type of additive valuations onR
with values in a linearly ordered additive commutative group with a top element,Γ₀
.
Implementation Details #
AddValuation R Γ₀
is implemented as Valuation R (Multiplicative Γ₀)ᵒᵈ
.
Notation #
In the DiscreteValuation
locale:
ℕₘ₀
is a shorthand forWithZero (Multiplicative ℕ)
ℤₘ₀
is a shorthand forWithZero (Multiplicative ℤ)
TODO #
If ever someone extends Valuation
, we should fully comply to the FunLike
by migrating the
boilerplate lemmas to ValuationClass
.
- toFun : R → Γ₀
- map_zero' : ZeroHom.toFun (↑s.toMonoidWithZeroHom) 0 = 0
- map_one' : ZeroHom.toFun (↑s.toMonoidWithZeroHom) 1 = 1
- map_mul' : ∀ (x y : R), ZeroHom.toFun (↑s.toMonoidWithZeroHom) (x * y) = ZeroHom.toFun (↑s.toMonoidWithZeroHom) x * ZeroHom.toFun (↑s.toMonoidWithZeroHom) y
- map_add_le_max' : ∀ (x y : R), ZeroHom.toFun (↑s.toMonoidWithZeroHom) (x + y) ≤ max (ZeroHom.toFun (↑s.toMonoidWithZeroHom) x) (ZeroHom.toFun (↑s.toMonoidWithZeroHom) y)
The valuation of a a sum is less that the sum of the valuations
The type of Γ₀
-valued valuations on R
.
When you extend this structure, make sure to extend ValuationClass
.
Instances For
- coe : F → R → Γ₀
- coe_injective' : Function.Injective FunLike.coe
- map_one : ∀ (f : F), ↑f 1 = 1
- map_zero : ∀ (f : F), ↑f 0 = 0
The valuation of a a sum is less that the sum of the valuations
ValuationClass F α β
states that F
is a type of valuations.
You should also extend this typeclass when you extend Valuation
.
Instances
Deprecated. Use FunLike.ext_iff
.
A valuation gives a preorder on the underlying ring.
Instances For
If v
is a valuation on a division ring then v(x) = 0
iff x = 0
.
A ≤
-preserving group homomorphism Γ₀ → Γ'₀
induces a map Valuation R Γ₀ → Valuation R Γ'₀
.
Instances For
Two valuations on R
are defined to be equivalent if they induce the same preorder on R
.
Instances For
The subgroup of elements whose valuation is less than a certain unit.
Instances For
comap
preserves equivalence.
The support of a valuation v : R → Γ₀
is the ideal of R
where v
vanishes.
Instances For
The support of a valuation is a prime ideal.
The type of Γ₀
-valued additive valuations on R
.
Instances For
A valuation is coerced to the underlying function R → Γ₀
.
An alternate constructor of AddValuation
, that doesn't reference Multiplicative Γ₀ᵒᵈ
Instances For
The Valuation
associated to an AddValuation
(useful if the latter is constructed using
AddValuation.of
).
Instances For
A helper function for Lean to inferring types correctly
Instances For
A valuation gives a preorder on the underlying ring.
Instances For
If v
is an additive valuation on a division ring then v(x) = ⊤
iff x = 0
.
A ring homomorphism S → R
induces a map AddValuation R Γ₀ → AddValuation S Γ₀
.
Instances For
A ≤
-preserving, ⊤
-preserving group homomorphism Γ₀ → Γ'₀
induces a map
AddValuation R Γ₀ → AddValuation R Γ'₀
.
Instances For
Two additive valuations on R
are defined to be equivalent if they induce the same
preorder on R
.
Instances For
comap
preserves equivalence.
The support of an additive valuation v : R → Γ₀
is the ideal of R
where v x = ⊤
Instances For
Notation for WithZero (Multiplicative ℕ)
Instances For
Notation for WithZero (Multiplicative ℤ)