feat(ring_theory/valuation/valuation_subring): define maximal ideal of valuation subring and provide basic API (#14656)

This PR defines the unique maximal ideal of a valuation subring as a subsemigroup of the field. We prove a few equivalent conditions for two valuations to be equivalent, and we use this to show two valuation subrings are equivalent iff they have the same maximal ideal. 



Co-authored-by: Vierkantor <vierkantor@vierkantor.com>
Co-authored-by: jackmckoen <104791831+jackmckoen@users.noreply.github.com>

Author: mckoen

src/ring_theory/valuation/basic.lean

@@ -67,7 +67,7 @@ noncomputable theory
 
 open function ideal
 
-variables {F R : Type*} -- This will be a ring, assumed commutative in some sections
+variables {K F R : Type*} [division_ring K]
 
 section
 variables (F R) (Γ₀ : Type*) [linear_ordered_comm_monoid_with_zero Γ₀] [ring R]
@@ -170,12 +170,12 @@ lemma ext_iff {v₁ v₂ : valuation R Γ₀} : v₁ = v₂ ↔ ∀ r, v₁ r =
 def to_preorder : preorder R := preorder.lift v
 
 /-- If `v` is a valuation on a division ring then `v(x) = 0` iff `x = 0`. -/
-@[simp] lemma zero_iff [nontrivial Γ₀] {K : Type*} [division_ring K]
-  (v : valuation K Γ₀) {x : K} : v x = 0 ↔ x = 0 :=
+@[simp] lemma zero_iff [nontrivial Γ₀] (v : valuation K Γ₀) {x : K} :
+  v x = 0 ↔ x = 0 :=
 v.to_monoid_with_zero_hom.map_eq_zero
 
-lemma ne_zero_iff [nontrivial Γ₀] {K : Type*} [division_ring K]
-  (v : valuation K Γ₀) {x : K} : v x ≠ 0 ↔ x ≠ 0 :=
+lemma ne_zero_iff [nontrivial Γ₀] (v : valuation K Γ₀) {x : K} :
+  v x ≠ 0 ↔ x ≠ 0 :=
 v.to_monoid_with_zero_hom.map_ne_zero
 
 theorem unit_map_eq (u : Rˣ) :
@@ -217,11 +217,11 @@ end monoid
 section group
 variables [linear_ordered_comm_group_with_zero Γ₀] {R} {Γ₀} (v : valuation R Γ₀) {x y z : R}
 
-@[simp] lemma map_inv {K : Type*} [division_ring K]
-  (v : valuation K Γ₀) {x : K} : v x⁻¹ = (v x)⁻¹ :=
+@[simp] lemma map_inv (v : valuation K Γ₀) {x : K} :
+  v x⁻¹ = (v x)⁻¹ :=
 v.to_monoid_with_zero_hom.map_inv x
 
-@[simp] lemma map_zpow {K : Type*} [division_ring K] (v : valuation K Γ₀) {x : K} {n : ℤ} :
+@[simp] lemma map_zpow (v : valuation K Γ₀) {x : K} {n : ℤ} :
   v (x^n) = (v x)^n :=
 v.to_monoid_with_zero_hom.map_zpow x n
 
@@ -293,6 +293,10 @@ begin
   simpa only [v.map_one, v.map_neg] using v.map_add_eq_of_lt_left h
 end
 
+lemma one_lt_val_iff (v : valuation K Γ₀) {x : K} (h : x ≠ 0) :
+  1 < v x ↔ v x⁻¹ < 1 :=
+by simpa using (inv_lt_inv₀ (v.ne_zero_iff.2 h) one_ne_zero).symm
+
 /-- The subgroup of elements whose valuation is less than a certain unit.-/
 def lt_add_subgroup (v : valuation R Γ₀) (γ : Γ₀ˣ) : add_subgroup R :=
 { carrier   := {x | v x < γ},
@@ -358,7 +362,6 @@ lemma is_equiv_of_map_strict_mono [linear_ordered_comm_monoid_with_zero Γ₀]
 
 lemma is_equiv_of_val_le_one [linear_ordered_comm_group_with_zero Γ₀]
   [linear_ordered_comm_group_with_zero Γ'₀]
-  {K : Type*} [division_ring K]
   (v : valuation K Γ₀) (v' : valuation K Γ'₀) (h : ∀ {x:K}, v x ≤ 1 ↔ v' x ≤ 1) :
   v.is_equiv v' :=
 begin
@@ -382,15 +385,13 @@ end
 lemma is_equiv_iff_val_le_one
   [linear_ordered_comm_group_with_zero Γ₀]
   [linear_ordered_comm_group_with_zero Γ'₀]
-  {K : Type*} [division_ring K]
   (v : valuation K Γ₀) (v' : valuation K Γ'₀) :
   v.is_equiv v' ↔ ∀ {x : K}, v x ≤ 1 ↔ v' x ≤ 1 :=
 ⟨λ h x, by  simpa using h x 1, is_equiv_of_val_le_one _ _⟩
 
 lemma is_equiv_iff_val_eq_one
   [linear_ordered_comm_group_with_zero Γ₀]
   [linear_ordered_comm_group_with_zero Γ'₀]
-  {K : Type*} [division_ring K]
   (v : valuation K Γ₀) (v' : valuation K Γ'₀) :
   v.is_equiv v' ↔ ∀ {x : K}, v x = 1 ↔ v' x = 1 :=
 begin
@@ -419,6 +420,61 @@ begin
       { rw ← h at hx', exact le_of_eq hx' } } }
 end
 
+lemma is_equiv_iff_val_lt_one
+  [linear_ordered_comm_group_with_zero Γ₀]
+  [linear_ordered_comm_group_with_zero Γ'₀]
+  (v : valuation K Γ₀) (v' : valuation K Γ'₀) :
+  v.is_equiv v' ↔ ∀ {x : K}, v x < 1 ↔ v' x < 1 :=
+begin
+  split,
+  { intros h x,
+    simp only [lt_iff_le_and_ne, and_congr ((is_equiv_iff_val_le_one _ _).1 h)
+      ((is_equiv_iff_val_eq_one _ _).1 h).not] },
+  { rw is_equiv_iff_val_eq_one,
+    intros h x,
+    by_cases hx : x = 0, { simp only [(zero_iff _).2 hx, zero_ne_one] },
+    split,
+    { intro hh,
+      by_contra h_1,
+      cases ne_iff_lt_or_gt.1 h_1,
+      { simpa [hh, lt_self_iff_false] using h.2 h_2 },
+      { rw [← inv_one, eq_inv_iff_eq_inv, ← map_inv] at hh,
+        exact hh.le.not_lt (h.2 ((one_lt_val_iff v' hx).1 h_2)) } },
+    { intro hh,
+      by_contra h_1,
+      cases ne_iff_lt_or_gt.1 h_1,
+      { simpa [hh, lt_self_iff_false] using h.1 h_2 },
+      { rw [← inv_one, eq_inv_iff_eq_inv, ← map_inv] at hh,
+        exact hh.le.not_lt (h.1 ((one_lt_val_iff v hx).1 h_2)) } } }
+end
+
+lemma is_equiv_iff_val_sub_one_lt_one
+  [linear_ordered_comm_group_with_zero Γ₀]
+  [linear_ordered_comm_group_with_zero Γ'₀]
+  (v : valuation K Γ₀) (v' : valuation K Γ'₀) :
+  v.is_equiv v' ↔ ∀ {x : K}, v (x - 1) < 1 ↔ v' (x - 1) < 1 :=
+begin
+  rw is_equiv_iff_val_lt_one,
+  exact (equiv.sub_right 1).surjective.forall
+end
+
+lemma is_equiv_tfae
+  [linear_ordered_comm_group_with_zero Γ₀]
+  [linear_ordered_comm_group_with_zero Γ'₀]
+  (v : valuation K Γ₀) (v' : valuation K Γ'₀) :
+  [v.is_equiv v',
+   ∀ {x}, v x ≤ 1 ↔ v' x ≤ 1,
+   ∀ {x}, v x = 1 ↔ v' x = 1,
+   ∀ {x}, v x < 1 ↔ v' x < 1,
+   ∀ {x}, v (x-1) < 1 ↔ v' (x-1) < 1].tfae :=
+begin
+  tfae_have : 1 ↔ 2, { apply is_equiv_iff_val_le_one },
+  tfae_have : 1 ↔ 3, { apply is_equiv_iff_val_eq_one },
+  tfae_have : 1 ↔ 4, { apply is_equiv_iff_val_lt_one },
+  tfae_have : 1 ↔ 5, { apply is_equiv_iff_val_sub_one_lt_one },
+  tfae_finish
+end
+
 end
 
 section supp
@@ -605,12 +661,13 @@ valuation.ext_iff
 def to_preorder : preorder R := preorder.lift v
 
 /-- If `v` is an additive valuation on a division ring then `v(x) = ⊤` iff `x = 0`. -/
-@[simp] lemma top_iff [nontrivial Γ₀] {K : Type*} [division_ring K]
-  (v : add_valuation K Γ₀) {x : K} : v x = ⊤ ↔ x = 0 :=
+@[simp] lemma top_iff [nontrivial Γ₀] (v : add_valuation K Γ₀) {x : K} :
+  v x = ⊤ ↔ x = 0 :=
 v.zero_iff
 
-lemma ne_top_iff [nontrivial Γ₀] {K : Type*} [division_ring K]
-  (v : add_valuation K Γ₀) {x : K} : v x ≠ ⊤ ↔ x ≠ 0 := v.ne_zero_iff
+lemma ne_top_iff [nontrivial Γ₀] (v : add_valuation K Γ₀) {x : K} :
+  v x ≠ ⊤ ↔ x ≠ 0 :=
+v.ne_zero_iff
 
 /-- A ring homomorphism `S → R` induces a map `add_valuation R Γ₀ → add_valuation S Γ₀`. -/
 def comap {S : Type*} [ring S] (f : S →+* R) (v : add_valuation R Γ₀) :
@@ -644,8 +701,8 @@ end monoid
 section group
 variables [linear_ordered_add_comm_group_with_top Γ₀] [ring R] (v : add_valuation R Γ₀) {x y z : R}
 
-@[simp] lemma map_inv {K : Type*} [division_ring K]
-  (v : add_valuation K Γ₀) {x : K} : v x⁻¹ = - (v x) :=
+@[simp] lemma map_inv (v : add_valuation K Γ₀) {x : K} :
+  v x⁻¹ = - (v x) :=
 v.map_inv
 
 lemma map_units_inv (x : Rˣ) : v (x⁻¹ : Rˣ) = - (v x) :=

src/ring_theory/valuation/valuation_subring.lean

@@ -72,9 +72,9 @@ instance : valuation_ring A :=
     by_cases (b : K) = 0, { use 0, left, ext, simp [h] },
     by_cases (a : K) = 0, { use 0, right, ext, simp [h] },
     cases A.mem_or_inv_mem (a/b) with hh hh,
-    { use ⟨a/b,hh⟩, right, ext, field_simp, ring },
+    { use ⟨a/b, hh⟩, right, ext, field_simp, ring },
     { rw (show (a/b : K)⁻¹ = b/a, by field_simp) at hh,
-      use ⟨b/a,hh⟩, left, ext, field_simp, ring },
+      use ⟨b/a, hh⟩, left, ext, field_simp, ring },
   end }
 
 instance : algebra A K :=
@@ -84,16 +84,16 @@ show algebra A.to_subring K, by apply_instance
 lemma algebra_map_apply (a : A) : algebra_map A K a = a := rfl
 
 instance : is_fraction_ring A K :=
-{ map_units := λ ⟨y,hy⟩,
+{ map_units := λ ⟨y, hy⟩,
     (units.mk0 (y : K) (λ c, non_zero_divisors.ne_zero hy $ subtype.ext c)).is_unit,
   surj := λ z, begin
-    by_cases z = 0, { use (0,1), simp [h] },
+    by_cases z = 0, { use (0, 1), simp [h] },
     cases A.mem_or_inv_mem z with hh hh,
-    { use (⟨z,hh⟩,1), simp },
-    { refine ⟨⟨1,⟨⟨_,hh⟩,_⟩⟩, mul_inv_cancel h⟩,
+    { use (⟨z, hh⟩, 1), simp },
+    { refine ⟨⟨1, ⟨⟨_, hh⟩, _⟩⟩, mul_inv_cancel h⟩,
       exact mem_non_zero_divisors_iff_ne_zero.2 (λ c, h (inv_eq_zero.mp (congr_arg coe c))) },
   end,
-  eq_iff_exists := λ a b, ⟨ λ h, ⟨1, by { ext, simpa using h }⟩, λ ⟨c,h⟩,
+  eq_iff_exists := λ a b, ⟨ λ h, ⟨1, by { ext, simpa using h }⟩, λ ⟨c, h⟩,
     congr_arg coe ((mul_eq_mul_right_iff.1 h).resolve_right (non_zero_divisors.ne_zero c.2)) ⟩ }
 
 /-- The value group of the valuation associated to `A`. -/
@@ -106,13 +106,13 @@ def valuation : valuation K A.value_group := valuation_ring.valuation A K
 instance inhabited_value_group : inhabited A.value_group := ⟨A.valuation 0⟩
 
 lemma valuation_le_one (a : A) : A.valuation a ≤ 1 :=
-(valuation_ring.mem_integer_iff A K _).2 ⟨a,rfl⟩
+(valuation_ring.mem_integer_iff A K _).2 ⟨a, rfl⟩
 
 lemma mem_of_valuation_le_one (x : K) (h : A.valuation x ≤ 1) : x ∈ A :=
-let ⟨a,ha⟩ := (valuation_ring.mem_integer_iff A K x).1 h in ha ▸ a.2
+let ⟨a, ha⟩ := (valuation_ring.mem_integer_iff A K x).1 h in ha ▸ a.2
 
 lemma valuation_le_one_iff (x : K) : A.valuation x ≤ 1 ↔ x ∈ A :=
-⟨mem_of_valuation_le_one _ _, λ ha, A.valuation_le_one ⟨x,ha⟩⟩
+⟨mem_of_valuation_le_one _ _, λ ha, A.valuation_le_one ⟨x, ha⟩⟩
 
 lemma valuation_eq_iff (x y : K) : A.valuation x = A.valuation y ↔
   ∃ a : Aˣ, (a : K) * y = x := quotient.eq'
@@ -179,15 +179,15 @@ subring.subtype R.to_subring
 /-- The canonical map on value groups induced by a coarsening of valuation rings. -/
 def map_of_le (R S : valuation_subring K) (h : R ≤ S) :
   R.value_group →*₀ S.value_group :=
-{ to_fun := quotient.map' id $ λ x y ⟨u,hu⟩, ⟨units.map (R.inclusion S h).to_monoid_hom u, hu⟩,
+{ to_fun := quotient.map' id $ λ x y ⟨u, hu⟩, ⟨units.map (R.inclusion S h).to_monoid_hom u, hu⟩,
   map_zero' := rfl,
   map_one' := rfl,
   map_mul' := by { rintro ⟨⟩ ⟨⟩, refl } }
 
 @[mono]
 lemma monotone_map_of_le (R S : valuation_subring K) (h : R ≤ S) :
   monotone (R.map_of_le S h) :=
-by { rintros ⟨⟩ ⟨⟩ ⟨a,ha⟩, exact ⟨R.inclusion S h a, ha⟩ }
+by { rintros ⟨⟩ ⟨⟩ ⟨a, ha⟩, exact ⟨R.inclusion S h a, ha⟩ }
 
 @[simp]
 lemma map_of_le_comp_valuation (R S : valuation_subring K) (h : R ≤ S) :
@@ -209,7 +209,7 @@ def of_prime (A : valuation_subring K) (P : ideal A) [P.is_prime] :
   valuation_subring K :=
 of_le A (localization.subalgebra.of_field K P.prime_compl $
   le_non_zero_divisors_of_no_zero_divisors $ not_not_intro P.zero_mem).to_subring $
-  λ a ha, subalgebra.algebra_map_mem _ (⟨a,ha⟩ : A)
+  λ a ha, subalgebra.algebra_map_mem _ (⟨a, ha⟩ : A)
 
 instance of_prime_algebra (A : valuation_subring K) (P : ideal A) [P.is_prime] :
   algebra A (A.of_prime P) := subalgebra.algebra _
@@ -223,7 +223,7 @@ by apply localization.subalgebra.is_localization_of_field K
 
 lemma le_of_prime (A : valuation_subring K) (P : ideal A) [P.is_prime] :
   A ≤ of_prime A P :=
-λ a ha, subalgebra.algebra_map_mem _ (⟨a,ha⟩ : A)
+λ a ha, subalgebra.algebra_map_mem _ (⟨a, ha⟩ : A)
 
 lemma of_prime_valuation_eq_one_iff_mem_prime_compl
   (A : valuation_subring K)
@@ -243,7 +243,7 @@ lemma of_prime_ideal_of_le (R S : valuation_subring K) (h : R ≤ S) :
   of_prime R (ideal_of_le R S h) = S :=
 begin
   ext x, split,
-  { rintro ⟨a,r,hr,rfl⟩, apply mul_mem, { exact h a.2 },
+  { rintro ⟨a, r, hr, rfl⟩, apply mul_mem, { exact h a.2 },
     { rw [← valuation_le_one_iff, valuation.map_inv, ← inv_one, inv_le_inv₀],
       { exact not_lt.1 ((not_iff_not.2 $ valuation_lt_one_iff S _).1 hr) },
       { intro hh, erw [valuation.zero_iff, subring.coe_eq_zero_iff] at hh,
@@ -255,7 +255,7 @@ begin
     { use [1, x⁻¹, hr], split,
       { change (⟨x⁻¹, h hr⟩ : S) ∉ nonunits S,
         erw [mem_nonunits_iff, not_not],
-        apply is_unit_of_mul_eq_one _ (⟨x,hx⟩ : S),
+        apply is_unit_of_mul_eq_one _ (⟨x, hx⟩ : S),
         ext, field_simp },
       { field_simp } } },
 end
@@ -407,7 +407,7 @@ lemma unit_group_le_unit_group {A B : valuation_subring K} :
   A.unit_group ≤ B.unit_group ↔ A ≤ B :=
 begin
   split,
-  { rintros h x hx,
+  { intros h x hx,
     rw [← A.valuation_le_one_iff x, le_iff_lt_or_eq] at hx,
     by_cases h_1 : x = 0, { simp only [h_1, zero_mem] },
     by_cases h_2 : 1 + x = 0,
@@ -435,4 +435,79 @@ unit_group_order_embedding.strict_mono
 
 end unit_group
 
+section nonunits
+
+/-- The nonunits of a valuation subring of `K`, as a subsemigroup of `K`-/
+def nonunits : subsemigroup K :=
+{ carrier := { x | A.valuation x < 1 },
+  mul_mem' := λ a b ha hb, (mul_lt_mul₀ ha hb).trans_eq $ mul_one _ }
+
+lemma mem_nonunits_iff {x : K} : x ∈ A.nonunits ↔ A.valuation x < 1 := iff.refl _
+
+lemma nonunits_injective :
+  function.injective (nonunits : valuation_subring K → subsemigroup _) :=
+λ A B h, begin
+  rw [← A.valuation_subring_valuation, ← B.valuation_subring_valuation,
+    ← valuation.is_equiv_iff_valuation_subring, valuation.is_equiv_iff_val_lt_one],
+  exact set_like.ext_iff.1 h,
+end
+
+lemma nonunits_inj {A B : valuation_subring K} : A.nonunits = B.nonunits ↔ A = B :=
+nonunits_injective.eq_iff
+
+lemma nonunits_le_nonunits {A B : valuation_subring K} :
+  B.nonunits ≤ A.nonunits ↔ A ≤ B :=
+begin
+  split,
+  { intros h x hx,
+    by_cases h_1 : x = 0, { simp only [h_1, zero_mem] },
+    rw [← valuation_le_one_iff, ← not_lt, valuation.one_lt_val_iff _ h_1] at hx ⊢,
+    by_contra h_2, from hx (h h_2) },
+  { intros h x hx,
+    by_contra h_1, from not_lt.2 (monotone_map_of_le _ _ h (not_lt.1 h_1)) hx }
+end
+
+/-- The map on valuation subrings to their nonunits is a dual order embedding. -/
+def nonunits_order_embedding :
+  valuation_subring K ↪o (subsemigroup K)ᵒᵈ :=
+{ to_fun := λ A, A.nonunits,
+  inj' := nonunits_injective,
+  map_rel_iff' := λ A B, nonunits_le_nonunits }
+
+variables {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 coe_mem_nonunits_iff {a : A} : (a : K) ∈ A.nonunits ↔ a ∈ local_ring.maximal_ideal A :=
+(valuation_lt_one_iff _ _).symm
+
+lemma nonunits_le : A.nonunits ≤ A.to_subring.to_submonoid.to_subsemigroup :=
+λ a ha, (A.valuation_le_one_iff _).mp (A.mem_nonunits_iff.mp ha).le
+
+lemma nonunits_subset : (A.nonunits : set K) ⊆ A := nonunits_le
+
+ /-- 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 mem_nonunits_iff_exists_mem_maximal_ideal {a : K} :
+  a ∈ A.nonunits ↔ ∃ ha, (⟨a, ha⟩ : A) ∈ local_ring.maximal_ideal A :=
+⟨λ h, ⟨nonunits_subset h, coe_mem_nonunits_iff.mp h⟩,
+ λ ⟨ha, h⟩, coe_mem_nonunits_iff.mpr h⟩
+
+ /-- `A.nonunits` agrees with the maximal ideal of `A`, after taking its image in `K`. -/
+theorem image_maximal_ideal : (coe : A → K) '' local_ring.maximal_ideal A = A.nonunits :=
+begin
+  ext a,
+  simp only [set.mem_image, set_like.mem_coe, mem_nonunits_iff_exists_mem_maximal_ideal],
+  erw subtype.exists,
+  simp_rw [subtype.coe_mk, exists_and_distrib_right, exists_eq_right],
+end
+
+end nonunits
+
 end valuation_subring