SinTan1729/comm_alg
1
0
Fork 0
mirror of https://github.com/GTBarkley/comm_alg.git synced 2024-12-26 23:48:36 -06:00
Code Issues Projects Releases Packages Wiki Activity

added associated prime graded

Browse source
This commit is contained in:
monula95 dutta 2023-06-14 20:31:39 +00:00
parent 0773a97fb5
commit cf7f08df3e
1 changed files with 6 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
CommAlg/monalisa.lean
View file

@ -4,6 +4,8 @@ import Mathlib.Algebra.Module.GradedModule
import Mathlib.RingTheory.Ideal.AssociatedPrime import Mathlib.RingTheory.Ideal.AssociatedPrime
import Mathlib.RingTheory.Artinian import Mathlib.RingTheory.Artinian
import Mathlib.Order.Height import Mathlib.Order.Height
import Mathlib.Order.ConditionallyCompleteLattice.Basic
import Mathlib.RingTheory.FiniteType
noncomputable def length ( A : Type _) (M : Type _) noncomputable def length ( A : Type _) (M : Type _)
[CommRing A] [AddCommGroup M] [Module A M] := Set.chainHeight {M' : Submodule A M | M' < ⊤} [CommRing A] [AddCommGroup M] [Module A M] := Set.chainHeight {M' : Submodule A M | M' < ⊤}
@ -87,19 +89,15 @@ theorem hilbert_polynomial_0 (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [
: true := by : true := by
sorry 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
lemma Associated_prime_of_graded_is_graded lemma Associated_prime_of_graded_is_graded
(𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _)
[∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)]
[DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜] [DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜]
(p : associatedPrimes (⨁ i, 𝒜 i) (⨁ i, 𝓜 i)) (p : associatedPrimes (⨁ i, 𝒜 i) (⨁ i, 𝓜 i))
: (Ideal.IsHomogeneous' 𝒜 p) ∧ ((∃ (i : ℤ ), ∃ (x : 𝒜 i), p = (Submodule.span (⨁ i, 𝒜 i) {DirectSum.of x i}).annihilator)) := by : (Ideal.IsHomogeneous' 𝒜 p) ∧ ((∃ (i : ℤ ), ∃ (x : 𝒜 i), p = (Submodule.span (⨁ i, 𝒜 i) {DirectSum.of _ i x}).annihilator)) := by
sorry sorry
def standard_graded (𝒜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜] (I : Ideal (⨁ i, 𝒜 i)) := (⨁ i, 𝒜 i) -- def standard_graded {𝒜 : ℤ → Type _} [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜] (n : ℕ) :
-- Prop :=
-- ∃ J, Ideal.IsHomogeneous' 𝒜 J (J :Nonempty ((⨁ i, 𝒜 i) ≃+* (MvPolynomial (Fin n) (𝒜 0)) ⧸ J)