SinTan1729/comm_alg
1
0
Fork 0
mirror of https://github.com/GTBarkley/comm_alg.git synced 2024-12-26 23:48:36 -06:00
Code Issues Projects Releases Packages Wiki Activity

proved krullDim_nonneg_of_nontrivial

Browse source
This commit is contained in:
GTBarkley 2023-06-13 05:01:18 +00:00
parent 53983475bb
commit 6a0a3768f8
1 changed files with 8 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
CommAlg/grant.lean
View file

@ -73,7 +73,7 @@ height 𝔭 > n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀
show ((↑(n + 1):ℕ∞) ≤ _) ↔ ∃c, _ ∧ _ ∧ ((_ : WithTop ℕ) = (_:ℕ∞)) show ((↑(n + 1):ℕ∞) ≤ _) ↔ ∃c, _ ∧ _ ∧ ((_ : WithTop ℕ) = (_:ℕ∞))
rw [{J | J < 𝔭}.le_chainHeight_iff] rw [{J | J < 𝔭}.le_chainHeight_iff]
show (∃ c, (List.Chain' _ c ∧ ∀𝔮, 𝔮 ∈ c → 𝔮 < 𝔭) ∧ _) ↔ _ show (∃ c, (List.Chain' _ c ∧ ∀𝔮, 𝔮 ∈ c → 𝔮 < 𝔭) ∧ _) ↔ _
have h := fun (c : List (PrimeSpectrum R)) => (@WithTop.coe_eq_coe _ (List.length c) n) -- have h := fun (c : List (PrimeSpectrum R)) => (@WithTop.coe_eq_coe _ (List.length c) n)
constructor <;> rintro ⟨c, hc⟩ <;> use c --<;> tauto--<;> exact ⟨hc.1, by tauto⟩ constructor <;> rintro ⟨c, hc⟩ <;> use c --<;> tauto--<;> exact ⟨hc.1, by tauto⟩
. --rw [and_assoc] . --rw [and_assoc]
-- show _ ∧ _ ∧ _ -- show _ ∧ _ ∧ _
@ -83,6 +83,11 @@ height 𝔭 > n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀
norm_cast at hc norm_cast at hc
tauto tauto
lemma krullDim_nonneg_of_nontrivial [Nontrivial R] : ∃ n : ℕ∞, Ideal.krullDim R = n := by
have h := dim_eq_bot_iff.not.mpr (not_subsingleton R)
lift (Ideal.krullDim R) to ℕ∞ using h with k
use k
lemma krullDim_le_iff' (R : Type _) [CommRing R] {n : WithBot ℕ∞} : 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 Ideal.krullDim R ≤ n ↔ (∀ c : List (PrimeSpectrum R), c.Chain' (· < ·) → c.length ≤ n + 1) := by
sorry sorry
@ -90,6 +95,8 @@ lemma krullDim_le_iff' (R : Type _) [CommRing R] {n : WithBot ℕ∞} :
lemma krullDim_ge_iff' (R : Type _) [CommRing R] {n : WithBot ℕ∞} : 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 Ideal.krullDim R ≥ n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ c.length = n + 1 := sorry
#check (sorry : False) #check (sorry : False)
#check (sorryAx) #check (sorryAx)
#check (4 : WithBot ℕ∞) #check (4 : WithBot ℕ∞)