From 7de57e84c5231c3876ed5f9c9e448dc7e0d7cb9e Mon Sep 17 00:00:00 2001
From: Kenny Lau <kc_kennylau@yahoo.com.hk>
Date: Fri, 8 Mar 2019 20:10:50 +0000
Subject: [PATCH] feat(ring_theory/noetherian): Nakayama's Lemma (#778)

* feat(ring_theory/noetherian): Nakayama's Lemma

* Update src/ring_theory/noetherian.lean

Co-Authored-By: kckennylau <kc_kennylau@yahoo.com.hk>
---
 src/ring_theory/ideal_operations.lean |  9 +++++++
 src/ring_theory/noetherian.lean       | 37 +++++++++++++++++++++++++++
 2 files changed, 46 insertions(+)

diff --git a/src/ring_theory/ideal_operations.lean b/src/ring_theory/ideal_operations.lean
index 21fcd2a321805..57e1dd8c5061d 100644
--- a/src/ring_theory/ideal_operations.lean
+++ b/src/ring_theory/ideal_operations.lean
@@ -85,6 +85,15 @@ theorem smul_induction_on {p : M → Prop} {x} (H : x ∈ I • N)
   (H2 : ∀ (c:R) n, p n → p (c • n)) : p x :=
 (@smul_le _ _ _ _ _ _ _ ⟨p, H0, H1, H2⟩).2 Hb H
 
+theorem mem_smul_span_singleton {I : ideal R} {m : M} {x : M} :
+  x ∈ I • span R ({m} : set M) ↔ ∃ y ∈ I, y • m = x :=
+⟨λ hx, smul_induction_on hx
+  (λ r hri n hnm, let ⟨s, hs⟩ := mem_span_singleton.1 hnm in ⟨r * s, I.mul_mem_right hri, hs ▸ mul_smul r s m⟩)
+  ⟨0, I.zero_mem, by rw [zero_smul]⟩
+  (λ m1 m2 ⟨y1, hyi1, hy1⟩ ⟨y2, hyi2, hy2⟩, ⟨y1 + y2, I.add_mem hyi1 hyi2, by rw [add_smul, hy1, hy2]⟩)
+  (λ c r ⟨y, hyi, hy⟩, ⟨c * y, I.mul_mem_left hyi, by rw [mul_smul, hy]⟩),
+λ ⟨y, hyi, hy⟩, hy ▸ smul_mem_smul hyi (subset_span $ set.mem_singleton m)⟩
+
 theorem smul_le_right : I • N ≤ N :=
 smul_le.2 $ λ r hr n, N.smul_mem r
 
diff --git a/src/ring_theory/noetherian.lean b/src/ring_theory/noetherian.lean
index e2af5ab60955f..896d0b61a5977 100644
--- a/src/ring_theory/noetherian.lean
+++ b/src/ring_theory/noetherian.lean
@@ -24,6 +24,43 @@ theorem fg_def {s : submodule α β} :
   exact ⟨t, rfl⟩
 end⟩
 
+/-- Nakayama's Lemma. Atiyah-Macdonald 2.5, Eisenbud 4.7, Matsumura 2.2, Stacks 00DV -/
+theorem exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul {R : Type*} [comm_ring R]
+  {M : Type*} [add_comm_group M] [module R M]
+  (I : ideal R) (N : submodule R M) (hn : N.fg) (hin : N ≤ I • N) :
+  ∃ r : R, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = (0 : M) :=
+begin
+  rw fg_def at hn, rcases hn with ⟨s, hfs, hs⟩,
+  have : ∃ r : R, r - 1 ∈ I ∧ N ≤ (I • span R s).comap (linear_map.lsmul R M r) ∧ s ⊆ N,
+  { refine ⟨1, _, _, _⟩,
+    { rw sub_self, exact I.zero_mem },
+    { rw [hs], intros n hn, rw [mem_coe, mem_comap], change (1:R) • n ∈ I • N, rw one_smul, exact hin hn },
+    { rw [← span_le, hs], exact le_refl N } },
+  clear hin hs, revert this,
+  refine set.finite.dinduction_on hfs (λ H, _) (λ i s his hfs ih H, _),
+  { rcases H with ⟨r, hr1, hrn, hs⟩, refine ⟨r, hr1, λ n hn, _⟩, specialize hrn hn,
+    rwa [mem_coe, mem_comap, span_empty, smul_bot, mem_bot] at hrn },
+  apply ih, rcases H with ⟨r, hr1, hrn, hs⟩,
+  rw [← set.singleton_union, span_union, smul_sup] at hrn,
+  rw [set.insert_subset] at hs,
+  have : ∃ c : R, c - 1 ∈ I ∧ c • i ∈ I • span R s,
+  { specialize hrn hs.1, rw [mem_coe, mem_comap, mem_sup] at hrn,
+    rcases hrn with ⟨y, hy, z, hz, hyz⟩, change y + z = r • i at hyz,
+    rw mem_smul_span_singleton at hy, rcases hy with ⟨c, hci, rfl⟩,
+    use r-c, split,
+    { rw [sub_right_comm], exact I.sub_mem hr1 hci },
+    { rw [sub_smul, ← hyz, add_sub_cancel'], exact hz } },
+  rcases this with ⟨c, hc1, hci⟩, refine ⟨c * r, _, _, hs.2⟩,
+  { rw [← ideal.quotient.eq, ideal.quotient.mk_one] at hr1 hc1 ⊢,
+    rw [ideal.quotient.mk_mul, hc1, hr1, mul_one] },
+  { intros n hn, specialize hrn hn, rw [mem_coe, mem_comap, mem_sup] at hrn,
+    rcases hrn with ⟨y, hy, z, hz, hyz⟩, change y + z = r • n at hyz,
+    rw mem_smul_span_singleton at hy, rcases hy with ⟨d, hdi, rfl⟩,
+    change _ • _ ∈ I • span R s,
+    rw [mul_smul, ← hyz, smul_add, smul_smul, mul_comm, mul_smul],
+    exact add_mem _ (smul_mem _ _ hci) (smul_mem _ _ hz) }
+end
+
 theorem fg_bot : (⊥ : submodule α β).fg :=
 ⟨∅, by rw [finset.coe_empty, span_empty]⟩