From afeeeb506fe6801f158593d292ff32dc636c3a3f Mon Sep 17 00:00:00 2001 From: GTBarkley Date: Tue, 13 Jun 2023 19:11:44 +0000 Subject: [PATCH 1/4] proved dim_eq_bot_iff --- CommAlg/grant.lean | 40 ++++++++++++++++++++++++++++++++-------- 1 file changed, 32 insertions(+), 8 deletions(-) diff --git a/CommAlg/grant.lean b/CommAlg/grant.lean index ef2cc9f..7951c54 100644 --- a/CommAlg/grant.lean +++ b/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,37 @@ 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 prime_elim_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 prime_elim_of_subsingleton R ⟨a, ha⟩ + +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) From f63286aff8ebf58f6a463b92068573ea4d9aa9d1 Mon Sep 17 00:00:00 2001 From: GTBarkley Date: Tue, 13 Jun 2023 20:34:02 +0000 Subject: [PATCH 2/4] moved dim_eq_bot_iff to krull.lean --- CommAlg/grant.lean | 7 ++++--- CommAlg/krull.lean | 26 +++++++++++++++++++++++++- 2 files changed, 29 insertions(+), 4 deletions(-) diff --git a/CommAlg/grant.lean b/CommAlg/grant.lean index 7951c54..ce5041d 100644 --- a/CommAlg/grant.lean +++ b/CommAlg/grant.lean @@ -95,7 +95,7 @@ lemma krullDim_nonneg_of_nontrivial [Nontrivial R] : ∃ n : ℕ∞, Ideal.krull -- 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 prime_elim_of_subsingleton (x : PrimeSpectrum R) [Subsingleton R] : False := +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 @@ -107,15 +107,16 @@ lemma primeSpectrum_empty_iff : IsEmpty (PrimeSpectrum R) ↔ Subsingleton R := by_contra hneg rw [not_isEmpty_iff] at hneg rcases hneg with ⟨a, ha⟩ - exact prime_elim_of_subsingleton R ⟨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⟩ + -- specialize h ⟨a, ha⟩ tauto . rw [h.forall_iff] trivial diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index 9b4c785..c021d74 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -62,7 +62,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 From dedb9711c76e58717d6a2c15693ec2e16069cfe6 Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Tue, 13 Jun 2023 14:08:04 -0700 Subject: [PATCH 3/4] update: Finally, the proof of dim_eq_zero_iff_field is complete --- CommAlg/sayantan.lean | 39 ++++++++++++++++++++------------------- 1 file changed, 20 insertions(+), 19 deletions(-) diff --git a/CommAlg/sayantan.lean b/CommAlg/sayantan.lean index 6140db5..7656924 100644 --- a/CommAlg/sayantan.lean +++ b/CommAlg/sayantan.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 \ No newline at end of file From db1875067783ee57b4013b8c5ce54d335a9c63ac Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Tue, 13 Jun 2023 14:11:13 -0700 Subject: [PATCH 4/4] Renamed a file --- CommAlg/{sayantan.lean => sayantan(dim_eq_zero_iff_field).lean} | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) rename CommAlg/{sayantan.lean => sayantan(dim_eq_zero_iff_field).lean} (99%) diff --git a/CommAlg/sayantan.lean b/CommAlg/sayantan(dim_eq_zero_iff_field).lean similarity index 99% rename from CommAlg/sayantan.lean rename to CommAlg/sayantan(dim_eq_zero_iff_field).lean index 7656924..35f197f 100644 --- a/CommAlg/sayantan.lean +++ b/CommAlg/sayantan(dim_eq_zero_iff_field).lean @@ -79,4 +79,4 @@ lemma dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krullDim D = · exact isField.dim_zero · intro fieldD let h : Field D := IsField.toField fieldD - exact dim_field_eq_zero \ No newline at end of file + exact dim_field_eq_zero