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 Γ₀)
:
Subring R
The ring of integers under a given valuation is the subring of elements with valuation ≤ 1.
Equations
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
.
- 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
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)
:
Function.Injective ⇑(algebraMap O R)
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
- v.instAlgebraSubtypeMemSubringInteger = Algebra.ofSubring v.integer
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)
:
IsUnit x
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