Ring of integers under a given valuation

The elements with valuation less than or equal to 1.

TODO: Define characteristic predicate.

def Valuation.integer {R : Type u} {Γ₀ : Type v} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) : Subring R

The ring of integers under a given valuation is the subring of elements with valuation ≤ 1.

Equations

• v.integer = { carrier := {x : R | v x ≤ 1}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

theorem Valuation.mem_integer_iff {R : Type u} {Γ₀ : Type v} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) (r : R) : r ∈ v.integer ↔ v r ≤ 1

structure Valuation.Integers {R : Type u} {Γ₀ : Type v} [CommRing R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) (O : Type w) [CommRing O] [Algebra O R] : Prop

Given a valuation v : R → Γ₀ and a ring homomorphism O →+* R, we say that O is the integers of v if f is injective, and its range is exactly v.integer.

• hom_inj : Function.Injective ⇑(algebraMap O R)
• map_le_one (x : O) : v ((algebraMap O R) x) ≤ 1
• exists_of_le_one ⦃r : R⦄ : v r ≤ 1 → ∃ (x : O), (algebraMap O R) x = r

instance Valuation.instAlgebraSubtypeMemSubringInteger {R : Type u} {Γ₀ : Type v} [CommRing R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) : Algebra (↥v.integer) R

Equations

• v.instAlgebraSubtypeMemSubringInteger = Algebra.ofSubring v.integer

theorem Valuation.integer.integers {R : Type u} {Γ₀ : Type v} [CommRing R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) : v.Integers ↥v.integer

theorem Valuation.Integers.one_of_isUnit' {R : Type u} {Γ₀ : Type v} [CommRing R] [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation R Γ₀} {O : Type w} [CommRing O] [Algebra O R] {x : O} (hx : IsUnit x) (H : ∀ (x : O), v ((algebraMap O R) x) ≤ 1) : v ((algebraMap O R) x) = 1

theorem Valuation.Integers.one_of_isUnit {R : Type u} {Γ₀ : Type v} [CommRing R] [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation R Γ₀} {O : Type w} [CommRing O] [Algebra O R] (hv : v.Integers O) {x : O} (hx : IsUnit x) : v ((algebraMap O R) x) = 1

theorem Valuation.Integers.isUnit_of_one {R : Type u} {Γ₀ : Type v} [CommRing R] [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation R Γ₀} {O : Type w} [CommRing O] [Algebra O R] (hv : v.Integers O) {x : O} (hx : IsUnit ((algebraMap O R) x)) (hvx : v ((algebraMap O R) x) = 1) : IsUnit x

Let O be the integers of the valuation v on some commutative ring R. For every element x in O, x is a unit in O if and only if the image of x in R is a unit and has valuation 1.

theorem Valuation.Integers.le_of_dvd {R : Type u} {Γ₀ : Type v} [CommRing R] [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation R Γ₀} {O : Type w} [CommRing O] [Algebra O R] (hv : v.Integers O) {x y : O} (h : x ∣ y) : v ((algebraMap O R) y) ≤ v ((algebraMap O R) x)

theorem Valuation.Integers.dvd_of_le {F : Type u} {Γ₀ : Type v} [Field F] [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation F Γ₀} {O : Type w} [CommRing O] [Algebra O F] (hv : v.Integers O) {x y : O} (h : v ((algebraMap O F) x) ≤ v ((algebraMap O F) y)) : y ∣ x

theorem Valuation.Integers.dvd_iff_le {F : Type u} {Γ₀ : Type v} [Field F] [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation F Γ₀} {O : Type w} [CommRing O] [Algebra O F] (hv : v.Integers O) {x y : O} : x ∣ y ↔ v ((algebraMap O F) y) ≤ v ((algebraMap O F) x)

theorem Valuation.Integers.le_iff_dvd {F : Type u} {Γ₀ : Type v} [Field F] [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation F Γ₀} {O : Type w} [CommRing O] [Algebra O F] (hv : v.Integers O) {x y : O} : v ((algebraMap O F) x) ≤ v ((algebraMap O F) y) ↔ y ∣ x

theorem Valuation.Integers.isUnit_of_one' {F : Type u} {Γ₀ : Type v} [Field F] [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation F Γ₀} {O : Type w} [CommRing O] [Algebra O F] (hv : v.Integers O) {x : O} (hvx : v ((algebraMap O F) x) = 1) : IsUnit x

This is the special case of Valuation.Integers.isUnit_of_one when the valuation is defined over a field. Let v be a valuation on some field F and O be its integers. For every element x in O, x is a unit in O if and only if the image of x in F has valuation 1.

theorem Valuation.Integers.isUnit_iff_valuation_eq_one {F : Type u} {Γ₀ : Type v} [Field F] [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation F Γ₀} {O : Type w} [CommRing O] [Algebra O F] (hv : v.Integers O) {x : O} : IsUnit x ↔ v ((algebraMap O F) x) = 1

theorem Valuation.Integers.valuation_unit {F : Type u} {Γ₀ : Type v} [Field F] [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation F Γ₀} {O : Type w} [CommRing O] [Algebra O F] (hv : v.Integers O) (x : Oˣ) : v ((algebraMap O F) ↑x) = 1

theorem Valuation.Integers.valuation_pos_iff_ne_zero {F : Type u} {Γ₀ : Type v} [Field F] [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation F Γ₀} {O : Type w} [CommRing O] [Algebra O F] (hv : v.Integers O) {x : O} : 0 < v ((algebraMap O F) x) ↔ x ≠ 0

theorem Valuation.Integers.dvdNotUnit_iff_lt {F : Type u} {Γ₀ : Type v} [Field F] [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation F Γ₀} {O : Type w} [CommRing O] [Algebra O F] (hv : v.Integers O) {x y : O} : DvdNotUnit x y ↔ v ((algebraMap O F) y) < v ((algebraMap O F) x)

theorem Valuation.Integers.eq_algebraMap_or_inv_eq_algebraMap {F : Type u} {Γ₀ : Type v} [Field F] [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation F Γ₀} {O : Type w} [CommRing O] [Algebra O F] (hv : v.Integers O) (x : F) : ∃ (a : O), x = (algebraMap O F) a ∨ x⁻¹ = (algebraMap O F) a

theorem Valuation.Integers.isPrincipal_iff_exists_isGreatest {F : Type u} {Γ₀ : Type v} [Field F] [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation F Γ₀} {O : Type w} [CommRing O] [Algebra O F] (hv : v.Integers O) {I : Ideal O} : Submodule.IsPrincipal I ↔ ∃ (x : Γ₀), IsGreatest (⇑v ∘ ⇑(algebraMap O F) '' ↑I) x

theorem Valuation.Integers.isPrincipal_iff_exists_eq_setOf_valuation_le {F : Type u} {Γ₀ : Type v} [Field F] [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation F Γ₀} {O : Type w} [CommRing O] [Algebra O F] (hv : v.Integers O) {I : Ideal O} : Submodule.IsPrincipal I ↔ ∃ (x : O), ↑I = {y : O | v ((algebraMap O F) y) ≤ v ((algebraMap O F) x)}

theorem Valuation.Integers.not_denselyOrdered_of_isPrincipalIdealRing {F : Type u} {Γ₀ : Type v} [Field F] [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation F Γ₀} {O : Type w} [CommRing O] [Algebra O F] [IsPrincipalIdealRing O] (hv : v.Integers O) : ¬DenselyOrdered ↑(Set.range ⇑v)