Merge branch 'monalisa' of github.com:GTBarkley/comm_alg into monalisa

CommAlg/monalisa.lean

@@ -1,8 +1,5 @@
 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
@@ -11,11 +8,6 @@ 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
-import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
 import Mathlib.RingTheory.FiniteType
 import Mathlib.Order.Height
 import Mathlib.RingTheory.PrincipalIdealDomain
@@ -25,27 +17,12 @@ import Mathlib.RingTheory.Localization.AtPrime
 import Mathlib.Order.ConditionallyCompleteLattice.Basic
 import Mathlib.Algebra.DirectSum.Ring
 import Mathlib.RingTheory.Ideal.LocalRing
-import Mathlib
+--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
 
 
 
@@ -53,11 +30,14 @@ import Mathlib.RingTheory.Ideal.Operations
 noncomputable def length ( A : Type _) (M : Type _)
  [CommRing A] [AddCommGroup M] [Module A M] :=  Set.chainHeight {M' : Submodule A M | M' < ⊤}
 
-
-def HomogeneousPrime { A σ : Type _} [CommRing A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ℤ → σ) [GradedRing 𝒜] (I : Ideal A):= (Ideal.IsPrime I) ∧ (Ideal.IsHomogeneous 𝒜 I)
+ 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 
 
 
-def HomogeneousMax { A σ : Type _} [CommRing A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ℤ → σ) [GradedRing 𝒜] (I : Ideal A):= (Ideal.IsMaximal I) ∧ (Ideal.IsHomogeneous 𝒜 I)
+def HomogeneousPrime (𝒜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜] (I : Ideal (⨁ i, 𝒜 i)):= (Ideal.IsPrime I) ∧ (Ideal.IsHomogeneous' 𝒜 I)
+
+
+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
@@ -67,6 +47,7 @@ open GradedMonoid.GSmul
 
 open DirectSum
 
+
 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)
@@ -88,32 +69,10 @@ instance tada3 (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGr
   letI := Module.compHom (⨁ j, 𝓜 j) (ofZeroRingHom 𝒜)
   exact Dfinsupp.single_injective.module (𝒜 0) (of 𝓜 i) (mylem 𝒜 𝓜 i)
 
-  -- (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0))
-
-noncomputable def dummyhil_function (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)]
-  [DirectSum.GCommRing 𝒜]
-  [DirectSum.Gmodule 𝒜 𝓜] (hilb : ℤ → ℕ∞) := ∀ i, hilb i = (length (𝒜 0) (𝓜 i))
-
-
-lemma hilbertz (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)]
-  [DirectSum.GCommRing 𝒜]
-  [DirectSum.Gmodule 𝒜 𝓜] 
-  (finlen : ∀ i, (length (𝒜 0) (𝓜 i)) < ⊤ ) : ℤ → ℤ := by
-  intro i
-  let h := dummyhil_function 𝒜 𝓜
-  simp  at h 
-  let n : ℤ → ℕ := fun i ↦ WithTop.untop _ (finlen i).ne
-  have hn : ∀ i, (n i : ℕ∞) = length (𝒜 0) (𝓜 i) := fun i ↦ WithTop.coe_untop _ _
-  have' := hn i
-  exact ((n i) : ℤ )
-
-
 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)
 
@@ -121,20 +80,38 @@ 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
 
 
-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
 
 
 
-theorem hilbert_polynomial (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)]
+theorem hilbert_polynomial (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 : ∃ d : ℕ , dimensionmodule (⨁ i, 𝒜 i) (⨁ i, 𝓜 i) = d):True := sorry
+[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
 
--- Semiring A]
 
--- variable [SetLike σ A]
+theorem hilbert_polynomial_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 : ℤ → ℤ)
+: true := by
+  sorry
+
+lemma ass_graded (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) 
+[∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)]
+[DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜]
+(p : associatedPrimes (⨁ i, 𝒜 i) (⨁ i, 𝓜 i)) : (HomogeneousMax 𝒜 p) := by
+sorry
+