feat(src/ring_theory): in a PID, all fractional ideals are invertible (…

…#2826)

This would show that all PIDs are Dedekind domains, once we have a definition of Dedekind domain (we could define it right now, but it would depend on the choice of field of fractions).

In `localization.lean`, I added a few small lemmas on localizations (`localization.exists_integer_multiple` and `fraction_map.to_map_eq_zero_iff`). @101damnations, are these additions compatible with your branches? I'm happy to change them if not.

src/ring_theory/fractional_ideal.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anne Baanen
 -/
 import ring_theory.localization
+import ring_theory.principal_ideal_domain
 
 /-!
 # Fractional ideals
@@ -119,6 +120,15 @@ instance coe_to_fractional_ideal : has_coe (ideal R) (fractional_ideal f) :=
 ⟨ λ I, ⟨↑I, fractional_of_subset_one _ $ λ x ⟨y, hy, h⟩,
   submodule.mem_span_singleton.2 ⟨y, by rw ←h; exact mul_one _⟩⟩ ⟩
 
+@[simp]
+lemma val_coe_ideal (I : ideal R) : (I : fractional_ideal f).1 = I := rfl
+
+@[simp]
+lemma mem_coe {x : f.codomain} {I : ideal R} :
+  x ∈ (I : fractional_ideal f) ↔ ∃ (x' ∈ I), f.to_map x' = x :=
+⟨ λ ⟨x', hx', hx⟩, ⟨x', hx', hx⟩,
+  λ ⟨x', hx', hx⟩, ⟨x', hx', hx⟩ ⟩
+
 instance : has_zero (fractional_ideal f) := ⟨(0 : ideal R)⟩
 
 @[simp]
@@ -146,6 +156,11 @@ iff.intro (λ ⟨x', _, h⟩, ⟨x', h⟩) (λ ⟨x', h⟩, ⟨x', ⟨x', set.me
 lemma coe_mem_one (x : R) : f.to_map x ∈ (1 : fractional_ideal f) :=
 mem_one_iff.mpr ⟨x, rfl⟩
 
+lemma one_mem_one : (1 : P) ∈ (1 : fractional_ideal f) :=
+mem_one_iff.mpr ⟨1, f.to_map.map_one⟩
+
+@[simp] lemma val_one : (1 : fractional_ideal f).1 = (1 : ideal R) := rfl
+
 section lattice
 
 /-!
@@ -289,8 +304,8 @@ instance comm_monoid : comm_monoid (fractional_ideal f) :=
       rintros x hx y ⟨y', y'_mem_R, y'_eq_y⟩,
       rw [←y'_eq_y, mul_comm],
       exact submodule.smul_mem _ _ hx },
-    { have : x * 1 ∈ (I * 1) := f.to_map.map_one ▸ mul_mem_mul h (coe_mem_one _),
-      simpa }
+    { have : x * 1 ∈ (I * 1) := mul_mem_mul h one_mem_one,
+      rwa [mul_one] at this }
   end,
   one_mul := λ I, begin
     ext,
@@ -299,8 +314,8 @@ instance comm_monoid : comm_monoid (fractional_ideal f) :=
       rintros x ⟨x', x'_mem_R, x'_eq_x⟩ y hy,
       rw ←x'_eq_x,
       exact submodule.smul_mem _ _ hy },
-    { have : 1 * x ∈ (1 * I) := f.to_map.map_one ▸ mul_mem_mul (coe_mem_one _) h,
-      simpa }
+    { have : 1 * x ∈ (1 * I) := mul_mem_mul one_mem_one h,
+      rwa [one_mul] at this }
   end,
   ..fractional_ideal.has_mul,
   ..fractional_ideal.has_one }
@@ -320,6 +335,7 @@ instance comm_semiring : comm_semiring (fractional_ideal f) :=
   right_distrib := λ I J K, ext (add_mul _ _ _),
   ..fractional_ideal.add_comm_monoid,
   ..fractional_ideal.comm_monoid }
+
 end semiring
 
 section quotient
