Merge branch 'monalisa' of github.com:GTBarkley/comm_alg into monalisa

.gitignore

@@ -1,2 +1,4 @@
 /build
 /lake-packages/*
+.DS_Store
+.cache/

.vscode/settings.json

@@ -0,0 +1,3 @@
+{
+    "search.useIgnoreFiles": false
+}

CommAlg/grant.lean

@@ -0,0 +1,228 @@
+import Mathlib.Order.KrullDimension
+import Mathlib.Order.JordanHolder
+import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
+import Mathlib.Order.Height
+import CommAlg.krull
+
+
+#check (p q : PrimeSpectrum _) → (p ≤ q)
+#check Preorder (PrimeSpectrum _)
+
+-- Dimension of a ring
+#check krullDim (PrimeSpectrum _)
+
+-- Length of a module
+#check krullDim (Submodule _ _)
+
+#check JordanHolderLattice
+
+
+section Chains
+
+variable {α : Type _} [Preorder α] (s : Set α)
+
+def finFun_to_list {n : ℕ} : (Fin n → α) → List α := by sorry
+
+def series_to_chain : StrictSeries s → s.subchain
+| ⟨length, toFun, strictMono⟩ => 
+    ⟨ finFun_to_list (fun x => toFun x),
+      sorry⟩
+
+-- there should be a coercion from WithTop ℕ to WithBot (WithTop ℕ) but it doesn't seem to work
+-- it looks like this might be because someone changed the instance from CoeCT to Coe during the port
+-- actually it looks like we can coerce to WithBot (ℕ∞) fine
+lemma twoHeights : s ≠ ∅ → (some (Set.chainHeight s) : WithBot (WithTop ℕ)) = krullDim s := by
+  intro hs
+  unfold Set.chainHeight
+  unfold krullDim
+  have hKrullSome : ∃n, krullDim s = some n := by
+    
+    sorry
+  -- norm_cast
+  sorry
+
+end Chains
+
+section Krull
+
+variable (R : Type _) [CommRing R] (M : Type _) [AddCommGroup M] [Module R M]
+
+open Ideal
+
+-- chain of primes 
+#check height 
+
+lemma lt_height_iff {𝔭 : PrimeSpectrum R} {n : ℕ∞} :
+  height 𝔭 > n ↔ ∃ c : List (PrimeSpectrum R), c ∈ {I : PrimeSpectrum R | I < 𝔭}.subchain ∧ c.length = n + 1 := sorry
+
+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
+  . constructor <;> intro h <;> exfalso
+    . exact (not_le.mpr h) le_top
+    . -- change ∃c, _ ∧ _ ∧ ((List.length c : ℕ∞) = ⊤ + 1) at h
+      -- rw [WithTop.top_add] at h
+      tauto
+  have (m : ℕ∞) : m > some n ↔ m ≥ some (n + 1) := by
+    symm
+    show (n + 1 ≤ m ↔ _ )
+    apply ENat.add_one_le_iff
+    exact ENat.coe_ne_top _
+  rw [this]
+  unfold Ideal.height
+  show ((↑(n + 1):ℕ∞) ≤ _) ↔ ∃c, _ ∧ _ ∧ ((_ : WithTop ℕ) = (_:ℕ∞))
+  rw [{J | J < 𝔭}.le_chainHeight_iff]
+  show (∃ c, (List.Chain' _ c ∧ ∀𝔮, 𝔮 ∈ c → 𝔮 < 𝔭) ∧ _) ↔ _
+  -- have h := fun (c : List (PrimeSpectrum R)) => (@WithTop.coe_eq_coe _ (List.length c) n) 
+  constructor <;> rintro ⟨c, hc⟩ <;> use c --<;> tauto--<;> exact ⟨hc.1, by tauto⟩
+  . --rw [and_assoc]
+    -- show _ ∧ _ ∧ _
+    --exact ⟨hc.1, _⟩
+    tauto
+  . change _ ∧ _ ∧ (List.length c : ℕ∞) = n + 1 at hc
+    norm_cast at hc
+    tauto
+
+lemma lt_height_iff'' {𝔭 : PrimeSpectrum R} {n : ℕ∞} : 
+height 𝔭 > (n : WithBot ℕ∞) ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by
+  show (_ < _) ↔ _
+  rw [WithBot.coe_lt_coe]
+  exact lt_height_iff' _
+
+lemma height_le_iff {𝔭 : PrimeSpectrum R} {n : ℕ∞} : 
+  height 𝔭 ≤ n ↔ ∀ c : List (PrimeSpectrum R), c ∈ {I : PrimeSpectrum R | I < 𝔭}.subchain ∧ c.length = n + 1 := by
+  sorry
+
+lemma krullDim_nonneg_of_nontrivial [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
+
+-- lemma krullDim_le_iff' (R : Type _) [CommRing R] {n : WithBot ℕ∞} : 
+--   Ideal.krullDim R ≤ n ↔ (∀ c : List (PrimeSpectrum R), c.Chain' (· < ·) → c.length ≤ n + 1) := by
+--     sorry
+
+-- lemma krullDim_ge_iff' (R : Type _) [CommRing R] {n : WithBot ℕ∞} : 
+--   Ideal.krullDim R ≥ n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ c.length = n + 1 := sorry
+
+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
+
+lemma primeSpectrum_empty_iff : IsEmpty (PrimeSpectrum R) ↔ Subsingleton R := by
+  constructor
+  . contrapose
+    rw [not_isEmpty_iff, ←not_nontrivial_iff_subsingleton, not_not]
+    apply PrimeSpectrum.instNonemptyPrimeSpectrum
+  . intro h
+    by_contra hneg
+    rw [not_isEmpty_iff] at hneg
+    rcases hneg with ⟨a, ha⟩
+    exact primeSpectrum_empty_of_subsingleton R ⟨a, ha⟩
+
+/-- A ring has Krull dimension -∞ if and only if it is the zero ring -/
+lemma dim_eq_bot_iff : krullDim R = ⊥ ↔ Subsingleton R := by
+  unfold Ideal.krullDim
+  rw [←primeSpectrum_empty_iff, iSup_eq_bot]
+  constructor <;> intro h
+  . rw [←not_nonempty_iff]
+    rintro ⟨a, ha⟩
+    specialize h ⟨a, ha⟩
+    tauto
+  . rw [h.forall_iff]
+    trivial
+
+#check (sorry : False)
+#check (sorryAx)
+#check (4 : WithBot ℕ∞)
+#check List.sum
+#check (_ ∈ (_ : List _))
+variable (α : Type ) 
+#synth Membership α (List α)
+#check bot_lt_iff_ne_bot
+-- #check ((4 : ℕ∞) : WithBot (WithTop ℕ))
+-- #check ( (Set.chainHeight s) : WithBot (ℕ∞))
+
+/-- The converse of this is false, because the definition of "dimension ≤ 1" in mathlib
+  applies only to dimension zero rings and domains of dimension 1. -/
+lemma dim_le_one_of_dimLEOne :  Ring.DimensionLEOne R → krullDim R ≤ (1 : ℕ) := by
+  rw [krullDim_le_iff R 1]
+  -- unfold Ring.DimensionLEOne
+  intro H p
+  -- have Hp := H p.asIdeal
+  -- have Hp := fun h => (Hp h) p.IsPrime
+  apply le_of_not_gt
+  intro h
+  rcases ((lt_height_iff'' R).mp h) with ⟨c, ⟨hc1, hc2, hc3⟩⟩
+  norm_cast at hc3
+  rw [List.chain'_iff_get] at hc1
+  specialize hc1 0 (by rw [hc3]; simp)
+  -- generalize hq0 : List.get _ _ = q0 at hc1
+  set q0 : PrimeSpectrum R := List.get c { val := 0, isLt := _ }
+  set q1 : PrimeSpectrum R := List.get c { val := 1, isLt := _ } 
+  -- have hq0 : q0 ∈ c := List.get_mem _ _ _ 
+  -- have hq1 : q1 ∈ c := List.get_mem _ _ _
+  specialize hc2 q1 (List.get_mem _ _ _)
+  -- have aa := (bot_le : (⊥ : Ideal R) ≤ q0.asIdeal)
+  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
+  -- change q1.asIdeal < p.asIdeal at hc2
+  apply IsPrime.ne_top p.IsPrime
+  apply (IsCoatom.lt_iff H.out).mp
+  exact hc2
+  --refine Iff.mp radical_eq_top (?_ (id (Eq.symm hc3))) 
+end Krull
+
+section iSupWithBot
+
+variable {α : Type _} [CompleteSemilatticeSup α] {I : Type _} (f : I → α)
+
+#synth SupSet (WithBot ℕ∞)
+
+protected lemma WithBot.iSup_ge_coe_iff {a : α} : 
+  (a ≤ ⨆ i : I, (f i : WithBot α) ) ↔ ∃ i : I, f i ≥ a := by
+  rw [WithBot.coe_le_iff]
+  sorry
+
+end iSupWithBot
+
+section myGreatElab
+open Lean Meta Elab
+
+syntax (name := lhsStx) "lhs% " term:max : term
+syntax (name := rhsStx) "rhs% " term:max : term
+
+@[term_elab lhsStx, term_elab rhsStx]
+def elabLhsStx : Term.TermElab := fun stx expectedType? =>
+  match stx with
+  | `(lhs% $t) => do
+    let (lhs, _, eq) ← mkExpected expectedType?
+    discard <| Term.elabTermEnsuringType t eq
+    return lhs
+  | `(rhs% $t) => do
+    let (_, rhs, eq) ← mkExpected expectedType?
+    discard <| Term.elabTermEnsuringType t eq
+    return rhs
+  | _ => throwUnsupportedSyntax
+where
+  mkExpected expectedType? := do
+    let α ←
+      if let some expectedType := expectedType? then
+        pure expectedType
+      else
+        mkFreshTypeMVar
+    let lhs ← mkFreshExprMVar α
+    let rhs ← mkFreshExprMVar α
+    let u ← getLevel α
+    let eq := mkAppN (.const ``Eq [u]) #[α, lhs, rhs]
+    return (lhs, rhs, eq)
+
+#check lhs% (add_comm 1 2)
+#check rhs% (add_comm 1 2)
+#check lhs% (add_comm _ _ : _ = 1 + 2)
+
+example (x y : α) (h : x = y) : lhs% h = rhs% h := h
+
+def lhsOf {α : Sort _} {x y : α} (h : x = y) : α := x
+
+#check lhsOf (add_comm 1 2)

CommAlg/jayden(krull-dim-zero).lean

@@ -0,0 +1,186 @@
+import Mathlib.RingTheory.Ideal.Basic
+import Mathlib.RingTheory.Ideal.Operations
+import Mathlib.RingTheory.JacobsonIdeal
+import Mathlib.RingTheory.Noetherian
+import Mathlib.Order.KrullDimension
+import Mathlib.RingTheory.Artinian
+import Mathlib.RingTheory.Ideal.Quotient
+import Mathlib.RingTheory.Nilpotent
+import Mathlib.AlgebraicGeometry.PrimeSpectrum.Maximal
+import Mathlib.AlgebraicGeometry.PrimeSpectrum.Noetherian
+import Mathlib.Data.Finite.Defs
+import Mathlib.Order.Height
+import Mathlib.RingTheory.DedekindDomain.Basic
+import Mathlib.RingTheory.Localization.AtPrime
+import Mathlib.Order.ConditionallyCompleteLattice.Basic
+import Mathlib.Algebra.Ring.Pi
+import Mathlib.RingTheory.Finiteness
+
+
+namespace Ideal
+
+variable (R : Type _) [CommRing R] (P : PrimeSpectrum R)
+
+noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < P}
+
+noncomputable def krullDim (R : Type) [CommRing R] :
+     WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height R I
+
+-- Stacks Lemma 10.26.1 (Should already exists)
+-- (1) The closure of a prime P is V(P)
+-- (2) the irreducible closed subsets are V(P) for P prime
+-- (3) the irreducible components are V(P) for P minimal prime
+
+-- Stacks Definition 10.32.1: An ideal is locally nilpotent
+-- if every element is nilpotent
+class IsLocallyNilpotent (I : Ideal R) : Prop :=
+    h : ∀ x ∈ I, IsNilpotent x
+#check Ideal.IsLocallyNilpotent
+end Ideal
+
+
+-- Repeats the definition of the length of a module by Monalisa
+variable (R : Type _) [CommRing R] (I J : Ideal R)
+variable (M : Type _) [AddCommMonoid M] [Module R M]
+
+-- change the definition of length of a module
+namespace Module
+noncomputable def length := Set.chainHeight {M' : Submodule R M | M' < ⊤}
+end Module
+
+-- Stacks Lemma 10.31.5: R is Noetherian iff Spec(R) is a Noetherian space
+example [IsNoetherianRing R] :
+    TopologicalSpace.NoetherianSpace (PrimeSpectrum R) :=
+  inferInstance
+
+instance ring_Noetherian_of_spec_Noetherian
+    [TopologicalSpace.NoetherianSpace (PrimeSpectrum R)] :
+    IsNoetherianRing R where
+  noetherian := by sorry
+
+lemma ring_Noetherian_iff_spec_Noetherian : IsNoetherianRing R 
+    ↔ TopologicalSpace.NoetherianSpace (PrimeSpectrum R) := by
+    constructor
+    intro RisNoetherian
+    -- how do I apply an instance to prove one direction?
+
+
+-- Use TopologicalSpace.NoetherianSpace.exists_finset_irreducible :
+-- Every closed subset of a noetherian space is a finite union 
+-- of irreducible closed subsets.
+
+-- Stacks Lemma 10.32.5: R Noetherian. I,J ideals.
+--  If J ⊂ √I, then J ^ n ⊂ I for some n. In particular, locally nilpotent
+-- and nilpotent are the same for Noetherian rings
+lemma containment_radical_power_containment : 
+    IsNoetherianRing R ∧ J ≤ Ideal.radical I → ∃ n : ℕ, J ^ n ≤ I :=  by 
+    rintro ⟨RisNoetherian, containment⟩ 
+    rw [isNoetherianRing_iff_ideal_fg] at RisNoetherian
+    specialize RisNoetherian (Ideal.radical I)
+    -- rcases RisNoetherian with ⟨S, Sgenerates⟩
+    have containment2 : ∃ n : ℕ,  (Ideal.radical I) ^ n ≤ I := by
+      apply Ideal.exists_radical_pow_le_of_fg I RisNoetherian
+    cases' containment2 with n containment2'
+    have containment3 : J ^ n ≤ (Ideal.radical I) ^ n := by 
+      apply Ideal.pow_mono containment
+    use n
+    apply le_trans containment3 containment2'
+-- The above can be proven using the following quicker theorem that is in the wrong place.
+-- Ideal.exists_pow_le_of_le_radical_of_fG
+
+
+-- Stacks Lemma 10.52.6: I is a maximal ideal and IM = 0. Then length of M is
+-- the same as the dimension as a vector space over R/I,
+lemma length_eq_dim_if_maximal_annihilates {I : Ideal R} [Ideal.IsMaximal I] 
+    : I • (⊤ : Submodule R M) = 0
+     → Module.length R M = Module.rank R⧸I M⧸(I • (⊤ : Submodule R M)) := by sorry
+
+-- Does lean know that M/IM is a R/I module?
+
+-- Stacks Lemma 10.52.8: I is a finitely generated maximal ideal of R.
+-- M is a finite R-mod and I^nM=0. Then length of M is finite.
+lemma power_zero_finite_length : Ideal.FG I → Ideal.IsMaximal I → Module.Finite R M
+    → (∃ n : ℕ, (I ^ n) • (⊤ : Submodule R M) = 0)
+    → (∃ m : ℕ, Module.length R M ≤ m) := by
+    intro IisFG IisMaximal MisFinite power
+    rcases power with ⟨n, npower⟩
+    -- how do I get a generating set?
+
+
+-- Stacks Lemma 10.53.3: R is Artinian iff R has finitely many maximal ideals
+lemma IsArtinian_iff_finite_max_ideal : 
+    IsArtinianRing R ↔ Finite (MaximalSpectrum R) := by sorry
+
+-- Stacks Lemma 10.53.4: R Artinian => Jacobson ideal of R is nilpotent
+lemma Jacobson_of_Artinian_is_nilpotent : 
+    IsArtinianRing R → IsNilpotent (Ideal.jacobson (⊤ : Ideal R)) := by sorry
+
+-- Stacks Lemma 10.53.5: If R has finitely many maximal ideals and 
+-- locally nilpotent Jacobson radical, then R is the product of its localizations at 
+-- its maximal ideals. Also, all primes are maximal
+
+-- lemma product_of_localization_at_maximal_ideal : Finite (MaximalSpectrum R)
+--      ∧ 
+
+def jaydensRing : Type _ := sorry
+  -- ∀ I : MaximalSpectrum R, Localization.AtPrime R I
+
+instance : CommRing jaydensRing := sorry -- this should come for free, don't even need to state it
+
+def foo : jaydensRing ≃+* R where
+  toFun := _
+  invFun := _
+  left_inv := _
+  right_inv := _
+  map_mul' := _
+  map_add' := _
+      -- Ideal.IsLocallyNilpotent (Ideal.jacobson (⊤ : Ideal R)) → 
+      --  Pi.commRing (MaximalSpectrum R) Localization.AtPrime R I
+      -- := by sorry
+-- Haven't finished this.
+
+-- Stacks Lemma 10.53.6: R is Artinian iff R has finite length as an R-mod
+lemma IsArtinian_iff_finite_length : 
+    IsArtinianRing R ↔ (∃ n : ℕ, Module.length R R ≤ n) := by sorry 
+
+-- Lemma: if R has finite length as R-mod, then R is Noetherian
+lemma finite_length_is_Noetherian : 
+    (∃ n : ℕ, Module.length R R ≤ n) → IsNoetherianRing R := by sorry 
+
+-- Lemma: if R is Artinian then all the prime ideals are maximal
+lemma primes_of_Artinian_are_maximal : 
+    IsArtinianRing R → Ideal.IsPrime I → Ideal.IsMaximal I := by sorry
+
+-- Lemma: Krull dimension of a ring is the supremum of height of maximal ideals
+
+
+-- Stacks Lemma 10.60.5: R is Artinian iff R is Noetherian of dimension 0
+lemma dim_zero_Noetherian_iff_Artinian (R : Type _) [CommRing R] : 
+    IsNoetherianRing R ∧ Ideal.krullDim R = 0 ↔ IsArtinianRing R := by 
+    constructor
+    sorry
+    intro RisArtinian
+    constructor
+    apply finite_length_is_Noetherian
+    rwa [IsArtinian_iff_finite_length] at RisArtinian
+    sorry
+
+
+
+
+    
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+

CommAlg/krull.lean

@@ -0,0 +1,232 @@
+import Mathlib.RingTheory.Ideal.Operations
+import Mathlib.RingTheory.FiniteType
+import Mathlib.Order.Height
+import Mathlib.RingTheory.PrincipalIdealDomain
+import Mathlib.RingTheory.DedekindDomain.Basic
+import Mathlib.RingTheory.Ideal.Quotient
+import Mathlib.RingTheory.Localization.AtPrime
+import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
+import Mathlib.Order.ConditionallyCompleteLattice.Basic
+
+/- This file contains the definitions of height of an ideal, and the krull
+  dimension of a commutative ring.
+  There are also sorried statements of many of the theorems that would be
+  really nice to prove.
+  I'm imagining for this file to ultimately contain basic API for height and
+  krull dimension, and the theorems will probably end up other files,
+  depending on how long the proofs are, and what extra API needs to be
+  developed.
+-/
+
+namespace Ideal
+open LocalRing
+
+variable {R : Type _} [CommRing R] (I : PrimeSpectrum R)
+
+noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < I}
+
+noncomputable def krullDim (R : Type _) [CommRing R] : WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height I
+
+lemma height_def : height I = Set.chainHeight {J : PrimeSpectrum R | J < I} := rfl
+lemma krullDim_def (R : Type _) [CommRing R] : krullDim R = (⨆ (I : PrimeSpectrum R), height I : WithBot ℕ∞) := rfl
+lemma krullDim_def' (R : Type _) [CommRing R] : krullDim R = iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) := rfl
+
+noncomputable instance : CompleteLattice (WithBot (ℕ∞)) := WithBot.WithTop.completeLattice
+
+lemma height_le_of_le {I J : PrimeSpectrum R} (I_le_J : I ≤ J) : height I ≤ height J := by
+  apply Set.chainHeight_mono
+  intro J' hJ'
+  show J' < J
+  exact lt_of_lt_of_le hJ' I_le_J
+
+lemma krullDim_le_iff (R : Type _) [CommRing R] (n : ℕ) :
+  krullDim R ≤ n ↔ ∀ I : PrimeSpectrum R, (height I : WithBot ℕ∞) ≤ ↑n := iSup_le_iff (α := WithBot ℕ∞)
+
+lemma krullDim_le_iff' (R : Type _) [CommRing R] (n : ℕ∞) :
+  krullDim R ≤ n ↔ ∀ I : PrimeSpectrum R, (height I : WithBot ℕ∞) ≤ ↑n := iSup_le_iff (α := WithBot ℕ∞)
+
+lemma le_krullDim_iff (R : Type _) [CommRing R] (n : ℕ) :
+  n ≤ krullDim R ↔ ∃ I : PrimeSpectrum R, n ≤ (height I : WithBot ℕ∞) := by sorry
+
+lemma le_krullDim_iff' (R : Type _) [CommRing R] (n : ℕ∞) :
+  n ≤ krullDim R ↔ ∃ I : PrimeSpectrum R, n ≤ (height I : WithBot ℕ∞) := by sorry
+
+@[simp]
+lemma height_le_krullDim (I : PrimeSpectrum R) : height I ≤ krullDim R := 
+  le_iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) I
+
+lemma krullDim_eq_height [LocalRing R] : krullDim R = height (closedPoint R) := by
+  apply le_antisymm
+  . rw [krullDim_le_iff']
+    intro I
+    apply WithBot.coe_mono
+    apply height_le_of_le
+    apply le_maximalIdeal
+    exact I.2.1
+  . simp
+
+#check height_le_krullDim
+--some propositions that would be nice to be able to eventually
+
+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
+
+lemma primeSpectrum_empty_iff : IsEmpty (PrimeSpectrum R) ↔ Subsingleton R := by
+  constructor
+  . contrapose
+    rw [not_isEmpty_iff, ←not_nontrivial_iff_subsingleton, not_not]
+    apply PrimeSpectrum.instNonemptyPrimeSpectrum
+  . intro h
+    by_contra hneg
+    rw [not_isEmpty_iff] at hneg
+    rcases hneg with ⟨a, ha⟩
+    exact primeSpectrum_empty_of_subsingleton ⟨a, ha⟩
+
+/-- A ring has Krull dimension -∞ if and only if it is the zero ring -/
+lemma dim_eq_bot_iff : krullDim R = ⊥ ↔ Subsingleton R := by
+  unfold Ideal.krullDim
+  rw [←primeSpectrum_empty_iff, iSup_eq_bot]
+  constructor <;> intro h
+  . rw [←not_nonempty_iff]
+    rintro ⟨a, ha⟩
+    specialize h ⟨a, ha⟩
+    tauto
+  . rw [h.forall_iff]
+    trivial
+
+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
+
+lemma dim_eq_zero_iff [Nontrivial R] : krullDim R = 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal I.asIdeal := by
+  constructor <;> intro h
+  . intro I
+    sorry
+  . sorry
+  
+@[simp]
+lemma field_prime_bot {K: Type _} [Field K] (P : Ideal K) : IsPrime P ↔ P = ⊥ := by
+      constructor
+      · intro primeP
+        obtain T := eq_bot_or_top P
+        have : ¬P = ⊤ := IsPrime.ne_top primeP
+        tauto
+      · intro botP
+        rw [botP]
+        exact bot_prime
+
+lemma field_prime_height_zero {K: Type _} [Field K] (P : PrimeSpectrum K) : height P = 0 := by
+    unfold height
+    simp
+    by_contra spec
+    change _ ≠ _ at spec
+    rw [← Set.nonempty_iff_ne_empty] at spec
+    obtain ⟨J, JlP : J < P⟩ := spec
+    have P0 : IsPrime P.asIdeal := P.IsPrime
+    have J0 : IsPrime J.asIdeal := J.IsPrime
+    rw [field_prime_bot] at P0 J0
+    have : J.asIdeal = P.asIdeal := Eq.trans J0 (Eq.symm P0)
+    have : J = P := PrimeSpectrum.ext J P this
+    have : J ≠ P := ne_of_lt JlP
+    contradiction
+
+lemma dim_field_eq_zero {K : Type _} [Field K] : krullDim K = 0 := by
+  unfold krullDim
+  simp [field_prime_height_zero]
+
+lemma isField.dim_zero {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
+  obtain ⟨P, ⟨h1, primeP⟩⟩ := x
+  let P' : PrimeSpectrum D := PrimeSpectrum.mk P primeP
+  have h2 : P' ≠ ⊥ := by
+    by_contra a
+    have : P = ⊥ := by rwa [PrimeSpectrum.ext_iff] at a
+    contradiction
+  have pos_height : ¬ (height P') ≤ 0  := by
+    have : ⊥ ∈ {J | J < P'} := Ne.bot_lt h2
+    have : {J | J < P'}.Nonempty := Set.nonempty_of_mem this
+    unfold height
+    rw [←Set.one_le_chainHeight_iff] at this
+    exact not_le_of_gt (Iff.mp ENat.one_le_iff_pos this)
+  have nonpos_height : height P' ≤ 0 := by
+    have := height_le_krullDim P'
+    rw [h] at this
+    aesop
+  contradiction
+
+lemma dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krullDim D = 0 ↔ IsField D := by
+  constructor
+  · exact isField.dim_zero
+  · intro fieldD
+    let h : Field D := IsField.toField fieldD
+    exact dim_field_eq_zero
+
+#check Ring.DimensionLEOne
+-- This lemma is false!
+lemma dim_le_one_iff : krullDim R ≤ 1 ↔ Ring.DimensionLEOne R := sorry
+
+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
+  . constructor <;> intro h <;> exfalso
+    . exact (not_le.mpr h) le_top
+    . tauto
+  have (m : ℕ∞) : m > some n ↔ m ≥ some (n + 1) := by
+    symm
+    show (n + 1 ≤ m ↔ _ )
+    apply ENat.add_one_le_iff
+    exact ENat.coe_ne_top _
+  rw [this]
+  unfold Ideal.height
+  show ((↑(n + 1):ℕ∞) ≤ _) ↔ ∃c, _ ∧ _ ∧ ((_ : WithTop ℕ) = (_:ℕ∞))
+  rw [{J | J < 𝔭}.le_chainHeight_iff]
+  show (∃ c, (List.Chain' _ c ∧ ∀𝔮, 𝔮 ∈ c → 𝔮 < 𝔭) ∧ _) ↔ _
+  constructor <;> rintro ⟨c, hc⟩ <;> use c
+  . tauto
+  . change _ ∧ _ ∧ (List.length c : ℕ∞) = n + 1 at hc
+    norm_cast at hc
+    tauto
+
+lemma lt_height_iff'' {𝔭 : PrimeSpectrum R} {n : ℕ∞} : 
+height 𝔭 > (n : WithBot ℕ∞) ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by
+  show (_ < _) ↔ _
+  rw [WithBot.coe_lt_coe]
+  exact lt_height_iff'
+
+/-- The converse of this is false, because the definition of "dimension ≤ 1" in mathlib
+  applies only to dimension zero rings and domains of dimension 1. -/
+lemma dim_le_one_of_dimLEOne :  Ring.DimensionLEOne R → krullDim R ≤ (1 : ℕ) := by
+  rw [krullDim_le_iff R 1]
+  intro H p
+  apply le_of_not_gt
+  intro h
+  rcases (lt_height_iff''.mp h) with ⟨c, ⟨hc1, hc2, hc3⟩⟩
+  norm_cast at hc3
+  rw [List.chain'_iff_get] at hc1
+  specialize hc1 0 (by rw [hc3]; simp)
+  set q0 : PrimeSpectrum R := List.get c { val := 0, isLt := _ }
+  set q1 : PrimeSpectrum R := List.get c { val := 1, isLt := _ } 
+  specialize hc2 q1 (List.get_mem _ _ _)
+  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
+
+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
+
+lemma dim_le_dim_polynomial_add_one [Nontrivial R] :
+  krullDim R + 1 ≤ krullDim (Polynomial R) := sorry
+
+lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] :
+  krullDim R + 1 = krullDim (Polynomial R) := sorry
+
+lemma height_eq_dim_localization :
+  height I = krullDim (Localization.AtPrime I.asIdeal) := sorry
+
+lemma height_add_dim_quotient_le_dim : height I + krullDim (R ⧸ I.asIdeal) ≤ krullDim R := sorry

CommAlg/monalisa.lean

@@ -0,0 +1,140 @@
+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
+import Mathlib.RingTheory.Artinian
+import Mathlib.Algebra.Module.GradedModule
+import Mathlib.RingTheory.Noetherian
+import Mathlib.RingTheory.Finiteness
+import Mathlib.RingTheory.Ideal.Operations
+import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
+import Mathlib.RingTheory.FiniteType
+import Mathlib.Order.Height
+import Mathlib.RingTheory.PrincipalIdealDomain
+import Mathlib.RingTheory.DedekindDomain.Basic
+import Mathlib.RingTheory.Ideal.Quotient
+import Mathlib.RingTheory.Localization.AtPrime
+import Mathlib.Order.ConditionallyCompleteLattice.Basic
+import Mathlib.Algebra.DirectSum.Ring
+import Mathlib.RingTheory.Ideal.LocalRing
+import Mathlib
+import Mathlib.Algebra.MonoidAlgebra.Basic
+import Mathlib.Data.Finset.Sort
+import Mathlib.Order.Height
+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
+import Mathlib.RingTheory.Artinian
+import Mathlib.Algebra.Module.GradedModule
+import Mathlib.RingTheory.Noetherian
+import Mathlib.RingTheory.Finiteness
+import Mathlib.RingTheory.Ideal.Operations
+
+
+
+
+noncomputable def length ( A : Type _) (M : Type _)
+ [CommRing A] [AddCommGroup M] [Module A M] :=  Set.chainHeight {M' : Submodule A M | M' < ⊤}
+
+
+def HomogeneousPrime { A σ : Type _} [CommRing A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ℤ → σ) [GradedRing 𝒜] (I : Ideal A):= (Ideal.IsPrime I) ∧ (Ideal.IsHomogeneous 𝒜 I)
+
+
+def HomogeneousMax { A σ : Type _} [CommRing A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ℤ → σ) [GradedRing 𝒜] (I : Ideal A):= (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]
+
+open GradedMonoid.GSmul
+
+open DirectSum
+
+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)
+
+  -- (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0))
+
+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 := 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 _ _
+  have' := hn i
+  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)
+
+
+noncomputable def dimensionmodule ( A : Type _) (M : Type _)
+ [CommRing A] [AddCommGroup M] [Module A M] := krullDim (PrimeSpectrum (A ⧸ ((⊤ : Submodule A M).annihilator)) )
+
+--  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
+
+
+def PolyType (f : ℤ → ℤ) (d : ℕ) := ∃ Poly : Polynomial ℚ, ∃ (N : ℤ), ∀ (n : ℤ), N ≤ n → f n = Polynomial.eval (n : ℚ) Poly ∧ d = Polynomial.degree Poly
+
+
+
+theorem hilbert_polynomial (𝒜 : ℤ → 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 : ∃ d : ℕ , dimensionmodule (⨁ i, 𝒜 i) (⨁ i, 𝓜 i) = d):True := sorry
+
+-- Semiring A]
+
+-- variable [SetLike σ A]

CommAlg/resources.lean

@@ -0,0 +1,89 @@
+/-
+We don't want to reinvent the wheel, but finding
+things in Mathlib can be pretty annoying. This is
+a temporary file intended to be a dumping ground for
+useful lemmas and definitions
+-/
+import Mathlib.RingTheory.Ideal.Basic
+import Mathlib.RingTheory.Noetherian
+import Mathlib.RingTheory.Artinian
+import Mathlib.RingTheory.FiniteType
+import Mathlib.Order.Height
+import Mathlib.RingTheory.MvPolynomial.Basic
+import Mathlib.RingTheory.Ideal.Over
+import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
+import Mathlib.Algebra.Homology.ShortExact.Abelian
+
+variable {R M : Type _} [CommRing R] [AddCommGroup M] [Module R M]
+
+--ideals are defined
+#check Ideal R
+
+variable (I : Ideal R)
+
+--as are prime and maximal (they are defined as typeclasses)
+#check (I.IsPrime)
+#check (I.IsMaximal)
+
+--a module being Noetherian is also a class
+#check IsNoetherian M
+#check IsNoetherian I
+
+--a ring is Noetherian if it is Noetherian as a module over itself
+#check IsNoetherianRing R
+
+--ditto for Artinian
+#check IsArtinian M
+#check IsArtinianRing R
+
+--I can't find the theorem that an Artinian ring is noetherian. That could be a good
+--thing to add at some point
+
+
+
+--Here's the main defintion that will be helpful
+#check Set.chainHeight
+
+--this is the polynomial ring R[x]
+#check Polynomial R
+--this is the polynomial ring with variables indexed by ℕ
+#check MvPolynomial ℕ R
+--hopefully there's good communication between them
+
+
+--There's a preliminary version of the going up theorem
+#check Ideal.exists_ideal_over_prime_of_isIntegral
+
+--Theorems relating primes of a ring to primes of its localization
+#check PrimeSpectrum.localization_comap_injective
+#check PrimeSpectrum.localization_comap_range
+--Theorems relating primes of a ring to primes of a quotient
+#check PrimeSpectrum.range_comap_of_surjective
+
+--There's a lot of theorems about finite-type algebras
+#check Algebra.FiniteType.polynomial
+#check Algebra.FiniteType.mvPolynomial
+#check Algebra.FiniteType.of_surjective
+
+-- There is a notion of short exact sequences but the number of theorems are lacking
+-- For example, I couldn't find anything saying that for a ses 0 -> A -> B -> C -> 0
+-- of R-modules, A and C being FG implies that B is FG
+open CategoryTheory CategoryTheory.Limits CategoryTheory.Preadditive
+
+variable {𝒜 : Type _} [Category 𝒜] [Abelian 𝒜]
+variable {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} {h : LeftSplit f g} {h' : RightSplit f g}
+
+#check ShortExact
+#check ShortExact f g
+-- There are some notion of splitting as well
+#check Splitting
+#check LeftSplit
+#check LeftSplit f g
+-- And there is a theorem that left split implies splitting
+#check LeftSplit.splitting
+#check LeftSplit.splitting h
+-- Similar things are there for RightSplit as well
+#check RightSplit.splitting
+#check RightSplit.splitting h'
+-- There's also a theorem about ismorphisms between short exact sequences
+#check isIso_of_shortExact_of_isIso_of_isIso

CommAlg/sameer(artinian-rings).lean

@@ -0,0 +1,68 @@
+import Mathlib.RingTheory.Ideal.Basic
+import Mathlib.RingTheory.Noetherian
+import Mathlib.RingTheory.Artinian
+import Mathlib.RingTheory.Ideal.Quotient
+import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
+import Mathlib.RingTheory.DedekindDomain.DVR
+
+
+lemma FieldisArtinian (R : Type _) [CommRing R] (IsField : ):= by sorry
+
+
+lemma ArtinianDomainIsField (R : Type _) [CommRing R] [IsDomain R]
+(IsArt : IsArtinianRing R) : IsField (R) := by 
+-- Assume P is nonzero and R is Artinian
+-- Localize at P; Then R_P is Artinian; 
+-- Assume R_P is not a field 
+-- Then Jacobson Radical of R_P is nilpotent so it's maximal ideal is nilpotent
+-- Maximal ideal is zero since local ring is a domain
+-- a contradiction since P is nonzero
+-- Therefore, R is a field
+have maxIdeal := Ideal.exists_maximal R
+obtain ⟨m,hm⟩ := maxIdeal
+have h:= Ideal.primeCompl_le_nonZeroDivisors m 
+have artRP : IsDomain _ := IsLocalization.isDomain_localization h
+have h' : IsArtinianRing (Localization (Ideal.primeCompl m)) := inferInstance
+have h' : IsNilpotent (Ideal.jacobson (⊥ : Ideal (Localization 
+  (Ideal.primeCompl m)))):= IsArtinianRing.isNilpotent_jacobson_bot
+have := LocalRing.jacobson_eq_maximalIdeal (⊥ : Ideal (Localization 
+  (Ideal.primeCompl m))) bot_ne_top
+rw [this] at h'
+have := IsNilpotent.eq_zero h'
+rw [Ideal.zero_eq_bot, ← LocalRing.isField_iff_maximalIdeal_eq] at this
+by_contra h''
+--by_cases h'' : m = ⊥
+have := Ring.ne_bot_of_isMaximal_of_not_isField hm h'' 
+have := IsLocalization.AtPrime.not_isField R this (Localization (Ideal.primeCompl m))
+contradiction
+
+
+#check Ideal.IsPrime
+#check IsDomain
+
+lemma isArtinianRing_of_quotient_of_artinian (R : Type _) [CommRing R]
+    (I : Ideal R) (IsArt : IsArtinianRing R) : IsArtinianRing (R ⧸ I) :=
+  isArtinian_of_tower R (isArtinian_of_quotient_of_artinian R R I IsArt)
+
+lemma IsPrimeMaximal (R : Type _) [CommRing R] (P : Ideal R) 
+(IsArt : IsArtinianRing R) (isPrime : Ideal.IsPrime P) : Ideal.IsMaximal P := 
+by 
+-- if R is Artinian and P is prime then R/P is Integral Domain 
+-- which is Artinian Domain 
+-- R⧸P is a field by the above lemma
+-- P is maximal
+
+  have : IsDomain (R⧸P) := Ideal.Quotient.isDomain P
+  have artRP : IsArtinianRing (R⧸P) := by
+    exact isArtinianRing_of_quotient_of_artinian R P IsArt
+  
+
+-- Then R/I is Artinian 
+ --  have' : IsArtinianRing R ∧ Ideal.IsPrime I → IsDomain (R⧸I) := by
+
+-- R⧸I.IsArtinian → monotone_stabilizes_iff_artinian.R⧸I
+
+
+
+
+-- Use Stacks project proof since it's broken into lemmas

CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean

@@ -0,0 +1,52 @@
+import Mathlib.RingTheory.Ideal.Basic
+import Mathlib.Order.Height
+import Mathlib.RingTheory.PrincipalIdealDomain
+import Mathlib.RingTheory.DedekindDomain.Basic
+import Mathlib.RingTheory.Ideal.Quotient
+import Mathlib.RingTheory.Localization.AtPrime
+import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
+import Mathlib.Order.ConditionallyCompleteLattice.Basic
+
+namespace Ideal
+
+variable {R : Type _} [CommRing R] (I : PrimeSpectrum R)
+noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < I}
+noncomputable def krullDim (R : Type) [CommRing R] : WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height I
+
+lemma height_def : height I = Set.chainHeight {J : PrimeSpectrum R | J < I} := rfl
+lemma krullDim_def (R : Type) [CommRing R] : krullDim R = (⨆ (I : PrimeSpectrum R), height I : WithBot ℕ∞) := rfl
+lemma krullDim_def' (R : Type) [CommRing R] : krullDim R = iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) := rfl
+
+noncomputable instance : CompleteLattice (WithBot (ℕ∞)) := WithBot.WithTop.completeLattice
+
+lemma dim_le_dim_polynomial_add_one [Nontrivial R] :
+  krullDim R + 1 ≤ krullDim (Polynomial R) := sorry -- Others are working on it
+
+-- private lemma sum_succ_of_succ_sum {ι : Type} (a : ℕ∞) [inst : Nonempty ι] :
+--       (⨆ (x : ι), a + 1) = (⨆ (x : ι), a) + 1 := by
+--   have : a + 1 = (⨆ (x : ι), a) + 1 := by rw [ciSup_const]
+--   have : a + 1 = (⨆ (x : ι), a + 1) := Eq.symm ciSup_const
+--   simp
+
+lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] :
+  krullDim R + 1 = krullDim (Polynomial R) := by
+  rw [le_antisymm_iff]
+  constructor
+  · exact dim_le_dim_polynomial_add_one
+  · unfold krullDim
+    have htPBdd : ∀ (P : PrimeSpectrum (Polynomial R)), (height P : WithBot ℕ∞) ≤ (⨆ (I : PrimeSpectrum R), ↑(height I + 1)) := by
+      intro P
+      have : ∃ (I : PrimeSpectrum R), (height P : WithBot ℕ∞) ≤ ↑(height I + 1) := by
+        sorry
+      obtain ⟨I, IP⟩ := this
+      have : (↑(height I + 1) : WithBot ℕ∞) ≤ ⨆ (I : PrimeSpectrum R), ↑(height I + 1) := by
+        apply @le_iSup (WithBot ℕ∞) _ _ _ I
+      apply ge_trans this IP
+    have oneOut : (⨆ (I : PrimeSpectrum R), (height I : WithBot ℕ∞) + 1) ≤ (⨆ (I : PrimeSpectrum R), ↑(height I)) + 1 := by
+      have : ∀ P : PrimeSpectrum R, (height P : WithBot ℕ∞) + 1 ≤ (⨆ (I : PrimeSpectrum R), ↑(height I)) + 1 :=
+        fun P ↦ (by apply add_le_add_right (@le_iSup (WithBot ℕ∞) _ _ _ P) 1)
+      apply iSup_le
+      apply this
+    simp
+    intro P
+    exact ge_trans oneOut (htPBdd P)

README.md

@@ -0,0 +1,54 @@
+# Commutative algebra in Lean
+
+Welcome to the repository for adding definitions and theorems related to Krull dimension and Hilbert polynomials to mathlib.
+
+We start the commutative algebra project with a list of important definitions and theorems and go from there.
+
+Feel free to add, modify, and expand this file. Below are starting points for the project:
+
+- Definitions of an ideal, prime ideal, and maximal ideal:
+```lean
+def Mathlib.RingTheory.Ideal.Basic.Ideal (R : Type u) [Semiring R] := Submodule R R
+class Mathlib.RingTheory.Ideal.Basic.IsPrime (I : Ideal α) : Prop
+class IsMaximal (I : Ideal α) : Prop
+```
+
+- Definition of a Spec of a ring: `Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic.PrimeSpectrum`
+
+- Definition of a Noetherian and Artinian rings:
+```lean
+class Mathlib.RingTheory.Noetherian.IsNoetherian (R M) [Semiring R] [AddCommMonoid M] [Module R M] : Prop
+class Mathlib.RingTheory.Artinian.IsArtinian (R M) [Semiring R] [AddCommMonoid M] [Module R M] : Prop
+```
+- Definition of a polynomial ring: `Mathlib.RingTheory.Polynomial.Basic`
+
+- Definitions of a local ring and quotient ring: `Mathlib.RingTheory.Ideal.Quotient.?`
+```lean
+class Mathlib.RingTheory.Ideal.LocalRing.LocalRing (R : Type u) [Semiring R] extends Nontrivial R : Prop
+```
+
+- Definition of the chain of prime ideals and the length of these chains
+
+- Definition of the Krull dimension (supremum of the lengh of chain of prime ideal): `Mathlib.Order.KrullDimension.krullDim`
+
+- Krull dimension of a module
+
+- Definition of the height of prime ideal (dimension of A_p): `Mathlib.Order.KrullDimension.height`
+
+
+Give Examples of each of the above cases for a particular instances of ring
+
+Theorem 0: Hilbert Basis Theorem:
+```lean
+theorem Mathlib.RingTheory.Polynomial.Basic.Polynomial.isNoetherianRing [inst : IsNoetherianRing R] : IsNoetherianRing R[X]
+```
+
+Theorem 1: If A is a nonzero ring, then dim A[t] >= dim A +1
+
+Theorem 2: If A is a nonzero noetherian ring, then dim A[t] = dim A + 1
+
+Theorem 3: If A is nonzero ring then dim A_p + dim A/p <= dim A
+
+Lemma 0: A ring is artinian iff it is noetherian of dimension 0.
+
+Definition of a graded module