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

Merge pull request #40 from GTBarkley/leo

Browse source 
Leo
This commit is contained in:
Leo Mayer 2023-06-13 14:19:34 -07:00 committed by GitHub
commit e3deef3322
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
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