Merge branch 'GTBarkley:main' into main

CommAlg/final_hil_pol.lean

@@ -6,7 +6,6 @@ import Mathlib.RingTheory.Artinian
 import Mathlib.Order.Height
 
 
-
 -- Setting for "library_search"
 set_option maxHeartbeats 0
 macro "ls" : tactic => `(tactic|library_search)
@@ -44,7 +43,7 @@ noncomputable def length ( A : Type _) (M : Type _)
  [CommRing A] [AddCommGroup M] [Module A M] :=  Set.chainHeight {M' : Submodule A M | M' < ⊤}
 
 -- Make instance of M_i being an R_0-module
-instance tada1 (𝒜 : ℤ   → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)]  [DirectSum.GCommRing 𝒜]
+instance tada1 (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)]  [DirectSum.GCommRing 𝒜]
   [DirectSum.Gmodule 𝒜 𝓜] (i : ℤ ) : SMul (𝒜 0) (𝓜 i)
     where smul x y := @Eq.rec ℤ (0+i) (fun a _ => 𝓜 a) (GradedMonoid.GSmul.smul x y) i (zero_add i)
 
@@ -109,8 +108,7 @@ instance {𝒜 : ℤ → Type _} [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GComm
     sorry)
 
 
-
+class StandardGraded (𝒜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜] : Prop where
-class StandardGraded {𝒜 : ℤ → Type _} [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜] : Prop where
   gen_in_first_piece :
     Algebra.adjoin (𝒜 0) (DirectSum.of _ 1 : 𝒜 1 →+ ⨁ i, 𝒜 i).range = (⊤ : Subalgebra (𝒜 0) (⨁ i, 𝒜 i))
 
@@ -124,7 +122,25 @@ def Component_of_graded_as_addsubgroup (𝒜 : ℤ → Type _)
 
 def graded_morphism (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) (𝓝 : ℤ → Type _)
 [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] [∀ i, AddCommGroup (𝓝 i)]
-[DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜][DirectSum.Gmodule 𝒜 𝓝] (f : (⨁ i, 𝓜 i) → (⨁ i, 𝓝 i)) : ∀ i, ∀ (r : 𝓜 i), ∀ j, (j ≠ i → f (DirectSum.of _ i r) j = 0) ∧ (IsLinearMap (⨁ i, 𝒜 i) f) := by sorry
+[DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜][DirectSum.Gmodule 𝒜 𝓝]
+(f : (⨁ i, 𝓜 i) →ₗ[(⨁ i, 𝒜 i)] (⨁ i, 𝓝 i)) 
+: ∀ i, ∀ (r : 𝓜 i), ∀ j, (j ≠ i → f (DirectSum.of _ i r) j = 0) 
+∧ (IsLinearMap (⨁ i, 𝒜 i) f) := by
+  sorry
+
+#check graded_morphism
+
+def graded_isomorphism (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) (𝓝 : ℤ → Type _)
+[∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] [∀ i, AddCommGroup (𝓝 i)]
+[DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜][DirectSum.Gmodule 𝒜 𝓝]
+(f : (⨁ i, 𝓜 i) →ₗ[(⨁ i, 𝒜 i)] (⨁ i, 𝓝 i))
+: IsLinearEquiv f := by
+  sorry
+-- f ∈ (⨁ i, 𝓜 i) ≃ₗ[(⨁ i, 𝒜 i)] (⨁ i, 𝓝 i)
+-- LinearEquivClass f (⨁ i, 𝒜 i) (⨁ i, 𝓜 i) (⨁ i, 𝓝 i)
+-- #print IsLinearEquiv
+#check graded_isomorphism
+
 
 
 def graded_submodule
@@ -143,6 +159,7 @@ end
 
 
 
+
 -- @Quotient of a graded ring R by a graded ideal p is a graded R-Mod, preserving each component
 instance Quotient_of_graded_is_graded
 (𝒜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜]
@@ -150,6 +167,13 @@ instance Quotient_of_graded_is_graded
   : DirectSum.Gmodule 𝒜 (fun i => (𝒜 i)⧸(Component_of_graded_as_addsubgroup 𝒜 p hp i)) := by
   sorry
 
+-- 
+lemma sss
+  : true := by
+  sorry
+
+
+
 
 -- If A_0 is Artinian and local, then A is graded local
 lemma Graded_local_if_zero_component_Artinian_and_local (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) 
@@ -189,10 +213,11 @@ lemma Associated_prime_of_graded_is_graded
 -- If M is a finite graed R-Mod of dimension d ≥ 1, then the Hilbert function H(M, n) is of polynomial type (d - 1)
 theorem Hilbert_polynomial_d_ge_1 (d : ℕ) (d1 : 1 ≤ d) (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)]
 [DirectSum.GCommRing 𝒜]
-[DirectSum.Gmodule 𝒜 𝓜] (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0)) 
+[DirectSum.Gmodule 𝒜 𝓜] (st: StandardGraded 𝒜) (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0)) 
 (fingen : IsNoetherian (⨁ i, 𝒜 i) (⨁ i, 𝓜 i))
 (findim :  dimensionmodule (⨁ i, 𝒜 i) (⨁ i, 𝓜 i) = d)
 (hilb : ℤ → ℤ) (Hhilb: hilbert_function 𝒜 𝓜 hilb)
+
 : PolyType hilb (d - 1) := by
   sorry
 
@@ -203,7 +228,7 @@ theorem Hilbert_polynomial_d_ge_1_reduced
 (d : ℕ) (d1 : 1 ≤ d)
 (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)]
 [DirectSum.GCommRing 𝒜]
-[DirectSum.Gmodule 𝒜 𝓜] (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0))
+[DirectSum.Gmodule 𝒜 𝓜] (st: StandardGraded 𝒜) (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0))
 (fingen : IsNoetherian (⨁ i, 𝒜 i) (⨁ i, 𝓜 i))
 (findim :  dimensionmodule (⨁ i, 𝒜 i) (⨁ i, 𝓜 i) = d)
 (hilb : ℤ → ℤ) (Hhilb: hilbert_function 𝒜 𝓜 hilb)
@@ -217,7 +242,7 @@ theorem Hilbert_polynomial_d_ge_1_reduced
 -- If M is a finite graed R-Mod of dimension zero, then the Hilbert function H(M, n) = 0 for n >> 0 
 theorem Hilbert_polynomial_d_0 (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)]
 [DirectSum.GCommRing 𝒜]
-[DirectSum.Gmodule 𝒜 𝓜] (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0)) 
+[DirectSum.Gmodule 𝒜 𝓜] (st: StandardGraded 𝒜) (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0)) 
 (fingen : IsNoetherian (⨁ i, 𝒜 i) (⨁ i, 𝓜 i))
 (findim :  dimensionmodule (⨁ i, 𝒜 i) (⨁ i, 𝓜 i) = 0)
 (hilb : ℤ → ℤ) (Hhilb : hilbert_function 𝒜 𝓜 hilb)
@@ -230,7 +255,7 @@ theorem Hilbert_polynomial_d_0 (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [
 theorem Hilbert_polynomial_d_0_reduced
 (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)]
 [DirectSum.GCommRing 𝒜]
-[DirectSum.Gmodule 𝒜 𝓜] (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0)) 
+[DirectSum.Gmodule 𝒜 𝓜] (st: StandardGraded 𝒜) (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0)) 
 (fingen : IsNoetherian (⨁ i, 𝒜 i) (⨁ i, 𝓜 i))
 (findim :  dimensionmodule (⨁ i, 𝒜 i) (⨁ i, 𝓜 i) = 0)
 (hilb : ℤ → ℤ) (Hhilb : hilbert_function 𝒜 𝓜 hilb)
@@ -252,6 +277,12 @@ theorem Hilbert_polynomial_d_0_reduced
 
 
 
+
+
+
+
+
+
 
 
 

CommAlg/final_poly_type.lean

@@ -0,0 +1,285 @@
+import Mathlib.Order.Height
+import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
+
+-- Setting for "library_search"
+set_option maxHeartbeats 0
+macro "ls" : tactic => `(tactic|library_search)
+
+-- New tactic "obviously"
+macro "obviously" : tactic =>
+  `(tactic| (
+      first
+        | dsimp; simp; done; dbg_trace "it was dsimp simp"
+        | simp; done; dbg_trace "it was simp"
+        | tauto; done; dbg_trace "it was tauto"
+        | simp; tauto; done; dbg_trace "it was simp tauto"
+        | rfl; done; dbg_trace "it was rfl"
+        | norm_num; done; dbg_trace "it was norm_num"
+        | /-change (@Eq ℝ _ _);-/ linarith; done; dbg_trace "it was linarith"
+        -- | gcongr; done
+        | ring; done; dbg_trace "it was ring"
+        | trivial; done; dbg_trace "it was trivial"
+        -- | nlinarith; done
+        | fail "No, this is not obvious."))
+
+
+-- Testing of Polynomial
+section Polynomial
+noncomputable section
+#check Polynomial 
+#check Polynomial (ℚ)
+#check Polynomial.eval
+
+
+example (f : Polynomial ℚ) (hf : f = Polynomial.C (1 : ℚ)) : Polynomial.eval 2 f = 1 := by
+  have : ∀ (q : ℚ), Polynomial.eval q f = 1 := by
+    sorry
+  obviously
+
+-- example (f : ℤ → ℤ) (hf : ∀ x, f x = x ^ 2) : Polynomial.eval 2 f = 4 := by
+--   sorry
+
+-- degree of a constant function is ⊥ (is this same as -1 ???)
+#print Polynomial.degree_zero
+
+def F : Polynomial ℚ := Polynomial.C (2 : ℚ)
+#print F
+#check F
+#check Polynomial.degree F
+#check Polynomial.degree 0
+#check WithBot ℕ
+-- #eval Polynomial.degree F
+#check Polynomial.eval 1 F
+example : Polynomial.eval (100 : ℚ) F = (2 : ℚ) := by
+  refine Iff.mpr (Rat.ext_iff (Polynomial.eval 100 F) 2) ?_
+  simp only [Rat.ofNat_num, Rat.ofNat_den]
+  rw [F]
+  simp
+
+-- Treat polynomial f ∈ ℚ[X] as a function f : ℚ → ℚ
+#check CoeFun
+
+
+
+
+end section
+
+
+
+
+
+-- @[BH, 4.1.2]
+
+
+
+-- All the polynomials are in ℚ[X], all the functions are considered as ℤ → ℤ
+noncomputable section
+-- Polynomial type of degree d
+@[simp]
+def PolyType (f : ℤ → ℤ) (d : ℕ) := ∃ Poly : Polynomial ℚ, ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → f n = Polynomial.eval (n : ℚ) Poly) ∧ d = Polynomial.degree Poly
+section
+-- structure PolyType (f : ℤ → ℤ) where
+--   Poly : Polynomial ℤ
+--   d : 
+--   N : ℤ
+--   Poly_equal : ∀ n ∈ ℤ → f n = Polynomial.eval n : ℤ Poly
+
+#check PolyType
+
+example (f : ℤ → ℤ) (hf : ∀ x, f x = x ^ 2) : PolyType f 2 := by
+  unfold PolyType
+  sorry
+  -- use Polynomial.monomial (2 : ℤ) (1 : ℤ)
+  -- have' := hf 0; ring_nf at this
+  -- exact this
+
+end section
+
+-- Δ operator (of d times)
+@[simp]
+def Δ : (ℤ → ℤ) → ℕ → (ℤ → ℤ)
+  | f, 0 => f
+  | f, d + 1 => fun (n : ℤ) ↦ (Δ f d) (n + 1) - (Δ f d) (n)  
+section
+-- def Δ (f : ℤ → ℤ) (d : ℕ) := fun (n : ℤ) ↦ f (n + 1) - f n
+-- def add' : ℕ → ℕ → ℕ
+--   | 0, m => m 
+--   | n+1, m => (add' n m) + 1
+-- #eval add' 5 10
+#check Δ
+def f (n : ℤ) := n
+#eval (Δ f 1) 100
+-- #check (by (show_term unfold Δ) : Δ f 0=0)
+end section
+
+
+
+
+
+
+-- (NO need to prove another direction) Constant polynomial function = constant function
+lemma Poly_constant (F : Polynomial ℚ) (c : ℚ) : 
+  (F = Polynomial.C (c : ℚ)) ↔ (∀ r : ℚ, (Polynomial.eval r F) = (c : ℚ)) := by
+  constructor
+  · intro h
+    rintro r
+    refine Iff.mpr (Rat.ext_iff (Polynomial.eval r F) c) ?_
+    simp only [Rat.ofNat_num, Rat.ofNat_den]
+    rw [h]
+    simp
+  · sorry
+
+
+
+
+-- Shifting doesn't change the polynomial type
+lemma Poly_shifting (f : ℤ → ℤ) (g : ℤ → ℤ) (hf : PolyType f d) (s : ℤ) (hfg : ∀ (n : ℤ), f (n + s) = g (n)) : PolyType g d := by
+  simp only [PolyType]
+  rcases hf with ⟨F, hh⟩
+  rcases hh with ⟨N,ss⟩
+  sorry
+
+-- PolyType 0 = constant function
+lemma PolyType_0 (f : ℤ → ℤ) : (PolyType f 0) ↔ (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ), 
+    (N ≤ n → f n = c)) ∧ c ≠ 0) := by
+  constructor
+  · rintro ⟨Poly, ⟨N, ⟨H1, H2⟩⟩⟩ 
+    have this1 : Polynomial.degree Poly = 0 := by rw [← H2]; rfl
+    have this2 : ∃ (c : ℤ), Poly = Polynomial.C (c : ℚ) := by
+      have HH : ∃ (c : ℚ), Poly = Polynomial.C (c : ℚ) := 
+        ⟨Poly.coeff 0, Polynomial.eq_C_of_degree_eq_zero (by rw[← H2]; rfl)⟩
+      cases' HH with c HHH
+      have HHHH : ∃ (d : ℤ), d = c := 
+        ⟨f N, by simp [(Poly_constant Poly c).mp HHH N, H1 N (le_refl N)]⟩
+      cases' HHHH with d H5; exact ⟨d, by rw[← H5] at HHH; exact HHH⟩
+    rcases this2 with ⟨c, hthis2⟩ 
+    use c; use N; intro n
+    constructor
+    · have this4 : Polynomial.eval (n : ℚ) Poly = c := by
+        rw [hthis2]; simp only [map_intCast, Polynomial.eval_int_cast]
+      exact fun HH1 => Iff.mp (Rat.coe_int_inj (f n) c) (by rw [←this4, H1 n HH1])
+    · intro c0
+      simp only [hthis2, c0, Int.cast_zero, map_zero, Polynomial.degree_zero] 
+        at this1
+  · rintro ⟨c, N, hh⟩
+    have H2 : (c : ℚ) ≠ 0 := by simp only [ne_eq, Int.cast_eq_zero]; exact (hh 0).2 
+    exact ⟨Polynomial.C (c : ℚ), N, fun n Nn 
+      => by rw [(hh n).1 Nn]; exact (((Poly_constant (Polynomial.C (c : ℚ)) 
+      (c : ℚ)).mp rfl) n).symm, by rw [Polynomial.degree_C H2]; rfl⟩
+
+-- Δ of 0 times preserves the function
+lemma Δ_0 (f : ℤ → ℤ) : (Δ f 0) = f := by tauto
+
+-- Δ of 1 times decreaes the polynomial type by one
+lemma Δ_1 (f : ℤ → ℤ) (d : ℕ): d > 0 → PolyType f d → PolyType (Δ f 1) (d - 1) := by
+  sorry
+
+-- Δ of d times maps polynomial of degree d to polynomial of degree 0
+lemma Δ_1_s_equiv_Δ_s_1 (f : ℤ → ℤ) (s : ℕ) : Δ (Δ f 1) s = (Δ f (s + 1)) := by
+  sorry
+lemma foofoo (d : ℕ) : (f : ℤ → ℤ) → (PolyType f d) → (PolyType (Δ f d) 0):= by
+  induction' d with d hd
+  · intro f h
+    rw [Δ_0]
+    tauto
+  · intro f hf
+    have this1 : PolyType f (d + 1) := by tauto
+    have this2 : PolyType (Δ f (d + 1)) 0 := by
+      have this3 : PolyType (Δ f 1) d := by
+        have this4 : d + 1 > 0 := by positivity
+        have this5 : (d + 1) > 0 → PolyType f (d + 1) → PolyType (Δ f 1) d := Δ_1 f (d + 1)
+        exact this5 this4 this1
+      clear hf
+      specialize hd (Δ f 1)
+      have this4 : PolyType (Δ (Δ f 1) d) 0 := by tauto
+      rw [Δ_1_s_equiv_Δ_s_1] at this4
+      tauto
+    tauto
+
+lemma Δ_d_PolyType_d_to_PolyType_0 (f : ℤ → ℤ) (d : ℕ): PolyType f d → PolyType (Δ f d) 0 := fun h => (foofoo d f) h
+
+lemma foofoofoo (d : ℕ) : (f : ℤ → ℤ) → (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → (Δ f d) (n) = c) ∧ c ≠ 0) → (PolyType f d)  := by
+  induction' d with d hd
+
+  -- Base case
+  · intro f
+    intro h
+    rcases h with ⟨c, N, hh⟩
+    rw [PolyType_0]
+    use c
+    use N
+    tauto
+
+  -- Induction step
+  · intro f
+    intro h
+    rcases h with ⟨c, N, h⟩
+    have this : PolyType f (d + 1) := by
+      sorry
+    tauto
+
+
+
+-- [BH, 4.1.2] (a) => (b)
+-- Δ^d f (n) = c for some nonzero integer c for n >> 0 → f is of polynomial type d
+lemma a_to_b (f : ℤ → ℤ) (d : ℕ) : (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → (Δ f d) (n) = c) ∧ c ≠ 0) → PolyType f d := by
+  sorry
+  -- intro h
+  -- rcases h with ⟨c, N, hh⟩
+  -- have H1 := λ n => (hh n).left
+  -- have H2 := λ n => (hh n).right
+  -- clear hh
+  -- have H2 : c ≠ 0 := by
+  --   tauto
+  -- induction' d with d hd
+
+  -- -- Base case
+  -- · rw [PolyType_0]
+  --   use c
+  --   use N
+  --   tauto
+
+  -- -- Induction step
+  -- · sorry
+
+-- [BH, 4.1.2] (a) <= (b)
+-- f is of polynomial type d → Δ^d f (n) = c for some nonzero integer c for n >> 0
+lemma b_to_a (f : ℤ → ℤ) (d : ℕ) : PolyType f d → (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → (Δ f d) (n) = c) ∧ c ≠ 0) := by
+  intro h
+  have : PolyType (Δ f d) 0 := by
+    apply Δ_d_PolyType_d_to_PolyType_0
+    exact h
+  have this1 : (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ), (N ≤ n → (Δ f d) n = c)) ∧ c ≠ 0) := by
+    rw [←PolyType_0]
+    exact this
+  exact this1
+end
+
+-- @Additive lemma of length for a SES
+-- Given a SES 0 → A → B → C → 0, then length (A) - length (B) + length (C) = 0 
+section
+open LinearMap
+
+-- Definitiion of the length of a module
+noncomputable def length (R M : Type _) [CommRing R] [AddCommGroup M] [Module R M] := Set.chainHeight {M' : Submodule R M | M' < ⊤}
+#check length ℤ ℤ
+
+-- Definition of a SES (Short Exact Sequence)
+-- @[ext]
+structure SES {R A B C : Type _} [CommRing R] [AddCommGroup A] [AddCommGroup B]
+  [AddCommGroup C] [Module R A] [Module R B] [Module R C] 
+  (f : A →ₗ[R] B) (g : B →ₗ[R] C)
+  where
+  left_exact : LinearMap.ker f = ⊥
+  middle_exact : LinearMap.range f = LinearMap.ker g
+  right_exact : LinearMap.range g = ⊤
+
+-- Additive lemma
+lemma length_Additive (R A B C : Type _) [CommRing R] [AddCommGroup A] [AddCommGroup B] [AddCommGroup C] [Module R A] [Module R B] [Module R C] 
+  (f : A →ₗ[R] B) (g : B →ₗ[R] C)
+  : (SES f g) → ((length R A) + (length R C) = (length R B)) := by
+  intro h
+  rcases h with ⟨left_exact, middle_exact, right_exact⟩
+  sorry
+
+end section

CommAlg/grant2.lean

@@ -54,9 +54,20 @@ def symbolicIdeal(Q : Ideal R) {hin : Q.IsPrime} (I : Ideal R) : Ideal R where
     rw [←mul_assoc, mul_comm s, mul_assoc]
     exact Ideal.mul_mem_left _ _ hs2
 
+
+theorem WF_interval_le_prime (I : Ideal R) (P : Ideal R) [P.IsPrime] 
+  (h : ∀ J ∈ (Set.Icc I P), J.IsPrime → J = P ):
+  WellFounded ((· < ·) : (Set.Icc I P) → (Set.Icc I P) → Prop ) := sorry 
+
 protected lemma LocalRing.height_le_one_of_minimal_over_principle
-  [LocalRing R] (q : PrimeSpectrum R) {x : R} 
+  [LocalRing R] {x : R} 
   (h : (closedPoint R).asIdeal ∈ (Ideal.span {x}).minimalPrimes) :
-  q = closedPoint R ∨ Ideal.height q = 0 := by
+  Ideal.height (closedPoint R) ≤ 1 := by
-  
+  -- by_contra hcont
+  -- push_neg at hcont
+  -- rw [Ideal.lt_height_iff'] at hcont
+  -- rcases hcont with ⟨c, hc1, hc2, hc3⟩
+  apply height_le_of_gt_height_lt
+  intro p hp
+
   sorry

CommAlg/jayden(krull-dim-zero).lean

@@ -16,6 +16,7 @@ import Mathlib.Order.ConditionallyCompleteLattice.Basic
 import Mathlib.Algebra.Ring.Pi
 import Mathlib.RingTheory.Finiteness
 import Mathlib.Util.PiNotation
+import CommAlg.krull
 
 open PiNotation
 
@@ -23,10 +24,10 @@ namespace Ideal
 
 variable (R : Type _) [CommRing R] (P : PrimeSpectrum R)
 
-noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < P}
+-- noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < P}
 
-noncomputable def krullDim (R : Type) [CommRing R] :
+-- noncomputable def krullDim (R : Type) [CommRing R] :
-     WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height R I
+--      WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height R I
 
 --variable {R}
 
@@ -42,7 +43,6 @@ class IsLocallyNilpotent {R : Type _} [CommRing R] (I : Ideal R) : Prop :=
 #check Ideal.IsLocallyNilpotent
 end Ideal
 
-
 -- Repeats the definition of the length of a module by Monalisa
 variable (R : Type _) [CommRing R] (I J : Ideal R)
 variable (M : Type _) [AddCommMonoid M] [Module R M]
@@ -66,9 +66,11 @@ lemma ring_Noetherian_iff_spec_Noetherian : IsNoetherianRing R
     ↔ TopologicalSpace.NoetherianSpace (PrimeSpectrum R) := by
     constructor
     intro RisNoetherian
+    sorry
+    sorry
     -- how do I apply an instance to prove one direction?
 
-
+-- Stacks Lemma 5.9.2: 
 -- Use TopologicalSpace.NoetherianSpace.exists_finset_irreducible :
 -- Every closed subset of a noetherian space is a finite union 
 -- of irreducible closed subsets.
@@ -99,9 +101,9 @@ lemma containment_radical_power_containment :
 
 -- 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] 
+-- lemma length_eq_dim_if_maximal_annihilates {I : Ideal R} [Ideal.IsMaximal I] 
-    : I • (⊤ : Submodule R M) = 0
+--     : I • (⊤ : Submodule R M) = 0
-     → Module.length R M = Module.rank R⧸I M⧸(I • (⊤ : Submodule R M)) := by sorry
+--      → 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?
 -- Use 10.52.5
@@ -125,30 +127,34 @@ lemma Artinian_has_finite_max_ideal
     let m' : ℕ ↪ MaximalSpectrum R := Infinite.natEmbedding (MaximalSpectrum R)
     have m'inj := m'.injective
     let m'' : ℕ → Ideal R := fun n : ℕ ↦ ⨅ k ∈ range n, (m' k).asIdeal
-    let f : ℕ → Ideal R := fun n : ℕ ↦ (m' n).asIdeal
+    -- let f : ℕ → MaximalSpectrum R := fun n : ℕ ↦ m' n
-    let F : Fin n → Ideal R := fun k ↦ (m' k).asIdeal
+    -- let F : (n : ℕ) → Fin n → MaximalSpectrum R := fun n k ↦ m' k
-    have comaximal : ∀ i j : ℕ, i ≠ j → (m' i).asIdeal ⊔ (m' j).asIdeal =
+    have DCC : ∃ n : ℕ, ∀ k : ℕ, n ≤ k → m'' n = m'' k := by
-      (⊤ : Ideal R) := by 
+      apply IsArtinian.monotone_stabilizes {
-      intro i j distinct
+        toFun := m''
-      apply Ideal.IsMaximal.coprime_of_ne
+        monotone' := sorry
-      exact (m' i).IsMaximal
+      }
-      exact (m' j).IsMaximal
+    cases' DCC with n DCCn
-      have : (m' i) ≠ (m' j) := by 
+    specialize DCCn (n+1)
-        exact Function.Injective.ne m'inj distinct
+    specialize DCCn (Nat.le_succ n)
-      intro h
+    have containment1 : m'' n < (m' (n + 1)).asIdeal := by sorry
-      apply this
+    have : ∀ (j : ℕ), (j ≠ n + 1) → ∃ x, x ∈ (m' j).asIdeal ∧ x ∉ (m' (n+1)).asIdeal := by
-      exact MaximalSpectrum.ext _ _ h
+      intro j jnotn
-    have ∀ n : ℕ, (R ⧸ ⨅ (i : Fin n), (F n) i) ≃+* ((i : Fin n) → R ⧸ (F n) i) := by
+      have notcontain : ¬ (m' j).asIdeal ≤ (m' (n+1)).asIdeal := by
+        -- apply Ideal.IsMaximal (m' j).asIdeal
+        sorry
       sorry
-    -- (let F : Fin n → Ideal R := fun k : Fin n ↦ (m' k).asIdeal) 
+    sorry
-    -- let g := Ideal.quotientInfRingEquivPiQuotient f comaximal 
+      -- have distinct : (m' j).asIdeal ≠ (m' (n+1)).asIdeal := by         
-
+      --   intro h
+      --   apply Function.Injective.ne m'inj jnotn
+      --   exact MaximalSpectrum.ext _ _ h      
+      -- simp
+      -- unfold 
+     
 
 -- Stacks Lemma 10.53.4: R Artinian => Jacobson ideal of R is nilpotent
-lemma Jacobson_of_Artinian_is_nilpotent 
+-- This is in mathlib: IsArtinianRing.isNilpotent_jacobson_bot
-    [IsArtinianRing R] : IsNilpotent (Ideal.jacobson (⊥ : Ideal R)) := by 
-    have J := Ideal.jacobson (⊥ : Ideal R)
-    
 
 -- Stacks Lemma 10.53.5: If R has finitely many maximal ideals and 
 -- locally nilpotent Jacobson radical, then R is the product of its localizations at 
@@ -162,7 +168,7 @@ abbrev Prod_of_localization :=
      
 def foo : Prod_of_localization R →+* R where
   toFun := sorry
-  invFun := sorry
+  -- invFun := sorry
   left_inv := sorry
   right_inv := sorry
   map_mul' := sorry
@@ -187,23 +193,27 @@ lemma primes_of_Artinian_are_maximal
 
 -- Lemma: Krull dimension of a ring is the supremum of height of maximal ideals
 
-
 -- Stacks Lemma 10.60.5: R is Artinian iff R is Noetherian of dimension 0
-lemma dim_zero_Noetherian_iff_Artinian (R : Type _) [CommRing R] : 
+lemma dim_le_zero_Noetherian_iff_Artinian (R : Type _) [CommRing R] : 
-    IsNoetherianRing R ∧ Ideal.krullDim R = 0 ↔ IsArtinianRing R := by 
+    IsNoetherianRing R ∧ Ideal.krullDim R ≤ 0 ↔ IsArtinianRing R := by 
     constructor
+    rintro ⟨RisNoetherian, dimzero⟩  
+    rw [ring_Noetherian_iff_spec_Noetherian] at RisNoetherian
+    let Z := irreducibleComponents (PrimeSpectrum R)
+    have Zfinite : Set.Finite Z := by
+      -- apply TopologicalSpace.NoetherianSpace.finite_irreducibleComponents ?_
+      sorry
+    
     sorry
     intro RisArtinian
     constructor
     apply finite_length_is_Noetherian
     rwa [IsArtinian_iff_finite_length] at RisArtinian
-    sorry -- can use Grant's lemma dim_eq_zero_iff
+    rw [Ideal.dim_le_zero_iff]
-
+    intro I
-
+    apply primes_of_Artinian_are_maximal
-
-
-    
 
+-- Use TopologicalSpace.NoetherianSpace.exists_finset_irreducible :
 
 
 

CommAlg/krull.lean

@@ -125,8 +125,32 @@ lemma le_krullDim_iff (R : Type _) [CommRing R] (n : ℕ) :
     have : height I ≤ krullDim R := by apply height_le_krullDim
     exact le_trans h this
 
-lemma le_krullDim_iff' (R : Type _) [CommRing R] (n : ℕ∞) :
+#check ENat.recTopCoe
-  n ≤ krullDim R ↔ ∃ I : PrimeSpectrum R, n ≤ (height I : WithBot ℕ∞) := by sorry
+
+/- terrible place for this lemma. Also this probably exists somewhere
+  Also this is a terrible proof
+-/
+lemma eq_top_iff (n : WithBot ℕ∞) : n = ⊤ ↔ ∀ m : ℕ, m ≤ n := by
+  aesop
+  induction' n using WithBot.recBotCoe with n
+  . exfalso
+    have := (a 0)
+    simp [not_lt_of_ge] at this
+  induction' n using ENat.recTopCoe with n
+  . rfl
+  . have := a (n + 1)
+    exfalso
+    change (((n + 1) : ℕ∞) : WithBot ℕ∞) ≤ _ at this
+    simp [WithBot.coe_le_coe] at this
+    change ((n + 1) : ℕ∞) ≤ (n : ℕ∞) at this
+    simp [ENat.add_one_le_iff] at this
+
+lemma krullDim_eq_top_iff (R : Type _) [CommRing R] :
+  krullDim R = ⊤ ↔ ∀ (n : ℕ), ∃ I : PrimeSpectrum R, n ≤ height I := by
+  simp [eq_top_iff, le_krullDim_iff]
+  change (∀ (m : ℕ), ∃ I, ((m : ℕ∞) : WithBot ℕ∞) ≤ height I) ↔ _
+  simp [WithBot.coe_le_coe]
+  
 
 /-- The Krull dimension of a local ring is the height of its maximal ideal. -/
 lemma krullDim_eq_height [LocalRing R] : krullDim R = height (closedPoint R) := by
@@ -142,31 +166,32 @@ lemma krullDim_eq_height [LocalRing R] : krullDim R = height (closedPoint R) :=
 /-- The height of a prime `𝔭` is greater than `n` if and only if there is a chain of primes less than `𝔭`
   with length `n + 1`. -/
 lemma lt_height_iff' {𝔭 : PrimeSpectrum R} {n : ℕ∞} : 
-height 𝔭 > n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by
+n < height 𝔭 ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by
-  rcases n with _ | n
+  match n with
-  . constructor <;> intro h <;> exfalso
+  | ⊤ =>  
+    constructor <;> intro h <;> exfalso
     . exact (not_le.mpr h) le_top
     . tauto
-  have (m : ℕ∞) : m > some n ↔ m ≥ some (n + 1) := by
+  | (n : ℕ) => 
-    symm
+    have (m : ℕ∞) : n < m ↔ (n + 1 : ℕ∞) ≤ m := by
-    show (n + 1 ≤ m ↔ _ )
+      symm
-    apply ENat.add_one_le_iff
+      show (n + 1 ≤ m ↔ _ )
-    exact ENat.coe_ne_top _
+      apply ENat.add_one_le_iff
-  rw [this]
+      exact ENat.coe_ne_top _
-  unfold Ideal.height
+    rw [this]
-  show ((↑(n + 1):ℕ∞) ≤ _) ↔ ∃c, _ ∧ _ ∧ ((_ : WithTop ℕ) = (_:ℕ∞))
+    unfold Ideal.height
-  rw [{J | J < 𝔭}.le_chainHeight_iff]
+    show ((↑(n + 1):ℕ∞) ≤ _) ↔ ∃c, _ ∧ _ ∧ ((_ : WithTop ℕ) = (_:ℕ∞))
-  show (∃ c, (List.Chain' _ c ∧ ∀𝔮, 𝔮 ∈ c → 𝔮 < 𝔭) ∧ _) ↔ _
+    rw [{J | J < 𝔭}.le_chainHeight_iff]
-  constructor <;> rintro ⟨c, hc⟩ <;> use c
+    show (∃ c, (List.Chain' _ c ∧ ∀𝔮, 𝔮 ∈ c → 𝔮 < 𝔭) ∧ _) ↔ _
-  . tauto
+    constructor <;> rintro ⟨c, hc⟩ <;> use c
-  . change _ ∧ _ ∧ (List.length c : ℕ∞) = n + 1 at hc
+    . tauto
-    norm_cast at hc
+    . change _ ∧ _ ∧ (List.length c : ℕ∞) = n + 1 at hc
-    tauto
+      norm_cast at hc
+      tauto
 
 /-- Form of `lt_height_iff''` for rewriting with the height coerced to `WithBot ℕ∞`. -/
 lemma lt_height_iff'' {𝔭 : PrimeSpectrum R} {n : ℕ∞} : 
-height 𝔭 > (n : WithBot ℕ∞) ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by
+(n : WithBot ℕ∞) < height 𝔭 ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by
-  show (_ < _) ↔ _
   rw [WithBot.coe_lt_coe]
   exact lt_height_iff'
 
@@ -228,7 +253,7 @@ lemma dim_le_zero_iff : krullDim R ≤ 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal
       rw [hcontr] at h
       exact h h𝔪.1
     use 𝔪p
-    show (_ : WithBot ℕ∞) > (0 : ℕ∞)
+    show (0 : ℕ∞) < (_ : WithBot ℕ∞) 
     rw [lt_height_iff'']
     use [I]
     constructor
@@ -239,7 +264,7 @@ lemma dim_le_zero_iff : krullDim R ≤ 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal
         rwa [hI']
       . simp only [List.length_singleton, Nat.cast_one, zero_add]
   . contrapose! h
-    change (_ : WithBot ℕ∞) > (0 : ℕ∞) at h
+    change (0 : ℕ∞) < (_ : WithBot ℕ∞) at h
     rw [lt_height_iff''] at h
     obtain ⟨c, _, hc2, hc3⟩ := h
     norm_cast at hc3

CommAlg/polynomial.lean

@@ -0,0 +1,167 @@
+import Mathlib.RingTheory.Ideal.Operations
+import Mathlib.RingTheory.FiniteType
+import Mathlib.Order.Height
+import Mathlib.RingTheory.Polynomial.Quotient
+import Mathlib.RingTheory.PrincipalIdealDomain
+import Mathlib.RingTheory.DedekindDomain.Basic
+import Mathlib.RingTheory.Ideal.Quotient
+import Mathlib.RingTheory.Localization.AtPrime
+import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
+import Mathlib.Order.ConditionallyCompleteLattice.Basic
+import CommAlg.krull
+
+section ChainLemma
+variable {α β : Type _}
+variable [LT α] [LT β] (s t : Set α)
+
+namespace Set
+open List
+
+/-
+Sorry for using aesop, but it doesn't take that long
+-/
+theorem append_mem_subchain_iff :
+l ++ l' ∈ s.subchain ↔ l ∈ s.subchain ∧ l' ∈ s.subchain ∧ ∀ a ∈ l.getLast?, ∀ b ∈ l'.head?, a < b := by
+  simp [subchain, chain'_append]
+  aesop
+
+end Set
+end ChainLemma
+
+variable {R : Type _} [CommRing R]
+open Ideal Polynomial
+
+namespace Polynomial
+/-
+The composition R → R[X] → R is the identity
+-/
+theorem coeff_C_eq : RingHom.comp constantCoeff C = RingHom.id R := by ext; simp
+
+end Polynomial
+
+/-
+Given an ideal I in R, we define the ideal adjoin_x' I to be the kernel
+of R[X] → R → R/I
+-/
+def adj_x_map (I : Ideal R) : R[X] →+* R ⧸ I := (Ideal.Quotient.mk I).comp constantCoeff
+def adjoin_x' (I : Ideal R) : Ideal (Polynomial R) := RingHom.ker (adj_x_map I)
+def adjoin_x (I : PrimeSpectrum R) : PrimeSpectrum (Polynomial R) where
+  asIdeal := adjoin_x' I.asIdeal
+  IsPrime := RingHom.ker_isPrime _
+
+@[simp]
+lemma adj_x_comp_C (I : Ideal R) : RingHom.comp (adj_x_map I) C = Ideal.Quotient.mk I := by
+  ext x; simp [adj_x_map]
+
+lemma adjoin_x_eq (I : Ideal R) : adjoin_x' I = I.map C ⊔ Ideal.span {X} := by
+  apply le_antisymm
+  . rintro p hp
+    have h : ∃ q r, p = C r + X * q := ⟨p.divX, p.coeff 0, p.divX_mul_X_add.symm.trans $ by ring⟩
+    obtain ⟨q, r, rfl⟩ := h
+    suffices : r ∈ I
+    . simp only [Submodule.mem_sup, Ideal.mem_span_singleton]
+      refine' ⟨C r, Ideal.mem_map_of_mem C this, X * q, ⟨q, rfl⟩, rfl⟩
+    rw [adjoin_x', adj_x_map, RingHom.mem_ker, RingHom.comp_apply] at hp
+    rw [constantCoeff_apply, coeff_add, coeff_C_zero, coeff_X_mul_zero, add_zero] at hp
+    rwa  [←RingHom.mem_ker, Ideal.mk_ker] at hp
+  . rw [sup_le_iff]
+    constructor
+    . simp [adjoin_x', RingHom.ker, ←map_le_iff_le_comap, Ideal.map_map]
+    . simp [span_le, adjoin_x', RingHom.mem_ker, adj_x_map]
+
+/-
+If I is prime in R, the pushforward I*R[X] is prime in R[X]
+-/
+def map_prime (I : PrimeSpectrum R) : PrimeSpectrum R[X] :=
+  ⟨I.asIdeal.map C, isPrime_map_C_of_isPrime I.IsPrime⟩
+
+/-
+The pushforward map (Ideal R) → (Ideal R[X]) is injective
+-/
+lemma map_inj {I J : Ideal R} (h : I.map C = J.map C) : I = J := by
+  have H : map constantCoeff (I.map C) = map constantCoeff (J.map C) := by rw [h]
+  simp [Ideal.map_map, coeff_C_eq] at H
+  exact H
+
+/-
+The pushforward map (Ideal R) → (Ideal R[X]) is strictly monotone
+-/
+lemma map_strictmono {I J : Ideal R} (h : I < J) : I.map C < J.map C := by
+  rw [lt_iff_le_and_ne] at h ⊢
+  exact ⟨map_mono h.1, fun H => h.2 (map_inj H)⟩
+
+lemma map_lt_adjoin_x (I : PrimeSpectrum R) : map_prime I < adjoin_x I := by
+  simp [adjoin_x, adjoin_x_eq]
+  show I.asIdeal.map C  < I.asIdeal.map C ⊔ span {X}
+  simp [Ideal.span_le, mem_map_C_iff]
+  use 1
+  simp
+  rw [←Ideal.eq_top_iff_one]
+  exact I.IsPrime.ne_top'
+
+lemma ht_adjoin_x_eq_ht_add_one [Nontrivial R] (I : PrimeSpectrum R) : height I + 1 ≤ height (adjoin_x I) := by
+  suffices H : height I + (1 : ℕ) ≤ height (adjoin_x I) + (0 : ℕ)
+  . norm_cast at H; rw [add_zero] at H; exact H
+  rw [height, height, Set.chainHeight_add_le_chainHeight_add {J | J < I} _ 1 0]
+  intro l hl
+  use ((l.map map_prime) ++ [map_prime I])
+  refine' ⟨_, by simp⟩
+  . simp [Set.append_mem_subchain_iff]
+    refine' ⟨_, map_lt_adjoin_x I, fun a ha => _⟩
+    . refine' ⟨_, fun i hi => _⟩
+      . apply List.chain'_map_of_chain' map_prime (fun a b hab => map_strictmono hab) hl.1
+      . rw [List.mem_map] at hi
+        obtain ⟨a, ha, rfl⟩ := hi
+        calc map_prime a < map_prime I := by apply map_strictmono; apply hl.2; apply ha
+          _ < adjoin_x I := by apply map_lt_adjoin_x
+    . have H : ∃ b : PrimeSpectrum R, b ∈ l ∧ map_prime b = a
+      . have H2 : l ≠ []
+        . intro h
+          rw [h] at ha
+          tauto
+        use l.getLast H2
+        refine' ⟨List.getLast_mem H2, _⟩
+        have H3 : l.map map_prime ≠ []
+        . intro hl
+          apply H2
+          apply List.eq_nil_of_map_eq_nil hl
+        rw [List.getLast?_eq_getLast _ H3, Option.some_inj] at ha
+        simp [←ha, List.getLast_map _ H2]
+      obtain ⟨b, hb, rfl⟩ := H
+      apply map_strictmono
+      apply hl.2
+      exact hb
+
+#check (⊤ : ℕ∞)
+/-
+dim R + 1 ≤ dim R[X]
+-/
+lemma dim_le_dim_polynomial_add_one [Nontrivial R] :
+  krullDim R + (1 : ℕ∞) ≤ krullDim R[X] := by
+  obtain ⟨n, hn⟩ := krullDim_nonneg_of_nontrivial R
+  rw [hn]
+  change ↑(n + 1) ≤ krullDim R[X]
+  have := le_of_eq hn.symm
+  induction' n using ENat.recTopCoe with n
+  . change krullDim R = ⊤ at hn
+    change ⊤ ≤ krullDim R[X] 
+    rw [krullDim_eq_top_iff] at hn
+    rw [top_le_iff, krullDim_eq_top_iff]
+    intro n
+    obtain ⟨I, hI⟩ := hn n
+    use adjoin_x I
+    calc n ≤ height I := hI
+      _ ≤ height I + 1 := le_self_add
+      _ ≤ height (adjoin_x I) := ht_adjoin_x_eq_ht_add_one I
+  change n ≤ krullDim R at this
+  change (n + 1 : ℕ) ≤ krullDim R[X]
+  rw [le_krullDim_iff] at this ⊢
+  obtain ⟨I, hI⟩ := this
+  use adjoin_x I
+  apply WithBot.coe_mono
+  calc n + 1 ≤ height I + 1 := by
+        apply add_le_add_right
+        change ((n : ℕ∞) : WithBot ℕ∞) ≤ (height I) at hI
+        rw [WithBot.coe_le_coe] at hI
+        exact hI
+    _ ≤ height (adjoin_x I) := ht_adjoin_x_eq_ht_add_one I