From 6d4b9b0f60663df52862416f24a8ee4555db4ae9 Mon Sep 17 00:00:00 2001
From: leopoldmayer <leomayer@uw.edu>
Date: Mon, 12 Jun 2023 09:49:40 -0700
Subject: [PATCH] updated krull_dim name, addd krullDim_le_iff

---
 comm_alg/krull.lean | 28 ++++++++++++++++++++--------
 1 file changed, 20 insertions(+), 8 deletions(-)

diff --git a/comm_alg/krull.lean b/comm_alg/krull.lean
index 5204b9a..1bd2829 100644
--- a/comm_alg/krull.lean
+++ b/comm_alg/krull.lean
@@ -5,6 +5,7 @@ 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.
@@ -22,26 +23,37 @@ variable {R : Type _} [CommRing R] (I : PrimeSpectrum R)
 
 noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < I}
 
-noncomputable def krull_dim (R : Type) [CommRing R]: WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height 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 krullDim_le_iff (R : Type) [CommRing R] (n : ℕ) :
+  iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) ≤ n ↔
+  ∀ I : PrimeSpectrum R, (height I : WithBot ℕ∞) ≤ ↑n := by
+    convert @iSup_le_iff (WithBot ℕ∞) (PrimeSpectrum R) inferInstance _ (↑n)
 
 --some propositions that would be nice to be able to eventually
 
-lemma dim_eq_zero_iff_field : krull_dim R = 0 ↔ IsField R := by sorry
+lemma dim_eq_zero_iff_field [IsDomain R] : krullDim 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_iff : krullDim R ≤ 1 ↔ Ring.DimensionLEOne R := sorry
 
-lemma dim_le_one_of_pid [IsDomain R] [IsPrincipalIdealRing R] : krull_dim R ≤ 1 := by
+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] :
-  krull_dim R ≤ krull_dim (Polynomial R) + 1 := sorry
+  krullDim R ≤ krullDim (Polynomial R) + 1 := sorry
 
 lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] :
-  krull_dim R = krull_dim (Polynomial R) + 1 := sorry
+  krullDim R = krullDim (Polynomial R) + 1 := sorry
 
 lemma height_eq_dim_localization :
-  height I = krull_dim (Localization.AtPrime I.asIdeal) := sorry
+  height I = krullDim (Localization.AtPrime I.asIdeal) := sorry
 
-lemma height_add_dim_quotient_le_dim : height I + krull_dim (R ⧸ I.asIdeal) ≤ krull_dim R := sorry
\ No newline at end of file
+lemma height_add_dim_quotient_le_dim : height I + krullDim (R ⧸ I.asIdeal) ≤ krullDim R := sorry
\ No newline at end of file