diff --git a/HilbertFunction.lean b/HilbertFunction.lean
index 8351133..21715f0 100644
--- a/HilbertFunction.lean
+++ b/HilbertFunction.lean
@@ -29,8 +29,6 @@ macro "obviously" : tactic =>
 
 
 
-
-
 -- @Definitions (to be classified)
 section
 open GradedMonoid.GSmul
@@ -81,15 +79,20 @@ end
 --   [DirectSum.Gmodule 𝒜 𝓜] (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0)) : ∃ ( I : Ideal ((⨁ i, 𝒜 i))),(HomogeneousMax 𝒜 I) := sorry
 
 
--- Definition(s) of homogeneous ideals
+-- 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]
@@ -99,12 +102,6 @@ end
 
 
 
-
-
-
-
-
-
 -- @[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_ge1 (d : ℕ) (d1 : 1 ≤ d) (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)]
@@ -165,14 +162,7 @@ lemma Associated_prime_of_graded_is_graded
 --   sorry
 
 
--- instance sdfasdf
--- (𝒜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜]
--- (p : Ideal (⨁ i, 𝒜 i)) (hp : Ideal.IsHomogeneous' 𝒜 p)
---   : ∀ i, AddCommGroup (p i) := by
---   sorry
-
-
-
+-- 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
@@ -186,10 +176,12 @@ instance Quotient_of_graded_is_graded
   : DirectSum.Gmodule 𝒜 (fun i => (𝒜 i)⧸(Component_of_graded_as_addsubgroup 𝒜 p hp i)) := by
   sorry
 
--- @Graded submodule
-instance Graded_submodule
-(𝒜 : ℤ → 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
+
+
+-- -- @Graded submodule
+-- instance Graded_submodule
+-- (𝒜 : ℤ → 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
 
diff --git a/PolyType.lean b/PolyType.lean
index 1def55d..07c1be7 100644
--- a/PolyType.lean
+++ b/PolyType.lean
@@ -1,24 +1,5 @@
-import Mathlib
-import Mathlib.Algebra.MonoidAlgebra.Basic
-import Mathlib.Data.Finset.Sort
 import Mathlib.Order.Height
-import Mathlib.Order.KrullDimension
-import Mathlib.Order.JordanHolder
 import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
-import Mathlib.Order.Height
-import Mathlib.RingTheory.Ideal.Basic
-import Mathlib.RingTheory.Ideal.Operations
-import Mathlib.LinearAlgebra.Finsupp
-import Mathlib.RingTheory.GradedAlgebra.Basic
-import Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal
-import Mathlib.Algebra.Module.GradedModule
-import Mathlib.RingTheory.Ideal.AssociatedPrime
-import Mathlib.RingTheory.Noetherian
-import Mathlib.RingTheory.Artinian
-import Mathlib.Algebra.Module.GradedModule
-import Mathlib.RingTheory.Noetherian
-import Mathlib.RingTheory.Finiteness
-import Mathlib.RingTheory.Ideal.Operations
 
 -- Setting for "library_search"
 set_option maxHeartbeats 0
@@ -86,6 +67,7 @@ example : Polynomial.eval (100 : ℚ) F = (2 : ℚ) := by
 
 end section
 
+
 -- @[BH, 4.1.2]
 -- All the polynomials are in ℚ[X], all the functions are considered as ℤ → ℤ
 noncomputable section
@@ -247,6 +229,7 @@ lemma b_to_a (f : ℤ → ℤ) (d : ℕ) : PolyType f d → (∃ (c : ℤ), ∃
 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
 -- variable {R M N : Type _} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N]
 --   (f : M →[R] N)
@@ -305,4 +288,3 @@ end section
 
 
 
-