mathlib documentation

ring_theory.valuation.valuation_subring

Valuation subrings of a field #

Projects #

The order structure on valuation_subring K.

structure valuation_subring (K : Type u_1) [field K] :
Type u_1

A valuation subring of a field K is a subring A such that for every x : K, either x ∈ A or x⁻¹ ∈ K.

Instances for valuation_subring
@[protected, instance]
Equations
@[simp]
theorem valuation_subring.mem_carrier {K : Type u_1} [field K] (A : valuation_subring K) (x : K) :
@[simp]
theorem valuation_subring.mem_to_subring {K : Type u_1} [field K] (A : valuation_subring K) (x : K) :
@[ext]
theorem valuation_subring.ext {K : Type u_1} [field K] (A B : valuation_subring K) (h : ∀ (x : K), x A x B) :
A = B
theorem valuation_subring.zero_mem {K : Type u_1} [field K] (A : valuation_subring K) :
0 A
theorem valuation_subring.one_mem {K : Type u_1} [field K] (A : valuation_subring K) :
1 A
theorem valuation_subring.add_mem {K : Type u_1} [field K] (A : valuation_subring K) (x y : K) :
x Ay Ax + y A
theorem valuation_subring.mul_mem {K : Type u_1} [field K] (A : valuation_subring K) (x y : K) :
x Ay Ax * y A
theorem valuation_subring.neg_mem {K : Type u_1} [field K] (A : valuation_subring K) (x : K) :
x A-x A
theorem valuation_subring.mem_or_inv_mem {K : Type u_1} [field K] (A : valuation_subring K) (x : K) :
x A x⁻¹ A
@[protected, instance]
def valuation_subring.comm_ring {K : Type u_1} [field K] (A : valuation_subring K) :
Equations
@[protected, instance]
def valuation_subring.is_domain {K : Type u_1} [field K] (A : valuation_subring K) :
@[protected, instance]
Equations
theorem valuation_subring.mem_top {K : Type u_1} [field K] (x : K) :
theorem valuation_subring.le_top {K : Type u_1} [field K] (A : valuation_subring K) :
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
def valuation_subring.algebra {K : Type u_1} [field K] (A : valuation_subring K) :
Equations
@[simp]
theorem valuation_subring.algebra_map_apply {K : Type u_1} [field K] (A : valuation_subring K) (a : A) :
@[protected, instance]
def valuation_subring.value_group {K : Type u_1} [field K] (A : valuation_subring K) :
Type u_1

The value group of the valuation associated to A.

Equations
Instances for valuation_subring.value_group

Any valuation subring of K induces a natural valuation on K.

Equations
@[protected, instance]
noncomputable def valuation_subring.inhabited_value_group {K : Type u_1} [field K] (A : valuation_subring K) :
Equations
theorem valuation_subring.valuation_le_one {K : Type u_1} [field K] (A : valuation_subring K) (a : A) :
theorem valuation_subring.mem_of_valuation_le_one {K : Type u_1} [field K] (A : valuation_subring K) (x : K) (h : (A.valuation) x 1) :
x A
theorem valuation_subring.valuation_le_one_iff {K : Type u_1} [field K] (A : valuation_subring K) (x : K) :
(A.valuation) x 1 x A
theorem valuation_subring.valuation_eq_iff {K : Type u_1} [field K] (A : valuation_subring K) (x y : K) :
(A.valuation) x = (A.valuation) y ∃ (a : (A)ˣ), a * y = x
theorem valuation_subring.valuation_le_iff {K : Type u_1} [field K] (A : valuation_subring K) (x y : K) :
(A.valuation) x (A.valuation) y ∃ (a : A), a * y = x
theorem valuation_subring.valuation_unit {K : Type u_1} [field K] (A : valuation_subring K) (a : (A)ˣ) :
theorem valuation_subring.valuation_eq_one_iff {K : Type u_1} [field K] (A : valuation_subring K) (a : A) :
def valuation_subring.of_subring {K : Type u_1} [field K] (R : subring K) (hR : ∀ (x : K), x R x⁻¹ R) :

A subring R of K such that for all x : K either x ∈ R or x⁻¹ ∈ R is a valuation subring of K.

Equations
@[simp]
theorem valuation_subring.mem_of_subring {K : Type u_1} [field K] (R : subring K) (hR : ∀ (x : K), x R x⁻¹ R) (x : K) :
def valuation_subring.of_le {K : Type u_1} [field K] (R : valuation_subring K) (S : subring K) (h : R.to_subring S) :

An overring of a valuation ring is a valuation ring.

