From 82a4ded17c0ee39277a7b5a5e9f804c46fa4091a Mon Sep 17 00:00:00 2001
From: chelseaandmadrid <53058005+chelseaandmadrid@users.noreply.github.com>
Date: Wed, 14 Jun 2023 21:30:17 -0700
Subject: [PATCH] Ultimate version of HilbertFunction

---
 HilbertFunction.lean | 43 +++++++++++++++++++++++++++++++++++++++----
 1 file changed, 39 insertions(+), 4 deletions(-)

diff --git a/HilbertFunction.lean b/HilbertFunction.lean
index 78b5eec..ce68f8c 100644
--- a/HilbertFunction.lean
+++ b/HilbertFunction.lean
@@ -97,7 +97,21 @@ def HomogeneousMax (𝒜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [Direc
 -- rw [isNoetherian_iff_wellFounded, WellFounded.monotone_chain_condition]
 
 
-end
+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
@@ -106,6 +120,28 @@ def Component_of_graded_as_addsubgroup (𝒜 : ℤ → Type _)
 (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 𝒜]
@@ -114,7 +150,6 @@ instance Quotient_of_graded_is_graded
   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)]
@@ -131,8 +166,6 @@ lemma Exist_chain_of_graded_submodules (𝒜 : ℤ → Type _) (𝓜 : ℤ → T
   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
@@ -149,6 +182,8 @@ lemma Associated_prime_of_graded_is_graded
 
 
 
+
+
 -- @[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)]