Ring of integers under a given valuation #

The elements with valuation less than or equal to 1.

TODO: Define characteristic predicate.

source

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' := ⋯ }

Instances For

source

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

r ∈ v.integer ↔ v r ≤ 1

source

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

Instances For

source

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

source

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

v.Integers ↥v.integer

source

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

source

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

source

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.

source

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)

source

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

Nontrivial O ↔ Nontrivial R

source

theorem Valuation.integers_nontrivial {R : Type u} {Γ₀ : Type v} [CommRing R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) :

Nontrivial ↥v.integer ↔ Nontrivial R

source

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

source

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)

source

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

source

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.

source

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

source

theorem Valuation.Integers.valuation_irreducible_lt_one {F : Type u} {Γ₀ : Type v} [Field F] [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation F Γ₀} {O : Type w} [CommRing O] [Algebra O F] (hv : v.Integers O) {ϖ : O} (h : Irreducible ϖ) :

v ((algebraMap O F) ϖ) < 1

source

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

source

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

source

theorem Valuation.Integers.valuation_irreducible_pos {F : Type u} {Γ₀ : Type v} [Field F] [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation F Γ₀} {O : Type w} [CommRing O] [Algebra O F] (hv : v.Integers O) {ϖ : O} (h : Irreducible ϖ) :

0 < v ((algebraMap O F) ϖ)

source

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)

source

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

source

theorem Valuation.Integers.coe_span_singleton_eq_setOf_le_v_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 : O) :

↑(Ideal.span {x}) = {y : O | v ((algebraMap O F) y) ≤ v ((algebraMap O F) x)}

source

theorem Valuation.Integers.bijective_algebraMap_of_subsingleton_units_mrange {F : Type u} {Γ₀ : Type v} [Field F] [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation F Γ₀} {O : Type w} [CommRing O] [Algebra O F] (hv : v.Integers O) [Subsingleton (↥(MonoidHom.mrange v))ˣ] :

Function.Bijective ⇑(algebraMap O F)

source

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

source

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)}

source

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)

source

theorem Valuation.Integer.not_isUnit_iff_valuation_lt_one {F : Type u} {Γ₀ : Type v} [Field F] [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation F Γ₀} {x : ↥v.integer} :

¬IsUnit x ↔ v ↑x < 1

source

theorem Valuation.integer.v_irreducible_lt_one {F : Type u} {Γ₀ : Type v} [Field F] [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation F Γ₀} {ϖ : ↥v.integer} (h : Irreducible ϖ) :

v ↑ϖ < 1

source

theorem Valuation.integer.v_irreducible_pos {F : Type u} {Γ₀ : Type v} [Field F] [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation F Γ₀} {ϖ : ↥v.integer} (h : Irreducible ϖ) :

0 < v ↑ϖ

source

theorem Valuation.integer.coe_span_singleton_eq_setOf_le_v_coe {F : Type u} {Γ₀ : Type v} [Field F] [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation F Γ₀} (x : ↥v.integer) :

↑(Ideal.span {x}) = {y : ↥v.integer | v ↑y ≤ v ↑x}

source

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

Submodule (↥v.integer) R

The v.integer-submodule of R of elements whose valuation is less than or equal to a certain value.

Equations

v.leSubmodule γ = { toAddSubmonoid := (v.leAddSubgroup γ).toAddSubmonoid, smul_mem' := ⋯ }

Instances For

source

def Valuation.ltSubmodule {R : Type u} {Γ₀ : Type v} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) (γ : Γ₀ˣ) :

Submodule (↥v.integer) R

The v.integer-submodule of R of elements whose valuation is less than a certain unit.

Equations

v.ltSubmodule γ = { toAddSubmonoid := (v.ltAddSubgroup γ).toAddSubmonoid, smul_mem' := ⋯ }

Instances For

source

theorem Valuation.leSubmodule_monotone {R : Type u} {Γ₀ : Type v} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) :

Monotone v.leSubmodule

source

theorem Valuation.ltSubmodule_monotone {R : Type u} {Γ₀ : Type v} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) :

Monotone v.ltSubmodule

source

theorem Valuation.ltSubmodule_le_leSubmodule {R : Type u} {Γ₀ : Type v} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) (γ : Γ₀ˣ) :

v.ltSubmodule γ ≤ v.leSubmodule ↑γ

source

@[simp]

theorem Valuation.mem_leSubmodule_iff {R : Type u} {Γ₀ : Type v} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation R Γ₀} {γ : Γ₀} {x : R} :

x ∈ v.leSubmodule γ ↔ v x ≤ γ

