Merge branch 'main' of github.com:GTBarkley/comm_alg into main

CommAlg/final_poly_type.lean

@@ -5,7 +5,7 @@ import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
 set_option maxHeartbeats 0
 macro "ls" : tactic => `(tactic|library_search)
 
--- New tactic "obviously"
+-- From Kyle : New tactic "obviously"
 macro "obviously" : tactic =>
   `(tactic| (
       first
@@ -15,6 +15,7 @@ macro "obviously" : tactic =>
         | 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"
+        | norm_cast; done; dbg_trace "it was norm_cast"
         | /-change (@Eq ℝ _ _);-/ linarith; done; dbg_trace "it was linarith"
         -- | gcongr; done
         | ring; done; dbg_trace "it was ring"
@@ -40,7 +41,7 @@ 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
+  simp [simp]
 
 -- Treat polynomial f ∈ ℚ[X] as a function f : ℚ → ℚ
 
@@ -50,11 +51,11 @@ end section
 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
+def PolyType (f : ℤ → ℤ) (d : ℕ) := 
+  ∃ Poly : Polynomial ℚ, ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → f n = Polynomial.eval (n : ℚ) Poly) ∧ 
+    d = Polynomial.degree Poly
 section
 
-#check PolyType
-
 example (f : ℤ → ℤ) (hf : ∀ x, f x = x ^ 2) : PolyType f 2 := by
   unfold PolyType
   sorry
@@ -69,14 +70,12 @@ def Δ : (ℤ → ℤ) → ℕ → (ℤ → ℤ)
 
 -- (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
+    (F = Polynomial.C (c : ℚ)) ↔ (∀ r : ℚ, (Polynomial.eval r F) = (c : ℚ)) := by
   constructor
-  · intro h
-    rintro r
+  · intro h r
     refine Iff.mpr (Rat.ext_iff (Polynomial.eval r F) c) ?_
     simp only [Rat.ofNat_num, Rat.ofNat_den]
-    rw [h]
-    simp
+    simp [h]
   · sorry
 
 -- Get the polynomial G (X) = F (X + s) from the polynomial F(X)
@@ -84,22 +83,15 @@ lemma Polynomial_shifting (F : Polynomial ℚ) (s : ℚ) : ∃ (G : Polynomial
   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,s1, s2⟩
-  have this : ∃ (G : Polynomial ℚ), (∀ (x : ℚ), Polynomial.eval x G = Polynomial.eval (x + s) F) ∧ (Polynomial.degree G = Polynomial.degree F) := by
-    exact Polynomial_shifting F s
-  rcases this with ⟨Poly, h1, h2⟩
-  use Poly
-  use N
-  constructor
-  · intro n
-    specialize s1 (n + s)
-    intro hN
-    have this1 : f (n + s) = Polynomial.eval (n + s : ℚ) F := by
-      sorry
-    sorry
+lemma Poly_shifting (f : ℤ → ℤ) (g : ℤ → ℤ) (hf : PolyType f d) (s : ℕ) 
+    (hfg : ∀ (n : ℤ), f (n + s) = g (n)) : PolyType g d := by
+  rcases hf with ⟨F, ⟨N, s1, s2⟩⟩
+  rcases (Polynomial_shifting F s) with ⟨Poly, h1, h2⟩
+  use Poly, N; constructor
+  · intro n hN
+    have this1 : f (n + s) = Polynomial.eval (n + (s : ℚ)) F := by
+      rw [s1 (n + s) (by linarith)]; norm_cast
+    rw [←hfg n, this1]; exact (h1 n).symm
   · rw [h2, s2]
 
 -- PolyType 0 = constant function
@@ -132,8 +124,8 @@ lemma PolyType_0 (f : ℤ → ℤ) : (PolyType f 0) ↔ (∃ (c : ℤ), ∃ (N :
 
 -- Δ of 0 times preserves the function
 lemma Δ_0 (f : ℤ → ℤ) : (Δ f 0) = f := by rfl
-  --simp only [Δ]
--- Δ of 1 times decreaes the polynomial type by one
+
+-- Δ of 1 times decreaes the polynomial type by one --can be golfed
 lemma Δ_1 (f : ℤ → ℤ) (d : ℕ) : PolyType f (d + 1) → PolyType (Δ f 1) d := by
   intro h
   simp only [PolyType, Δ, Int.cast_sub, exists_and_right]
@@ -186,53 +178,21 @@ lemma Δ_d_PolyType_d_to_PolyType_0 (f : ℤ → ℤ) (d : ℕ): PolyType f d
 
 -- The "reverse" of Δ of 1 times increases the polynomial type by one
 lemma Δ_1_ (f : ℤ → ℤ) (d : ℕ) : PolyType (Δ f 1) d → PolyType f (d + 1) := by
-  intro h
+  rintro ⟨P, N, ⟨h1, h2⟩⟩ 
   simp only [PolyType, Nat.cast_add, Nat.cast_one, exists_and_right]
-  rcases h with ⟨P, N, h⟩
-  rcases h with ⟨h1, h2⟩
   let G := fun (q : ℤ) => f (N)
   sorry
 
-
-lemma foo (d : ℕ) : (f : ℤ → ℤ) → (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → (Δ f d) (n) = c) ∧ c ≠ 0) → (PolyType f d)  := by
+lemma foo (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
-      rcases h with ⟨H,c0⟩
-      let g := (Δ f 1)
-      have this1 : (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → (Δ g d) (n) = c) ∧ c ≠ 0) := by
-        use c; use N
-        constructor
-        · intro n
-          specialize H n
-          intro h
-          have this : Δ f (d + 1) n = c := by tauto
-          rw [←this]
-          rw [Δ_1_s_equiv_Δ_s_1] 
-        · tauto 
-      have this2 : PolyType g d := by
-        apply hd
-        tauto
-      exact Δ_1_ f d this2
-    exact this
+  · rintro f ⟨c, N, hh⟩; rw [PolyType_0 f]; exact ⟨c, N, hh⟩
+  · exact fun f ⟨c, N, ⟨H, c0⟩⟩ =>
+      Δ_1_ f d (hd (Δ f 1) ⟨c, N, fun n h => by rw [← H n h, Δ_1_s_equiv_Δ_s_1], c0⟩)
 
 -- [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
+lemma a_to_b (f : ℤ → ℤ) (d : ℕ) : (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → (Δ f d) (n) = c) ∧ c ≠ 0) → PolyType f d := fun h => (foo d f) h
 
 -- [BH, 4.1.2] (a) <= (b)
 -- f is of polynomial type d → Δ^d f (n) = c for some nonzero integer c for n >> 0
@@ -241,6 +201,7 @@ lemma b_to_a (f : ℤ → ℤ) (d : ℕ) (poly : PolyType f d) :
   rw [←PolyType_0]; exact Δ_d_PolyType_d_to_PolyType_0 f d poly
 
 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

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 Mathlib.RingTheory.Ideal.MinimalPrime
 import CommAlg.krull
 
 open PiNotation
@@ -43,6 +44,8 @@ class IsLocallyNilpotent {R : Type _} [CommRing R] (I : Ideal R) : Prop :=
 #check Ideal.IsLocallyNilpotent
 end Ideal
 
+def RingJacobson (R) [Ring R] := Ideal.jacobson (⊥ : Ideal R)
+
 -- 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]
@@ -169,15 +172,15 @@ abbrev Prod_of_localization :=
 def foo : Prod_of_localization R →+* R where
   toFun := sorry
   -- invFun := sorry
-  left_inv := sorry
-  right_inv := sorry
+  --left_inv := sorry
+  --right_inv := sorry
   map_mul' := sorry
   map_add' := sorry
 
 
 def product_of_localization_at_maximal_ideal [Finite (MaximalSpectrum R)]
-    (h : Ideal.IsLocallyNilpotent (Ideal.jacobson (⊥ : Ideal R))) :
-    Prod_of_localization R ≃+* R := by sorry
+    (h : Ideal.IsLocallyNilpotent (RingJacobson R)) :
+    R ≃+* Prod_of_localization R := by sorry
 
 -- Stacks Lemma 10.53.6: R is Artinian iff R has finite length as an R-mod
 lemma IsArtinian_iff_finite_length : 
@@ -193,18 +196,61 @@ 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_le_zero_Noetherian_iff_Artinian (R : Type _) [CommRing R] : 
-    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 ?_
+-- Lemma: X is an irreducible component of Spec(R) ↔ X = V(I) for I a minimal prime
+lemma irred_comp_minmimal_prime (X) : 
+    X ∈ irreducibleComponents (PrimeSpectrum R) 
+      ↔ ∃ (P : minimalPrimes R), X = PrimeSpectrum.zeroLocus P := by
       sorry
 
-    sorry
+-- Lemma: localization of Noetherian ring is Noetherian
+-- lemma localization_of_Noetherian_at_prime [IsNoetherianRing R]
+--      (atprime: Ideal.IsPrime I) :
+--     IsNoetherianRing (Localization.AtPrime I) := by sorry
+
+
+-- Stacks Lemma 10.60.5: R is Artinian iff R is Noetherian of dimension 0
+lemma Artinian_if_dim_le_zero_Noetherian (R : Type _) [CommRing R] : 
+    IsNoetherianRing R ∧ Ideal.krullDim R ≤ 0 → IsArtinianRing R := by
+    rintro ⟨RisNoetherian, dimzero⟩  
+    rw [ring_Noetherian_iff_spec_Noetherian] at RisNoetherian
+    have := fun X => (irred_comp_minmimal_prime R X).mp
+    choose F hf using this
+    let Z := irreducibleComponents (PrimeSpectrum R)
+    -- have Zfinite : Set.Finite Z := by
+      -- apply TopologicalSpace.NoetherianSpace.finite_irreducibleComponents ?_
+      -- sorry
+    --let P := fun 
+    rw [← ring_Noetherian_iff_spec_Noetherian] at RisNoetherian
+    have PrimeIsMaximal : ∀ X : Z, Ideal.IsMaximal (F X X.2).1 := by
+      intro X
+      have prime : Ideal.IsPrime (F X X.2).1 := (F X X.2).2.1.1
+      rw [Ideal.dim_le_zero_iff] at dimzero
+      exact dimzero ⟨_, prime⟩
+    have JacLocallyNil : Ideal.IsLocallyNilpotent (RingJacobson R) := by sorry 
+    let Loc := fun X : Z ↦ Localization.AtPrime (F X.1 X.2).1 
+    have LocNoetherian : ∀ X, IsNoetherianRing (Loc X) := by 
+      intro X
+      sorry
+      -- apply IsLocalization.isNoetherianRing (F X.1 X.2).1 (Loc X) RisNoetherian
+    have Locdimzero : ∀ X, Ideal.krullDim (Loc X) ≤ 0 := by sorry
+    have powerannihilates : ∀ X, ∃ n : ℕ, 
+      ((F X.1 X.2).1) ^ n • (⊤: Submodule R (Loc X)) = 0 := by sorry
+    have LocFinitelength : ∀ X, ∃ n : ℕ, Module.length R (Loc X) ≤ n := by
+      intro X
+      have idealfg : Ideal.FG (F X.1 X.2).1 := by
+        rw [isNoetherianRing_iff_ideal_fg] at RisNoetherian
+        specialize RisNoetherian (F X.1 X.2).1
+        exact RisNoetherian
+      have modulefg : Module.Finite R (Loc X) := by sorry -- not sure if this is true
+      specialize PrimeIsMaximal X
+      specialize powerannihilates X
+      apply power_zero_finite_length R (F X.1 X.2).1 (Loc X) idealfg powerannihilates
+    have RingFinitelength : ∃ n : ℕ, Module.length R R ≤ n := by sorry
+    rw [IsArtinian_iff_finite_length]
+    exact RingFinitelength
+
+lemma dim_le_zero_Noetherian_if_Artinian (R : Type _) [CommRing R] : 
+    IsArtinianRing R → IsNoetherianRing R ∧ Ideal.krullDim R ≤ 0 := by 
     intro RisArtinian
     constructor
     apply finite_length_is_Noetherian
@@ -213,7 +259,6 @@ lemma dim_le_zero_Noetherian_iff_Artinian (R : Type _) [CommRing R] :
     intro I
     apply primes_of_Artinian_are_maximal
 
--- Use TopologicalSpace.NoetherianSpace.exists_finset_irreducible :