rearranged defs

This commit is contained in:
monula95 dutta 2023-06-16 22:00:43 +00:00
parent 96d1b2d83c
commit e85ea6b119
2 changed files with 8 additions and 10 deletions

View file

@ -48,9 +48,6 @@ section
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
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 -- 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) [DirectSum.Gmodule 𝒜 𝓜] (i : ) : SMul (𝒜 0) (𝓜 i)
@ -77,14 +74,18 @@ instance tada3 (𝒜 : → Type _) (𝓜 : → Type _) [∀ i, AddCommGr
-- Definition of a Hilbert function of a graded module -- Definition of a Hilbert function of a graded module
section section
noncomputable def hilbert_function (𝒜 : → Type _) (𝓜 : → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] noncomputable def length ( A : Type _) (M : Type _)
[DirectSum.GCommRing 𝒜] [CommRing A] [AddCommGroup M] [Module A M] := Set.chainHeight {M' : Submodule A M | M' < }
[DirectSum.Gmodule 𝒜 𝓜] (hilb : ) := ∀ i, hilb i = (ENat.toNat (length (𝒜 0) (𝓜 i)))
noncomputable def dimensionmodule ( A : Type _) (M : Type _) noncomputable def dimensionmodule ( A : Type _) (M : Type _)
[CommRing A] [AddCommGroup M] [Module A M] := Ideal.krullDim (A (( : Submodule A M).annihilator)) [CommRing A] [AddCommGroup M] [Module A M] := Ideal.krullDim (A (( : Submodule A M).annihilator))
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)))
lemma lengthfield ( k : Type _) [Field k] : length (k) (k) = 1 := by lemma lengthfield ( k : Type _) [Field k] : length (k) (k) = 1 := by
sorry sorry
@ -227,9 +228,6 @@ instance : DirectSum.Gmodule 𝒜 (GradedOneComponent 𝒜) := by sorry
lemma Graded_local [StandardGraded 𝒜] (I : Ideal (⨁ i, 𝒜 i)) (hp : (HomogeneousMax 𝒜 I)) [∀ i, Module (𝒜 0) ((𝒜 i)(Component_of_graded_as_addsubgroup 𝒜 I hp.2 i))] (art: IsArtinianRing (𝒜 0)) : (∀ (i : ), (i ≠ 0 → Nonempty (((𝒜 i)(Component_of_graded_as_addsubgroup 𝒜 I hp.2 i)) →ₗ[𝒜 0] (𝒜 i))) ) := by lemma Graded_local [StandardGraded 𝒜] (I : Ideal (⨁ i, 𝒜 i)) (hp : (HomogeneousMax 𝒜 I)) [∀ i, Module (𝒜 0) ((𝒜 i)(Component_of_graded_as_addsubgroup 𝒜 I hp.2 i))] (art: IsArtinianRing (𝒜 0)) : (∀ (i : ), (i ≠ 0 → Nonempty (((𝒜 i)(Component_of_graded_as_addsubgroup 𝒜 I hp.2 i)) →ₗ[𝒜 0] (𝒜 i))) ) := by
sorry sorry
-- lemma Graded_local [StandardGraded 𝒜] (I : Ideal (⨁ i, 𝒜 i)) (hp : (HomogeneousMax 𝒜 I)) (art: IsArtinianRing (𝒜 0)) : (∀ (i : ), (i ≠ 0 → (Nonempty (((𝒜 i)(Component_of_graded_as_addsubgroup 𝒜 I hp.2 i)) →ₛₗ[𝒜 0] (𝒜 i)))) ∧ (i = 0 → Nonempty (((𝒜 i)(Component_of_graded_as_addsubgroup 𝒜 I hp.2 i)) →ₛₗ[𝒜 0] (𝒜 0 LocalRing.maximalIdeal (𝒜 0))))) := by
-- sorry
end end
lemma Quotient_of_graded_ringiso (𝒜 : → Type _) [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜](p : Ideal (⨁ i, 𝒜 i)) (hp : Ideal.IsHomogeneous' 𝒜 p) lemma Quotient_of_graded_ringiso (𝒜 : → Type _) [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜](p : Ideal (⨁ i, 𝒜 i)) (hp : Ideal.IsHomogeneous' 𝒜 p)

View file

@ -31,7 +31,7 @@ theorem Hilbert_polynomial_d_0_reduced
-- have h0 : m.IsMaximal := LocalRing.maximalIdeal.isMaximal (𝒜 0) -- have h0 : m.IsMaximal := LocalRing.maximalIdeal.isMaximal (𝒜 0)
-- have h9 : IsField ((𝒜 0)m) := (Ideal.Quotient.maximal_ideal_iff_isField_quotient m).mp h0 -- have h9 : IsField ((𝒜 0)m) := (Ideal.Quotient.maximal_ideal_iff_isField_quotient m).mp h0
-- set k := ((𝒜 0)m) -- set k := ((𝒜 0)m)
have hilb n -- have hilb n
sorry sorry