mathlib documentation

ring_theory.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] [linear_ordered_comm_group_with_zero Γ₀] (v : valuation R Γ₀) :

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

Equations
structure valuation.integers {R : Type u} {Γ₀ : Type v} [comm_ring R] [linear_ordered_comm_group_with_zero Γ₀] (v : valuation R Γ₀) (O : Type w) [comm_ring 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.

@[instance]
def valuation.algebra {R : Type u} {Γ₀ : Type v} [comm_ring R] [linear_ordered_comm_group_with_zero Γ₀] (v : valuation R Γ₀) :

Equations
theorem valuation.integer.integers {R : Type u} {Γ₀ : Type v} [comm_ring R] [linear_ordered_comm_group_with_zero Γ₀] (v : valuation R Γ₀) :

theorem valuation.integers.one_of_is_unit {R : Type u} {Γ₀ : Type v} [comm_ring R] [linear_ordered_comm_group_with_zero Γ₀] {v : valuation R Γ₀} {O : Type w} [comm_ring O] [algebra O R] (hv : v.integers O) {x : O} (hx : is_unit x) :
v ((algebra_map O R) x) = 1

theorem valuation.integers.is_unit_of_one {R : Type u} {Γ₀ : Type v} [comm_ring R] [linear_ordered_comm_group_with_zero Γ₀] {v : valuation R Γ₀} {O : Type w} [comm_ring O] [algebra O R] (hv : v.integers O) {x : O} (hx : is_unit ((algebra_map O R) x)) (hvx : v ((algebra_map O R) x) = 1) :

theorem valuation.integers.le_of_dvd {R : Type u} {Γ₀ : Type v} [comm_ring R] [linear_ordered_comm_group_with_zero Γ₀] {v : valuation R Γ₀} {O : Type w} [comm_ring O] [algebra O R] (hv : v.integers O) {x y : O} (h : x y) :
v ((algebra_map O R) y) v ((algebra_map O R) x)

theorem valuation.integers.dvd_of_le {F : Type u} {Γ₀ : Type v} [field F] [linear_ordered_comm_group_with_zero Γ₀] {v : valuation F Γ₀} {O : Type w} [comm_ring O] [algebra O F] (hv : v.integers O) {x y : O} (h : v ((algebra_map O F) x) v ((algebra_map O F) y)) :
y x

theorem valuation.integers.dvd_iff_le {F : Type u} {Γ₀ : Type v} [field F] [linear_ordered_comm_group_with_zero Γ₀] {v : valuation F Γ₀} {O : Type w} [comm_ring O] [algebra O F] (hv : v.integers O) {x y : O} :
x y v ((algebra_map O F) y) v ((algebra_map O F) x)

theorem valuation.integers.le_iff_dvd {F : Type u} {Γ₀ : Type v} [field F] [linear_ordered_comm_group_with_zero Γ₀] {v : valuation F Γ₀} {O : Type w} [comm_ring O] [algebra O F] (hv : v.integers O) {x y : O} :
v ((algebra_map O F) x) v ((algebra_map O F) y) y x