Rings of integers: domains and perfection

A ring of integers O for a valuation v on a domain R (in the sense of Valuation.Integers) embeds into R, so it is a domain.

If O is a ring of integers for a valuation v on a ring R (in the sense of Valuation.Integers) and R is perfect, then so is O: a p-th root of an integral element is integral, since v y ^ p ≤ 1 forces v y ≤ 1. For instance the ring of integers 𝒪_F of a perfect valued field F of characteristic p is perfect, as is needed to form the Witt vectors W(𝒪_F) with their Teichmüller expansions.

A ring is its own ring of integers for any valuation that is at most 1 everywhere, for instance a domain for its trivial valuation. So constructions taking a ring of integers, such as the Gauss valuations on Witt vectors, apply to a perfect field with its trivial valuation.

Main results

• Valuation.Integers.isDomain: the ring of integers of a domain is a domain.
• Valuation.Integers.perfectRing: the ring of integers of a perfect ring is perfect.
• Valuation.integers_self_iff: a ring is the ring of integers of a valuation on it iff the valuation is at most 1 everywhere.

theorem Valuation.Integers.isDomain {R : Type u_1} {Γ₀ : Type u_2} {O : Type u_3} [CommRing R] [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation R Γ₀} [CommRing O] [Algebra O R] [IsDomain R] (hv : v.Integers O) : IsDomain O

The ring of integers of a domain is a domain, as it embeds into it.

theorem Valuation.Integers.perfectRing {R : Type u_1} {Γ₀ : Type u_2} {O : Type u_3} [CommRing R] [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation R Γ₀} [CommRing O] [Algebra O R] (hv : v.Integers O) (p : ℕ) [PerfectRing R p] : PerfectRing O p

The ring of integers of a perfect ring is perfect. If O is a ring of integers for a valuation on a ring R that is perfect for the exponent p, then O is perfect for p.

theorem Valuation.integers_self_iff {R : Type u_1} {Γ₀ : Type u_2} [CommRing R] [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation R Γ₀} : v.Integers R ↔ ∀ (x : R), v x ≤ 1

A ring is the ring of integers of a valuation on it exactly when the valuation is at most 1 everywhere. For instance a domain is the ring of integers of its trivial valuation (Valuation.one_apply_le_one).