From 5a869021189bd2a993aa2c8e9aa28dc10f5f9937 Mon Sep 17 00:00:00 2001
From: chelseaandmadrid <53058005+chelseaandmadrid@users.noreply.github.com>
Date: Wed, 14 Jun 2023 22:10:22 -0700
Subject: [PATCH 01/16] changed

---
 CommAlg/final_hil_pol.lean | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

diff --git a/CommAlg/final_hil_pol.lean b/CommAlg/final_hil_pol.lean
index 591c6cc..7176de2 100644
--- a/CommAlg/final_hil_pol.lean
+++ b/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)
 
@@ -110,7 +109,7 @@ instance {𝒜 : ℤ → Type _} [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GComm
 
 
 
-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))
 
@@ -189,10 +188,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 +203,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 +217,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 +230,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)
@@ -256,3 +256,4 @@ theorem Hilbert_polynomial_d_0_reduced
 
 
 
+

From 766c740c8d76d6a344713b92dcfa796a41183fbe Mon Sep 17 00:00:00 2001
From: chelseaandmadrid <53058005+chelseaandmadrid@users.noreply.github.com>
Date: Wed, 14 Jun 2023 23:35:46 -0700
Subject: [PATCH 02/16] Add graded_isom (with error)

---
 CommAlg/final_hil_pol.lean | 34 ++++++++++++++++++++++++++++++++--
 1 file changed, 32 insertions(+), 2 deletions(-)

diff --git a/CommAlg/final_hil_pol.lean b/CommAlg/final_hil_pol.lean
index 7176de2..e3c141e 100644
--- a/CommAlg/final_hil_pol.lean
+++ b/CommAlg/final_hil_pol.lean
@@ -108,7 +108,6 @@ instance {𝒜 : ℤ → Type _} [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GComm
     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))
@@ -123,7 +122,27 @@ 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))
+(hf : graded_morphism (fun i => (𝒜 i)) (fun i => (𝓜 i)) (fun i => (𝓝 i)) f)
+: (f : (⨁ i, 𝓜 i) ≃ₗ[(⨁ i, 𝒜 i)] (⨁ i, 𝓝 i)) := by
+  sorry
+
+
+-- (⊕ i, 𝒜 i) (⨁ i, 𝓜 i) (⊕ i, 𝓝 i)
+
+#check graded_isomorphism
+
 
 
 def graded_submodule
@@ -142,6 +161,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 𝒜]
@@ -149,6 +169,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 _) 
@@ -255,5 +282,8 @@ theorem Hilbert_polynomial_d_0_reduced
 
 
 
+
+
+
 
 

From 75cc002bef90567bf47193dde474eb7ebabadbd9 Mon Sep 17 00:00:00 2001
From: chelseaandmadrid <53058005+chelseaandmadrid@users.noreply.github.com>
Date: Thu, 15 Jun 2023 12:31:37 -0700
Subject: [PATCH 03/16] finished a case of polytype 0

---
 CommAlg/PolyTEST.lean      |  0
 CommAlg/final_hil_pol.lean | 12 ++++++------
 2 files changed, 6 insertions(+), 6 deletions(-)
 create mode 100644 CommAlg/PolyTEST.lean

