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
  • One or more equations did not get rendered due to their size.
Instances For
    theorem Valuation.mem_integer_iff {R : Type u} {Γ₀ : Type v} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) (r : R) :
    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.one_of_isUnit {R : Type u} {Γ₀ : Type v} [CommRing R] [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation R Γ₀} {O : Type w} [CommRing O] [Algebra O R] (hv : Valuation.Integers v 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 : Valuation.Integers v O) {x : O} (hx : IsUnit ((algebraMap O R) x)) (hvx : v ((algebraMap O R) x) = 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 : Valuation.Integers v 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 : Valuation.Integers v 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 : Valuation.Integers v 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 : Valuation.Integers v O) {x : O} {y : O} :
      v ((algebraMap O F) x) v ((algebraMap O F) y) y x