mathlib3 documentation

ring_theory.valuation.valuation_ring

Valuation Rings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

A valuation ring is a domain such that for every pair of elements a b, either a divides b or vice-versa.

Any valuation ring induces a natural valuation on its fraction field, as we show in this file. Namely, given the following instances: [comm_ring A] [is_domain A] [valuation_ring A] [field K] [algebra A K] [is_fraction_ring A K], there is a natural valuation valuation A K on K with values in value_group A K where the image of A under algebra_map A K agrees with (valuation A K).integer.

We also provide the equivalence of the following notions for a domain R in valuation_ring.tfae.

R is a valuation ring.
For each x : fraction_ring K, either x or x⁻¹ is in R.
"divides" is a total relation on the elements of R.
"contains" is a total relation on the ideals of R.
R is a local bezout domain.

@[class]

structure valuation_ring (A : Type u) [comm_ring A] [is_domain A] :

Prop

cond : ∀ (a b : A), ∃ (c : A), a * c = b ∨ b * c = a

An integral domain is called a valuation ring provided that for any pair of elements a b : A, either a divides b or vice versa.

Instances of this typeclass

def valuation_ring.value_group (A : Type u) [comm_ring A] (K : Type v) [field K] [algebra A K] :

The value group of the valuation ring A. Note: this is actually a group with zero.

Equations

valuation_ring.value_group A K = quotient (mul_action.orbit_rel Aˣ K)

Instances for valuation_ring.value_group

@[protected, instance]

def valuation_ring.value_group.inhabited (A : Type u) [comm_ring A] (K : Type v) [field K] [algebra A K] :

inhabited (valuation_ring.value_group A K)

Equations

