Merge pull request #11 from GTBarkley/HEAD

Head

CommAlg.lean

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

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