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

added krullDim_nonneg_of_nontrivial to krull

Browse source
This commit is contained in:
GTBarkley 2023-06-13 21:43:06 +00:00
parent e3deef3322
commit 1ed0a5499c
1 changed files with 6 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
CommAlg/krull.lean
View file

@ -39,7 +39,7 @@ lemma height_le_of_le {I J : PrimeSpectrum R} (I_le_J : I ≤ J) : height I ≤
show J' < J show J' < J
exact lt_of_lt_of_le hJ' I_le_J exact lt_of_lt_of_le hJ' I_le_J
lemma krullDim_le_iff (R : Type) [CommRing R] (n : ℕ) : lemma krullDim_le_iff (R : Type _) [CommRing R] (n : ℕ) :
krullDim R ≤ n ↔ ∀ I : PrimeSpectrum R, (height I : WithBot ℕ∞) ≤ ↑n := iSup_le_iff (α := WithBot ℕ∞) krullDim R ≤ n ↔ ∀ I : PrimeSpectrum R, (height I : WithBot ℕ∞) ≤ ↑n := iSup_le_iff (α := WithBot ℕ∞)
lemma krullDim_le_iff' (R : Type) [CommRing R] (n : ℕ∞) : lemma krullDim_le_iff' (R : Type) [CommRing R] (n : ℕ∞) :
@ -94,6 +94,11 @@ lemma dim_eq_bot_iff : krullDim R = ⊥ ↔ Subsingleton R := by
. rw [h.forall_iff] . rw [h.forall_iff]
trivial trivial
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 dim_eq_zero_iff_field [IsDomain R] : krullDim R = 0 ↔ IsField R := by sorry lemma dim_eq_zero_iff_field [IsDomain R] : krullDim R = 0 ↔ IsField R := by sorry
#check Ring.DimensionLEOne #check Ring.DimensionLEOne