source

@[simp]

theorem Valuation.mem_ltSubmodule_iff {R : Type u} {Γ₀ : Type v} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation R Γ₀} {γ : Γ₀ˣ} {x : R} :

x ∈ v.ltSubmodule γ ↔ v x < ↑γ

source

@[simp]

theorem Valuation.leSubmodule_zero {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] (K : Type u_1) [Field K] (v : Valuation K Γ₀) :

v.leSubmodule 0 = ⊥

source

theorem Valuation.leSubmodule_v_le_of_mem {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] {K : Type u_1} [Field K] (v : Valuation K Γ₀) {S : Submodule (↥v.integer) K} {x : K} (hx : x ∈ S) :

v.leSubmodule (v x) ≤ S

source

theorem Valuation.ltSubmodule_v_le_of_mem {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] {K : Type u_1} [Field K] {v : Valuation K Γ₀} {S : Submodule (↥v.integer) K} {x : K} (hx : x ∈ S) (hxv : v x ≠ 0) :

v.ltSubmodule (Units.mk0 (v x) hxv) ≤ S

source

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

Ideal ↥v.integer

The ideal of elements of the valuation subring whose valuation is less than or equal to a certain value.

Equations

v.leIdeal γ = { toAddSubmonoid := ((v.leAddSubgroup γ).addSubgroupOf v.integer.toAddSubgroup).toAddSubmonoid, smul_mem' := ⋯ }

Instances For

source

def Valuation.ltIdeal {R : Type u} {Γ₀ : Type v} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) (γ : Γ₀ˣ) :

Ideal ↥v.integer

The ideal of elements of the valuation subring whose valuation is less than a certain unit.

Equations

v.ltIdeal γ = { toAddSubmonoid := ((v.ltAddSubgroup γ).addSubgroupOf v.integer.toAddSubgroup).toAddSubmonoid, smul_mem' := ⋯ }

Instances For

source

theorem Valuation.leIdeal_mono {R : Type u} {Γ₀ : Type v} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) :

Monotone v.leIdeal

source

theorem Valuation.ltIdeal_mono {R : Type u} {Γ₀ : Type v} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) :

Monotone v.ltIdeal

source

theorem Valuation.ltIdeal_le_leIdeal {R : Type u} {Γ₀ : Type v} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) (γ : Γ₀ˣ) :

v.ltIdeal γ ≤ v.leIdeal ↑γ

source

@[simp]

theorem Valuation.mem_leIdeal_iff {R : Type u} {Γ₀ : Type v} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation R Γ₀} {γ : Γ₀} {x : ↥v.integer} :

x ∈ v.leIdeal γ ↔ v ↑x ≤ γ

source

@[simp]

theorem Valuation.mem_ltIdeal_iff {R : Type u} {Γ₀ : Type v} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation R Γ₀} {γ : Γ₀ˣ} {x : ↥v.integer} :

x ∈ v.ltIdeal γ ↔ v ↑x < ↑γ

source

@[simp]

theorem Valuation.leIdeal_zero {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] (K : Type u_1) [Field K] (v : Valuation K Γ₀) :

v.leIdeal 0 = ⊥

source

theorem Valuation.leSubmodule_comap_algebraMap_eq_leIdeal {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] {K : Type u_1} [Field K] (v : Valuation K Γ₀) (γ : Γ₀) :

Submodule.comap (Algebra.linearMap (↥v.integer) K) (v.leSubmodule γ) = v.leIdeal γ

source

theorem Valuation.leIdeal_map_algebraMap_eq_leSubmodule_min {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] {K : Type u_1} [Field K] (v : Valuation K Γ₀) (γ : Γ₀) :

Submodule.map (Algebra.linearMap (↥v.integer) K) (v.leIdeal γ) = v.leSubmodule (min 1 γ)

source

theorem Valuation.leIdeal_v_le_of_mem {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] {K : Type u_1} [Field K] (v : Valuation K Γ₀) {I : Ideal ↥v.integer} {x : ↥v.integer} (hx : x ∈ I) :

v.leIdeal (v ↑x) ≤ I

source

theorem Valuation.ltIdeal_v_le_of_mem {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] {K : Type u_1} [Field K] {v : Valuation K Γ₀} {I : Ideal ↥v.integer} {x : ↥v.integer} (hx : x ∈ I) (hxv : v ↑x ≠ 0) :

v.ltIdeal (Units.mk0 (v ↑x) hxv) ≤ I

Documentation

Mathlib.RingTheory.Valuation.Integers

Ring of integers under a given valuation #