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
structure
Valuation.Integers
{R : Type u}
{Γ₀ : Type v}
[CommRing R]
[LinearOrderedCommGroupWithZero Γ₀]
(v : Valuation R Γ₀)
(O : Type w)
[CommRing O]
[Algebra O R]
:
- 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, ↑(algebraMap 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.
Instances For
instance
Valuation.instAlgebraSubtypeMemSubringToRingInstMembershipInstSetLikeSubringIntegerToCommSemiringToCommSemiringToSubsemiringToSemiring
{R : Type u}
{Γ₀ : Type v}
[CommRing R]
[LinearOrderedCommGroupWithZero Γ₀]
(v : Valuation R Γ₀)
:
Algebra { x // x ∈ Valuation.integer v } R
theorem
Valuation.integer.integers
{R : Type u}
{Γ₀ : Type v}
[CommRing R]
[LinearOrderedCommGroupWithZero Γ₀]
(v : Valuation R Γ₀)
:
Valuation.Integers v { x // x ∈ Valuation.integer v }
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