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
- 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)
:
r ∈ Valuation.integer v ↔ v r ≤ 1
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
instance
Valuation.instAlgebraSubtypeMemSubringToRingInstMembershipInstSetLikeSubringIntegerToCommSemiringToCommSemiringToSubsemiringToSemiring
{R : Type u}
{Γ₀ : Type v}
[CommRing R]
[LinearOrderedCommGroupWithZero Γ₀]
(v : Valuation R Γ₀)
:
Algebra (↥(Valuation.integer v)) R
theorem
Valuation.integer.integers
{R : Type u}
{Γ₀ : Type v}
[CommRing R]
[LinearOrderedCommGroupWithZero Γ₀]
(v : Valuation R Γ₀)
:
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 : 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)
:
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 : 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