From b6bbf7af8c1d08ac35f49898d632f4cedb1d8f9a Mon Sep 17 00:00:00 2001
From: monula95 dutta <monula95@gmail.com>
Date: Wed, 14 Jun 2023 04:49:17 +0000
Subject: [PATCH] udpated def final
---
.docker/test.lean | 10 ++++++++--
1 file changed, 8 insertions(+), 2 deletions(-)
diff --git a/.docker/test.lean b/.docker/test.lean
index 888270c..d3a272e 100644
--- a/.docker/test.lean
+++ b/.docker/test.lean
@@ -90,16 +90,17 @@ instance tada3 (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGr
-- (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0))
-noncomputable def hilbert_function (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)]
+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 := hilbert_function 𝒜 𝓜
+ 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 _ _
@@ -107,6 +108,11 @@ lemma hilbertz (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGr
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)