From b2c5d9b2b3397af0a5c01e9a845581708a46320b Mon Sep 17 00:00:00 2001
From: Chase Meadors <c.ed.mead@gmail.com>
Date: Wed, 27 Jan 2021 08:41:40 +0000
Subject: [PATCH] feat(ring_theory/noetherian, linear_algebra/basic): Show that
 finitely generated submodules are the compact elements in the submodule
 lattice (#5871)

Show that a submodule is finitely generated if and only if it is a compact lattice element. Add lemma showing that any submodule is the supremum of the spans of its elements.
---
 src/data/finset/lattice.lean       |  4 +++
 src/linear_algebra/basic.lean      |  3 +++
 src/order/compactly_generated.lean | 16 ++++++++++++
 src/ring_theory/noetherian.lean    | 39 ++++++++++++++++++++++++++++++
 4 files changed, 62 insertions(+)

diff --git a/src/data/finset/lattice.lean b/src/data/finset/lattice.lean
index 202d93f4ebb4f..0ab7c3be88db4 100644
--- a/src/data/finset/lattice.lean
+++ b/src/data/finset/lattice.lean
@@ -606,6 +606,10 @@ lemma supr_finset_image {f : γ → α} {g : α → β} {s : finset γ} :
   (⨆ x ∈ s.image f, g x) = (⨆ y ∈ s, g (f y)) :=
 by rw [← supr_coe, coe_image, supr_image, supr_coe]
 
+lemma sup_finset_image {f : γ → α} {g : α → β} {s : finset γ} :
+  s.sup (g ∘ f) = (s.image f).sup g :=
+by { simp_rw [sup_eq_supr, comp_app], rw supr_finset_image, }
+
 lemma infi_finset_image {f : γ → α} {g : α → β} {s : finset γ} :
   (⨅ x ∈ s.image f, g x) = (⨅ y ∈ s, g (f y)) :=
 by rw [← infi_coe, coe_image, infi_image, infi_coe]
diff --git a/src/linear_algebra/basic.lean b/src/linear_algebra/basic.lean
index 6df552378ae59..4193b351e6956 100644
--- a/src/linear_algebra/basic.lean
+++ b/src/linear_algebra/basic.lean
@@ -826,6 +826,9 @@ lemma span_union (s t : set M) : span R (s ∪ t) = span R s ⊔ span R t :=
 lemma span_Union {ι} (s : ι → set M) : span R (⋃ i, s i) = ⨆ i, span R (s i) :=
 (submodule.gi R M).gc.l_supr
 
+lemma span_eq_supr_of_singleton_spans (s : set M) : span R s = ⨆ x ∈ s, span R {x} :=
+by simp only [←span_Union, set.bUnion_of_singleton s]
+
 @[simp] theorem coe_supr_of_directed {ι} [hι : nonempty ι]
   (S : ι → submodule R M) (H : directed (≤) S) :
   ((supr S : submodule R M) : set M) = ⋃ i, S i :=
diff --git a/src/order/compactly_generated.lean b/src/order/compactly_generated.lean
index d4ce6c62d242c..1457248d240ad 100644
--- a/src/order/compactly_generated.lean
+++ b/src/order/compactly_generated.lean
@@ -120,6 +120,22 @@ begin
     use t, exact ⟨htS, by rwa ←htsup⟩, },
 end
 
+lemma finset_sup_compact_of_compact {α β : Type*} [complete_lattice α] {f : β → α}
+  (s : finset β) (h : ∀ x ∈ s, is_compact_element (f x)) : is_compact_element (s.sup f) :=
+begin
+  classical,
+  rw is_compact_element_iff_le_of_directed_Sup_le,
+  intros d hemp hdir hsup,
+  change f with id ∘ f, rw finset.sup_finset_image,
+  apply finset.sup_le_of_le_directed d hemp hdir,
+  rintros x hx,
+  obtain ⟨p, ⟨hps, rfl⟩⟩ := finset.mem_image.mp hx,
+  specialize h p hps,
+  rw is_compact_element_iff_le_of_directed_Sup_le at h,
+  specialize h d hemp hdir (_root_.le_trans (finset.le_sup hps) hsup),
+  simpa only [exists_prop],
+end
+
 lemma well_founded.is_Sup_finite_compact (h : well_founded ((>) : α → α → Prop)) :
   is_Sup_finite_compact α :=
 begin
diff --git a/src/ring_theory/noetherian.lean b/src/ring_theory/noetherian.lean
index 81d1c0f054b7f..6db0d96fbd1d1 100644
--- a/src/ring_theory/noetherian.lean
+++ b/src/ring_theory/noetherian.lean
@@ -7,6 +7,7 @@ import algebraic_geometry.prime_spectrum
 import data.multiset.finset_ops
 import linear_algebra.linear_independent
 import order.order_iso_nat
+import order.compactly_generated
 import ring_theory.ideal.operations
 
 /-!
@@ -199,6 +200,44 @@ begin
     { exact zero_smul _ }, { exact λ _ _ _, add_smul _ _ _ } }
 end
 
+lemma singleton_span_is_compact_element (x : M) :
+  complete_lattice.is_compact_element (span R {x} : submodule R M) :=
+begin
+  rw complete_lattice.is_compact_element_iff_le_of_directed_Sup_le,
+  intros d hemp hdir hsup,
+  have : x ∈ Sup d, from (le_def.mp hsup) (mem_span_singleton_self x),
+  obtain ⟨y, ⟨hyd, hxy⟩⟩ := (mem_Sup_of_directed hemp hdir).mp this,
+  exact ⟨y, ⟨hyd, by simpa only [span_le, singleton_subset_iff]⟩⟩,
+end
+
+/-- Finitely generated submodules are precisely compact elements in the submodule lattice -/
+theorem fg_iff_compact (s : submodule R M) : s.fg ↔ complete_lattice.is_compact_element s :=
+begin
+  classical,
+  -- Introduce shorthand for span of an element
+  let sp : M → submodule R M := λ a, span R {a},
+  -- Trivial rewrite lemma; a small hack since simp (only) & rw can't accomplish this smoothly.
+  have supr_rw : ∀ t : finset M, (⨆ x ∈ t, sp x) = (⨆ x ∈ (↑t : set M), sp x), from λ t, by refl,
+  split,
+  { rintro ⟨t, rfl⟩,
+    rw [span_eq_supr_of_singleton_spans, ←supr_rw, ←(finset.sup_eq_supr t sp)],
+    apply complete_lattice.finset_sup_compact_of_compact,
+    exact λ n _, singleton_span_is_compact_element n, },
+  { intro h,
+    -- s is the Sup of the spans of its elements.
+    have sSup : s = Sup (sp '' ↑s),
+    by rw [Sup_eq_supr, supr_image, ←span_eq_supr_of_singleton_spans, eq_comm, span_eq],
+    -- by h, s is then below (and equal to) the sup of the spans of finitely many elements.
+    obtain ⟨u, ⟨huspan, husup⟩⟩ := h (sp '' ↑s) (le_of_eq sSup),
+    have ssup : s = u.sup id,
+    { suffices : u.sup id ≤ s, from le_antisymm husup this,
+      rw [sSup, finset.sup_eq_Sup], exact Sup_le_Sup huspan, },
+    obtain ⟨t, ⟨hts, rfl⟩⟩ := finset.subset_image_iff.mp huspan,
+    rw [←finset.sup_finset_image, function.comp.left_id, finset.sup_eq_supr, supr_rw,
+      ←span_eq_supr_of_singleton_spans, eq_comm] at ssup,
+    exact ⟨t, ssup⟩, },
+end
+
 end submodule
 
 /--