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 valuationsValuation.supp
, the support of a valuationAddValuation 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 DFunLike
by migrating the
boilerplate lemmas to ValuationClass
.
The type of Γ₀
-valued valuations on R
.
When you extend this structure, make sure to extend ValuationClass
.
- toFun : R → Γ₀
- map_zero' : (↑self.toMonoidWithZeroHom).toFun 0 = 0
- map_one' : (↑self.toMonoidWithZeroHom).toFun 1 = 1
- map_add_le_max' : ∀ (x y : R), (↑self.toMonoidWithZeroHom).toFun (x + y) ≤ max ((↑self.toMonoidWithZeroHom).toFun x) ((↑self.toMonoidWithZeroHom).toFun y)
The valuation of a a sum is less that the sum of the valuations
Instances For
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
.
- 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
Instances
The valuation of a a sum is less that the sum of the valuations
Equations
- instCoeTCValuationOfValuationClass F R Γ₀ = { coe := fun (f : F) => { toFun := ⇑f, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯, map_add_le_max' := ⋯ } }
Equations
- ⋯ = ⋯
Deprecated. Use DFunLike.ext_iff
.
A valuation gives a preorder on the underlying ring.
Equations
- v.toPreorder = Preorder.lift ⇑v
Instances For
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 Γ₀
.
Equations
- Valuation.comap f v = let __src := v.comp f.toMonoidWithZeroHom; { toFun := ⇑v ∘ ⇑f, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯, map_add_le_max' := ⋯ }
Instances For
A ≤
-preserving group homomorphism Γ₀ → Γ'₀
induces a map Valuation R Γ₀ → Valuation R Γ'₀
.
Equations
- Valuation.map f hf v = let __src := f.comp v.toMonoidWithZeroHom; { toFun := ⇑f ∘ ⇑v, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯, map_add_le_max' := ⋯ }
Instances For
Two valuations on R
are defined to be equivalent if they induce the same preorder on R
.
Instances For
This theorem is a weaker version of Valuation.val_le_one_or_val_inv_lt_one
, but more symmetric
in x
and x⁻¹
.
The subgroup of elements whose valuation is less than a certain unit.
Equations
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.
Equations
- ⋯ = ⋯
The type of Γ₀
-valued additive valuations on R
.
Equations
- AddValuation R Γ₀ = Valuation R (Multiplicative Γ₀ᵒᵈ)
Instances For
A valuation is coerced to the underlying function R → Γ₀
.
Equations
- AddValuation.instFunLike R Γ₀ = { coe := fun (v : AddValuation R Γ₀) => (↑v.toMonoidWithZeroHom).toFun, coe_injective' := ⋯ }
An alternate constructor of AddValuation
, that doesn't reference Multiplicative Γ₀ᵒᵈ
Equations
- AddValuation.of f h0 h1 hadd hmul = { toFun := f, map_zero' := h0, map_one' := h1, map_mul' := hmul, map_add_le_max' := hadd }
Instances For
The Valuation
associated to an AddValuation
(useful if the latter is constructed using
AddValuation.of
).
Equations
- v.valuation = v
Instances For
A helper function for Lean to inferring types correctly
Equations
- v.asFun = ⇑v
Instances For
A valuation gives a preorder on the underlying ring.
Equations
- v.toPreorder = Preorder.lift ⇑v
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 Γ₀
.
Equations
- AddValuation.comap f v = Valuation.comap f v
Instances For
A ≤
-preserving, ⊤
-preserving group homomorphism Γ₀ → Γ'₀
induces a map
AddValuation R Γ₀ → AddValuation R Γ'₀
.
Equations
- AddValuation.map f ht hf v = Valuation.map { toFun := ⇑f, map_zero' := ht, map_one' := ⋯, map_mul' := ⋯ } ⋯ v
Instances For
Two additive valuations on R
are defined to be equivalent if they induce the same
preorder on R
.
Equations
- v₁.IsEquiv v₂ = Valuation.IsEquiv v₁ v₂
Instances For
comap
preserves equivalence.
The support of an additive valuation v : R → Γ₀
is the ideal of R
where v x = ⊤
Equations
- v.supp = Valuation.supp v
Instances For
Notation for WithZero (Multiplicative ℕ)
Equations
- DiscreteValuation.termℕₘ₀ = Lean.ParserDescr.node `DiscreteValuation.termℕₘ₀ 1024 (Lean.ParserDescr.symbol "ℕₘ₀")
Instances For
Notation for WithZero (Multiplicative ℤ)
Equations
- DiscreteValuation.termℤₘ₀ = Lean.ParserDescr.node `DiscreteValuation.termℤₘ₀ 1024 (Lean.ParserDescr.symbol "ℤₘ₀")