# 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 A y A x + y A
theorem valuation_subring.mul_mem {K : Type u_1} [field K] (A : valuation_subring K) (x y : K) :
x A y A x * 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]
@[protected, instance]
Equations
@[protected, instance]
@[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]
@[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]
@[protected, instance]

The value group of the valuation associated to `A`. Note: it is actually a group with zero.

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.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)ˣ) :
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]
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

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]
@[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) :
{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 : Γ) :
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
@[simp]
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
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

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_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

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.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.

`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

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

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]
@[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 S g 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
def valuation_subring.comap {K : Type u_1} [field K] {L : Type u_2} [field L] (A : valuation_subring L) (f : K →+* L) :

The pullback of a valuation subring `A` along a ring homomorphism `K →+* L`.

Equations
@[simp]
theorem valuation_subring.coe_comap {K : Type u_1} [field K] {L : Type u_2} [field L] (A : valuation_subring L) (f : K →+* L) :
@[simp]
theorem valuation_subring.mem_comap {K : Type u_1} [field K] {L : Type u_2} [field L] {A : valuation_subring L} {f : K →+* L} {x : K} :
x A.comap f f x A
theorem valuation_subring.comap_comap {K : Type u_1} [field K] {L : Type u_2} {J : Type u_3} [field L] [field J] (A : valuation_subring J) (g : L →+* J) (f : K →+* L) :
(A.comap g).comap f = A.comap (g.comp f)
@[simp]
theorem valuation.mem_unit_group_iff (K : Type u_1) [field K] {Γ : Type u_2} (v : Γ) (x : Kˣ) :
v x = 1