feat(ring_theory): submodules and quotients of Noetherian modules are…

… Noetherian

Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Johannes Hölzl <johannes.hoelzl@gmx.de>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>

algebra/order.lean

@@ -47,6 +47,12 @@ lemma lt_iff_lt_of_strict_mono {β} [linear_order α] [preorder β]
   .resolve_left $ λ h', lt_asymm h $ H _ _ h')
   .resolve_left $ λ e, ne_of_gt h $ congr_arg _ e, H _ _⟩
 
+lemma le_iff_le_of_strict_mono {β} [linear_order α] [preorder β]
+  (f : α → β) (H : ∀ a b, a < b → f a < f b) {a b} :
+  f a ≤ f b ↔ a ≤ b :=
+⟨λ h, le_of_not_gt $ λ h', not_le_of_lt (H b a h') h,
+ λ h, (lt_or_eq_of_le h).elim (λ h', le_of_lt (H _ _ h')) (λ h', h' ▸ le_refl _)⟩
+
 lemma injective_of_strict_mono {β} [linear_order α] [preorder β]
   (f : α → β) (H : ∀ a b, a < b → f a < f b) : function.injective f
 | a b e := ((lt_trichotomy a b)

data/set/basic.lean

@@ -453,9 +453,12 @@ by finish
 theorem set_compr_eq_eq_singleton {a : α} : {b | b = a} = {a} :=
 set.ext $ by simp
 
-theorem union_singleton : s ∪ {a} = insert a s :=
+@[simp] theorem union_singleton : s ∪ {a} = insert a s :=
 by simp [singleton_def]
 
+@[simp] theorem singleton_union : {a} ∪ s = insert a s :=
+by rw [union_comm, union_singleton]
+
 theorem singleton_inter_eq_empty : {a} ∩ s = ∅ ↔ a ∉ s :=
 by simp [eq_empty_iff_forall_not_mem]
 
@@ -640,7 +643,7 @@ diff_eq_self.2 $ by simp [singleton_inter_eq_empty.2 h]
 
 @[simp] theorem insert_diff_singleton {a : α} {s : set α} :
   insert a (s \ {a}) = insert a s :=
-by simp [insert_eq, union_diff_self]
+by simp [insert_eq, union_diff_self, -union_singleton, -singleton_union]
 
 /- powerset -/
 

data/set/finite.lean

@@ -59,6 +59,10 @@ theorem finite.exists_finset {s : set α} : finite s →
   ∃ s' : finset α, ∀ a : α, a ∈ s' ↔ a ∈ s
 | ⟨h⟩ := by exactI ⟨to_finset s, λ _, mem_to_finset⟩
 
+theorem finite.exists_finset_coe {s : set α} (hs : finite s) :
+  ∃ s' : finset α, ↑s' = s :=
+let ⟨s', h⟩ := hs.exists_finset in ⟨s', set.ext h⟩
+
 theorem finite_mem_finset (s : finset α) : finite {a | a ∈ s} :=
 ⟨fintype_of_finset s (λ _, iff.rfl)⟩
 

linear_algebra/basic.lean

@@ -178,7 +178,7 @@ span_eq is_submodule_span (set.insert_subset.mpr ⟨h, subset_span⟩) (span_mon
 lemma span_insert : span (insert b s) = {z | ∃a, ∃x∈span s, z = a • b + x } :=
 set.ext $ assume b',
 begin
-  split; simp [insert_eq, span_union, span_singleton, set.ext_iff, range, -add_comm],
+  split; rw [insert_eq, span_union]; simp [span_singleton, set.ext_iff, range, -add_comm],
   exact (assume y a eq_y x hx eq, ⟨a, x, hx, by simp [eq_y, eq]⟩),
   exact (assume a b₂ hb₂ eq, ⟨a • b, ⟨a, rfl⟩, b₂, hb₂, eq⟩)
 end
@@ -745,11 +745,11 @@ assume t, finset.induction_on t
         have s ⊆ span ↑(insert b₂ s' ∪ t), from
           assume b₃ hb₃,
           have ↑(s' ∪ insert b₁ t) ⊆ insert b₁ (insert b₂ ↑(s' ∪ t) : set β),
-            by simp [insert_eq, union_subset_union, subset.refl, subset_union_right],
+            by simp [insert_eq, -singleton_union, -union_singleton, union_subset_union, subset.refl, subset_union_right],
           have hb₃ : b₃ ∈ span (insert b₁ (insert b₂ ↑(s' ∪ t) : set β)),
             from span_mono this (hss' hb₃),
           have s ⊆ span (insert b₁ ↑(s' ∪ t)),
-            by simpa [insert_eq] using hss',
+            by simpa [insert_eq, -singleton_union, -union_singleton] using hss',
           have hb₁ : b₁ ∈ span (insert b₂ ↑(s' ∪ t)),
             from mem_span_insert_exchange (this hb₂s) hb₂t,
           by rw [span_insert_eq_span hb₁] at hb₃; simpa using hb₃,

linear_algebra/quotient_module.lean

@@ -124,4 +124,7 @@ assume a b, quotient.induction_on₂' a b $ assume a b (h : f a = f b), quotient
   have f (a - b) = 0, by rw [hf.sub]; simp [h],
   show a - b ∈ s, from hs.symm ▸ this
 
-end quotient_module
+lemma quotient.exists_rep {s : set β} [is_submodule s] : ∀ q : quotient β s, ∃ b : β, mk b = q :=
+@_root_.quotient.exists_rep _ (quotient_rel s)
+
+end quotient_module

linear_algebra/subtype_module.lean

@@ -43,10 +43,12 @@ instance {α β} {f : field α} [vector_space α β] {p : set β} [is_submodule
 
 @[simp] lemma sub_val : (x - y).val = x.val - y.val := by simp
 
+-- should this be in the root namespace?
 lemma is_linear_map_subtype_val {f : γ → {x : β // x ∈ p}} (hf : is_linear_map f) :
   is_linear_map (λb, (f b).val) :=
 by refine {..}; simp [hf.add, hf.smul]
 
+-- should this be in the root namespace?
 lemma is_linear_map_subtype_mk (f : γ → β) (hf : is_linear_map f) (h : ∀c, f c ∈ p) :
   is_linear_map (λc, ⟨f c, h c⟩ : γ → {x : β // x ∈ p}) :=
 by refine {..}; intros; apply subtype.eq; simp [hf.add, hf.smul]
@@ -55,4 +57,10 @@ instance {s t : set β} [is_submodule s] [is_submodule t] :
   is_submodule (@subtype.val β (λx, x ∈ s) ⁻¹' t) :=
 is_submodule.preimage (is_linear_map_subtype_val is_linear_map.id)
 
+-- shouldn't this be the thing called is_linear_map_subtype_val?
+lemma is_submodule.is_linear_map_inclusion : is_linear_map (λ x : {x : β // x ∈ p}, x.val) :=
+{ add := by simp,
+  smul := by simp
+}
+
 end

order/conditionally_complete_lattice.lean

@@ -128,7 +128,7 @@ show (bdd_above s ∧ bdd_above t) → bdd_above (s ∪ t), from
 /--Adding a point to a set preserves its boundedness above.-/
 @[simp] lemma bdd_above_insert : bdd_above (insert a s) ↔ bdd_above s :=
 ⟨show bdd_above (insert a s) → bdd_above s, from bdd_above_subset (by simp),
- show bdd_above s → bdd_above (insert a s), by rw[insert_eq]; finish⟩
+ show bdd_above s → bdd_above (insert a s), by rw [insert_eq]; simp [-singleton_union] {contextual := tt}⟩
 
 /--A finite set is bounded above.-/
 lemma bdd_above_finite [inhabited α] (_ : finite s) : bdd_above s :=
@@ -183,7 +183,7 @@ show (bdd_below s ∧ bdd_below t) → bdd_below (s ∪ t), from
 /--Adding a point to a set preserves its boundedness below.-/
 @[simp] lemma bdd_below_insert : bdd_below (insert a s) ↔ bdd_below s :=
 ⟨show bdd_below (insert a s) → bdd_below s, from bdd_below_subset (by simp),
- show bdd_below s → bdd_below (insert a s), by rw[insert_eq]; finish⟩
+ show bdd_below s → bdd_below (insert a s), by rw[insert_eq]; simp [-singleton_union] {contextual := tt}⟩
 
 /--A finite set is bounded below.-/
 lemma bdd_below_finite [inhabited α] (_ : finite s) : bdd_below s :=

order/order_iso.lean

@@ -24,6 +24,11 @@ def order.preimage {α β} (f : α → β) (s : β → β → Prop) (x y : α) :
 
 infix ` ⁻¹'o `:80 := order.preimage
 
+/-- the induced order on a subtype is an embedding under the natural inclusion. -/
+definition subtype.order_embedding {X : Type*} (r : X → X → Prop) (p : X → Prop) : 
+((subtype.val : subtype p → X) ⁻¹'o r) ≼o r := 
+⟨⟨subtype.val,subtype.val_injective⟩,by intros;refl⟩
+
 namespace order_embedding
 
 instance : has_coe_to_fun (r ≼o s) := ⟨λ _, α → β, λ o, o.to_embedding⟩
@@ -129,6 +134,15 @@ end
 @[simp] theorem of_monotone_coe [is_trichotomous α r] [is_asymm β s] (f : α → β) (H) :
   (@of_monotone _ _ r s _ _ f H : α → β) = f := rfl
 
+-- If le is preserved by an order embedding of preorders, then lt is too
+definition lt_embedding_of_le_embedding [preorder α] [preorder β]
+  (f : (has_le.le : α → α → Prop) ≼o (has_le.le : β → β → Prop)) :
+(has_lt.lt : α → α → Prop) ≼o (has_lt.lt : β → β → Prop) :=
+{ to_fun := f,
+  inj := f.inj,
+  ord := by intros;simp [lt_iff_le_not_le,f.ord],
+  }
+
 theorem nat_lt [is_strict_order α r] (f : ℕ → α) (H : ∀ n:ℕ, r (f n) (f (n+1))) :
   ((<) : ℕ → ℕ → Prop) ≼o r :=
 of_monotone f $ λ a b h, begin
@@ -283,6 +297,14 @@ order_embedding.is_well_order (subrel.order_embedding r p)
 
 end subrel
 
+-- KMB is only putting this here because subrel is cool
+instance subtype.partial_order (X) [partial_order X] (p : X → Prop) : partial_order ({x : X // p x}) :=
+{ le := subrel (≤) p,
+  le_refl := λ a, le_refl (a : X),
+  le_trans := λ a b c, le_trans,
+  le_antisymm := λ a b hab hba, subtype.eq $ le_antisymm hab hba
+}
+
 /-- Restrict the codomain of an order embedding -/
 def order_embedding.cod_restrict (p : set β) (f : r ≼o s) (H : ∀ a, f a ∈ p) : r ≼o subrel s p :=
 ⟨f.to_embedding.cod_restrict p H, f.ord⟩

ring_theory/correspondence_theorem.lean

@@ -0,0 +1,52 @@
+import ring_theory.submodule
+import linear_algebra.quotient_module -- I propose moving this to ring_theory
+import tactic.tidy
+import order.order_iso
+
+open is_submodule
+open quotient_module
+
+definition module.correspondence_equiv (R) [ring R] (M) [module R M] (N : set M) [is_submodule N] :
+(has_le.le : submodule R (quotient M N) → submodule R (quotient M N) → Prop) ≃o 
+(has_le.le : {X : submodule R M // N ⊆ X} → {X : submodule R M // N ⊆ X} → Prop) := {
+  to_fun := λ Xbar, ⟨submodule.pullback (mk : M → (quotient M N))
+    (is_linear_map_quotient_mk N) Xbar,λ n Hn,begin
+      show ↑n ∈ Xbar.s,
+      haveI := Xbar.sub,
+      have : ((0 : M) : quotient M N) ∈ Xbar.s,
+        exact @is_submodule.zero _ _ _ _ Xbar.s _,
+      suffices : (n : quotient M N) = (0 : M),
+        rwa this,
+      rw quotient_module.eq,
+      simp [Hn],
+    end⟩,
+  inv_fun := λ X, submodule.pushforward mk (is_linear_map_quotient_mk N) X.val,
+  left_inv := λ P, submodule.eq $ set.image_preimage_eq quotient_module.quotient.exists_rep,
+  right_inv := λ ⟨P,HP⟩, subtype.eq $ begin
+    show submodule.pullback mk _ (submodule.pushforward mk _ P) = P,
+    ext x,
+    split,swap,apply set.subset_preimage_image,
+    rintro ⟨y,Hy,Hyx⟩,
+    change (y : quotient M N) = x at Hyx,
+    rw quotient_module.eq at Hyx,
+    suffices : y - (y - x) ∈ P,
+      simpa,
+    haveI := P.sub,
+    exact is_submodule.sub Hy (HP Hyx),
+  end,
+  ord := by tidy
+}
+
+namespace quotient_module
+
+definition le_order_embedding (R) [ring R] (M) [module R M] (N : set M) [is_submodule N] :
+  (has_le.le : submodule R (quotient M N) → submodule R (quotient M N) → Prop) ≼o
+  (has_le.le : submodule R M → submodule R M → Prop) :=
+order_embedding.trans (order_iso.to_order_embedding $ module.correspondence_equiv R M N) (subtype.order_embedding _ _)
+
+definition lt_order_embedding (R) [ring R] (M) [module R M] (N : set M) [is_submodule N] :
+  (has_lt.lt : submodule R (quotient M N) → submodule R (quotient M N) → Prop) ≼o
+  (has_lt.lt : submodule R M → submodule R M → Prop) :=
+order_embedding.lt_embedding_of_le_embedding $ quotient_module.le_order_embedding R M N
+
+end quotient_module

ring_theory/noetherian.lean

@@ -0,0 +1,102 @@
+import ring_theory.ideals data.fintype order.order_iso data.polynomial linear_algebra.subtype_module
+import tactic.tidy
+import ring_theory.submodule -- KMB moved some stuff from this file to here 
+import linear_algebra.quotient_module
+import ring_theory.correspondence_theorem
+
+local attribute [instance] classical.dec
+open set lattice
+
+def is_fg {α β} [ring α] [module α β]
+  (s : set β) [is_submodule s] : Prop :=
+∃ t : finset β, _root_.span ↑t = s
+
+namespace submodule
+universes u v
+variables {α : Type u} {β : Type v} [ring α] [module α β]
+
+-- KMB moved around 90 lines to ring_theory/submodule.lean
+
+def fg (s : submodule α β) : Prop := is_fg (s : set β)
+
+theorem fg_def {s : submodule α β} :
+  s.fg ↔ ∃ t : set β, finite t ∧ span t = s :=
+⟨λ ⟨t, h⟩, ⟨_, finset.finite_to_set t, ext h⟩, begin
+  rintro ⟨t', h, rfl⟩,
+  rcases finite.exists_finset_coe h with ⟨t, rfl⟩,
+  exact ⟨t, rfl⟩
+end⟩
+
+def univ : submodule α β :=
+{ s := univ,
+  sub := is_submodule.univ }
+
+end submodule
+
+def is_noetherian (α β) [ring α] [module α β] : Prop :=
+∀ (s : submodule α β), s.fg
+
+theorem is_noetherian_iff_well_founded
+  {α β} [ring α] [module α β] :
+  is_noetherian α β ↔ well_founded ((>) : submodule α β → submodule α β → Prop) :=
+⟨λ h, begin
+  apply order_embedding.well_founded_iff_no_descending_seq.2,
+  swap, { apply is_strict_order.swap },
+  rintro ⟨⟨N, hN⟩⟩,
+  let M := ⨆ n, N n,
+  rcases submodule.fg_def.1 (h M) with ⟨t, h₁, h₂⟩,
+  have hN' : ∀ {a b}, a ≤ b → N a ≤ N b :=
+    λ a b, (le_iff_le_of_strict_mono N (λ _ _, hN.1)).2,
+  have : t ⊆ ⋃ i, (N i : set β),
+  { rw [← submodule.Union_set_of_directed _ N _],
+    { show t ⊆ M, rw ← h₂,
+      apply subset_span },
+    { apply_instance },
+    { exact λ i j, ⟨max i j,
+        hN' (le_max_left _ _),
+        hN' (le_max_right _ _)⟩ } },
+  simp [subset_def] at this,
+  have : ∀ x : t, (∃ (i : ℕ), x.1 ∈ N i), {simpa},
+  rcases classical.axiom_of_choice this with ⟨f, hf⟩,
+  dsimp at f hf,
+  cases h₁ with h₁,
+  let A := finset.sup (@finset.univ t h₁) f,
+  have : M ≤ N A,
+  { rw ← h₂, apply submodule.span_subset_iff.2,
+    exact λ x h, hN' (finset.le_sup (@finset.mem_univ t h₁ _))
+      (hf ⟨x, h⟩) },
+  exact not_le_of_lt (hN.1 (nat.lt_succ_self A))
+    (le_trans (le_supr _ _) this)
+ end,
+ λ h N, begin
+  suffices : ∀ M ≤ N, ∃ s, finite s ∧ M ⊔ submodule.span s = N,
+  { rcases this ⊥ bot_le with ⟨s, hs, e⟩,
+    exact submodule.fg_def.2 ⟨s, hs, by simpa using e⟩ },
+  refine λ M, h.induction M _, intros M IH MN,
+  by_cases h : ∀ x, x ∈ N → x ∈ M,
+  { cases le_antisymm MN h, exact ⟨∅, by simp⟩ },
+  { simp [not_forall] at h,
+    rcases h with ⟨x, h, h₂⟩,
+    have : ¬M ⊔ submodule.span {x} ≤ M,
+    { intro hn, apply h₂,
+      simpa using submodule.span_subset_iff.1 (le_trans le_sup_right hn) },
+    rcases IH (M ⊔ submodule.span {x})
+      ⟨le_sup_left, this⟩
+      (sup_le MN (submodule.span_subset_iff.2 (by simpa))) with ⟨s, hs, hs₂⟩,
+    refine ⟨insert x s, finite_insert _ hs, _⟩,
+    rw [← hs₂, sup_assoc, ← submodule.span_union], simp }
+ end⟩
+
+def is_noetherian_ring (α) [ring α] : Prop := is_noetherian α α
+
+theorem is_noetherian_of_submodule_of_noetherian (R M) [ring R] [module R M] (N : set M) [is_submodule N]
+  (h : is_noetherian R M) : is_noetherian R N :=
+begin
+  rw is_noetherian_iff_well_founded at h ⊢,
+  convert order_embedding.well_founded (order_embedding.rsymm (submodule.lt_order_embedding R M N)) h,end
+
+theorem is_noetherian_of_quotient_of_noetherian (R) [ring R] (M) [module R M] (N : set M) [is_submodule N]
+  (h : is_noetherian R M) : is_noetherian R (quotient_module.quotient M N) :=
+begin
+  rw is_noetherian_iff_well_founded at h ⊢,
+  convert order_embedding.well_founded (order_embedding.rsymm (quotient_module.lt_order_embedding R M N)) h,end