# mathlibdocumentation

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⁻¹ ∈ A.

Instances for valuation_subring
@[protected, instance]
def valuation_subring.set_like {K : Type u_1} [field K] :
Equations
@[simp]
theorem valuation_subring.mem_carrier {K : Type u_1} [field K] (A : valuation_subring K) (x : K) :
x A
@[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
theorem valuation_subring.to_subring_injective {K : Type u_1} [field K] :
@[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]
def valuation_subring.has_top {K : Type u_1} [field K] :
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]
def valuation_subring.order_top {K : Type u_1} [field K] :
Equations
@[protected, instance]
def valuation_subring.inhabited {K : Type u_1} [field K] :
Equations
@[protected, instance]
def valuation_subring.valuation_ring {K : Type u_1} [field K] (A : valuation_subring K) :
@[protected, instance]
def valuation_subring.algebra {K : Type u_1} [field K] (A : valuation_subring K) :
K
Equations
@[simp]
theorem valuation_subring.algebra_map_apply {K : Type u_1} [field K] (A : valuation_subring K) (a : A) :
K) a = a
@[protected, instance]
def valuation_subring.is_fraction_ring {K : Type u_1} [field K] (A : valuation_subring K) :
@[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. Note: it is actually a group with zero.

Equations
Instances for valuation_subring.value_group
def valuation_subring.valuation {K : Type u_1} [field K] (A : valuation_subring K) :

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) :
theorem valuation_subring.valuation_lt_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) :
x R
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
@[protected, instance]
def valuation_subring.semilattice_sup {K : Type u_1} [field K] :
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]
def valuation_subring.of_prime_scalar_tower {K : Type u_1} [field K] (A : valuation_subring K) (P : ideal A) [P.is_prime] :
(A.of_prime P) K
@[protected, instance]
def valuation_subring.of_prime_localization {K : Type u_1} [field K] (A : valuation_subring K) (P : ideal A) [P.is_prime] :
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) :
@[simp]
noncomputable def valuation_subring.prime_spectrum_equiv {K : Type u_1} [field K] (A : valuation_subring K) :
{S : | A S}

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

Equations
@[simp]
theorem valuation_subring.prime_spectrum_order_equiv_symm_apply {K : Type u_1} [field K] (A : valuation_subring K) (ᾰ : {S : | A S}) :
noncomputable def valuation_subring.prime_spectrum_order_equiv {K : Type u_1} [field K] (A : valuation_subring K) :
≃o {S : | A S}

An ordered variant of prime_spectrum_equiv.

Equations
@[protected, instance]
noncomputable def valuation_subring.linear_order_overring {K : Type u_1} [field K] (A : valuation_subring K) :
linear_order {S : | A S}
Equations
def valuation.valuation_subring {K : Type u_1} [field K] {Γ : Type u_2} (v : Γ) :

The valuation subring associated to a valuation.

Equations
@[simp]
theorem valuation.mem_valuation_subring_iff {K : Type u_1} [field K] {Γ : Type u_2} (v : Γ) (x : K) :
v x 1
theorem valuation.is_equiv_iff_valuation_subring {K : Type u_1} [field K] {Γ₁ : Type u_3} {Γ₂ : Type u_4} (v₁ : Γ₁) (v₂ : Γ₂) :
v₁.is_equiv v₂
theorem valuation.is_equiv_valuation_valuation_subring {K : Type u_1} [field K] {Γ : Type u_2} (v : Γ) :
@[simp]
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 Kˣ.

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
theorem valuation_subring.unit_group_le_unit_group {K : Type u_1} [field K] {A B : valuation_subring K} :
A B
theorem valuation_subring.unit_group_injective {K : Type u_1} [field K] :
theorem valuation_subring.eq_iff_unit_group {K : Type u_1} [field K] {A B : valuation_subring K} :
A = B
noncomputable def valuation_subring.unit_group_order_embedding {K : Type u_1} [field K] :

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

Equations
theorem valuation_subring.unit_group_strict_mono {K : Type u_1} [field K] :
def valuation_subring.nonunits {K : Type u_1} [field K] (A : valuation_subring K) :

The nonunits of a valuation subring of K, as a subsemigroup of K

Equations
theorem valuation_subring.mem_nonunits_iff {K : Type u_1} [field K] (A : valuation_subring K) {x : K} :
theorem valuation_subring.nonunits_le_nonunits {K : Type u_1} [field K] {A B : valuation_subring K} :
A B
theorem valuation_subring.nonunits_injective {K : Type u_1} [field K] :
theorem valuation_subring.nonunits_inj {K : Type u_1} [field K] {A B : valuation_subring K} :
A = B

The map on valuation subrings to their nonunits is a dual order embedding.

Equations
theorem valuation_subring.coe_mem_nonunits_iff {K : Type u_1} [field K] {A : valuation_subring K} {a : A} :

The elements of A.nonunits are those of the maximal ideal of A after coercion to K.

