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

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. 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.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
@[simp]
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
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_inj {K : Type u_1} [field K] {A B : valuation_subring K} :

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.

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 .

Equations

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

Equations

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

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] [mul_semiring_action 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] [mul_semiring_action 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] [mul_semiring_action 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] [mul_semiring_action 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] [mul_semiring_action 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] [mul_semiring_action G K] (g : G) (x : K) (S : valuation_subring K) :
x g S ∃ (s : K), s S g s = x
@[simp]
theorem valuation_subring.smul_mem_pointwise_smul_iff {K : Type u_1} [field K] {G : Type u_2} [group G] [mul_semiring_action 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] [mul_semiring_action 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] [mul_semiring_action 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] [mul_semiring_action 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] [mul_semiring_action 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] [mul_semiring_action G K] {g : G} {S T : valuation_subring K} :
S g T g⁻¹ S T
@[simp]
theorem valuation.mem_unit_group_iff (K : Type u_1) [field K] {Γ : Type u_2} [linear_ordered_comm_group_with_zero Γ] (v : valuation K Γ) (x : Kˣ) :