Equations
def valuation_subring.inclusion {K : Type u_1} [field K] (R S : valuation_subring K) (h : R S) :

The ring homomorphism induced by the partial order.

Equations
def valuation_subring.subtype {K : Type u_1} [field K] (R : valuation_subring K) :

The canonical ring homomorphism from a valuation ring to its field of fractions.

Equations
def valuation_subring.map_of_le {K : Type u_1} [field K] (R S : valuation_subring K) (h : R S) :

The canonical map on value groups induced by a coarsening of valuation rings.

Equations
theorem valuation_subring.monotone_map_of_le {K : Type u_1} [field K] (R S : valuation_subring K) (h : R S) :
@[simp]
theorem valuation_subring.map_of_le_comp_valuation {K : Type u_1} [field K] (R S : valuation_subring K) (h : R S) :
@[simp]
theorem valuation_subring.map_of_le_valuation_apply {K : Type u_1} [field K] (R S : valuation_subring K) (h : R S) (x : K) :
(R.map_of_le S h) ((R.valuation) x) = (S.valuation) x
def valuation_subring.ideal_of_le {K : Type u_1} [field K] (R S : valuation_subring K) (h : R S) :

The ideal corresponding to a coarsening of a valuation ring.

Equations
Instances for valuation_subring.ideal_of_le
@[protected, instance]
def valuation_subring.prime_ideal_of_le {K : Type u_1} [field K] (R S : valuation_subring K) (h : R S) :
noncomputable def valuation_subring.of_prime {K : Type u_1} [field K] (A : valuation_subring K) (P : ideal A) [P.is_prime] :

The coarsening of a valuation ring associated to a prime ideal.

Equations
Instances for valuation_subring.of_prime
@[protected, instance]
noncomputable def valuation_subring.of_prime_algebra {K : Type u_1} [field K] (A : valuation_subring K) (P : ideal A) [P.is_prime] :
Equations
@[protected, instance]
@[protected, instance]
theorem valuation_subring.le_of_prime {K : Type u_1} [field K] (A : valuation_subring K) (P : ideal A) [P.is_prime] :
@[simp]
theorem valuation_subring.ideal_of_le_of_prime {K : Type u_1} [field K] (A : valuation_subring K) (P : ideal A) [P.is_prime] :
A.ideal_of_le (A.of_prime P) _ = P
@[simp]
theorem valuation_subring.of_prime_ideal_of_le {K : Type u_1} [field K] (R S : valuation_subring K) (h : R S) :
R.of_prime (R.ideal_of_le S h) = S
theorem valuation_subring.of_prime_le_of_le {K : Type u_1} [field K] (A : valuation_subring K) (P Q : ideal A) [P.is_prime] [Q.is_prime] (h : P Q) :
theorem valuation_subring.ideal_of_le_le_of_le {K : Type u_1} [field K] (A R S : valuation_subring K) (hR : A R) (hS : A S) (h : R S) :
noncomputable def valuation_subring.prime_spectrum_equiv {K : Type u_1} [field K] (A : valuation_subring K) :

The equivalence between coarsenings of a valuation ring and its prime ideals.

Equations

An ordered variant of prime_spectrum_equiv.

Equations
def valuation.valuation_subring {K : Type u_1} [field K] {Γ : Type u_2} [linear_ordered_comm_group_with_zero Γ] (v : valuation K Γ) :

The valuation subring associated to a valuation.

Equations
@[simp]
theorem valuation.mem_valuation_subring_iff {K : Type u_1} [field K] {Γ : Type u_2} [linear_ordered_comm_group_with_zero Γ] (v : valuation K Γ) (x : K) :
theorem valuation.is_equiv_iff_valuation_subring {K : Type u_1} [field K] {Γ₁ : Type u_3} {Γ₂ : Type u_4} [linear_ordered_comm_group_with_zero Γ₁] [linear_ordered_comm_group_with_zero Γ₂] (v₁ : valuation K Γ₁) (v₂ : valuation K Γ₂) :
noncomputable def valuation_subring.unit_group {K : Type u_1} [field K] (A : valuation_subring K) :

The unit group of a valuation subring, as a subgroup of .

Equations
theorem valuation_subring.mem_unit_group_iff {K : Type u_1} [field K] (A : valuation_subring K) (x : Kˣ) :
noncomputable def valuation_subring.unit_group_mul_equiv {K : Type u_1} [field K] (A : valuation_subring K) :

For a valuation subring A, A.unit_group agrees with the units of A.

Equations

The map on valuation subrings to their unit groups is an order embedding.

Equations