diff --git a/HilbertFunction.lean b/HilbertFunction.lean
index 4ed1a2b..21d7eb7 100644
--- a/HilbertFunction.lean
+++ b/HilbertFunction.lean
@@ -29,11 +29,13 @@ macro "obviously" : tactic =>
 
 
 
+open GradedMonoid.GSmul
+open DirectSum
+
+
 
 -- @Definitions (to be classified)
 section
-open GradedMonoid.GSmul
-open DirectSum
 
 -- 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
@@ -78,7 +80,6 @@ end
 
 
 
-
 -- Definition of homogeneous ideal
 def Ideal.IsHomogeneous' (𝒜 : ℤ → Type _) 
 [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜] 
@@ -99,10 +100,30 @@ def HomogeneousMax (𝒜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [Direc
 end
 
 
+-- 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
+
+-- @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) := sorry
+[DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜] (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0)) : ∃ ( I : Ideal ((⨁ i, 𝒜 i))),(HomogeneousMax 𝒜 I) := by
+  sorry
+
+
+
 
 
 
@@ -159,25 +180,11 @@ lemma Associated_prime_of_graded_is_graded
   sorry
 
 
--- instance gyhoiu
--- (𝒜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜]
--- (p : Ideal (⨁ i, 𝒜 i)) (hp : Ideal.IsHomogeneous' 𝒜 p)
---   : (𝒫 : ℤ → Type _) [∀ i, AddCommGroup (𝒫 i)] [DirectSum.GCommRing 𝒫] → Gmodule (⊕ i, 𝒜 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
+
+
+
+def Graded_homo : true := 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
-
-
diff --git a/PolyType.lean b/PolyType.lean
index e69eec2..a81d027 100644
--- a/PolyType.lean
+++ b/PolyType.lean
@@ -110,7 +110,7 @@ def f (n : ℤ) := n
 end section
 
 
--- (NO need to prove) Constant polynomial function = constant function
+-- (NO NEED TO PROVE) Constant polynomial function = constant function
 lemma Poly_constant (F : Polynomial ℚ) (c : ℚ) : 
   (F = Polynomial.C c) ↔ (∀ r : ℚ, (Polynomial.eval r F) = c) := by
   constructor
@@ -123,10 +123,20 @@ lemma Poly_constant (F : Polynomial ℚ) (c : ℚ) :
   · 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
@@ -188,6 +198,14 @@ lemma PolyType_0 (f : ℤ → ℤ) : (PolyType f 0) ↔ (∃ (c : ℤ), ∃ (N :
     · sorry
       -- apply Polynomial.degree_C c
 
+
+
+
+
+-- Δ of 0 times preserve the function
+lemma Δ_0 (f : ℤ → ℤ) : (Δ f 0) = f := by
+  tauto
+
 -- Δ of d times maps polynomial of degree d to polynomial of degree 0
 lemma Δ_PolyType_d_to_PolyType_0 (f : ℤ → ℤ) (d : ℕ): PolyType f d → PolyType (Δ f d) 0 := by
   intro h
@@ -203,6 +221,10 @@ lemma Δ_PolyType_d_to_PolyType_0 (f : ℤ → ℤ) (d : ℕ): PolyType f d →
     sorry
   · sorry
 
+
+
+
+
 -- [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