See also mem_nonunits_iff_exists_mem_maximal_ideal, which gets rid of the coercion to K, at the expense of a more complicated right hand side.

theorem valuation_subring.nonunits_le {K : Type u_1} [field K] {A : valuation_subring K} :
theorem valuation_subring.mem_nonunits_iff_exists_mem_maximal_ideal {K : Type u_1} [field K] {A : valuation_subring K} {a : K} :
a A.nonunits ∃ (ha : a A), a, ha⟩

The elements of A.nonunits are those of the maximal ideal of A.

See also coe_mem_nonunits_iff, which has a simpler right hand side but requires the element to be in A already.

theorem valuation_subring.image_maximal_ideal {K : Type u_1} [field K] {A : valuation_subring K} :

A.nonunits agrees with the maximal ideal of A, after taking its image in K.

The principal unit group of a valuation subring, as a subgroup of Kˣ.

Equations
theorem valuation_subring.mem_principal_unit_group_iff {K : Type u_1} [field K] (A : valuation_subring K) (x : Kˣ) :
(A.valuation) (x - 1) < 1

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

Equations
noncomputable def valuation_subring.principal_unit_group_equiv {K : Type u_1} [field K] (A : valuation_subring K) :

The principal unit group agrees with the kernel of the canonical map from the units of A to the units of the residue field of A.

Equations
noncomputable def valuation_subring.unit_group_to_residue_field_units {K : Type u_1} [field K] (A : valuation_subring K) :

The canonical map from the unit group of A to the units of the residue field of A.

Equations

The quotient of the unit group of A by the principal unit group of A agrees with the units of the residue field of A.

Equations
@[simp]

### Pointwise actions #

This transfers the action from subring.pointwise_mul_action, noting that it only applies when the action is by a group. Notably this provides an instances when G is K ≃+* K.

These instances are in the pointwise locale.

The lemmas in this section are copied from ring_theory/subring/pointwise.lean; try to keep these in sync.

def valuation_subring.pointwise_has_smul {K : Type u_1} [field K] {G : Type u_2} [group G] [ K] :

The action on a valuation subring corresponding to applying the action to every element.

This is available as an instance in the pointwise locale.

Equations
@[simp]
theorem valuation_subring.coe_pointwise_smul {K : Type u_1} [field K] {G : Type u_2} [group G] [ K] (g : G) (S : valuation_subring K) :
(g S) = g S
@[simp]
theorem valuation_subring.pointwise_smul_to_subring {K : Type u_1} [field K] {G : Type u_2} [group G] [ K] (g : G) (S : valuation_subring K) :
def valuation_subring.pointwise_mul_action {K : Type u_1} [field K] {G : Type u_2} [group G] [ K] :

The action on a valuation subring corresponding to applying the action to every element.

This is available as an instance in the pointwise locale.

This is a stronger version of valuation_subring.pointwise_has_smul.

Equations
theorem valuation_subring.smul_mem_pointwise_smul {K : Type u_1} [field K] {G : Type u_2} [group G] [ K] (g : G) (x : K) (S : valuation_subring K) :
x Sg x g S
theorem valuation_subring.mem_smul_pointwise_iff_exists {K : Type u_1} [field K] {G : Type u_2} [group G] [ K] (g : G) (x : K) (S : valuation_subring K) :
x g S ∃ (s : K), s S g s = x
@[protected, instance]
def valuation_subring.pointwise_central_scalar {K : Type u_1} [field K] {G : Type u_2} [group G] [ K] [ K] :
@[simp]
theorem valuation_subring.smul_mem_pointwise_smul_iff {K : Type u_1} [field K] {G : Type u_2} [group G] [ K] {g : G} {S : valuation_subring K} {x : K} :
g x g S x S
theorem valuation_subring.mem_pointwise_smul_iff_inv_smul_mem {K : Type u_1} [field K] {G : Type u_2} [group G] [ K] {g : G} {S : valuation_subring K} {x : K} :
x g S g⁻¹ x S
theorem valuation_subring.mem_inv_pointwise_smul_iff {K : Type u_1} [field K] {G : Type u_2} [group G] [ K] {g : G} {S : valuation_subring K} {x : K} :
x g⁻¹ S g x S
@[simp]
theorem valuation_subring.pointwise_smul_le_pointwise_smul_iff {K : Type u_1} [field K] {G : Type u_2} [group G] [ K] {g : G} {S T : valuation_subring K} :
g S g T S T
theorem valuation_subring.pointwise_smul_subset_iff {K : Type u_1} [field K] {G : Type u_2} [group G] [ K] {g : G} {S T : valuation_subring K} :
g S T S g⁻¹ T
theorem valuation_subring.subset_pointwise_smul_iff {K : Type u_1} [field K] {G : Type u_2} [group G] [ K] {g : G} {S T : valuation_subring K} :
S g T g⁻¹ S T