diff --git a/CommAlg/final_hil_pol.lean b/CommAlg/final_hil_pol.lean
new file mode 100644
index 0000000..591c6cc
--- /dev/null
+++ b/CommAlg/final_hil_pol.lean
@@ -0,0 +1,258 @@
+import Mathlib.Order.KrullDimension
+import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
+import Mathlib.Algebra.Module.GradedModule
+import Mathlib.RingTheory.Ideal.AssociatedPrime
+import Mathlib.RingTheory.Artinian
+import Mathlib.Order.Height
+
+
+
+-- 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."))
+
+
+
+open GradedMonoid.GSmul
+open DirectSum
+
+
+
+-- @Definitions (to be classified)
+section
+
+-- Definition of polynomail of type d 
+def PolyType (f : ℤ → ℤ) (d : ℕ) := ∃ Poly : Polynomial ℚ, ∃ (N : ℤ), ∀ (n : ℤ), N ≤ n → f n = Polynomial.eval (n : ℚ) Poly ∧ d = Polynomial.degree Poly
+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 𝒜]
+  [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)
+
+lemma mylem (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)]  [DirectSum.GCommRing 𝒜]
+  [h : DirectSum.Gmodule 𝒜 𝓜] (i : ℤ) (a : 𝒜 0) (m : 𝓜 i) :
+  of _ _ (a • m) = of _ _ a • of _ _ m := by
+  refine' Eq.trans _ (Gmodule.of_smul_of 𝒜 𝓜 a m).symm
+  refine' of_eq_of_gradedMonoid_eq _
+  exact Sigma.ext (zero_add _).symm <| eq_rec_heq _ _
+
+instance tada2 (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)]  [DirectSum.GCommRing 𝒜]
+  [h : DirectSum.Gmodule 𝒜 𝓜] (i : ℤ ) : SMulWithZero (𝒜 0) (𝓜 i) := by
+  letI := SMulWithZero.compHom (⨁ i, 𝓜 i) (of 𝒜 0).toZeroHom
+  exact Function.Injective.smulWithZero (of 𝓜 i).toZeroHom Dfinsupp.single_injective (mylem 𝒜 𝓜 i)
+
+instance tada3 (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)]  [DirectSum.GCommRing 𝒜]
+  [h : DirectSum.Gmodule 𝒜 𝓜] (i : ℤ ): Module (𝒜 0) (𝓜 i) := by
+  letI := Module.compHom (⨁ j, 𝓜 j) (ofZeroRingHom 𝒜)
+  exact Dfinsupp.single_injective.module (𝒜 0) (of 𝓜 i) (mylem 𝒜 𝓜 i)
+
+
+-- Definition of a Hilbert function of a graded module
+section
+noncomputable def hilbert_function (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)]
+  [DirectSum.GCommRing 𝒜]
+  [DirectSum.Gmodule 𝒜 𝓜] (hilb : ℤ → ℤ) := ∀ i, hilb i = (ENat.toNat (length (𝒜 0) (𝓜 i)))
+
+noncomputable def dimensionring { A: Type _}
+ [CommRing A] := krullDim (PrimeSpectrum A)
+
+noncomputable def dimensionmodule ( A : Type _) (M : Type _)
+ [CommRing A] [AddCommGroup M] [Module A M] := krullDim (PrimeSpectrum (A ⧸ ((⊤ : Submodule A M).annihilator)) )
+end
+
+
+
+-- Definition of homogeneous ideal
+def Ideal.IsHomogeneous' (𝒜 : ℤ → Type _) 
+[∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜] 
+(I : Ideal (⨁ i, 𝒜 i)) := ∀ (i : ℤ ) 
+⦃r : (⨁ i, 𝒜 i)⦄, r ∈ I → DirectSum.of _ i ( r i : 𝒜 i) ∈ I
+
+-- Definition of homogeneous prime ideal
+def HomogeneousPrime (𝒜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜] (I : Ideal (⨁ i, 𝒜 i)):= (Ideal.IsPrime I) ∧ (Ideal.IsHomogeneous' 𝒜 I)
+
+-- Definition of homogeneous maximal ideal
+def HomogeneousMax (𝒜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜] (I : Ideal (⨁ i, 𝒜 i)):= (Ideal.IsMaximal I) ∧ (Ideal.IsHomogeneous' 𝒜 I)
+
+--theorem monotone_stabilizes_iff_noetherian :
+-- (∀ f : ℕ →o Submodule R M, ∃ n, ∀ m, n ≤ m → f n = f m) ↔ IsNoetherian R M := by
+-- rw [isNoetherian_iff_wellFounded, WellFounded.monotone_chain_condition]
+
+
+instance {𝒜 : ℤ → Type _} [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜] :
+    Algebra (𝒜 0) (⨁ i, 𝒜 i) :=
+  Algebra.ofModule'
+  (by
+    intro r x
+    sorry)
+  (by
+    intro r x
+    sorry)
+
+
+
+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))
+
+
+-- Each component of a graded ring is an additive subgroup
+def Component_of_graded_as_addsubgroup (𝒜 : ℤ → Type _) 
+[∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜]
+(p : Ideal (⨁ i, 𝒜 i)) (hp : Ideal.IsHomogeneous' 𝒜 p) (i : ℤ) : AddSubgroup (𝒜 i) := by
+  sorry
+
+
+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
+
+
+def graded_submodule
+(𝒜 : ℤ → Type _) (𝓜 : ℤ → Type u) (𝓝 : ℤ → Type u)
+[∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] [∀ i, AddCommGroup (𝓝 i)]
+[DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜][DirectSum.Gmodule 𝒜 𝓝]
+(opn : Submodule (⨁ i, 𝒜 i) (⨁ i, 𝓜 i)) (opnis : opn = (⨁ i, 𝓝 i)) (i : ℤ )
+ : ∃(piece : Submodule (𝒜 0) (𝓜 i)), piece = 𝓝 i := by
+  sorry
+
+
+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 𝒜]
+(p : Ideal (⨁ i, 𝒜 i)) (hp : Ideal.IsHomogeneous' 𝒜 p)
+  : DirectSum.Gmodule 𝒜 (fun i => (𝒜 i)⧸(Component_of_graded_as_addsubgroup 𝒜 p hp i)) := 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 _) 
+[∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)]
+[DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜] (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0)) : ∃ ( I : Ideal ((⨁ i, 𝒜 i))),(HomogeneousMax 𝒜 I) := by
+  sorry
+
+
+-- @Existence of a chain of submodules of graded submoduels of a f.g graded R-mod M
+lemma Exist_chain_of_graded_submodules (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) 
+[∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)]
+  [DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜] 
+  (fingen : IsNoetherian (⨁ i, 𝒜 i) (⨁ i, 𝓜 i))
+  : ∃ (c : List (Submodule (⨁ i, 𝒜 i) (⨁ i, 𝓜 i))), c.Chain' (· < ·) ∧ ∀ M ∈ c, Ture := by
+  sorry
+
+
+-- @[BH, 1.5.6 (b)(ii)]
+-- An associated prime of a graded R-Mod M is graded
+lemma Associated_prime_of_graded_is_graded
+(𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) 
+[∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)]
+[DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜]
+(p : associatedPrimes (⨁ i, 𝒜 i) (⨁ i, 𝓜 i))
+  : (Ideal.IsHomogeneous' 𝒜 p) ∧ ((∃ (i : ℤ ), ∃ (x :  𝒜 i), p = (Submodule.span (⨁ i, 𝒜 i) {DirectSum.of _ i x}).annihilator)) := by
+  sorry
+
+
+
+
+
+
+
+
+
+-- @[BH, 4.1.3] when d ≥ 1
+-- 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)) 
+(fingen : IsNoetherian (⨁ i, 𝒜 i) (⨁ i, 𝓜 i))
+(findim :  dimensionmodule (⨁ i, 𝒜 i) (⨁ i, 𝓜 i) = d)
+(hilb : ℤ → ℤ) (Hhilb: hilbert_function 𝒜 𝓜 hilb)
+: PolyType hilb (d - 1) := by
+  sorry
+
+
+-- (reduced version) [BH, 4.1.3] when d ≥ 1
+-- If M is a finite graed R-Mod of dimension d ≥ 1, and M = R⧸ 𝓅 for a graded prime ideal 𝓅, then the Hilbert function H(M, n) is of polynomial type (d - 1)
+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))
+(fingen : IsNoetherian (⨁ i, 𝒜 i) (⨁ i, 𝓜 i))
+(findim :  dimensionmodule (⨁ i, 𝒜 i) (⨁ i, 𝓜 i) = d)
+(hilb : ℤ → ℤ) (Hhilb: hilbert_function 𝒜 𝓜 hilb)
+(p : Ideal (⨁ i, 𝒜 i)) (hp : Ideal.IsHomogeneous' 𝒜 p)
+(hm : 𝓜 = (fun i => (𝒜 i)⧸(Component_of_graded_as_addsubgroup 𝒜 p hp i)))
+: PolyType hilb (d - 1) := by
+  sorry
+
+
+-- @[BH, 4.1.3] when d = 0
+-- 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)) 
+(fingen : IsNoetherian (⨁ i, 𝒜 i) (⨁ i, 𝓜 i))
+(findim :  dimensionmodule (⨁ i, 𝒜 i) (⨁ i, 𝓜 i) = 0)
+(hilb : ℤ → ℤ) (Hhilb : hilbert_function 𝒜 𝓜 hilb)
+: (∃ (N : ℤ), ∀ (n : ℤ), n ≥ N → hilb n = 0) := by
+  sorry
+
+
+-- (reduced version) [BH, 4.1.3] when d = 0
+-- If M is a finite graed R-Mod of dimension zero, and M = R⧸ 𝓅 for a graded prime ideal 𝓅, then the Hilbert function H(M, n) = 0 for n >> 0 
+theorem Hilbert_polynomial_d_0_reduced
+(𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)]
+[DirectSum.GCommRing 𝒜]
+[DirectSum.Gmodule 𝒜 𝓜] (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0)) 
+(fingen : IsNoetherian (⨁ i, 𝒜 i) (⨁ i, 𝓜 i))
+(findim :  dimensionmodule (⨁ i, 𝒜 i) (⨁ i, 𝓜 i) = 0)
+(hilb : ℤ → ℤ) (Hhilb : hilbert_function 𝒜 𝓜 hilb)
+(p : Ideal (⨁ i, 𝒜 i)) (hp : Ideal.IsHomogeneous' 𝒜 p)
+(hm : 𝓜 = (fun i => (𝒜 i)⧸(Component_of_graded_as_addsubgroup 𝒜 p hp i)))
+: (∃ (N : ℤ), ∀ (n : ℤ), n ≥ N → hilb n = 0) := by
+  sorry
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/CommAlg/jayden(krull-dim-zero).lean b/CommAlg/jayden(krull-dim-zero).lean
index eba40ab..f75912a 100644
--- a/CommAlg/jayden(krull-dim-zero).lean
+++ b/CommAlg/jayden(krull-dim-zero).lean
@@ -125,19 +125,23 @@ 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 : Fin n → Ideal R := fun k ↦ (m' k).asIdeal
     have comaximal : ∀ i j : ℕ, i ≠ j → (m' i).asIdeal ⊔ (m' j).asIdeal =
       (⊤ : Ideal R) := by 
       intro i j distinct
       apply Ideal.IsMaximal.coprime_of_ne
-      sorry
-      sorry
-      --  by_contra equal
+      exact (m' i).IsMaximal
+      exact (m' j).IsMaximal
       have : (m' i) ≠ (m' j) := by 
         exact Function.Injective.ne m'inj distinct
       intro h
       apply this
       exact MaximalSpectrum.ext _ _ h
-    -- let g :`= Ideal.quotientInfRingEquivPiQuotient m' comaximal
+    have ∀ n : ℕ, (R ⧸ ⨅ (i : Fin n), (F n) i) ≃+* ((i : Fin n) → R ⧸ (F n) i) := by
+      sorry
+    -- (let F : Fin n → Ideal R := fun k : Fin n ↦ (m' k).asIdeal) 
+    -- let g := Ideal.quotientInfRingEquivPiQuotient f comaximal 
 
 
 -- Stacks Lemma 10.53.4: R Artinian => Jacobson ideal of R is nilpotent
@@ -193,7 +197,7 @@ lemma dim_zero_Noetherian_iff_Artinian (R : Type _) [CommRing R] :
     constructor
     apply finite_length_is_Noetherian
     rwa [IsArtinian_iff_finite_length] at RisArtinian
-    sorry
+    sorry -- can use Grant's lemma dim_eq_zero_iff
 
 
 
diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean
index 2b86416..a559b1d 100644
--- a/CommAlg/krull.lean
+++ b/CommAlg/krull.lean
@@ -56,6 +56,7 @@ lemma le_krullDim_iff' (R : Type _) [CommRing R] (n : ℕ∞) :
 lemma height_le_krullDim (I : PrimeSpectrum R) : height I ≤ krullDim R := 
   le_iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) I
 
+/-- 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
   apply le_antisymm
   . rw [krullDim_le_iff']
@@ -66,6 +67,8 @@ lemma krullDim_eq_height [LocalRing R] : krullDim R = height (closedPoint R) :=
     exact I.2.1
   . simp only [height_le_krullDim]
 
+/-- 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
   rcases n with _ | n
@@ -88,6 +91,7 @@ height 𝔭 > n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀
     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
   show (_ < _) ↔ _
@@ -97,9 +101,11 @@ height 𝔭 > (n : WithBot ℕ∞) ↔ ∃ c : List (PrimeSpectrum R), c.Chain'
 #check height_le_krullDim
 --some propositions that would be nice to be able to eventually
 
+/-- The prime spectrum of the zero ring is empty. -/
 lemma primeSpectrum_empty_of_subsingleton (x : PrimeSpectrum R) [Subsingleton R] : False :=
   x.1.ne_top_iff_one.1 x.2.1 <| Eq.substr (Subsingleton.elim 1 (0 : R)) x.1.zero_mem
 
+/-- A CommRing has empty prime spectrum if and only if it is the zero ring. -/
 lemma primeSpectrum_empty_iff : IsEmpty (PrimeSpectrum R) ↔ Subsingleton R := by
   constructor
   . contrapose
@@ -123,17 +129,20 @@ lemma dim_eq_bot_iff : krullDim R = ⊥ ↔ Subsingleton R := by
   . rw [h.forall_iff]
     trivial
 
+/-- Nonzero rings have Krull dimension in ℕ∞ -/
 lemma krullDim_nonneg_of_nontrivial (R : Type _) [CommRing R] [Nontrivial R] : ∃ n : ℕ∞, Ideal.krullDim R = n := by
   have h := dim_eq_bot_iff.not.mpr (not_subsingleton R)
   lift (Ideal.krullDim R) to ℕ∞ using h with k
   use k
 
+/-- An ideal which is less than a prime is not a maximal ideal. -/
 lemma not_maximal_of_lt_prime {p : Ideal R} {q : Ideal R} (hq : IsPrime q) (h : p < q) : ¬IsMaximal p := by
   intro hp
   apply IsPrime.ne_top hq
   apply (IsCoatom.lt_iff hp.out).mp
   exact h
 
+/-- Krull dimension is ≤ 0 if and only if all primes are maximal. -/
 lemma dim_le_zero_iff : krullDim R ≤ 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal I.asIdeal := by
   show ((_ : WithBot ℕ∞) ≤ (0 : ℕ)) ↔ _
   rw [krullDim_le_iff R 0]
@@ -169,6 +178,7 @@ lemma dim_le_zero_iff : krullDim R ≤ 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal
     apply not_maximal_of_lt_prime I.IsPrime
     exact hc2
 
+/-- For a nonzero ring, Krull dimension is 0 if and only if all primes are maximal. -/
 lemma dim_eq_zero_iff [Nontrivial R] : krullDim R = 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal I.asIdeal := by
   rw [←dim_le_zero_iff]
   obtain ⟨n, hn⟩ := krullDim_nonneg_of_nontrivial R
@@ -177,9 +187,10 @@ lemma dim_eq_zero_iff [Nontrivial R] : krullDim R = 0 ↔ ∀ I : PrimeSpectrum
   rw [←WithBot.coe_le_coe,←hn] at this
   change (0 : WithBot ℕ∞) ≤ _ at this
   constructor <;> intro h'
-  rw [h']
-  exact le_antisymm h' this
+  . rw [h']
+  . exact le_antisymm h' this
 
+/-- In a field, the unique prime ideal is the zero ideal. -/
 @[simp]
 lemma field_prime_bot {K: Type _} [Field K] (P : Ideal K) : IsPrime P ↔ P = ⊥ := by
       constructor
@@ -191,6 +202,7 @@ lemma field_prime_bot {K: Type _} [Field K] (P : Ideal K) : IsPrime P ↔ P = 
         rw [botP]
         exact bot_prime
 
+/-- In a field, all primes have height 0. -/
 lemma field_prime_height_zero {K: Type _} [Field K] (P : PrimeSpectrum K) : height P = 0 := by
     unfold height
     simp
@@ -206,10 +218,12 @@ lemma field_prime_height_zero {K: Type _} [Field K] (P : PrimeSpectrum K) : heig
     have : J ≠ P := ne_of_lt JlP
     contradiction
 
+/-- The Krull dimension of a field is 0. -/
 lemma dim_field_eq_zero {K : Type _} [Field K] : krullDim K = 0 := by
   unfold krullDim
   simp [field_prime_height_zero]
 
+/-- A domain with Krull dimension 0 is a field. -/
 lemma domain_dim_zero.isField {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0) : IsField D := by
   by_contra x
   rw [Ring.not_isField_iff_exists_prime] at x
@@ -231,6 +245,7 @@ lemma domain_dim_zero.isField {D: Type _} [CommRing D] [IsDomain D] (h: krullDim
     aesop
   contradiction
 
+/-- A domain has Krull dimension 0 if and only if it is a field. -/
 lemma domain_dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krullDim D = 0 ↔ IsField D := by
   constructor
   · exact domain_dim_zero.isField
@@ -260,10 +275,9 @@ lemma dim_le_one_of_dimLEOne :  Ring.DimensionLEOne R → krullDim R ≤ 1 := by
   change q0.asIdeal < q1.asIdeal at hc1
   have q1nbot := Trans.trans (bot_le : ⊥ ≤ q0.asIdeal) hc1
   specialize H q1.asIdeal (bot_lt_iff_ne_bot.mp q1nbot) q1.IsPrime
-  apply IsPrime.ne_top p.IsPrime
-  apply (IsCoatom.lt_iff H.out).mp
-  exact hc2
+  exact (not_maximal_of_lt_prime p.IsPrime hc2) H
 
+/-- The Krull dimension of a PID is at most 1. -/
 lemma dim_le_one_of_pid [IsDomain R] [IsPrincipalIdealRing R] : krullDim R ≤ 1 := by
   rw [dim_le_one_iff]
   exact Ring.DimensionLEOne.principal_ideal_ring R
diff --git a/CommAlg/monalisa.lean b/CommAlg/monalisa.lean
index 68579da..7a8635e 100644
--- a/CommAlg/monalisa.lean
+++ b/CommAlg/monalisa.lean
@@ -4,6 +4,18 @@ import Mathlib.Algebra.Module.GradedModule
 import Mathlib.RingTheory.Ideal.AssociatedPrime
 import Mathlib.RingTheory.Artinian
 import Mathlib.Order.Height
+import Mathlib.Algebra.Algebra.Subalgebra.Basic
+import Mathlib.Algebra.Module.LinearMap
+
+instance {𝒜 : ℤ → Type _} [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜] :
+    Algebra (𝒜 0) (⨁ i, 𝒜 i) :=
+  Algebra.ofModule'
+  (by
+    intro r x
+    sorry)
+  (by
+    intro r x
+    sorry)
 
 noncomputable def length ( A : Type _) (M : Type _)
  [CommRing A] [AddCommGroup M] [Module A M] :=  Set.chainHeight {M' : Submodule A M | M' < ⊤}
@@ -58,11 +70,11 @@ noncomputable def dimensionring { A: Type _}
 noncomputable def dimensionmodule ( A : Type _) (M : Type _)
  [CommRing A] [AddCommGroup M] [Module A M] := krullDim (PrimeSpectrum (A ⧸ ((⊤ : Submodule A M).annihilator)) )
 
--- (∃ (i : ℤ ), ∃ (x :  𝒜 i), p = (Submodule.span (⨁ i, 𝒜 i) {x}).annihilator ) 
+ 
 
---  lemma graded_local (𝒜 : ℤ → Type _) [SetLike (⨁ i, 𝒜 i)] (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)]
---   [DirectSum.GCommRing 𝒜]
---   [DirectSum.Gmodule 𝒜 𝓜] (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0)) : ∃ ( I : Ideal ((⨁ i, 𝒜 i))),(HomogeneousMax 𝒜 I) := sorry
+lemma graded_local (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) 
+[∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)]
+[DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜] (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0)) : ∃ ( I : Ideal ((⨁ i, 𝒜 i))),(HomogeneousMax 𝒜 I) := sorry
 
 
 def PolyType (f : ℤ → ℤ) (d : ℕ  ) := ∃ Poly : Polynomial ℚ, ∃ (N : ℤ), ∀ (n : ℤ), N ≤ n → f n = Polynomial.eval (n : ℚ) Poly ∧ d = Polynomial.degree Poly
@@ -96,6 +108,43 @@ lemma Associated_prime_of_graded_is_graded
   sorry
 
 
--- def standard_graded {𝒜 : ℤ → Type _} [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜] (n : ℕ) :
---     Prop :=
---   ∃ J, Ideal.IsHomogeneous' 𝒜 J (J :Nonempty ((⨁ i, 𝒜 i) ≃+* (MvPolynomial (Fin n) (𝒜 0)) ⧸ J)
+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))
+
+def Component_of_graded_as_addsubgroup (𝒜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜]
+(p : Ideal (⨁ i, 𝒜 i)) (hp : Ideal.IsHomogeneous' 𝒜 p) (i : ℤ) : AddSubgroup (𝒜 i) := sorry
+
+
+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
+
+
+def graded_submodule
+(𝒜 : ℤ → Type _) (𝓜 : ℤ → Type u) (𝓝 : ℤ → Type u)
+[∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] [∀ i, AddCommGroup (𝓝 i)]
+[DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜][DirectSum.Gmodule 𝒜 𝓝]
+(opn : Submodule (⨁ i, 𝒜 i) (⨁ i, 𝓜 i)) (opnis : opn = (⨁ i, 𝓝 i)) (i : ℤ )
+ : ∃(piece : Submodule (𝒜 0) (𝓜 i)), piece = 𝓝 i := by
+  sorry
+
+
+
+-- @ 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 𝒜]
+(p : Ideal (⨁ i, 𝒜 i)) (hp : Ideal.IsHomogeneous' 𝒜 p)
+  : DirectSum.Gmodule 𝒜 (fun i => (𝒜 i)⧸(Component_of_graded_as_addsubgroup 𝒜 p hp i)) := by
+  sorry
+
+theorem quotient_hilbert_polynomial (d : ℕ) (d1 : 1 ≤ d) (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)]
+[DirectSum.GCommRing 𝒜]
+[DirectSum.Gmodule 𝒜 𝓜] (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0)) (p : Ideal (⨁ i, 𝒜 i)) 
+(findim :  dimensionmodule (⨁ i, 𝒜 i) (⨁ i, ((𝒜 i)⧸(Component_of_graded_as_addsubgroup 𝒜 p hp i)) = d) (hilb : ℤ → ℤ)
+ (Hhilb: hilbert_function 𝒜 𝓜 hilb) (homprime: HomogeneousPrime 𝒜 p)
+: PolyType hilb (d - 1) := by
+  sorry
+
+ 
+