diff --git a/CommAlg/PolyTEST.lean b/CommAlg/PolyTEST.lean
new file mode 100644
index 0000000..e69de29
diff --git a/CommAlg/final_hil_pol.lean b/CommAlg/final_hil_pol.lean
index e3c141e..eff9302 100644
--- a/CommAlg/final_hil_pol.lean
+++ b/CommAlg/final_hil_pol.lean
@@ -134,13 +134,11 @@ def graded_isomorphism (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) (𝓝 : 
 [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] [∀ i, AddCommGroup (𝓝 i)]
 [DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜][DirectSum.Gmodule 𝒜 𝓝]
 (f : (⨁ i, 𝓜 i) →ₗ[(⨁ i, 𝒜 i)] (⨁ i, 𝓝 i))
-(hf : graded_morphism (fun i => (𝒜 i)) (fun i => (𝓜 i)) (fun i => (𝓝 i)) f)
-: (f : (⨁ i, 𝓜 i) ≃ₗ[(⨁ i, 𝒜 i)] (⨁ i, 𝓝 i)) := by
+: IsLinearEquiv f := by
   sorry
-
-
--- (⊕ i, 𝒜 i) (⨁ i, 𝓜 i) (⊕ i, 𝓝 i)
-
+-- f ∈ (⨁ i, 𝓜 i) ≃ₗ[(⨁ i, 𝒜 i)] (⨁ i, 𝓝 i)
+-- LinearEquivClass f (⨁ i, 𝒜 i) (⨁ i, 𝓜 i) (⨁ i, 𝓝 i)
+-- #print IsLinearEquiv
 #check graded_isomorphism
 
 
@@ -284,6 +282,8 @@ theorem Hilbert_polynomial_d_0_reduced
 
 
 
+
+
 
 
 

From 41105f8623d584ea652f0b2c8d2ed0f59fd0d6b2 Mon Sep 17 00:00:00 2001
From: chelseaandmadrid <53058005+chelseaandmadrid@users.noreply.github.com>
Date: Thu, 15 Jun 2023 12:40:41 -0700
Subject: [PATCH 04/16] Rename the file

---
 CommAlg/PolyTEST.lean        |   0
 CommAlg/final_poly_type.lean | 325 +++++++++++++++++++++++++++++++++++
 2 files changed, 325 insertions(+)
 delete mode 100644 CommAlg/PolyTEST.lean
 create mode 100644 CommAlg/final_poly_type.lean

diff --git a/CommAlg/PolyTEST.lean b/CommAlg/PolyTEST.lean
deleted file mode 100644
index e69de29..0000000
diff --git a/CommAlg/final_poly_type.lean b/CommAlg/final_poly_type.lean
new file mode 100644
index 0000000..c62acf3
--- /dev/null
+++ b/CommAlg/final_poly_type.lean
@@ -0,0 +1,325 @@
+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) 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
+
+
+
+
+-- set_option pp.all true in
+-- PolyType 0 = constant function
+lemma PolyType_0 (f : ℤ → ℤ) : (PolyType f 0) ↔ (∃ (c : ℤ), ∃ (N : ℤ), ∀ (n : ℤ), (N ≤ n → f n = c) ∧ c ≠ 0) := by
+  constructor
+  · intro h
+    rcases h with ⟨Poly, hN⟩
+    rcases hN with ⟨N, hh⟩
+    have H1 := λ n hn => (hh n hn).left
+    have H2 := λ n hn => (hh n hn).right
+    clear hh
+    specialize H2 (N + 1)
+    have this1 : Polynomial.degree Poly = 0 := by
+      have : N ≤ N + 1 := by
+        norm_num
+      tauto
+    have this2 : ∃ (c : ℤ), Poly = Polynomial.C (c : ℚ) := by
+      have HH : ∃ (c : ℚ), Poly = Polynomial.C (c : ℚ) := by
+        use Poly.coeff 0
+        apply Polynomial.eq_C_of_degree_eq_zero
+        exact this1
+      cases' HH with c HHH
+      have HHHH : ∃ (d : ℤ), d = c := by
+        have H3 := (Poly_constant Poly c).mp HHH N
+        have H4 := H1 N (le_refl N)
+        rw[H3] at H4
+        exact ⟨f N, H4⟩
+      cases' HHHH with d H5
+      use d
+      rw [H5]
+      exact HHH
+    rcases this2 with ⟨c, hthis2⟩
+    use c 
+    use N
+    intro n
+    specialize H1 n
+    constructor
+    · intro HH1
+      -- have H6 := H1 HH1
+    --
+      have this3 : f n = Polynomial.eval (n : ℚ) Poly := by
+        tauto
+      have this4 : Polynomial.eval (n : ℚ) Poly = c := by
+        rw [hthis2]
+        simp
+      have this5 : f n = (c : ℚ) := by
+        rw [←this4, this3]
+      exact Iff.mp (Rat.coe_int_inj (f n) c) this5
+    --
+    
+    · intro c0
+      have H7 := H2 (by norm_num)
+      rw [hthis2] at this1
+      rw [c0] at this1
+      simp at this1
+    --   
+
+
+  · intro h
+    rcases h with ⟨c, N, aaa⟩
+    let (Poly : Polynomial ℚ) := Polynomial.C (c : ℚ)
+    use Poly
+    use N
+    intro n Nn
+    specialize aaa n
+    have this1 : c ≠ 0 →  f n = c := by
+      tauto
+    constructor
+    · sorry
+    · 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
+  rcases h with ⟨Poly, hN⟩
+  rcases hN with ⟨N, hh⟩
+  have H1 := λ n hn => (hh n hn).left
+  have H2 := λ n hn => (hh n hn).right
+  clear hh
+  have HH2 : d = Polynomial.degree Poly := by
+    sorry
+  induction' d with d hd
+  · rw [PolyType_0]
+    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
+  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
+  · rw [PolyType_0]
+    use c
+    use N
+    tauto
+  · 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 Δ_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
+-- variable {R M N : Type _} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N]
+--   (f : M →[R] N)
+open LinearMap
+-- variable {R M : Type _} [CommRing R] [AddCommGroup M] [Module R M]
+-- noncomputable def length := Set.chainHeight {M' : Submodule R M | M' < ⊤}
+
+
+-- 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 ℤ ℤ
+-- #eval length ℤ ℤ
+
+
+-- @[ext]
+-- structure SES (R : Type _) [CommRing R] where
+--   A : Type _
+--   B : Type _
+--   C : Type _
+--   f : A →ₗ[R] B
+--   g : B →ₗ[R] C
+-- left_exact : LinearMap.ker f = 0
+-- middle_exact : LinearMap.range f = LinearMap.ker g
+-- right_exact : LinearMap.range g = C
+
+
+
+-- 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 = ⊤
+
+#check SES.right_exact
+#check SES
+
+
+-- 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
+
+
+
+
+
+
+

From 61a7ae54bfee1c5176466078d59487bb8ef66c33 Mon Sep 17 00:00:00 2001
From: chelseaandmadrid <53058005+chelseaandmadrid@users.noreply.github.com>
Date: Thu, 15 Jun 2023 13:31:48 -0700
Subject: [PATCH 05/16] change PolyType

---
 CommAlg/final_poly_type.lean | 51 +++++++++++++++++++++++++++---------
 1 file changed, 39 insertions(+), 12 deletions(-)

diff --git a/CommAlg/final_poly_type.lean b/CommAlg/final_poly_type.lean
index c62acf3..94dd153 100644
--- a/CommAlg/final_poly_type.lean
+++ b/CommAlg/final_poly_type.lean
@@ -70,7 +70,7 @@ 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
 -- structure PolyType (f : ℤ → ℤ) where
 --   Poly : Polynomial ℤ
