Valuation Rings #
A valuation ring is a domain such that for every pair of elements
a b, either
b or vice-versa.
Any valuation ring induces a natural valuation on its fraction field, as we show in this file.
Namely, given the following instances:
[CommRing A] [IsDomain A] [ValuationRing A] [Field K] [Algebra A K] [IsFractionRing A K],
there is a natural valuation
Valuation A K on
K with values in
value_group A K where
the image of
algebraMap A K agrees with
(Valuation A K).integer.
We also provide the equivalence of the following notions for a domain
Ris a valuation ring.
- For each
x : FractionRing K, either
- "divides" is a total relation on the elements of
- "contains" is a total relation on the ideals of
Ris a local bezout domain.
The valuation ring
A is isomorphic to the ring of integers of its associated valuation.
v.integers 𝒪 where
v is a valuation on a field, then
is a valuation ring.