Merge branch 'main' of https://github.com/GTBarkley/comm_alg

CommAlg.lean

@@ -1,4 +0,0 @@
-import Mathlib.Tactic
-def hello := "world"
-
--- Thank Grant for setting this up.

README.md

@@ -31,6 +31,8 @@ class Mathlib.RingTheory.Ideal.LocalRing.LocalRing (R : Type u) [Semiring R] ext
 
 - 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`
 
 
@@ -47,4 +49,6 @@ 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

comm_alg/grant.lean

@@ -1,6 +1,12 @@
-import Mathlib.Analysis.Seminorm
+import Mathlib.Order.KrullDimension
+import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
 
 def hello : IO Unit := do
   IO.println "Hello, World!"
 
-#eval hello
+#eval hello
+
+#check (p q : PrimeSpectrum _) → (p ≤ q)
+#check Preorder (PrimeSpectrum _)
+
+#check krullDim (PrimeSpectrum _)

comm_alg/krull.lean

@@ -0,0 +1,44 @@
+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
+
+/- 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.
+-/
+
+variable {R : Type _} [CommRing R] (I : Ideal R)
+
+namespace ideal
+
+noncomputable def height : ℕ∞ := Set.chainHeight {J | J ≤ I ∧ J.IsPrime}
+
+noncomputable def krull_dim (R : Type _) [CommRing R] := height (⊤ : Ideal R)
+
+--some propositions that would be nice to be able to eventually
+
+lemma dim_eq_zero_iff_field : krull_dim R = 0 ↔ IsField R := sorry
+
+#check Ring.DimensionLEOne
+lemma dim_le_one_iff : krull_dim R ≤ 1 ↔ Ring.DimensionLEOne R := sorry
+
+lemma dim_le_one_of_pid [IsDomain R] [IsPrincipalIdealRing R] : krull_dim R ≤ 1 := sorry
+
+lemma dim_le_dim_polynomial_add_one [Nontrivial R] :
+  krull_dim R ≤ krull_dim (Polynomial R) + 1 := sorry
+
+lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] :
+  krull_dim R = krull_dim (Polynomial R) + 1 := sorry
+
+lemma height_eq_dim_localization [Ideal.IsPrime I] :
+  height I = krull_dim (Localization.AtPrime I) := sorry
+
+lemma height_add_dim_quotient_le_dim : height I + krull_dim (R ⧸ I) ≤ krull_dim R := sorry

comm_alg/resources.lean

@@ -0,0 +1,47 @@
+/-
+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.Order.Height
+import Mathlib.RingTheory.MvPolynomial.Basic
+
+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