Test

comm_alg/Defhil.lean

@@ -1,23 +1,15 @@
 import Mathlib
+import Mathlib.RingTheory.Ideal.Basic
+import Mathlib.RingTheory.Ideal.Operations
+import Mathlib.LinearAlgebra.Finsupp
+import Mathlib.RingTheory.GradedAlgebra.Basic
+import Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal
+
+
+
 
 variable {R : Type _} (M A B C : Type _) [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup A] [Module R A] [AddCommGroup B] [Module R B] [AddCommGroup C] [Module R C]
-variable (A' B' C' : ModuleCat R)
-#check ModuleCat.of R A
 
-example : Module R A' := inferInstance
-
-#check ModuleCat.of R B
-
-example : Module R B' := inferInstance
-
-#check ModuleCat.of R C
-
-example : Module R C' := inferInstance
-
-namespace CategoryTheory
-
-noncomputable instance abelian : Abelian (ModuleCat.{v} R) := inferInstance
-noncomputable instance haszero : Limits.HasZeroMorphisms (ModuleCat.{v} R) := inferInstance
 
 #check (A B : Submodule _ _) → (A ≤ B)
 
@@ -25,17 +17,13 @@ noncomputable instance haszero : Limits.HasZeroMorphisms (ModuleCat.{v} R) := in
 
 #check krullDim (Submodule _ _)
 
-noncomputable def length := krullDim (Submodule R M) 
+noncomputable def length := Set.chainHeight {M' : Submodule R M | M' < ⊤}
- 
-open ZeroObject
-
-namespace HasZeroMorphisms
 
 open LinearMap
 
 #check length M
 
-#check ModuleCat.of R
 
-lemma length_additive_shortexact {f : A ⟶ B} {g : B ⟶ C} (h : ShortExact f g) : length B = length A + length C := sorry
+
+--lemma length_additive_shortexact {f : A ⟶ B} {g : B ⟶ C} (h : ShortExact f g) : length B = length A + length C := sorry
 

comm_alg/hilpol.lean

@@ -1,14 +1,41 @@
-import Mathlib
+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
 
+variable {ι σ R A : Type _}
 
---class GradedRing 
+section HomogeneousDef
 
-variable [GradedRing S]
+variable [Semiring A]
 
-namespace DirectSum
+variable [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ℤ → σ)
 
-namespace ideal
+variable [GradedRing 𝒜]
 
-def S_+ := ⊕ (i ≥ 0) S_i
+variable (I : HomogeneousIdeal 𝒜)
 
-lemma  A set of homogeneous elements fi∈S+ generates S as an algebra over S0 ↔ they generate S+ as an ideal of S.
+-- def Ideal.IsHomogeneous : Prop :=
+-- ∀ (i : ι) ⦃r : A⦄, r ∈ I → (DirectSum.decompose 𝒜 r i : A) ∈ I
+-- #align ideal.is_homogeneous Ideal.IsHomogeneous
+
+-- structure HomogeneousIdeal extends Submodule A A where
+-- is_homogeneous' : Ideal.IsHomogeneous 𝒜 toSubmodule
+
+--#check Ideal.IsPrime hI
+
+def HomogeneousPrime (I : Ideal A):= Ideal.IsPrime I
+
+def HomogeneousMax (I : Ideal A):= Ideal.IsMaximal 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]