Merge pull request #14 from GTBarkley/HEAD

Head

comm_alg/krull.lean

@@ -4,6 +4,7 @@ import Mathlib.RingTheory.PrincipalIdealDomain
 import Mathlib.RingTheory.DedekindDomain.Basic
 import Mathlib.RingTheory.Ideal.Quotient
 import Mathlib.RingTheory.Localization.AtPrime
+import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
 
 /- This file contains the definitions of height of an ideal, and the krull
   dimension of a commutative ring.
@@ -15,22 +16,24 @@ import Mathlib.RingTheory.Localization.AtPrime
   developed.
 -/
 
-variable {R : Type _} [CommRing R] (I : Ideal R)
+namespace Ideal
 
-namespace ideal
+variable {R : Type _} [CommRing R] (I : PrimeSpectrum R)
 
-noncomputable def height : ℕ∞ := Set.chainHeight {J | J ≤ I ∧ J.IsPrime}
+noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J ≤ I} - 1
 
-noncomputable def krull_dim (R : Type _) [CommRing R] := height (⊤ : Ideal R)
+noncomputable def krull_dim (R : Type) [CommRing R]: WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height I
 
 --some propositions that would be nice to be able to eventually
 
-lemma dim_eq_zero_iff_field : krull_dim R = 0 ↔ IsField R := sorry
+lemma dim_eq_zero_iff_field : krull_dim R = 0 ↔ IsField R := by 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_one_of_pid [IsDomain R] [IsPrincipalIdealRing R] : krull_dim R ≤ 1 := by
+  rw [dim_le_one_iff]
+  exact Ring.DimensionLEOne.principal_ideal_ring R
 
 lemma dim_le_dim_polynomial_add_one [Nontrivial R] :
   krull_dim R ≤ krull_dim (Polynomial R) + 1 := sorry
@@ -38,7 +41,7 @@ lemma dim_le_dim_polynomial_add_one [Nontrivial R] :
 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_eq_dim_localization :
+  height I = krull_dim (Localization.AtPrime I.asIdeal) := sorry
 
-lemma height_add_dim_quotient_le_dim : height I + krull_dim (R ⧸ I) ≤ krull_dim R := sorry
+lemma height_add_dim_quotient_le_dim : height I + krull_dim (R ⧸ I.asIdeal) ≤ krull_dim R := sorry

comm_alg/resources.lean

@@ -9,6 +9,8 @@ import Mathlib.RingTheory.Noetherian
 import Mathlib.RingTheory.Artinian
 import Mathlib.Order.Height
 import Mathlib.RingTheory.MvPolynomial.Basic
+import Mathlib.RingTheory.Ideal.Over
+import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
 
 variable {R M : Type _} [CommRing R] [AddCommGroup M] [Module R M]
 
@@ -44,4 +46,14 @@ variable (I : Ideal R)
 #check Polynomial R
 --this is the polynomial ring with variables indexed by ℕ
 #check MvPolynomial ℕ R
---hopefully there's good communication between them
+--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