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

two new sorried statements

Browse source
This commit is contained in:
leopoldmayer 2023-06-13 14:17:59 -07:00
parent 0291df2283
commit 4c7b6b3022
1 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
CommAlg/krull.lean
View file

@ -45,6 +45,12 @@ lemma krullDim_le_iff (R : Type) [CommRing R] (n : ℕ) :
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 le_krullDim_iff (R : Type) [CommRing R] (n : ℕ) :
n ≤ krullDim R ↔ ∃ I : PrimeSpectrum R, n ≤ (height I : WithBot ℕ∞) := by sorry
lemma le_krullDim_iff' (R : Type) [CommRing R] (n : ℕ∞) :
n ≤ krullDim R ↔ ∃ I : PrimeSpectrum R, n ≤ (height I : WithBot ℕ∞) := by sorry
@[simp] @[simp]
lemma height_le_krullDim (I : PrimeSpectrum R) : height I ≤ krullDim R := lemma height_le_krullDim (I : PrimeSpectrum R) : height I ≤ krullDim R :=
le_iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) I le_iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) I