valuation_ring.value_group.inhabited A K = {default := quotient.mk' 0}

@[protected, instance]

def valuation_ring.value_group.has_le (A : Type u) [comm_ring A] (K : Type v) [field K] [algebra A K] :

has_le (valuation_ring.value_group A K)

Equations

valuation_ring.value_group.has_le A K = {le := λ (x y : valuation_ring.value_group A K), quotient.lift_on₂' x y (λ (a b : K), ∃ (c : A), c • b = a) _}

@[protected, instance]

def valuation_ring.value_group.has_zero (A : Type u) [comm_ring A] (K : Type v) [field K] [algebra A K] :

has_zero (valuation_ring.value_group A K)

Equations

valuation_ring.value_group.has_zero A K = {zero := quotient.mk' 0}

@[protected, instance]

def valuation_ring.value_group.has_one (A : Type u) [comm_ring A] (K : Type v) [field K] [algebra A K] :

has_one (valuation_ring.value_group A K)

Equations

valuation_ring.value_group.has_one A K = {one := quotient.mk' 1}

@[protected, instance]

def valuation_ring.value_group.has_mul (A : Type u) [comm_ring A] (K : Type v) [field K] [algebra A K] :

has_mul (valuation_ring.value_group A K)

Equations

valuation_ring.value_group.has_mul A K = {mul := λ (x y : valuation_ring.value_group A K), quotient.lift_on₂' x y (λ (a b : K), quotient.mk' (a * b)) _}

@[protected, instance]

def valuation_ring.value_group.has_inv (A : Type u) [comm_ring A] (K : Type v) [field K] [algebra A K] :

has_inv (valuation_ring.value_group A K)

Equations

valuation_ring.value_group.has_inv A K = {inv := λ (x : valuation_ring.value_group A K), quotient.lift_on' x (λ (a : K), quotient.mk' a⁻¹) _}

@[protected]

theorem valuation_ring.le_total (A : Type u) [comm_ring A] (K : Type v) [field K] [algebra A K] [is_domain A] [valuation_ring A] [is_fraction_ring A K] (a b : valuation_ring.value_group A K) :

a ≤ b ∨ b ≤ a

@[protected, instance]

noncomputable def valuation_ring.value_group.linear_ordered_comm_group_with_zero (A : Type u) [comm_ring A] (K : Type v) [field K] [algebra A K] [is_domain A] [valuation_ring A] [is_fraction_ring A K] :

linear_ordered_comm_group_with_zero (valuation_ring.value_group A K)

Equations

valuation_ring.value_group.linear_ordered_comm_group_with_zero A K = {le := has_le.le infer_instance, lt := linear_ordered_comm_monoid_with_zero.lt._default has_le.le, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := λ (a b : valuation_ring.value_group A K), quotient.lift_on₂'.decidable a b (λ (a₁ : K), (λ (a b : K), ∃ (c : A), c • b = a) a₁) _, decidable_eq := linear_ordered_comm_monoid_with_zero.decidable_eq._default has_le.le (linear_ordered_comm_monoid_with_zero.lt._default has_le.le) _ _ _ _ (λ (a b : valuation_ring.value_group A K), quotient.lift_on₂'.decidable a b (λ (a₁ : K), (λ (a b : K), ∃ (c : A), c • b = a) a₁) _), decidable_lt := linear_ordered_comm_monoid_with_zero.decidable_lt._default has_le.le (linear_ordered_comm_monoid_with_zero.lt._default has_le.le) _ _ _ _ (λ (a b : valuation_ring.value_group A K), quotient.lift_on₂'.decidable a b (λ (a₁ : K), (λ (a b : K), ∃ (c : A), c • b = a) a₁) _), max := linear_ordered_comm_monoid_with_zero.max._default has_le.le (linear_ordered_comm_monoid_with_zero.lt._default has_le.le) _ _ _ _ (λ (a b : valuation_ring.value_group A K), quotient.lift_on₂'.decidable a b (λ (a₁ : K), (λ (a b : K), ∃ (c : A), c • b = a) a₁) _), max_def := _, min := linear_ordered_comm_monoid_with_zero.min._default has_le.le (linear_ordered_comm_monoid_with_zero.lt._default has_le.le) _ _ _ _ (λ (a b : valuation_ring.value_group A K), quotient.lift_on₂'.decidable a b (λ (a₁ : K), (λ (a b : K), ∃ (c : A), c • b = a) a₁) _), min_def := _, mul := has_mul.mul infer_instance, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := linear_ordered_comm_monoid_with_zero.npow._default 1 has_mul.mul _ _, npow_zero' := _, npow_succ' := _, mul_comm := _, mul_le_mul_left := _, zero := 0, zero_mul := _, mul_zero := _, zero_le_one := _, inv := has_inv.inv infer_instance, div := comm_group_with_zero.div._default has_mul.mul _ 1 _ _ (linear_ordered_comm_monoid_with_zero.npow._default 1 has_mul.mul _ _) _ _ has_inv.inv, div_eq_mul_inv := _, zpow := comm_group_with_zero.zpow._default has_mul.mul _ 1 _ _ (linear_ordered_comm_monoid_with_zero.npow._default 1 has_mul.mul _ _) _ _ has_inv.inv, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, inv_zero := _, mul_inv_cancel := _}

def valuation_ring.valuation (A : Type u) [comm_ring A] (K : Type v) [field K] [algebra A K] [is_domain A] [valuation_ring A] [is_fraction_ring A K] :

valuation K (valuation_ring.value_group A K)

Any valuation ring induces a valuation on its fraction field.

Equations

valuation_ring.valuation A K = {to_monoid_with_zero_hom := {to_fun := quotient.mk' (mul_action.orbit_rel Aˣ K), map_zero' := _, map_one' := _, map_mul' := _}, map_add_le_max' := _}

theorem valuation_ring.mem_integer_iff (A : Type u) [comm_ring A] (K : Type v) [field K] [algebra A K] [is_domain A] [valuation_ring A] [is_fraction_ring A K] (x : K) :

x ∈ (valuation_ring.valuation A K).integer ↔ ∃ (a : A), ⇑(algebra_map A K) a = x

noncomputable def valuation_ring.equiv_integer (A : Type u) [comm_ring A] (K : Type v) [field K] [algebra A K] [is_domain A] [valuation_ring A] [is_fraction_ring A K] :

A ≃+* ↥((valuation_ring.valuation A K).integer)

The valuation ring A is isomorphic to the ring of integers of its associated valuation.

Equations

valuation_ring.equiv_integer A K = ring_equiv.of_bijective (show A →ₙ+* ↥((valuation_ring.valuation A K).integer), from {to_fun := λ (a : A), ⟨⇑(algebra_map A K) a, _⟩, map_mul' := _, map_zero' := _, map_add' := _}) _

@[simp]

theorem valuation_ring.coe_equiv_integer_apply (A : Type u) [comm_ring A] (K : Type v) [field K] [algebra A K] [is_domain A] [valuation_ring A] [is_fraction_ring A K] (a : A) :

↑(⇑(valuation_ring.equiv_integer A K) a) = ⇑(algebra_map A K) a

theorem valuation_ring.range_algebra_map_eq (A : Type u) [comm_ring A] (K : Type v) [field K] [algebra A K] [is_domain A] [valuation_ring A] [is_fraction_ring A K] :

(valuation_ring.valuation A K).integer = (algebra_map A K).range

@[protected, instance]

def valuation_ring.local_ring (A : Type u) [comm_ring A] [is_domain A] [valuation_ring A] :

@[protected, instance]

def valuation_ring.ideal.linear_order (A : Type u) [comm_ring A] [is_domain A] [valuation_ring A] [decidable_rel has_le.le] :

linear_order (ideal A)

Equations

valuation_ring.ideal.linear_order A = {le := complete_lattice.le infer_instance, lt := complete_lattice.lt infer_instance, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := infer_instance (λ (a b : ideal A), _inst_4 a b), decidable_eq := decidable_eq_of_decidable_le infer_instance, decidable_lt := decidable_lt_of_decidable_le infer_instance, max := max_default (λ (a b : ideal A), infer_instance a b), max_def := _, min := min_default (λ (a b : ideal A), infer_instance a b), min_def := _}

theorem valuation_ring.iff_dvd_total {R : Type u_1} [comm_ring R] [is_domain R] :

valuation_ring R ↔ is_total R has_dvd.dvd

theorem valuation_ring.iff_ideal_total {R : Type u_1} [comm_ring R] [is_domain R] :

valuation_ring R ↔ is_total (ideal R) has_le.le

theorem valuation_ring.dvd_total {R : Type u_1} [comm_ring R] [is_domain R] [h : valuation_ring R] (x y : R) :

x ∣ y ∨ y ∣ x

theorem valuation_ring.unique_irreducible {R : Type u_1} [comm_ring R] [is_domain R] [valuation_ring R] ⦃p q : R⦄ (hp : irreducible p) (hq : irreducible q) :

theorem valuation_ring.iff_is_integer_or_is_integer (R : Type u_1) [comm_ring R] [is_domain R] (K : Type u_2) [field K] [algebra R K] [is_fraction_ring R K] :

valuation_ring R ↔ ∀ (x : K), is_localization.is_integer R x ∨ is_localization.is_integer R x⁻¹

theorem valuation_ring.is_integer_or_is_integer (R : Type u_1) [comm_ring R] [is_domain R] {K : Type u_2} [field K] [algebra R K] [is_fraction_ring R K] [h : valuation_ring R] (x : K) :

is_localization.is_integer R x ∨ is_localization.is_integer R x⁻¹

@[protected, instance]

def valuation_ring.is_bezout {R : Type u_1} [comm_ring R] [is_domain R] [valuation_ring R] :

theorem valuation_ring.iff_local_bezout_domain {R : Type u_1} [comm_ring R] [is_domain R] :

valuation_ring R ↔ local_ring R ∧ is_bezout R

@[protected]

theorem valuation_ring.tfae (R : Type u) [comm_ring R] [is_domain R] :

[valuation_ring R, ∀ (x : fraction_ring R), is_localization.is_integer R x ∨ is_localization.is_integer R x⁻¹, is_total R has_dvd.dvd, is_total (ideal R) has_le.le, local_ring R ∧ is_bezout R].tfae

theorem function.surjective.valuation_ring {R : Type u_1} {S : Type u_2} [comm_ring R] [is_domain R] [valuation_ring R] [comm_ring S] [is_domain S] (f : R →+* S) (hf : function.surjective ⇑f) :

valuation_ring S

theorem valuation_ring.of_integers {𝒪 : Type u} {K : Type v} {Γ : Type w} [comm_ring 𝒪] [is_domain 𝒪] [field K] [algebra 𝒪 K] [linear_ordered_comm_group_with_zero Γ] (v : valuation K Γ) (hh : v.integers 𝒪) :

valuation_ring 𝒪

If 𝒪 satisfies v.integers 𝒪 where v is a valuation on a field, then 𝒪 is a valuation ring.

@[protected, instance]

def valuation_ring.of_field (K : Type u) [field K] :

valuation_ring K

A field is a valuation ring.

@[protected, instance]

def valuation_ring.of_discrete_valuation_ring (A : Type u) [comm_ring A] [is_domain A] [discrete_valuation_ring A] :

valuation_ring A

A DVR is a valuation ring.