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

CommAlg/grant.lean

@@ -52,10 +52,10 @@ open Ideal
 -- chain of primes 
 #check height 
 
--- lemma height_ge_iff {𝔭 : PrimeSpectrum R} {n : ℕ∞} :
---   height 𝔭 ≥ n ↔ := sorry
+lemma lt_height_iff {𝔭 : PrimeSpectrum R} {n : ℕ∞} :
+  height 𝔭 > n ↔ ∃ c : List (PrimeSpectrum R), c ∈ {I : PrimeSpectrum R | I < 𝔭}.subchain ∧ c.length = n + 1 := sorry
 
-lemma height_ge_iff' {𝔭 : PrimeSpectrum R} {n : ℕ∞} : 
+lemma lt_height_iff' {𝔭 : PrimeSpectrum R} {n : ℕ∞} : 
 height 𝔭 > n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by
   rcases n with _ | n
   . constructor <;> intro h <;> exfalso
@@ -88,13 +88,38 @@ lemma krullDim_nonneg_of_nontrivial [Nontrivial R] : ∃ n : ℕ∞, Ideal.krull
   lift (Ideal.krullDim R) to ℕ∞ using h with k
   use k
 
-lemma krullDim_le_iff' (R : Type _) [CommRing R] {n : WithBot ℕ∞} : 
-  Ideal.krullDim R ≤ n ↔ (∀ c : List (PrimeSpectrum R), c.Chain' (· < ·) → c.length ≤ n + 1) := by
-    sorry
+-- lemma krullDim_le_iff' (R : Type _) [CommRing R] {n : WithBot ℕ∞} : 
+--   Ideal.krullDim R ≤ n ↔ (∀ c : List (PrimeSpectrum R), c.Chain' (· < ·) → c.length ≤ n + 1) := by
+--     sorry
 
-lemma krullDim_ge_iff' (R : Type _) [CommRing R] {n : WithBot ℕ∞} : 
-  Ideal.krullDim R ≥ n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ c.length = n + 1 := sorry
+-- lemma krullDim_ge_iff' (R : Type _) [CommRing R] {n : WithBot ℕ∞} : 
+--   Ideal.krullDim R ≥ n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ c.length = n + 1 := sorry
 
+lemma primeSpectrum_empty_of_subsingleton (x : PrimeSpectrum R) [Subsingleton R] : False :=
+  x.1.ne_top_iff_one.1 x.2.1 <| Eq.substr (Subsingleton.elim 1 (0 : R)) x.1.zero_mem
+
+lemma primeSpectrum_empty_iff : IsEmpty (PrimeSpectrum R) ↔ Subsingleton R := by
+  constructor
+  . contrapose
+    rw [not_isEmpty_iff, ←not_nontrivial_iff_subsingleton, not_not]
+    apply PrimeSpectrum.instNonemptyPrimeSpectrum
+  . intro h
+    by_contra hneg
+    rw [not_isEmpty_iff] at hneg
+    rcases hneg with ⟨a, ha⟩
+    exact primeSpectrum_empty_of_subsingleton R ⟨a, ha⟩
+
+/-- A ring has Krull dimension -∞ if and only if it is the zero ring -/
+lemma dim_eq_bot_iff : krullDim R = ⊥ ↔ Subsingleton R := by
+  unfold Ideal.krullDim
+  rw [←primeSpectrum_empty_iff, iSup_eq_bot]
+  constructor <;> intro h
+  . rw [←not_nonempty_iff]
+    rintro ⟨a, ha⟩
+    -- specialize h ⟨a, ha⟩
+    tauto
+  . rw [h.forall_iff]
+    trivial
 
 
 #check (sorry : False)

CommAlg/krull.lean

@@ -68,7 +68,31 @@ lemma krullDim_eq_height [LocalRing R] : krullDim R = height (closedPoint R) :=
 #check height_le_krullDim
 --some propositions that would be nice to be able to eventually
 
-lemma dim_eq_bot_iff : krullDim R = ⊥ ↔ Subsingleton R := sorry
+lemma primeSpectrum_empty_of_subsingleton (x : PrimeSpectrum R) [Subsingleton R] : False :=
+  x.1.ne_top_iff_one.1 x.2.1 <| Eq.substr (Subsingleton.elim 1 (0 : R)) x.1.zero_mem
+
+lemma primeSpectrum_empty_iff : IsEmpty (PrimeSpectrum R) ↔ Subsingleton R := by
+  constructor
+  . contrapose
+    rw [not_isEmpty_iff, ←not_nontrivial_iff_subsingleton, not_not]
+    apply PrimeSpectrum.instNonemptyPrimeSpectrum
+  . intro h
+    by_contra hneg
+    rw [not_isEmpty_iff] at hneg
+    rcases hneg with ⟨a, ha⟩
+    exact primeSpectrum_empty_of_subsingleton ⟨a, ha⟩
+
+/-- A ring has Krull dimension -∞ if and only if it is the zero ring -/
+lemma dim_eq_bot_iff : krullDim R = ⊥ ↔ Subsingleton R := by
+  unfold Ideal.krullDim
+  rw [←primeSpectrum_empty_iff, iSup_eq_bot]
+  constructor <;> intro h
+  . rw [←not_nonempty_iff]
+    rintro ⟨a, ha⟩
+    specialize h ⟨a, ha⟩
+    tauto
+  . rw [h.forall_iff]
+    trivial
 
 lemma dim_eq_zero_iff_field [IsDomain R] : krullDim R = 0 ↔ IsField R := by sorry
 

CommAlg/sayantan(dim_eq_zero_iff_field).lean

@@ -9,11 +9,6 @@ import Mathlib.Order.ConditionallyCompleteLattice.Basic
 
 namespace Ideal
 
-example (x : Nat) : List.Chain' (· < ·)  [x] := by
-  constructor
-
-
-  
 variable {R : Type _} [CommRing R] (I : PrimeSpectrum R)
 noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < I}
 noncomputable def krullDim (R : Type) [CommRing R] : WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height I
@@ -52,30 +47,36 @@ lemma dim_field_eq_zero {K : Type _} [Field K] : krullDim K = 0 := by
   unfold krullDim
   simp [field_prime_height_zero]
 
+noncomputable
+instance : CompleteLattice (WithBot ℕ∞) :=
+  inferInstanceAs <| CompleteLattice (WithBot (WithTop ℕ))
+
 lemma isField.dim_zero {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0) : IsField D := by
   unfold krullDim at h
   simp [height] at h
   by_contra x
   rw [Ring.not_isField_iff_exists_prime] at x
   obtain ⟨P, ⟨h1, primeP⟩⟩ := x
-  have PgtBot : P > ⊥ := Ne.bot_lt h1
-  have pos_height : ↑(Set.chainHeight {J | J < P}) > 0 := by
-    have : ⊥ ∈ {J | J < P} := PgtBot
-    have : {J | J < P}.Nonempty := Set.nonempty_of_mem this
-    -- have : {J | J < P} ≠ ∅ := Set.Nonempty.ne_empty this
+  let P' : PrimeSpectrum D := PrimeSpectrum.mk P primeP
+  have h2 : P' ≠ ⊥ := by
+    by_contra a
+    have : P = ⊥ := by rwa [PrimeSpectrum.ext_iff] at a
+    contradiction
+  have PgtBot : P' > ⊥ := Ne.bot_lt h2
+  have pos_height : ¬ ↑(Set.chainHeight {J | J < P'}) ≤ 0  := by
+    have : ⊥ ∈ {J | J < P'} := PgtBot
+    have : {J | J < P'}.Nonempty := Set.nonempty_of_mem this
     rw [←Set.one_le_chainHeight_iff] at this
-    exact Iff.mp ENat.one_le_iff_pos this
-  have zero_height : ↑(Set.chainHeight {J | J < P}) = 0 := by
-    -- Probably need to use Sup_le or something here
-    sorry
-  have : ↑(Set.chainHeight {J | J < P}) ≠ 0 := Iff.mp pos_iff_ne_zero pos_height
+    exact not_le_of_gt (Iff.mp ENat.one_le_iff_pos this)
+  have zero_height : (Set.chainHeight {J | J < P'}) ≤ 0 := by
+    have : (⨆ (I : PrimeSpectrum D), (Set.chainHeight {J | J < I} : WithBot ℕ∞)) ≤ 0 := h.le
+    rw [iSup_le_iff] at this
+    exact Iff.mp WithBot.coe_le_zero (this P')
   contradiction
 
 lemma dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krullDim D = 0 ↔ IsField D := by
   constructor
   · exact isField.dim_zero
   · intro fieldD
-    have : Field D := IsField.toField fieldD
-    -- Not exactly sure why this is failing
-    -- apply @dim_field_eq_zero D _
-    sorry
+    let h : Field D := IsField.toField fieldD
+    exact dim_field_eq_zero