Documentation

Mathlib.RingTheory.Valuation.Integers

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 Γ₀) :

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' := }
Instances For
    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] :

    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.

    Instances For
      theorem Valuation.Integers.hom_inj {R : Type u} {Γ₀ : Type v} [CommRing R] [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation R Γ₀} {O : Type w} [CommRing O] [Algebra O R] (self : v.Integers O) :
      theorem Valuation.Integers.map_le_one {R : Type u} {Γ₀ : Type v} [CommRing R] [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation R Γ₀} {O : Type w} [CommRing O] [Algebra O R] (self : v.Integers O) (x : O) :
      v ((algebraMap O R) x) 1
      theorem Valuation.Integers.exists_of_le_one {R : Type u} {Γ₀ : Type v} [CommRing R] [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation R Γ₀} {O : Type w} [CommRing O] [Algebra O R] (self : v.Integers O) ⦃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
      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) :

      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 : O} {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 : O} {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 : O} {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 : O} {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) :

      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.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