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

added some lemmas

Browse source
This commit is contained in:
leopoldmayer 2023-06-12 14:27:09 -07:00
parent ab1c24cd8b
commit 8b2be97b5a
1 changed files with 27 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

30
CommAlg/krull.lean
View file

@ -19,6 +19,7 @@ import Mathlib.Order.ConditionallyCompleteLattice.Basic
-/
namespace Ideal
open LocalRing
variable {R : Type _} [CommRing R] (I : PrimeSpectrum R)
@ -32,10 +33,33 @@ lemma krullDim_def' (R : Type) [CommRing R] : krullDim R = iSup (λ I : PrimeSpe
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 := iSup_le_iff (α := WithBot ℕ∞)
lemma height_le_of_le {I J : PrimeSpectrum R} (I_le_J : I ≤ J) : height I ≤ height J := by
apply Set.chainHeight_mono
intro J' hJ'
show J' < J
exact lt_of_lt_of_le hJ' I_le_J
lemma krullDim_le_iff (R : Type) [CommRing R] (n : ℕ) :
krullDim R ≤ n ↔ ∀ I : PrimeSpectrum R, (height I : WithBot ℕ∞) ≤ ↑n := iSup_le_iff (α := WithBot ℕ∞)
lemma krullDim_le_iff' (R : Type) [CommRing R] (n : ℕ∞) :
krullDim R ≤ n ↔ ∀ I : PrimeSpectrum R, (height I : WithBot ℕ∞) ≤ ↑n := iSup_le_iff (α := WithBot ℕ∞)
@[simp]
lemma height_le_krullDim (I : PrimeSpectrum R) : height I ≤ krullDim R :=
le_iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) I
lemma krullDim_eq_height [LocalRing R] : krullDim R = height (closedPoint R) := by
apply le_antisymm
. rw [krullDim_le_iff']
intro I
apply WithBot.coe_mono
apply height_le_of_le
apply le_maximalIdeal
exact I.2.1
. simp
#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