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 Γ₀) :
subring R
The ring of integers under a given valuation is the subring of elements with valuation ≤ 1.
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
- hom_inj : function.injective ⇑(algebra_map O R)
- map_le_one : ∀ (x : O), ⇑v (⇑(algebra_map O R) x) ≤ 1
- exists_of_le_one : ∀ ⦃r : R⦄, ⇑v r ≤ 1 → (∃ (x : O), ⇑(algebra_map O R) x = 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.
@[protected, 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) :
is_unit x
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