diff --git a/comm_alg/krull.lean b/comm_alg/krull.lean
index 2a5af42..431b8f6 100644
--- a/comm_alg/krull.lean
+++ b/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
\ No newline at end of file
+lemma height_add_dim_quotient_le_dim : height I + krull_dim (R ⧸ I.asIdeal) ≤ krull_dim R := sorry
\ No newline at end of file