@@ -382,6 +398,10 @@ lemma inv_nonzero {I : fractional_ideal g} (h : I ≠ 0) :
   I⁻¹ = ⟨(1 : fractional_ideal g).val / I.1, fractional_div_of_nonzero h⟩ :=
 div_nonzero h
 
+lemma val_inv_of_nonzero {I : fractional_ideal g} (h : I ≠ 0) :
+  I⁻¹.val = (1 : ideal R) / I.val :=
+by { rw inv_nonzero h, refl }
+
 @[simp] lemma div_one {I : fractional_ideal g} : I / 1 = I :=
 begin
   rw [div_nonzero (@one_ne_zero (fractional_ideal g) _)],
@@ -422,8 +442,148 @@ begin
   exact mul_mem_mul hx hy
 end
 
+theorem mul_inv_cancel_iff {I : fractional_ideal g} :
+  I * I⁻¹ = 1 ↔ ∃ J, I * J = 1 :=
+⟨λ h, ⟨I⁻¹, h⟩, λ ⟨J, hJ⟩, by rwa [←right_inverse_eq I J hJ]⟩
+
 end quotient
 
+section principal_ideal_domain
+
+variables {K : Type*} [field K] {g : fraction_map R K}
+
+open_locale classical
+
+open submodule submodule.is_principal
+
+lemma span_fractional_iff {s : set f.codomain} :
+  is_fractional f (span R s) ↔ ∃ (a ≠ (0 : R)), ∀ (b : P), b ∈ s → f.is_integer (f.to_map a * b) :=
+⟨ λ ⟨a, a_nonzero, h⟩, ⟨a, a_nonzero, λ b hb, h b (subset_span hb)⟩,
+  λ ⟨a, a_nonzero, h⟩, ⟨a, a_nonzero, λ b hb, span_induction hb
+    h
+    (is_integer_smul ⟨0, f.to_map.map_zero⟩)
+    (λ x y hx hy, by { rw mul_add, exact is_integer_add hx hy })
+    (λ s x hx, by { rw algebra.mul_smul_comm, exact is_integer_smul hx }) ⟩ ⟩
+
+lemma span_singleton_fractional {x : g.codomain} : is_fractional g (span R {x}) :=
+let ⟨a, ha⟩ := g.exists_integer_multiple x in
+span_fractional_iff.mpr
+  ⟨ a,
+    mem_non_zero_divisors_iff_ne_zero.mp a.2,
+    λ x hx, (mem_singleton_iff.mp hx).symm ▸ ha⟩
+
+/-- `span_singleton x` is the fractional ideal generated by `x` -/
+def span_singleton (x : g.codomain) : fractional_ideal g := ⟨span R {x}, span_singleton_fractional⟩
+
+@[simp] lemma val_span_singleton (x : g.codomain) : (span_singleton x).val = span R {x} := rfl
+
+lemma eq_span_singleton_of_principal (I : fractional_ideal g) [is_principal I.1] :
+  I = span_singleton (generator I.1) :=
+ext (span_singleton_generator I.1).symm
+
+@[simp] lemma span_singleton_zero : span_singleton (0 : g.codomain) = 0 :=
+by { ext, simp [submodule.mem_span_singleton, eq_comm] }
+
+@[simp] lemma span_singleton_one : span_singleton (1 : g.codomain) = 1 :=
+begin
+  ext,
+  refine mem_span_singleton.trans ((exists_congr _).trans mem_one_iff.symm),
+  intro x',
+  refine eq.congr (mul_one _) rfl,
+end
+
+@[simp]
+lemma span_singleton_mul_span_singleton (x y : g.codomain) :
+  span_singleton x * span_singleton y = span_singleton (x * y) :=
+begin
+  ext,
+  simp_rw [val_mul, val_span_singleton, span_mul_span, singleton.is_mul_hom.map_mul]
+end
+
+@[simp]
+lemma coe_span_singleton (x : R) :
+  (↑(span R {x} : ideal R) : fractional_ideal g) = span_singleton (g.to_map x) :=
+begin
+  ext y,
+  refine mem_coe.trans (iff.trans _ mem_span_singleton.symm),
+  split,
+  { rintros ⟨y', hy', rfl⟩,
+    obtain ⟨x', rfl⟩ := mem_span_singleton.mp hy',
+    use x',
+    rw [smul_eq_mul, g.to_map.map_mul],
+    refl },
+  { rintros ⟨y', rfl⟩,
+    exact ⟨y' * x, mem_span_singleton.mpr ⟨y', rfl⟩, g.to_map.map_mul _ _⟩ }
+end
+
+lemma mem_singleton_mul {x y : g.codomain} {I : fractional_ideal g} :
+  y ∈ span_singleton x * I ↔ ∃ y' ∈ I, y = x * y' :=
+begin
+  split,
+  { intro h,
+    apply submodule.mul_induction_on h,
+    { intros x' hx' y' hy',
+      obtain ⟨a, ha⟩ := mem_span_singleton.mp hx',
+      use [a • y', I.1.smul_mem a hy'],
+      rw [←ha, algebra.mul_smul_comm, algebra.smul_mul_assoc] },
+    { exact ⟨0, I.1.zero_mem, (mul_zero x).symm⟩ },
+    { rintros _ _ ⟨y, hy, rfl⟩ ⟨y', hy', rfl⟩,
+      exact ⟨y + y', I.1.add_mem hy hy', (mul_add _ _ _).symm⟩ },
+    { rintros r _ ⟨y', hy', rfl⟩,
+      exact ⟨r • y', I.1.smul_mem r hy', (algebra.mul_smul_comm _ _ _).symm ⟩ } },
+  { rintros ⟨y', hy', rfl⟩,
+    exact mul_mem_mul (mem_span_singleton.mpr ⟨1, one_smul _ _⟩) hy' }
+end
+
+lemma invertible_of_principal (I : fractional_ideal g)
+  [submodule.is_principal I.1] (h : I ≠ 0) :
+  I * I⁻¹ = 1 :=
+begin
+  refine mul_inv_cancel_iff.mpr ⟨span_singleton (generator I.1)⁻¹, _⟩,
+  -- Rewrite only the `I` that appears alone.
+  conv_lhs { congr, rw eq_span_singleton_of_principal I },
+  rw [span_singleton_mul_span_singleton, mul_inv_cancel, span_singleton_one],
+  intro generator_I_eq_zero,
+  apply h,
+  rw [eq_span_singleton_of_principal I, generator_I_eq_zero, span_singleton_zero]
+end
+
+lemma exists_eq_span_singleton_mul (I : fractional_ideal g) :
+  ∃ (a : K) (aI : ideal R), I = span_singleton a * aI :=
+begin
+  obtain ⟨a_inv, nonzero, ha⟩ := I.2,
+  have map_a_nonzero := mt g.to_map_eq_zero_iff.mpr nonzero,
+  use (g.to_map a_inv)⁻¹,
+  use (span_singleton (g.to_map a_inv) * I).1.comap g.lin_coe,
+  ext,
+  refine iff.trans _ mem_singleton_mul.symm,
+  split,
+  { intro hx,
+    obtain ⟨x', hx'⟩ := ha x hx,
+    refine ⟨g.to_map x', mem_coe.mpr ⟨x', (mem_singleton_mul.mpr ⟨x, hx, hx'⟩), rfl⟩, _⟩,
+    erw [hx', ←mul_assoc, inv_mul_cancel map_a_nonzero, one_mul] },
+  { rintros ⟨y, hy, rfl⟩,
+    obtain ⟨x', hx', rfl⟩ := mem_coe.mp hy,
+    obtain ⟨y', hy', hx'⟩ := mem_singleton_mul.mp hx',
+    rw lin_coe_apply at hx',
+    erw [hx', ←mul_assoc, inv_mul_cancel map_a_nonzero, one_mul],
+    exact hy' }
+end
+
+instance is_principal {R} [principal_ideal_domain R] {g : fraction_map R K}
+  (I : fractional_ideal g) : I.val.is_principal :=
+⟨ begin
+  obtain ⟨a, aI, ha⟩ := exists_eq_span_singleton_mul I,
+  have := a * g.to_map (generator aI),
+  use a * g.to_map (generator aI),
+  suffices : I = span_singleton (a * g.to_map (generator aI)),
+  { exact congr_arg subtype.val this },
+  conv_lhs { rw [ha, ←span_singleton_generator aI] },
+  rw [coe_span_singleton (generator aI), span_singleton_mul_span_singleton]
+end ⟩
+
+end principal_ideal_domain
+
 end fractional_ideal
 
 end ring

src/ring_theory/localization.lean

@@ -155,6 +155,23 @@ end
 
 variables (f)
 
+/-- Each element `a : S` has an `M`-multiple which is an integer.
+
+This version multiplies `a` on the right, matching the argument order in `localization.surj`.
+-/
+lemma exists_integer_multiple' (a : S) :
+  ∃ (b : M), is_integer f (a * f.to_map b) :=
+let ⟨⟨num, denom⟩, h⟩ := f.surj a in ⟨denom, set.mem_range.mpr ⟨num, h.symm⟩⟩
+
+/-- Each element `a : S` has an `M`-multiple which is an integer.
+
+This version multiplies `a` on the left, matching the argument order in the `has_scalar` instance.
+-/
+lemma exists_integer_multiple (a : S) :
+  ∃ (b : M), is_integer f (f.to_map b * a) :=
+by { simp_rw mul_comm _ a, apply exists_integer_multiple' }
+
+
 /-- Given `z : S`, `f.to_localization_map.sec z` is defined to be a pair `(x, y) : R × M` such
 that `z * f y = f x` (so this lemma is true by definition). -/
 lemma sec_spec {f : localization M S} (z : S) :
@@ -466,6 +483,8 @@ lemma mem_coe (I : ideal R) {x : S} :
   x ∈ (I : submodule R f.codomain) ↔ ∃ y : R, y ∈ I ∧ f.to_map y = x :=
 iff.rfl
 
+@[simp] lemma lin_coe_apply {x} : f.lin_coe x = f.to_map x := rfl
+
 end localization
 variables (R)
 
@@ -495,15 +514,20 @@ namespace fraction_map
 open localization
 variables {R K}
 
+lemma to_map_eq_zero_iff [comm_ring K] (φ : fraction_map R K) {x : R} :
+  x = 0 ↔ φ.to_map x = 0 :=
+begin
+  rw ← φ.to_map.map_zero,
+  split; intro h,
+  { rw h },
+  { cases φ.eq_iff_exists.mp h with c hc,
+    rw zero_mul at hc,
+    exact c.2 x hc }
+end
+
 protected theorem injective [comm_ring K] (φ : fraction_map R K) :
   injective φ.to_map :=
-φ.to_map.injective_iff.2 $ λ x h,
-  begin
-    rw ←φ.to_map.map_zero at h,
-    cases φ.eq_iff_exists.1 h with c hc,
-    rw zero_mul at hc,
-    exact c.2 x hc
-  end
+φ.to_map.injective_iff.2 (λ _ h, φ.to_map_eq_zero_iff.mpr h)
 
 variables {A : Type*} [integral_domain A]
 
@@ -521,8 +545,7 @@ def to_integral_domain [comm_ring K] (φ : fraction_map A K) : integral_domain K
         rw [mul_assoc z, hy, ←hx]; ac_refl,
       erw h at this,
       rw [zero_mul, zero_mul, ←φ.to_map.map_mul] at this,
-      cases eq_zero_or_eq_zero_of_mul_eq_zero (φ.to_map.injective_iff.1
-        φ.injective _ this.symm) with H H,
+      cases eq_zero_or_eq_zero_of_mul_eq_zero (φ.to_map_eq_zero_iff.mpr this.symm) with H H,
         { exact or.inl (φ.eq_zero_of_fst_eq_zero hx H) },
       { exact or.inr (φ.eq_zero_of_fst_eq_zero hy H) },
     end,