@@ -109,7 +109,7 @@ end section
 
 -- (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
+  (F = Polynomial.C (c : ℚ)) ↔ (∀ r : ℚ, (Polynomial.eval r F) = (c : ℚ)) := by
   constructor
   · intro h
     rintro r
@@ -134,13 +134,13 @@ lemma Poly_shifting (f : ℤ → ℤ) (g : ℤ → ℤ) (hf : PolyType f d) (s :
 
 -- set_option pp.all true in
 -- PolyType 0 = constant function
-lemma PolyType_0 (f : ℤ → ℤ) : (PolyType f 0) ↔ (∃ (c : ℤ), ∃ (N : ℤ), ∀ (n : ℤ), (N ≤ n → f n = c) ∧ c ≠ 0) := by
+lemma PolyType_0 (f : ℤ → ℤ) : (PolyType f 0) ↔ (∃ (c : ℤ), ∃ (N : ℤ), ∀ (n : ℤ), (N ≤ n → f n = c) ∧ (c ≠ 0)) := by
   constructor
   · intro h
     rcases h with ⟨Poly, hN⟩
     rcases hN with ⟨N, hh⟩
-    have H1 := λ n hn => (hh n hn).left
-    have H2 := λ n hn => (hh n hn).right
+    have H1 := λ n=> (hh n).left
+    have H2 := λ n=> (hh n).right
     clear hh
     specialize H2 (N + 1)
     have this1 : Polynomial.degree Poly = 0 := by
@@ -182,11 +182,10 @@ lemma PolyType_0 (f : ℤ → ℤ) : (PolyType f 0) ↔ (∃ (c : ℤ), ∃ (N :
     --
     
     · intro c0
-      have H7 := H2 (by norm_num)
+      -- have H7 := H2 (by norm_num)
       rw [hthis2] at this1
       rw [c0] at this1
       simp at this1
-    --   
 
 
   · intro h
@@ -194,17 +193,45 @@ lemma PolyType_0 (f : ℤ → ℤ) : (PolyType f 0) ↔ (∃ (c : ℤ), ∃ (N :
     let (Poly : Polynomial ℚ) := Polynomial.C (c : ℚ)
     use Poly
     use N
-    intro n Nn
+    intro n
     specialize aaa n
     have this1 : c ≠ 0 →  f n = c := by
       tauto
+    rcases aaa with ⟨A, B⟩
+    have this1 : f n = c := by
+      tauto
     constructor
-    · sorry
-    · sorry
+    clear A
+    · have this2 : ∀ (t : ℚ), (Polynomial.eval t Poly) = (c : ℚ) := by
+        rw [← Poly_constant Poly (c : ℚ)]
+        sorry
+      specialize this2 n
+      rw [this2]
+      tauto
+    · sorry 
       -- apply Polynomial.degree_C c
 
 
 
+    -- constructor
+    -- · intro n Nn
+    --   specialize aaa n
+    --   have this1 : c ≠ 0 →  f n = c := by
+    --     tauto
+    --   rcases aaa with ⟨A, B⟩
+    --   have this1 : f n = c := by
+    --     tauto
+    --   clear A
+    --   have this2 : ∀ (t : ℚ), (Polynomial.eval t Poly) = (c : ℚ) := by
+    --     rw [← Poly_constant Poly (c : ℚ)]
+    --     sorry
+    --   specialize this2 n
+    --   rw [this2]
+    --   tauto
+    -- · sorry
+
+
+
 
 
 
@@ -217,8 +244,8 @@ lemma Δ_PolyType_d_to_PolyType_0 (f : ℤ → ℤ) (d : ℕ): PolyType f d →
   intro h
   rcases h with ⟨Poly, hN⟩
   rcases hN with ⟨N, hh⟩
-  have H1 := λ n hn => (hh n hn).left
-  have H2 := λ n hn => (hh n hn).right
+  have H1 := λ n => (hh n).left
+  have H2 := λ n => (hh n).right
   clear hh
   have HH2 : d = Polynomial.degree Poly := by
     sorry

From 007e8cf7950442d3fa16cd151eba2e1def637c93 Mon Sep 17 00:00:00 2001
From: chelseaandmadrid <53058005+chelseaandmadrid@users.noreply.github.com>
Date: Thu, 15 Jun 2023 15:10:30 -0700
Subject: [PATCH 06/16] finish more on the PolyType_0 lemma

---
 CommAlg/final_poly_type.lean | 74 ++++++++++++++++++++++--------------
 1 file changed, 45 insertions(+), 29 deletions(-)

diff --git a/CommAlg/final_poly_type.lean b/CommAlg/final_poly_type.lean
index 94dd153..ebd6043 100644
--- a/CommAlg/final_poly_type.lean
+++ b/CommAlg/final_poly_type.lean
@@ -70,7 +70,7 @@ 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
 -- structure PolyType (f : ℤ → ℤ) where
 --   Poly : Polynomial ℤ
@@ -107,7 +107,7 @@ def f (n : ℤ) := n
 end section
 
 
--- (NO NEED TO PROVE) Constant polynomial function = constant function
+-- (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
@@ -132,6 +132,8 @@ lemma Poly_shifting (f : ℤ → ℤ) (g : ℤ → ℤ) (hf : PolyType f d) (s :
 
 
 
+
+
 -- set_option pp.all true in
 -- PolyType 0 = constant function
 lemma PolyType_0 (f : ℤ → ℤ) : (PolyType f 0) ↔ (∃ (c : ℤ), ∃ (N : ℤ), ∀ (n : ℤ), (N ≤ n → f n = c) ∧ (c ≠ 0)) := by
@@ -139,10 +141,9 @@ lemma PolyType_0 (f : ℤ → ℤ) : (PolyType f 0) ↔ (∃ (c : ℤ), ∃ (N :
   · intro h
     rcases h with ⟨Poly, hN⟩
     rcases hN with ⟨N, hh⟩
-    have H1 := λ n=> (hh n).left
-    have H2 := λ n=> (hh n).right
-    clear hh
-    specialize H2 (N + 1)
+    rcases hh with ⟨H1, H2⟩
+    -- have H1 := λ n=> (hh n).left
+    -- have H2 := λ n=> (hh n).right
     have this1 : Polynomial.degree Poly = 0 := by
       have : N ≤ N + 1 := by
         norm_num
@@ -170,7 +171,6 @@ lemma PolyType_0 (f : ℤ → ℤ) : (PolyType f 0) ↔ (∃ (c : ℤ), ∃ (N :
     constructor
     · intro HH1
       -- have H6 := H1 HH1
-    --
       have this3 : f n = Polynomial.eval (n : ℚ) Poly := by
         tauto
       have this4 : Polynomial.eval (n : ℚ) Poly = c := by
@@ -179,7 +179,6 @@ lemma PolyType_0 (f : ℤ → ℤ) : (PolyType f 0) ↔ (∃ (c : ℤ), ∃ (N :
       have this5 : f n = (c : ℚ) := by
         rw [←this4, this3]
       exact Iff.mp (Rat.coe_int_inj (f n) c) this5
-    --
     
     · intro c0
       -- have H7 := H2 (by norm_num)
@@ -189,27 +188,46 @@ lemma PolyType_0 (f : ℤ → ℤ) : (PolyType f 0) ↔ (∃ (c : ℤ), ∃ (N :
 
 
   · intro h
-    rcases h with ⟨c, N, aaa⟩
-    let (Poly : Polynomial ℚ) := Polynomial.C (c : ℚ)
+    rcases h with ⟨c, N, hh⟩
+    let Poly := Polynomial.C (c : ℚ)
+    --unfold PolyType
     use Poly
+    --simp at Poly
     use N
-    intro n
-    specialize aaa n
-    have this1 : c ≠ 0 →  f n = c := by
-      tauto
-    rcases aaa with ⟨A, B⟩
-    have this1 : f n = c := by
-      tauto
+    have H1 := λ n=> (hh n).left
+    have H22 := λ n=> (hh n).right
+    have H2 : c ≠ 0 := by
+      exact H22 0
+    clear H22
     constructor
-    clear A
-    · have this2 : ∀ (t : ℚ), (Polynomial.eval t Poly) = (c : ℚ) := by
-        rw [← Poly_constant Poly (c : ℚ)]
-        sorry
-      specialize this2 n
-      rw [this2]
-      tauto
-    · sorry 
-      -- apply Polynomial.degree_C c
+    · intro n Nn
+      specialize H1 n
+      have this : f n = c := by
+        tauto
+      rw [this]
+      have this2 : Polynomial.eval (n : ℚ) Poly = (c : ℚ) := by
+        have this3 : ∀ r : ℚ, (Polynomial.eval r Poly) = (c : ℚ) :=  (Poly_constant Poly (c : ℚ)).mp rfl
+        exact this3 n
+      exact this2.symm
+    
+
+    · sorry
+    -- intro n
+    -- specialize aaa n
+    -- have this1 : c ≠ 0 →  f n = c := by
+    --   sorry
+    -- rcases aaa with ⟨A, B⟩
+    -- have this1 : f n = c := by
+    --   tauto
+    -- constructor
+    -- clear A
+    -- · have this2 : ∀ (t : ℚ), (Polynomial.eval t Poly) = (c : ℚ) := by
+    --     rw [← Poly_constant Poly (c : ℚ)]
+    --     sorry
+    --   specialize this2 n
+    --   rw [this2]
+    --   tauto
+    -- · sorry
 
 
 
@@ -244,9 +262,7 @@ lemma Δ_PolyType_d_to_PolyType_0 (f : ℤ → ℤ) (d : ℕ): PolyType f d →
   intro h
   rcases h with ⟨Poly, hN⟩
   rcases hN with ⟨N, hh⟩
-  have H1 := λ n => (hh n).left
-  have H2 := λ n => (hh n).right
-  clear hh
+  rcases hh with ⟨H1, H2⟩
   have HH2 : d = Polynomial.degree Poly := by
     sorry
   induction' d with d hd

From 300007621a41a50bb0d75eef3034a2378a9af6d1 Mon Sep 17 00:00:00 2001
From: chelseaandmadrid <53058005+chelseaandmadrid@users.noreply.github.com>
Date: Thu, 15 Jun 2023 15:38:25 -0700
Subject: [PATCH 07/16] Finish the PolyType_0 lemma!

---
 CommAlg/final_poly_type.lean | 44 ++++++------------------------------
 1 file changed, 7 insertions(+), 37 deletions(-)

diff --git a/CommAlg/final_poly_type.lean b/CommAlg/final_poly_type.lean
index ebd6043..60df0d4 100644
--- a/CommAlg/final_poly_type.lean
+++ b/CommAlg/final_poly_type.lean
@@ -198,6 +198,8 @@ lemma PolyType_0 (f : ℤ → ℤ) : (PolyType f 0) ↔ (∃ (c : ℤ), ∃ (N :
     have H22 := λ n=> (hh n).right
     have H2 : c ≠ 0 := by
       exact H22 0
+    have H2 : (c : ℚ) ≠ 0 := by
+      simp; tauto
     clear H22
     constructor
     · intro n Nn
@@ -206,47 +208,15 @@ lemma PolyType_0 (f : ℤ → ℤ) : (PolyType f 0) ↔ (∃ (c : ℤ), ∃ (N :
         tauto
       rw [this]
       have this2 : Polynomial.eval (n : ℚ) Poly = (c : ℚ) := by
-        have this3 : ∀ r : ℚ, (Polynomial.eval r Poly) = (c : ℚ) :=  (Poly_constant Poly (c : ℚ)).mp rfl
+        have this3 : ∀ r : ℚ, (Polynomial.eval r Poly) = (c : ℚ) := (Poly_constant Poly (c : ℚ)).mp rfl
         exact this3 n
       exact this2.symm
     
 
-    · sorry
-    -- intro n
-    -- specialize aaa n
-    -- have this1 : c ≠ 0 →  f n = c := by
-    --   sorry
-    -- rcases aaa with ⟨A, B⟩
-    -- have this1 : f n = c := by
-    --   tauto
-    -- constructor
-    -- clear A
-    -- · have this2 : ∀ (t : ℚ), (Polynomial.eval t Poly) = (c : ℚ) := by
-    --     rw [← Poly_constant Poly (c : ℚ)]
-    --     sorry
-    --   specialize this2 n
-    --   rw [this2]
-    --   tauto
-    -- · sorry
-
-
-
-    -- constructor
-    -- · intro n Nn
-    --   specialize aaa n
-    --   have this1 : c ≠ 0 →  f n = c := by
-    --     tauto
-    --   rcases aaa with ⟨A, B⟩
-    --   have this1 : f n = c := by
-    --     tauto
-    --   clear A
-    --   have this2 : ∀ (t : ℚ), (Polynomial.eval t Poly) = (c : ℚ) := by
-    --     rw [← Poly_constant Poly (c : ℚ)]
-    --     sorry
-    --   specialize this2 n
-    --   rw [this2]
-    --   tauto
-    -- · sorry
+    · have this : Polynomial.degree Poly = 0 := by
+        simp only [map_intCast]
+        exact Polynomial.degree_C H2
+      tauto
 
 
 

From d5b2e4d431c4edf47b7e01e3317281e5122b64e8 Mon Sep 17 00:00:00 2001
From: chelseaandmadrid <53058005+chelseaandmadrid@users.noreply.github.com>
Date: Thu, 15 Jun 2023 17:51:32 -0700
Subject: [PATCH 08/16] Part of the base case of \Delta lemma

---
 CommAlg/final_poly_type.lean | 60 +++++++++++++++++++++++++++++++-----
 1 file changed, 52 insertions(+), 8 deletions(-)

diff --git a/CommAlg/final_poly_type.lean b/CommAlg/final_poly_type.lean
index 60df0d4..403e14e 100644
--- a/CommAlg/final_poly_type.lean
+++ b/CommAlg/final_poly_type.lean
@@ -65,7 +65,13 @@ 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
 -- Polynomial type of degree d
@@ -107,6 +113,10 @@ def f (n : ℤ) := n
 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
@@ -133,7 +143,6 @@ lemma Poly_shifting (f : ℤ → ℤ) (g : ℤ → ℤ) (hf : PolyType f d) (s :
 
 
 
-
 -- set_option pp.all true in
 -- PolyType 0 = constant function
 lemma PolyType_0 (f : ℤ → ℤ) : (PolyType f 0) ↔ (∃ (c : ℤ), ∃ (N : ℤ), ∀ (n : ℤ), (N ≤ n → f n = c) ∧ (c ≠ 0)) := by
@@ -211,7 +220,6 @@ lemma PolyType_0 (f : ℤ → ℤ) : (PolyType f 0) ↔ (∃ (c : ℤ), ∃ (N :
         have this3 : ∀ r : ℚ, (Polynomial.eval r Poly) = (c : ℚ) := (Poly_constant Poly (c : ℚ)).mp rfl
         exact this3 n
       exact this2.symm
-    
 
     · have this : Polynomial.degree Poly = 0 := by
         simp only [map_intCast]
@@ -221,23 +229,54 @@ lemma PolyType_0 (f : ℤ → ℤ) : (PolyType f 0) ↔ (∃ (c : ℤ), ∃ (N :
 
 
 
-
-
 -- Δ 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
+lemma Δ_d_PolyType_d_to_PolyType_0 (f : ℤ → ℤ) (d : ℕ): PolyType f d → PolyType (Δ f d) 0 := by
   intro h
   rcases h with ⟨Poly, hN⟩
   rcases hN with ⟨N, hh⟩
   rcases hh with ⟨H1, H2⟩
   have HH2 : d = Polynomial.degree Poly := by
-    sorry
+    tauto
+  have HH3 : Polynomial.degree Poly = d := by
+    tauto
   induction' d with d hd
+  -- Base case
   · rw [PolyType_0]
-    sorry
+    have this : Poly = Polynomial.C (Polynomial.coeff Poly 0) := by
+      exact Polynomial.eq_C_of_degree_eq_zero HH3
+    let d := Polynomial.coeff Poly 0
+    have this11 : ∃ (c : ℤ), c = d := by
+      sorry
+    rcases this11 with ⟨c, this1⟩
+    have this1 : c = Polynomial.coeff Poly 0 := by
+      tauto
+    use c; use N; intro n
+    constructor
+    · specialize H1 n
+      rw [Δ_0]
+      intro h
+      have this2 : f n = Polynomial.eval (n : ℚ) Poly := by
+        tauto
+      have this3 : f n = (c : ℚ) := by
+        rw [this2, this1]
+        let HHH := (Poly_constant Poly c).mp
+        sorry
+      exact Iff.mp (Rat.coe_int_inj (f n) c) this3
+    · intro c0
+      have this2 : (c : ℚ) = 0 := by
+        exact congrArg Int.cast c0
+      have this3 : Polynomial.coeff Poly 0 = 0 := by
+        rw [←this1, this2]
+      sorry
+  -- Induction step
   · sorry
 
 
@@ -260,12 +299,14 @@ lemma a_to_b (f : ℤ → ℤ) (d : ℕ) : (∃ (c : ℤ), ∃ (N : ℤ), ∀ (n
     tauto
   · 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 Δ_PolyType_d_to_PolyType_0
+    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]
@@ -277,6 +318,9 @@ 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

From b8928c8d90964e6d996746a2df3bc7c0e4ab6dfc Mon Sep 17 00:00:00 2001
From: Andre <espietandre@gmail.com>
Date: Thu, 15 Jun 2023 22:09:13 -0400
Subject: [PATCH 09/16] refactored PolyType_0

---
 CommAlg/final_poly_type.lean | 97 ++++++------------------------------
 1 file changed, 16 insertions(+), 81 deletions(-)

diff --git a/CommAlg/final_poly_type.lean b/CommAlg/final_poly_type.lean
index 60df0d4..aca056a 100644
--- a/CommAlg/final_poly_type.lean
+++ b/CommAlg/final_poly_type.lean
@@ -136,92 +136,27 @@ lemma Poly_shifting (f : ℤ → ℤ) (g : ℤ → ℤ) (hf : PolyType f d) (s :
 
 -- set_option pp.all true in
 -- PolyType 0 = constant function
-lemma PolyType_0 (f : ℤ → ℤ) : (PolyType f 0) ↔ (∃ (c : ℤ), ∃ (N : ℤ), ∀ (n : ℤ), (N ≤ n → f n = c) ∧ (c ≠ 0)) := by
+lemma PolyType_0 (f : ℤ → ℤ) : (PolyType f 0) ↔ (∃ (c : ℤ), ∃ (N : ℤ), ∀ (n : ℤ), 
+    (N ≤ n → f n = c) ∧ c ≠ 0) := by
   constructor
-  · intro h
-    rcases h with ⟨Poly, hN⟩
-    rcases hN with ⟨N, hh⟩
-    rcases hh with ⟨H1, H2⟩
-    -- have H1 := λ n=> (hh n).left
-    -- have H2 := λ n=> (hh n).right
-    have this1 : Polynomial.degree Poly = 0 := by
-      have : N ≤ N + 1 := by
-        norm_num
-      tauto
+  · 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 : ℚ) := by
-        use Poly.coeff 0
-        apply Polynomial.eq_C_of_degree_eq_zero
-        exact this1
+      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 := by
-        have H3 := (Poly_constant Poly c).mp HHH N
-        have H4 := H1 N (le_refl N)
-        rw[H3] at H4
-        exact ⟨f N, H4⟩
-      cases' HHHH with d H5
-      use d
-      rw [H5]
-      exact HHH
-    rcases this2 with ⟨c, hthis2⟩
-    use c 
-    use N
-    intro n
-    specialize H1 n
+      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
-    · intro HH1
-      -- have H6 := H1 HH1
-      have this3 : f n = Polynomial.eval (n : ℚ) Poly := by
-        tauto
-      have this4 : Polynomial.eval (n : ℚ) Poly = c := by
-        rw [hthis2]
-        simp
-      have this5 : f n = (c : ℚ) := by
-        rw [←this4, this3]
-      exact Iff.mp (Rat.coe_int_inj (f n) c) this5
-    
+    · 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
-      -- have H7 := H2 (by norm_num)
-      rw [hthis2] at this1
-      rw [c0] at this1
-      simp at this1
-
-
-  · intro h
-    rcases h with ⟨c, N, hh⟩
-    let Poly := Polynomial.C (c : ℚ)
-    --unfold PolyType
-    use Poly
-    --simp at Poly
-    use N
-    have H1 := λ n=> (hh n).left
-    have H22 := λ n=> (hh n).right
-    have H2 : c ≠ 0 := by
-      exact H22 0
-    have H2 : (c : ℚ) ≠ 0 := by
-      simp; tauto
-    clear H22
-    constructor
-    · intro n Nn
-      specialize H1 n
-      have this : f n = c := by
-        tauto
-      rw [this]
-      have this2 : Polynomial.eval (n : ℚ) Poly = (c : ℚ) := by
-        have this3 : ∀ r : ℚ, (Polynomial.eval r Poly) = (c : ℚ) := (Poly_constant Poly (c : ℚ)).mp rfl
-        exact this3 n
-      exact this2.symm
-    
-
-    · have this : Polynomial.degree Poly = 0 := by
-        simp only [map_intCast]
-        exact Polynomial.degree_C H2
-      tauto
-
-
-
-
-
+      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 preserve the function
 lemma Δ_0 (f : ℤ → ℤ) : (Δ f 0) = f := by

From 31210a9bf5f2fece27ba9c7c829cd1688bdc3327 Mon Sep 17 00:00:00 2001
From: chelseaandmadrid <53058005+chelseaandmadrid@users.noreply.github.com>
Date: Thu, 15 Jun 2023 20:27:29 -0700
Subject: [PATCH 10/16] add foo and foofoo

---
 CommAlg/final_poly_type.lean | 79 +++++++++++++++++-------------------
 1 file changed, 38 insertions(+), 41 deletions(-)

diff --git a/CommAlg/final_poly_type.lean b/CommAlg/final_poly_type.lean
index 403e14e..3669cb6 100644
--- a/CommAlg/final_poly_type.lean
+++ b/CommAlg/final_poly_type.lean
@@ -229,55 +229,49 @@ lemma PolyType_0 (f : ℤ → ℤ) : (PolyType f 0) ↔ (∃ (c : ℤ), ∃ (N :
 
 
 
--- Δ of 0 times preserve the function
-lemma Δ_0 (f : ℤ → ℤ) : (Δ f 0) = f := by
-  tauto
+-- Δ 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
+
+
+lemma foo (f : ℤ → ℤ) (s : ℕ) : Δ (Δ f 1) s = (Δ f (s + 1)) := by
+  sorry
 
 
 
 
 
 -- Δ of d times maps polynomial of degree d to polynomial of degree 0
+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
+        sorry
+      clear hf
+      specialize hd (Δ f 1)
+      have this4 : PolyType (Δ (Δ f 1) d) 0 := by tauto
+      rw [foo] at this4
+      tauto
+    tauto
+
+
+
 lemma Δ_d_PolyType_d_to_PolyType_0 (f : ℤ → ℤ) (d : ℕ): PolyType f d → PolyType (Δ f d) 0 := by
   intro h
-  rcases h with ⟨Poly, hN⟩
-  rcases hN with ⟨N, hh⟩
-  rcases hh with ⟨H1, H2⟩
-  have HH2 : d = Polynomial.degree Poly := by
-    tauto
-  have HH3 : Polynomial.degree Poly = d := by
-    tauto
-  induction' d with d hd
-  -- Base case
-  · rw [PolyType_0]
-    have this : Poly = Polynomial.C (Polynomial.coeff Poly 0) := by
-      exact Polynomial.eq_C_of_degree_eq_zero HH3
-    let d := Polynomial.coeff Poly 0
-    have this11 : ∃ (c : ℤ), c = d := by
-      sorry
-    rcases this11 with ⟨c, this1⟩
-    have this1 : c = Polynomial.coeff Poly 0 := by
-      tauto
-    use c; use N; intro n
-    constructor
-    · specialize H1 n
-      rw [Δ_0]
-      intro h
-      have this2 : f n = Polynomial.eval (n : ℚ) Poly := by
-        tauto
-      have this3 : f n = (c : ℚ) := by
-        rw [this2, this1]
-        let HHH := (Poly_constant Poly c).mp
-        sorry
-      exact Iff.mp (Rat.coe_int_inj (f n) c) this3
-    · intro c0
-      have this2 : (c : ℚ) = 0 := by
-        exact congrArg Int.cast c0
-      have this3 : Polynomial.coeff Poly 0 = 0 := by
-        rw [←this1, this2]
-      sorry
-  -- Induction step
-  · sorry
+  have this : ∀ (d : ℕ), ∀ (f :ℤ → ℤ), (PolyType f d) → (PolyType (Δ f d) 0) := by 
+    exact foofoo
+  specialize this d f
+  tauto
+
+
 
 
 
@@ -293,10 +287,13 @@ lemma a_to_b (f : ℤ → ℤ) (d : ℕ) : (∃ (c : ℤ), ∃ (N : ℤ), ∀ (n
   have H2 : c ≠ 0 := by
     tauto
   induction' d with d hd
+  -- Base case
   · rw [PolyType_0]
     use c
     use N
     tauto
+
+  -- Induction step
   · sorry
 
 

From a3c376de01fc08b5a1dc3eebc8ff579e42302ff7 Mon Sep 17 00:00:00 2001
From: chelseaandmadrid <53058005+chelseaandmadrid@users.noreply.github.com>
Date: Thu, 15 Jun 2023 20:28:30 -0700
Subject: [PATCH 11/16] merge two files

---
 CommAlg/final_poly_type.lean | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/CommAlg/final_poly_type.lean b/CommAlg/final_poly_type.lean
index 3fc34d7..96a3aca 100644
--- a/CommAlg/final_poly_type.lean
+++ b/CommAlg/final_poly_type.lean
@@ -167,14 +167,21 @@ lemma PolyType_0 (f : ℤ → ℤ) : (PolyType f 0) ↔ (∃ (c : ℤ), ∃ (N :
     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
 
 
+
+
 lemma foo (f : ℤ → ℤ) (s : ℕ) : Δ (Δ f 1) s = (Δ f (s + 1)) := by
   sorry
 

From 01f628cf986c8bdc6d9a13592c888408278f1246 Mon Sep 17 00:00:00 2001
From: chelseaandmadrid <53058005+chelseaandmadrid@users.noreply.github.com>
Date: Thu, 15 Jun 2023 20:43:52 -0700
Subject: [PATCH 12/16] kind of finish \Delta of d times lemma

---
 CommAlg/final_poly_type.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/CommAlg/final_poly_type.lean b/CommAlg/final_poly_type.lean
index 96a3aca..4405e42 100644
--- a/CommAlg/final_poly_type.lean
+++ b/CommAlg/final_poly_type.lean
@@ -199,7 +199,9 @@ lemma foofoo (d : ℕ) : (f : ℤ → ℤ) → (PolyType f d) → (PolyType (Δ
     have this1 : PolyType f (d + 1) := by tauto
     have this2 : PolyType (Δ f (d + 1)) 0 := by
       have this3 : PolyType (Δ f 1) d := by
-        sorry
+        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

From 85263016c118b8b2f8363110a0ccc589e6c0222a Mon Sep 17 00:00:00 2001
From: Andre <espietandre@gmail.com>
Date: Fri, 16 Jun 2023 00:00:20 -0400
Subject: [PATCH 13/16] fixed indentation for PolyType_0

---
 CommAlg/final_poly_type.lean | 15 ++++++++++-----
 1 file changed, 10 insertions(+), 5 deletions(-)

diff --git a/CommAlg/final_poly_type.lean b/CommAlg/final_poly_type.lean
index 4405e42..bfbef39 100644
--- a/CommAlg/final_poly_type.lean
+++ b/CommAlg/final_poly_type.lean
@@ -151,9 +151,11 @@ lemma PolyType_0 (f : ℤ → ℤ) : (PolyType f 0) ↔ (∃ (c : ℤ), ∃ (N :
   · 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)⟩
+      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)]⟩
+      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
@@ -162,10 +164,13 @@ lemma PolyType_0 (f : ℤ → ℤ) : (PolyType f 0) ↔ (∃ (c : ℤ), ∃ (N :
         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
+      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⟩
+    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⟩
 
 
 

From 04bda915d14865967076122446152a5dd830213c Mon Sep 17 00:00:00 2001
From: chelseaandmadrid <53058005+chelseaandmadrid@users.noreply.github.com>
Date: Thu, 15 Jun 2023 21:27:52 -0700
Subject: [PATCH 14/16] change statement of PolyType_0

---
 CommAlg/final_poly_type.lean | 69 ++++++++++++++++++++++--------------
 1 file changed, 43 insertions(+), 26 deletions(-)

diff --git a/CommAlg/final_poly_type.lean b/CommAlg/final_poly_type.lean
index 4405e42..377619c 100644
--- a/CommAlg/final_poly_type.lean
+++ b/CommAlg/final_poly_type.lean
@@ -145,8 +145,8 @@ lemma Poly_shifting (f : ℤ → ℤ) (g : ℤ → ℤ) (hf : PolyType f d) (s :
 
 -- set_option pp.all true in
 -- PolyType 0 = constant function
-lemma PolyType_0 (f : ℤ → ℤ) : (PolyType f 0) ↔ (∃ (c : ℤ), ∃ (N : ℤ), ∀ (n : ℤ), 
-    (N ≤ n → f n = c) ∧ c ≠ 0) := by
+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
@@ -182,14 +182,11 @@ lemma Δ_1 (f : ℤ → ℤ) (d : ℕ): d > 0 → PolyType f d → PolyType (Δ
 
 
 
-lemma foo (f : ℤ → ℤ) (s : ℕ) : Δ (Δ f 1) s = (Δ f (s + 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
@@ -205,12 +202,9 @@ lemma foofoo (d : ℕ) : (f : ℤ → ℤ) → (PolyType f d) → (PolyType (Δ
       clear hf
       specialize hd (Δ f 1)
       have this4 : PolyType (Δ (Δ f 1) d) 0 := by tauto
-      rw [foo] at this4
+      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 := by
   intro h
   have this : ∀ (d : ℕ), ∀ (f :ℤ → ℤ), (PolyType f d) → (PolyType (Δ f d) 0) := by 
@@ -222,37 +216,60 @@ lemma Δ_d_PolyType_d_to_PolyType_0 (f : ℤ → ℤ) (d : ℕ): PolyType f d 
 
 
 
-
--- [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
-  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
+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
-  · rw [PolyType_0]
+  · intro f
+    intro h
+    rcases h with ⟨c, N, hh⟩
+    rw [PolyType_0]
     use c
     use N
     tauto
 
   -- Induction step
-  · sorry
+  · 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
+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
+  have this1 : (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ), (N ≤ n → (Δ f d) n = c)) ∧ c ≠ 0) := by
     rw [←PolyType_0]
     exact this
   exact this1

From de995bf2f33858d41766845a1e793d6e91f34a25 Mon Sep 17 00:00:00 2001
From: Andre <espietandre@gmail.com>
Date: Fri, 16 Jun 2023 00:28:44 -0400
Subject: [PATCH 15/16] fixed some formatting

---
 CommAlg/final_poly_type.lean | 74 +-----------------------------------
 1 file changed, 2 insertions(+), 72 deletions(-)

diff --git a/CommAlg/final_poly_type.lean b/CommAlg/final_poly_type.lean
index bfbef39..40f66e7 100644
--- a/CommAlg/final_poly_type.lean
+++ b/CommAlg/final_poly_type.lean
@@ -139,12 +139,6 @@ lemma Poly_shifting (f : ℤ → ℤ) (g : ℤ → ℤ) (hf : PolyType f d) (s :
   rcases hh with ⟨N,ss⟩
   sorry
 
-
-
-
-
--- set_option pp.all true in
--- PolyType 0 = constant function
 lemma PolyType_0 (f : ℤ → ℤ) : (PolyType f 0) ↔ (∃ (c : ℤ), ∃ (N : ℤ), ∀ (n : ℤ), 
     (N ≤ n → f n = c) ∧ c ≠ 0) := by
   constructor
@@ -172,28 +166,16 @@ lemma PolyType_0 (f : ℤ → ℤ) : (PolyType f 0) ↔ (∃ (c : ℤ), ∃ (N :
       => 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
 
-
-
-
 lemma foo (f : ℤ → ℤ) (s : ℕ) : Δ (Δ f 1) s = (Δ f (s + 1)) := by
   sorry
 
-
-
-
-
 -- Δ of d times maps polynomial of degree d to polynomial of degree 0
 lemma foofoo (d : ℕ) : (f : ℤ → ℤ) → (PolyType f d) → (PolyType (Δ f d) 0):= by
   induction' d with d hd
@@ -214,19 +196,7 @@ lemma foofoo (d : ℕ) : (f : ℤ → ℤ) → (PolyType f d) → (PolyType (Δ
       tauto
     tauto
 
-
-
-lemma Δ_d_PolyType_d_to_PolyType_0 (f : ℤ → ℤ) (d : ℕ): PolyType f d → PolyType (Δ f d) 0 := by
-  intro h
-  have this : ∀ (d : ℕ), ∀ (f :ℤ → ℤ), (PolyType f d) → (PolyType (Δ f d) 0) := by 
-    exact foofoo
-  specialize this d f
-  tauto
-
-
-
-
-
+lemma Δ_d_PolyType_d_to_PolyType_0 (f : ℤ → ℤ) (d : ℕ): PolyType f d → PolyType (Δ f d) 0 := fun h => (foofoo d f) h
 
 -- [BH, 4.1.2] (a) => (b)
 -- Δ^d f (n) = c for some nonzero integer c for n >> 0 → f is of polynomial type d
@@ -248,8 +218,6 @@ lemma a_to_b (f : ℤ → ℤ) (d : ℕ) : (∃ (c : ℤ), ∃ (N : ℤ), ∀ (n
   -- 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
@@ -263,41 +231,14 @@ lemma b_to_a (f : ℤ → ℤ) (d : ℕ) : PolyType f d → (∃ (c : ℤ), ∃
   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
--- variable {R M N : Type _} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N]
---   (f : M →[R] N)
 open LinearMap
--- variable {R M : Type _} [CommRing R] [AddCommGroup M] [Module R M]
--- noncomputable def length := Set.chainHeight {M' : Submodule R M | M' < ⊤}
-
 
 -- 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 ℤ ℤ
--- #eval length ℤ ℤ
-
-
--- @[ext]
--- structure SES (R : Type _) [CommRing R] where
---   A : Type _
---   B : Type _
---   C : Type _
---   f : A →ₗ[R] B
---   g : B →ₗ[R] C
--- left_exact : LinearMap.ker f = 0
--- middle_exact : LinearMap.range f = LinearMap.ker g
--- right_exact : LinearMap.range g = C
-
-
 
 -- Definition of a SES (Short Exact Sequence)
 -- @[ext]
@@ -309,10 +250,6 @@ structure SES {R A B C : Type _} [CommRing R] [AddCommGroup A] [AddCommGroup B]
   middle_exact : LinearMap.range f = LinearMap.ker g
   right_exact : LinearMap.range g = ⊤
 
-#check SES.right_exact
-#check SES
-
-
 -- 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)
@@ -321,11 +258,4 @@ lemma length_Additive (R A B C : Type _) [CommRing R] [AddCommGroup A] [AddCommG
   rcases h with ⟨left_exact, middle_exact, right_exact⟩
   sorry
 
-end section
-
-
-
-
-
-
-
+end section
\ No newline at end of file

From 0089e927e1380662e1b8fcb4b1ba2b20404ed530 Mon Sep 17 00:00:00 2001
From: Andre <espietandre@gmail.com>
Date: Fri, 16 Jun 2023 00:44:03 -0400
Subject: [PATCH 16/16] fixed merge conflics

---
 CommAlg/final_poly_type.lean | 27 ---------------------------
 1 file changed, 27 deletions(-)

diff --git a/CommAlg/final_poly_type.lean b/CommAlg/final_poly_type.lean
index e192575..dcb0e70 100644
--- a/CommAlg/final_poly_type.lean
+++ b/CommAlg/final_poly_type.lean
@@ -139,11 +139,6 @@ lemma Poly_shifting (f : ℤ → ℤ) (g : ℤ → ℤ) (hf : PolyType f d) (s :
   rcases hh with ⟨N,ss⟩
   sorry
 
-
-
-
-
--- set_option pp.all true in
 -- PolyType 0 = constant function
 lemma PolyType_0 (f : ℤ → ℤ) : (PolyType f 0) ↔ (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ), 
     (N ≤ n → f n = c)) ∧ c ≠ 0) := by
@@ -179,11 +174,6 @@ lemma Δ_0 (f : ℤ → ℤ) : (Δ f 0) = f := by tauto
 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
@@ -208,23 +198,6 @@ lemma foofoo (d : ℕ) : (f : ℤ → ℤ) → (PolyType f d) → (PolyType (Δ
 
 lemma Δ_d_PolyType_d_to_PolyType_0 (f : ℤ → ℤ) (d : ℕ): PolyType f d → PolyType (Δ f d) 0 := fun h => (foofoo d f) h
 
--- [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
-  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
-lemma Δ_d_PolyType_d_to_PolyType_0 (f : ℤ → ℤ) (d : ℕ): PolyType f d → PolyType (Δ f d) 0 := by
-  intro h
-  have this : ∀ (d : ℕ), ∀ (f :ℤ → ℤ), (PolyType f d) → (PolyType (Δ f d) 0) := by 
-    exact foofoo
-  specialize this d f
-  tauto
-
 lemma foofoofoo (d : ℕ) : (f : ℤ → ℤ) → (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → (Δ f d) (n) = c) ∧ c ≠ 0) → (PolyType f d)  := by
   induction' d with d hd