From bbfba6a2f722ecd933ed6feb4494885eb28e9675 Mon Sep 17 00:00:00 2001 From: monula95 dutta Date: Wed, 14 Jun 2023 21:50:00 +0000 Subject: [PATCH 1/7] added graded submodule --- CommAlg/monalisa.lean | 25 +++++++++++++++++++++++-- 1 file changed, 23 insertions(+), 2 deletions(-) diff --git a/CommAlg/monalisa.lean b/CommAlg/monalisa.lean index 68579da..4d5f4d8 100644 --- a/CommAlg/monalisa.lean +++ b/CommAlg/monalisa.lean @@ -58,7 +58,7 @@ 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 𝒜] @@ -98,4 +98,25 @@ lemma Associated_prime_of_graded_is_graded -- def standard_graded {𝒜 : ℤ → Type _} [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜] (n : ℕ) : -- Prop := --- ∃ J, Ideal.IsHomogeneous' 𝒜 J (J :Nonempty ((⨁ i, 𝒜 i) ≃+* (MvPolynomial (Fin n) (𝒜 0)) ⧸ J) + +def Component_of_graded_as_addsubgroup (𝒜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜] +(p : Ideal (⨁ i, 𝒜 i)) (hp : Ideal.IsHomogeneous' 𝒜 p) (i : ℤ) : AddSubgroup (𝒜 i) := 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 + +instance graded_submodule +(𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) (𝓝 : ℤ → Type _) +[∀ 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 : Submodule (𝒜 0) (𝓜 i)) := by + sorry + + From 79a6844707076920aa6f83bac6023eba1f04a358 Mon Sep 17 00:00:00 2001 From: monula95 dutta Date: Wed, 14 Jun 2023 22:00:39 +0000 Subject: [PATCH 2/7] graded local lemmma added --- CommAlg/monalisa.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/CommAlg/monalisa.lean b/CommAlg/monalisa.lean index 4d5f4d8..f3d174b 100644 --- a/CommAlg/monalisa.lean +++ b/CommAlg/monalisa.lean @@ -60,9 +60,9 @@ noncomputable def dimensionmodule ( A : Type _) (M : Type _) --- 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 +lemma graded_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 def PolyType (f : ℤ → ℤ) (d : ℕ ) := ∃ Poly : Polynomial ℚ, ∃ (N : ℤ), ∀ (n : ℤ), N ≤ n → f n = Polynomial.eval (n : ℚ) Poly ∧ d = Polynomial.degree Poly From 08711d7689ae4112d2d6e6a5297b512d8b3ccab9 Mon Sep 17 00:00:00 2001 From: GTBarkley Date: Wed, 14 Jun 2023 22:36:08 +0000 Subject: [PATCH 3/7] not_maximal_of_lt_prime in dim_le_one_of_dimLEOne --- CommAlg/krull.lean | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index 8da4d27..83902bb 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -176,8 +176,8 @@ lemma dim_eq_zero_iff [Nontrivial R] : krullDim R = 0 ↔ ∀ I : PrimeSpectrum rw [←WithBot.coe_le_coe,←hn] at this change (0 : WithBot ℕ∞) ≤ _ at this constructor <;> intro h' - rw [h'] - exact le_antisymm h' this + . rw [h'] + . exact le_antisymm h' this @[simp] lemma field_prime_bot {K: Type _} [Field K] (P : Ideal K) : IsPrime P ↔ P = ⊥ := by @@ -259,9 +259,7 @@ lemma dim_le_one_of_dimLEOne : Ring.DimensionLEOne R → krullDim R ≤ 1 := by change q0.asIdeal < q1.asIdeal at hc1 have q1nbot := Trans.trans (bot_le : ⊥ ≤ q0.asIdeal) hc1 specialize H q1.asIdeal (bot_lt_iff_ne_bot.mp q1nbot) q1.IsPrime - apply IsPrime.ne_top p.IsPrime - apply (IsCoatom.lt_iff H.out).mp - exact hc2 + exact (not_maximal_of_lt_prime p.IsPrime hc2) H lemma dim_le_one_of_pid [IsDomain R] [IsPrincipalIdealRing R] : krullDim R ≤ 1 := by rw [dim_le_one_iff] From 89d7be5bc9a03189dd345fd63db0a8d4f7bac552 Mon Sep 17 00:00:00 2001 From: GTBarkley Date: Thu, 15 Jun 2023 00:40:57 +0000 Subject: [PATCH 4/7] added docstrings to krull.lean --- CommAlg/krull.lean | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index 83902bb..b4227aa 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -55,6 +55,7 @@ lemma le_krullDim_iff' (R : Type _) [CommRing R] (n : ℕ∞) : lemma height_le_krullDim (I : PrimeSpectrum R) : height I ≤ krullDim R := le_iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) I +/-- The Krull dimension of a local ring is the height of its maximal ideal. -/ lemma krullDim_eq_height [LocalRing R] : krullDim R = height (closedPoint R) := by apply le_antisymm . rw [krullDim_le_iff'] @@ -65,6 +66,8 @@ lemma krullDim_eq_height [LocalRing R] : krullDim R = height (closedPoint R) := exact I.2.1 . simp only [height_le_krullDim] +/-- The height of a prime `𝔭` is greater than `n` if and only if there is a chain of primes less than `𝔭` + with length `n + 1`. -/ lemma lt_height_iff' {𝔭 : PrimeSpectrum R} {n : ℕ∞} : height 𝔭 > n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by rcases n with _ | n @@ -87,6 +90,7 @@ height 𝔭 > n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ norm_cast at hc tauto +/-- Form of `lt_height_iff''` for rewriting with the height coerced to `WithBot ℕ∞`. -/ lemma lt_height_iff'' {𝔭 : PrimeSpectrum R} {n : ℕ∞} : height 𝔭 > (n : WithBot ℕ∞) ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by show (_ < _) ↔ _ @@ -96,9 +100,11 @@ height 𝔭 > (n : WithBot ℕ∞) ↔ ∃ c : List (PrimeSpectrum R), c.Chain' #check height_le_krullDim --some propositions that would be nice to be able to eventually +/-- The prime spectrum of the zero ring is empty. -/ lemma primeSpectrum_empty_of_subsingleton (x : PrimeSpectrum R) [Subsingleton R] : False := x.1.ne_top_iff_one.1 x.2.1 <| Eq.substr (Subsingleton.elim 1 (0 : R)) x.1.zero_mem +/-- A CommRing has empty prime spectrum if and only if it is the zero ring. -/ lemma primeSpectrum_empty_iff : IsEmpty (PrimeSpectrum R) ↔ Subsingleton R := by constructor . contrapose @@ -122,17 +128,20 @@ lemma dim_eq_bot_iff : krullDim R = ⊥ ↔ Subsingleton R := by . rw [h.forall_iff] trivial +/-- Nonzero rings have Krull dimension in ℕ∞ -/ lemma krullDim_nonneg_of_nontrivial (R : Type _) [CommRing R] [Nontrivial R] : ∃ n : ℕ∞, Ideal.krullDim R = n := by have h := dim_eq_bot_iff.not.mpr (not_subsingleton R) lift (Ideal.krullDim R) to ℕ∞ using h with k use k +/-- An ideal which is less than a prime is not a maximal ideal. -/ lemma not_maximal_of_lt_prime {p : Ideal R} {q : Ideal R} (hq : IsPrime q) (h : p < q) : ¬IsMaximal p := by intro hp apply IsPrime.ne_top hq apply (IsCoatom.lt_iff hp.out).mp exact h +/-- Krull dimension is ≤ 0 if and only if all primes are maximal. -/ lemma dim_le_zero_iff : krullDim R ≤ 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal I.asIdeal := by show ((_ : WithBot ℕ∞) ≤ (0 : ℕ)) ↔ _ rw [krullDim_le_iff R 0] @@ -168,6 +177,7 @@ lemma dim_le_zero_iff : krullDim R ≤ 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal apply not_maximal_of_lt_prime I.IsPrime exact hc2 +/-- For a nonzero ring, Krull dimension is 0 if and only if all primes are maximal. -/ lemma dim_eq_zero_iff [Nontrivial R] : krullDim R = 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal I.asIdeal := by rw [←dim_le_zero_iff] obtain ⟨n, hn⟩ := krullDim_nonneg_of_nontrivial R @@ -179,6 +189,7 @@ lemma dim_eq_zero_iff [Nontrivial R] : krullDim R = 0 ↔ ∀ I : PrimeSpectrum . rw [h'] . exact le_antisymm h' this +/-- In a field, the unique prime ideal is the zero ideal. -/ @[simp] lemma field_prime_bot {K: Type _} [Field K] (P : Ideal K) : IsPrime P ↔ P = ⊥ := by constructor @@ -190,6 +201,7 @@ lemma field_prime_bot {K: Type _} [Field K] (P : Ideal K) : IsPrime P ↔ P = rw [botP] exact bot_prime +/-- In a field, all primes have height 0. -/ lemma field_prime_height_zero {K: Type _} [Field K] (P : PrimeSpectrum K) : height P = 0 := by unfold height simp @@ -205,10 +217,12 @@ lemma field_prime_height_zero {K: Type _} [Field K] (P : PrimeSpectrum K) : heig have : J ≠ P := ne_of_lt JlP contradiction +/-- The Krull dimension of a field is 0. -/ lemma dim_field_eq_zero {K : Type _} [Field K] : krullDim K = 0 := by unfold krullDim simp [field_prime_height_zero] +/-- A domain with Krull dimension 0 is a field. -/ lemma domain_dim_zero.isField {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0) : IsField D := by by_contra x rw [Ring.not_isField_iff_exists_prime] at x @@ -230,6 +244,7 @@ lemma domain_dim_zero.isField {D: Type _} [CommRing D] [IsDomain D] (h: krullDim aesop contradiction +/-- A domain has Krull dimension 0 if and only if it is a field. -/ lemma domain_dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krullDim D = 0 ↔ IsField D := by constructor · exact domain_dim_zero.isField @@ -261,6 +276,7 @@ lemma dim_le_one_of_dimLEOne : Ring.DimensionLEOne R → krullDim R ≤ 1 := by specialize H q1.asIdeal (bot_lt_iff_ne_bot.mp q1nbot) q1.IsPrime exact (not_maximal_of_lt_prime p.IsPrime hc2) H +/-- The Krull dimension of a PID is at most 1. -/ lemma dim_le_one_of_pid [IsDomain R] [IsPrincipalIdealRing R] : krullDim R ≤ 1 := by rw [dim_le_one_iff] exact Ring.DimensionLEOne.principal_ideal_ring R From 37cc2c5a3c9a8e5de6900570f0ead7600b8d6e69 Mon Sep 17 00:00:00 2001 From: monula95 dutta Date: Thu, 15 Jun 2023 04:19:56 +0000 Subject: [PATCH 5/7] added graded morphism def --- CommAlg/monalisa.lean | 44 +++++++++++++++++++++++++++++++++++-------- 1 file changed, 36 insertions(+), 8 deletions(-) diff --git a/CommAlg/monalisa.lean b/CommAlg/monalisa.lean index f3d174b..7a8635e 100644 --- a/CommAlg/monalisa.lean +++ b/CommAlg/monalisa.lean @@ -4,6 +4,18 @@ import Mathlib.Algebra.Module.GradedModule import Mathlib.RingTheory.Ideal.AssociatedPrime import Mathlib.RingTheory.Artinian import Mathlib.Order.Height +import Mathlib.Algebra.Algebra.Subalgebra.Basic +import Mathlib.Algebra.Module.LinearMap + +instance {𝒜 : ℤ → Type _} [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜] : + Algebra (𝒜 0) (⨁ i, 𝒜 i) := + Algebra.ofModule' + (by + intro r x + sorry) + (by + intro r x + sorry) noncomputable def length ( A : Type _) (M : Type _) [CommRing A] [AddCommGroup M] [Module A M] := Set.chainHeight {M' : Submodule A M | M' < ⊤} @@ -96,13 +108,28 @@ lemma Associated_prime_of_graded_is_graded sorry --- def standard_graded {𝒜 : ℤ → Type _} [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜] (n : ℕ) : --- Prop := +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)) def Component_of_graded_as_addsubgroup (𝒜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜] (p : Ideal (⨁ i, 𝒜 i)) (hp : Ideal.IsHomogeneous' 𝒜 p) (i : ℤ) : AddSubgroup (𝒜 i) := 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 + + -- @ 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 @@ -111,12 +138,13 @@ instance Quotient_of_graded_is_graded : DirectSum.Gmodule 𝒜 (fun i => (𝒜 i)⧸(Component_of_graded_as_addsubgroup 𝒜 p hp i)) := by sorry -instance graded_submodule -(𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) (𝓝 : ℤ → Type _) -[∀ 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 : Submodule (𝒜 0) (𝓜 i)) := by +theorem quotient_hilbert_polynomial (d : ℕ) (d1 : 1 ≤ d) (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] +[DirectSum.GCommRing 𝒜] +[DirectSum.Gmodule 𝒜 𝓜] (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0)) (p : Ideal (⨁ i, 𝒜 i)) +(findim : dimensionmodule (⨁ i, 𝒜 i) (⨁ i, ((𝒜 i)⧸(Component_of_graded_as_addsubgroup 𝒜 p hp i)) = d) (hilb : ℤ → ℤ) + (Hhilb: hilbert_function 𝒜 𝓜 hilb) (homprime: HomogeneousPrime 𝒜 p) +: PolyType hilb (d - 1) := by sorry + From 40e26d86367baef91942d2aa1a7c9511afea3751 Mon Sep 17 00:00:00 2001 From: poincare-duality Date: Wed, 14 Jun 2023 21:32:22 -0700 Subject: [PATCH 6/7] Hahaha --- CommAlg/jayden(krull-dim-zero).lean | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/CommAlg/jayden(krull-dim-zero).lean b/CommAlg/jayden(krull-dim-zero).lean index eba40ab..f75912a 100644 --- a/CommAlg/jayden(krull-dim-zero).lean +++ b/CommAlg/jayden(krull-dim-zero).lean @@ -125,19 +125,23 @@ lemma Artinian_has_finite_max_ideal let m' : ℕ ↪ MaximalSpectrum R := Infinite.natEmbedding (MaximalSpectrum R) have m'inj := m'.injective let m'' : ℕ → Ideal R := fun n : ℕ ↦ ⨅ k ∈ range n, (m' k).asIdeal + let f : ℕ → Ideal R := fun n : ℕ ↦ (m' n).asIdeal + let F : Fin n → Ideal R := fun k ↦ (m' k).asIdeal have comaximal : ∀ i j : ℕ, i ≠ j → (m' i).asIdeal ⊔ (m' j).asIdeal = (⊤ : Ideal R) := by intro i j distinct apply Ideal.IsMaximal.coprime_of_ne - sorry - sorry - -- by_contra equal + exact (m' i).IsMaximal + exact (m' j).IsMaximal have : (m' i) ≠ (m' j) := by exact Function.Injective.ne m'inj distinct intro h apply this exact MaximalSpectrum.ext _ _ h - -- let g :`= Ideal.quotientInfRingEquivPiQuotient m' comaximal + have ∀ n : ℕ, (R ⧸ ⨅ (i : Fin n), (F n) i) ≃+* ((i : Fin n) → R ⧸ (F n) i) := by + sorry + -- (let F : Fin n → Ideal R := fun k : Fin n ↦ (m' k).asIdeal) + -- let g := Ideal.quotientInfRingEquivPiQuotient f comaximal -- Stacks Lemma 10.53.4: R Artinian => Jacobson ideal of R is nilpotent @@ -193,7 +197,7 @@ lemma dim_zero_Noetherian_iff_Artinian (R : Type _) [CommRing R] : constructor apply finite_length_is_Noetherian rwa [IsArtinian_iff_finite_length] at RisArtinian - sorry + sorry -- can use Grant's lemma dim_eq_zero_iff From 1f7a809e2c9ac2c91cdbdba17b72bba68564745d Mon Sep 17 00:00:00 2001 From: monula95 dutta Date: Thu, 15 Jun 2023 05:02:47 +0000 Subject: [PATCH 7/7] unified monalisa.lean and HilbertFunction.lean --- CommAlg/final_hil_pol.lean | 258 +++++++++++++++++++++++++++++++++++++ 1 file changed, 258 insertions(+) create mode 100644 CommAlg/final_hil_pol.lean diff --git a/CommAlg/final_hil_pol.lean b/CommAlg/final_hil_pol.lean new file mode 100644 index 0000000..591c6cc --- /dev/null +++ b/CommAlg/final_hil_pol.lean @@ -0,0 +1,258 @@ +import Mathlib.Order.KrullDimension +import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic +import Mathlib.Algebra.Module.GradedModule +import Mathlib.RingTheory.Ideal.AssociatedPrime +import Mathlib.RingTheory.Artinian +import Mathlib.Order.Height + + + +-- 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.")) + + + +open GradedMonoid.GSmul +open DirectSum + + + +-- @Definitions (to be classified) +section + +-- 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 +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 𝒜] + [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) + +lemma mylem (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] [DirectSum.GCommRing 𝒜] + [h : DirectSum.Gmodule 𝒜 𝓜] (i : ℤ) (a : 𝒜 0) (m : 𝓜 i) : + of _ _ (a • m) = of _ _ a • of _ _ m := by + refine' Eq.trans _ (Gmodule.of_smul_of 𝒜 𝓜 a m).symm + refine' of_eq_of_gradedMonoid_eq _ + exact Sigma.ext (zero_add _).symm <| eq_rec_heq _ _ + +instance tada2 (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] [DirectSum.GCommRing 𝒜] + [h : DirectSum.Gmodule 𝒜 𝓜] (i : ℤ ) : SMulWithZero (𝒜 0) (𝓜 i) := by + letI := SMulWithZero.compHom (⨁ i, 𝓜 i) (of 𝒜 0).toZeroHom + exact Function.Injective.smulWithZero (of 𝓜 i).toZeroHom Dfinsupp.single_injective (mylem 𝒜 𝓜 i) + +instance tada3 (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] [DirectSum.GCommRing 𝒜] + [h : DirectSum.Gmodule 𝒜 𝓜] (i : ℤ ): Module (𝒜 0) (𝓜 i) := by + letI := Module.compHom (⨁ j, 𝓜 j) (ofZeroRingHom 𝒜) + exact Dfinsupp.single_injective.module (𝒜 0) (of 𝓜 i) (mylem 𝒜 𝓜 i) + + +-- Definition of a Hilbert function of a graded module +section +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) + +noncomputable def dimensionmodule ( A : Type _) (M : Type _) + [CommRing A] [AddCommGroup M] [Module A M] := krullDim (PrimeSpectrum (A ⧸ ((⊤ : Submodule A M).annihilator)) ) +end + + + +-- 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] + + +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 +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 + + +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 𝒜] +(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) := by + sorry + + +-- @Existence of a chain of submodules of graded submoduels of a f.g graded R-mod M +lemma Exist_chain_of_graded_submodules (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) +[∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] + [DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜] + (fingen : IsNoetherian (⨁ i, 𝒜 i) (⨁ i, 𝓜 i)) + : ∃ (c : List (Submodule (⨁ i, 𝒜 i) (⨁ i, 𝓜 i))), c.Chain' (· < ·) ∧ ∀ M ∈ c, Ture := by + 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 +(𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) +[∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] +[DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜] +(p : associatedPrimes (⨁ i, 𝒜 i) (⨁ i, 𝓜 i)) + : (Ideal.IsHomogeneous' 𝒜 p) ∧ ((∃ (i : ℤ ), ∃ (x : 𝒜 i), p = (Submodule.span (⨁ i, 𝒜 i) {DirectSum.of _ i x}).annihilator)) := by + sorry + + + + + + + + + +-- @[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)] +[DirectSum.GCommRing 𝒜] +[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 + + +-- (reduced version) [BH, 4.1.3] when d ≥ 1 +-- If M is a finite graed R-Mod of dimension d ≥ 1, and M = R⧸ 𝓅 for a graded prime ideal 𝓅, then the Hilbert function H(M, n) is of polynomial type (d - 1) +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)) +(fingen : IsNoetherian (⨁ i, 𝒜 i) (⨁ i, 𝓜 i)) +(findim : dimensionmodule (⨁ i, 𝒜 i) (⨁ i, 𝓜 i) = d) +(hilb : ℤ → ℤ) (Hhilb: hilbert_function 𝒜 𝓜 hilb) +(p : Ideal (⨁ i, 𝒜 i)) (hp : Ideal.IsHomogeneous' 𝒜 p) +(hm : 𝓜 = (fun i => (𝒜 i)⧸(Component_of_graded_as_addsubgroup 𝒜 p hp i))) +: PolyType hilb (d - 1) := by + sorry + + +-- @[BH, 4.1.3] when d = 0 +-- 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)) +(fingen : IsNoetherian (⨁ i, 𝒜 i) (⨁ i, 𝓜 i)) +(findim : dimensionmodule (⨁ i, 𝒜 i) (⨁ i, 𝓜 i) = 0) +(hilb : ℤ → ℤ) (Hhilb : hilbert_function 𝒜 𝓜 hilb) +: (∃ (N : ℤ), ∀ (n : ℤ), n ≥ N → hilb n = 0) := by + sorry + + +-- (reduced version) [BH, 4.1.3] when d = 0 +-- If M is a finite graed R-Mod of dimension zero, and M = R⧸ 𝓅 for a graded prime ideal 𝓅, then the Hilbert function H(M, n) = 0 for n >> 0 +theorem Hilbert_polynomial_d_0_reduced +(𝒜 : ℤ → 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 : ℤ → ℤ) (Hhilb : hilbert_function 𝒜 𝓜 hilb) +(p : Ideal (⨁ i, 𝒜 i)) (hp : Ideal.IsHomogeneous' 𝒜 p) +(hm : 𝓜 = (fun i => (𝒜 i)⧸(Component_of_graded_as_addsubgroup 𝒜 p hp i))) +: (∃ (N : ℤ), ∀ (n : ℤ), n ≥ N → hilb n = 0) := by + sorry + + + + + + + + + + + + + + + + + +