From 4d2aeea2c2739003c9b15337115a8bc96840671f Mon Sep 17 00:00:00 2001
From: poincare-duality <jidongw@uoregon.edu>
Date: Tue, 13 Jun 2023 21:17:54 -0700
Subject: [PATCH] more updates

---
 CommAlg/jayden(krull-dim-zero).lean | 19 ++++++++++++++++---
 1 file changed, 16 insertions(+), 3 deletions(-)

diff --git a/CommAlg/jayden(krull-dim-zero).lean b/CommAlg/jayden(krull-dim-zero).lean
index 6f282ba..523eb90 100644
--- a/CommAlg/jayden(krull-dim-zero).lean
+++ b/CommAlg/jayden(krull-dim-zero).lean
@@ -77,12 +77,25 @@ lemma containment_radical_power_containment :
     rintro ⟨RisNoetherian, containment⟩ 
     rw [isNoetherianRing_iff_ideal_fg] at RisNoetherian
     specialize RisNoetherian (Ideal.radical I)
-    rcases RisNoetherian with ⟨S, Sgenerates⟩
+    -- rcases RisNoetherian with ⟨S, Sgenerates⟩
+    have containment2 : ∃ n : ℕ,  (Ideal.radical I) ^ n ≤ I := by
+      apply Ideal.exists_radical_pow_le_of_fg I RisNoetherian
+    cases' containment2 with n containment2'
+    have containment3 : J ^ n ≤ (Ideal.radical I) ^ n := by 
+      apply Ideal.pow_mono containment
+    use n
+    apply le_trans containment3 containment2'
+-- The above can be proven using the following quicker theorem that is in the wrong place.
+-- Ideal.exists_pow_le_of_le_radical_of_fG
 
-    -- how to I get a generating set?
 
 -- Stacks Lemma 10.52.6: I is a maximal ideal and IM = 0. Then length of M is
--- 
+-- the same as the dimension as a vector space over R/I,
+lemma length_eq_dim_if_maximal_annihilates {I : Ideal R} [Ideal.IsMaximal I] 
+    : I • (⊤ : Submodule R M) = 0
+     → Module.length R M = Module.rank R⧸I M⧸(I • (⊤ : Submodule R M)) := by sorry
+
+-- Does lean know that M/IM is a R/I module?
 
 -- Stacks Lemma 10.52.8: I is a finitely generated maximal ideal of R.
 -- M is a finite R-mod and I^nM=0. Then length of M is finite.