feat(ring_theory/discrete_valuation_ring): add DVR (#3476)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: kbuzzard

src/algebra/associated.lean

@@ -239,6 +239,11 @@ lemma associated_mul_mul [comm_monoid α] {a₁ a₂ b₁ b₂ : α} :
   a₁ ~ᵤ b₁ → a₂ ~ᵤ b₂ → (a₁ * a₂) ~ᵤ (b₁ * b₂)
 | ⟨c₁, h₁⟩ ⟨c₂, h₂⟩ := ⟨c₁ * c₂, by simp [h₁.symm, h₂.symm, mul_assoc, mul_comm, mul_left_comm]⟩
 
+lemma dvd_of_associated [comm_ring α] {a b : α} : a ~ᵤ b → a ∣ b := λ ⟨u, hu⟩, ⟨u, hu.symm⟩
+
+lemma dvd_dvd_of_associated [comm_ring α] {a b : α} (h : a ~ᵤ b) : a ∣ b ∧ b ∣ a :=
+⟨dvd_of_associated h, dvd_of_associated h.symm⟩
+
 theorem associated_of_dvd_dvd [integral_domain α] {a b : α} (hab : a ∣ b) (hba : b ∣ a) : a ~ᵤ b :=
 begin
   haveI := classical.dec_eq α,
@@ -252,6 +257,9 @@ begin
   exact ⟨units.mk_of_mul_eq_one c d (this.symm), by rw [units.mk_of_mul_eq_one, units.val_coe]⟩
 end
 
+theorem dvd_dvd_iff_associated [integral_domain α] {a b : α} : a ∣ b ∧ b ∣ a ↔ a ~ᵤ b :=
+⟨λ ⟨h1, h2⟩, associated_of_dvd_dvd h1 h2, dvd_dvd_of_associated⟩
+
 lemma exists_associated_mem_of_dvd_prod [integral_domain α] {p : α}
   (hp : prime p) {s : multiset α} : (∀ r ∈ s, prime r) → p ∣ s.prod → ∃ q ∈ s, p ~ᵤ q :=
 multiset.induction_on s (by simp [mt is_unit_iff_dvd_one.2 hp.not_unit])

src/ring_theory/discrete_valuation_ring.lean

@@ -0,0 +1,142 @@
+/-
+Copyright (c) 2020 Kevin Buzzard. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kevin Buzzard
+-/
+
+import ring_theory.principal_ideal_domain order.conditionally_complete_lattice
+import ring_theory.multiplicity
+import ring_theory.valuation.basic
+import tactic
+
+/-!
+# Discrete valuation rings
+
+This file defines discrete valuation rings (DVRs) and develops a basic interface
+for them.
+
+## Important definitions
+
+There are various definitions of a DVR in the literature; we define a DVR to be a local PID
+which is not a field (the first definition in Wikipedia) and prove that this is equivalent
+to being a PID with a unique non-zero prime ideal (the definition in Serre's
+book "Local Fields").
+
+Let R be an integral domain, assumed to be a principal ideal ring and a local ring.
+
+* `discrete_valuation_ring R` : a predicate expressing that R is a DVR
+
+### Notation
+
+It's a theorem that an element of a DVR is a uniformiser if and only if it's irreducible.
+We do not hence define `uniformiser` at all, because we can use `irreducible` instead.
+
+### Definitions
+
+## Implementation notes
+
+## Tags
+
+discrete valuation ring
+-/
+
+open_locale classical
+
+universe u
+
+open ideal local_ring
+
+section prio
+set_option default_priority 100 -- see Note [default priority]
+/-- An integral domain is a discrete valuation ring if it's a local PID which is not a field -/
+class discrete_valuation_ring (R : Type u) [integral_domain R]
+  extends is_principal_ideal_ring R, local_ring R : Prop :=
+(not_a_field' : maximal_ideal R ≠ ⊥)
+end prio
+
+namespace discrete_valuation_ring
+
+variables (R : Type u) [integral_domain R] [discrete_valuation_ring R]
+
+lemma not_a_field : maximal_ideal R ≠ ⊥ := not_a_field'
+
+variable {R}
+
+open principal_ideal_ring
+
+/-- An element of a DVR is irreducible iff it is a uniformiser, that is, generates the
+  maximal ideal of R -/
+theorem irreducible_iff_uniformiser (ϖ : R) :
+  irreducible ϖ ↔ maximal_ideal R = ideal.span {ϖ} :=
+⟨λ hϖ, (eq_maximal_ideal (is_maximal_of_irreducible hϖ)).symm,
+begin
+  intro h,
+  have h2 : ¬(is_unit ϖ) := show ϖ ∈ maximal_ideal R,
+    from h.symm ▸ submodule.mem_span_singleton_self ϖ,
+  split, exact h2,
+  intros a b hab,
+  by_contra h,
+  push_neg at h,
+  cases h with ha hb,
+  change a ∈ maximal_ideal R at ha,
+  change b ∈ maximal_ideal R at hb,
+  rw h at ha hb,
+  rw mem_span_singleton' at ha hb,
+  rcases ha with ⟨a, rfl⟩,
+  rcases hb with ⟨b, rfl⟩,
+  rw (show a * ϖ * (b * ϖ) = ϖ * (ϖ * (a * b)), by ring) at hab,
+  have h3 := eq_zero_of_mul_eq_self_right _ hab.symm,
+  { apply not_a_field R,
+    simp [h, h3]},
+  { intro hh, apply h2,
+    refine is_unit_of_dvd_one ϖ _,
+    use a * b, exact hh.symm}
+end⟩
+
+variable (R)
+
+/-- Uniformisers exist in a DVR -/
+theorem exists_irreducible : ∃ ϖ : R, irreducible ϖ :=
+by {simp_rw [irreducible_iff_uniformiser],
+    exact (is_principal_ideal_ring.principal $ maximal_ideal R).principal}
+
+/-- an integral domain is a DVR iff it's a PID with a unique non-zero prime ideal -/
+theorem iff_PID_with_one_nonzero_prime (R : Type u) [integral_domain R] :
+  discrete_valuation_ring R ↔ is_principal_ideal_ring R ∧ ∃! P : ideal R, P ≠ ⊥ ∧ is_prime P :=
+begin
+  split,
+  { intro RDVR,
+    rcases id RDVR with ⟨RPID, Rlocal, Rnotafield⟩,
+    split, assumption,
+    resetI,
+    use local_ring.maximal_ideal R,
+    split, split,
+    { assumption},
+    { apply_instance},
+    { rintro Q ⟨hQ1, hQ2⟩,
+      obtain ⟨q, rfl⟩ := (is_principal_ideal_ring.principal Q).1,
+      have hq : q ≠ 0,
+      { rintro rfl,
+        apply hQ1,
+        simp,
+      },
+      erw span_singleton_prime hq at hQ2,
+      replace hQ2 := irreducible_of_prime hQ2,
+      rw irreducible_iff_uniformiser at hQ2,
+      exact hQ2.symm}},
+  { rintro ⟨RPID, Punique⟩,
+    haveI : local_ring R := local_of_unique_nonzero_prime R Punique,
+    refine {not_a_field' := _},
+    rcases Punique with ⟨P, ⟨hP1, hP2⟩, hP3⟩,
+    have hPM : P ≤ maximal_ideal R := le_maximal_ideal (hP2.1),
+    intro h, rw [h, le_bot_iff] at hPM, exact hP1 hPM}
+end
+
+lemma associated_of_irreducible {a b : R} (ha : irreducible a) (hb : irreducible b) :
+  associated a b :=
+begin
+  rw irreducible_iff_uniformiser at ha hb,
+  rw [←span_singleton_eq_span_singleton, ←ha, hb],
+end
+
+end discrete_valuation_ring

src/ring_theory/ideals.lean

@@ -68,6 +68,14 @@ lemma span_singleton_le_span_singleton {x y : α} :
   span ({x} : set α) ≤ span ({y} : set α) ↔ y ∣ x :=
 span_le.trans $ singleton_subset_iff.trans mem_span_singleton
 
+lemma span_singleton_eq_span_singleton {α : Type u} [integral_domain α] {x y : α} :
+  span ({x} : set α) = span ({y} : set α) ↔ associated x y :=
+begin
+  rw [←dvd_dvd_iff_associated, le_antisymm_iff, and_comm],
+  apply and_congr;
+  rw span_singleton_le_span_singleton,
+end
+
 lemma span_eq_bot {s : set α} : span s = ⊥ ↔ ∀ x ∈ s, (x:α) = 0 := submodule.span_eq_bot
 
 @[simp] lemma span_singleton_eq_bot {x} : span ({x} : set α) = ⊥ ↔ x = 0 :=
@@ -79,6 +87,17 @@ lemma span_singleton_eq_top {x} : span ({x} : set α) = ⊤ ↔ is_unit x :=
 by rw [is_unit_iff_dvd_one, ← span_singleton_le_span_singleton, singleton_one, span_singleton_one,
   eq_top_iff]
 
+lemma span_singleton_mul_right_unit {a : α} (h2 : is_unit a) (x : α) :
+  span ({x * a} : set α) = span {x} :=
+begin
+  apply le_antisymm,
+  { rw span_singleton_le_span_singleton, use a},
+  { rw span_singleton_le_span_singleton, rw mul_dvd_of_is_unit_right h2}
+end
+
+lemma span_singleton_mul_left_unit {a : α} (h2 : is_unit a) (x : α) :
+  span ({a * x} : set α) = span {x} := by rw [mul_comm, span_singleton_mul_right_unit h2]
+
 /-- An ideal `P` of a ring `R` is prime if `P ≠ R` and `xy ∈ P → x ∈ P ∨ y ∈ P` -/
 @[class] def is_prime (I : ideal α) : Prop :=
 I ≠ ⊤ ∧ ∀ {x y : α}, x * y ∈ I → x ∈ I ∨ y ∈ I
@@ -158,6 +177,16 @@ begin
     exact SC JS ((eq_top_iff_one _).2 J0) }
 end
 
+/-- If P is not properly contained in any maximal ideal then it is not properly contained
+  in any proper ideal -/
+lemma maximal_of_no_maximal {R : Type u} [comm_ring R] {P : ideal R}
+(hmax : ∀ m : ideal R, P < m → ¬is_maximal m) (J : ideal R) (hPJ : P < J) : J = ⊤ :=
+begin
+  by_contradiction hnonmax,
+  rcases exists_le_maximal J hnonmax with ⟨M, hM1, hM2⟩,
+  exact hmax M (lt_of_lt_of_le hPJ hM2) hM1,
+end
+
 theorem mem_span_pair {x y z : α} :
   z ∈ span ({x, y} : set α) ↔ ∃ a b, a * x + b * y = z :=
 by simp [mem_span_insert, mem_span_singleton', @eq_comm _ _ z]
@@ -402,14 +431,23 @@ begin
     simpa using I.smul_mem ↑u⁻¹ H }
 end
 
-lemma max_ideal_unique :
+lemma maximal_ideal_unique :
   ∃! I : ideal α, I.is_maximal :=
 ⟨maximal_ideal α, maximal_ideal.is_maximal α,
   λ I hI, hI.eq_of_le (maximal_ideal.is_maximal α).1 $
   λ x hx, hI.1 ∘ I.eq_top_of_is_unit_mem hx⟩
 
 variable {α}
 
+lemma eq_maximal_ideal {I : ideal α} (hI : I.is_maximal) : I = maximal_ideal α :=
+unique_of_exists_unique (maximal_ideal_unique α) hI $ maximal_ideal.is_maximal α
+
+lemma le_maximal_ideal {J : ideal α} (hJ : J ≠ ⊤) : J ≤ maximal_ideal α :=
+begin
+  rcases ideal.exists_le_maximal J hJ with ⟨M, hM1, hM2⟩,
+  rwa ←eq_maximal_ideal hM1
+end
+
 @[simp] lemma mem_maximal_ideal (x) :
   x ∈ maximal_ideal α ↔ x ∈ nonunits α := iff.rfl
 
@@ -437,6 +475,17 @@ have xmemI : x ∈ I, from ((Iuniq Ix Ixmax) ▸ Hx),
 have ymemI : y ∈ I, from ((Iuniq Iy Iymax) ▸ Hy),
 Imax.1 $ I.eq_top_of_is_unit_mem (I.add_mem xmemI ymemI) H
 
+lemma local_of_unique_nonzero_prime (R : Type u) [comm_ring R]
+  (h : ∃! P : ideal R, P ≠ ⊥ ∧ ideal.is_prime P) : local_ring R :=
+local_of_unique_max_ideal begin
+  rcases h with ⟨P, ⟨hPnonzero, hPnot_top, _⟩, hPunique⟩,
+  refine ⟨P, ⟨hPnot_top, _⟩, λ M hM, hPunique _ ⟨_, ideal.is_maximal.is_prime hM⟩⟩,
+  { refine ideal.maximal_of_no_maximal (λ M hPM hM, ne_of_lt hPM _),
+    exact (hPunique _ ⟨ne_bot_of_gt hPM, ideal.is_maximal.is_prime hM⟩).symm },
+  { rintro rfl,
+    exact hPnot_top (hM.2 P (bot_lt_iff_ne_bot.2 hPnonzero)) },
+end
+
 section prio
 set_option default_priority 100 -- see Note [default priority]
 /-- A local ring homomorphism is a homomorphism between local rings