Merge pull request #86 from GTBarkley/leo

removed dependency on false sorried lemma
This commit is contained in:
Leo Mayer 2023-06-16 00:08:04 -07:00 committed by GitHub
commit 253ac17bb6
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 42 additions and 4 deletions

View file

@ -95,8 +95,32 @@ lemma le_krullDim_iff (R : Type _) [CommRing R] (n : ) :
have : height I ≤ krullDim R := by apply height_le_krullDim have : height I ≤ krullDim R := by apply height_le_krullDim
exact le_trans h this exact le_trans h this
lemma le_krullDim_iff' (R : Type _) [CommRing R] (n : ℕ∞) : #check ENat.recTopCoe
n ≤ krullDim R ↔ ∃ I : PrimeSpectrum R, n ≤ (height I : WithBot ℕ∞) := by sorry
/- terrible place for this lemma. Also this probably exists somewhere
Also this is a terrible proof
-/
lemma eq_top_iff (n : WithBot ℕ∞) : n = ↔ ∀ m : , m ≤ n := by
aesop
induction' n using WithBot.recBotCoe with n
. exfalso
have := (a 0)
simp [not_lt_of_ge] at this
induction' n using ENat.recTopCoe with n
. rfl
. have := a (n + 1)
exfalso
change (((n + 1) : ℕ∞) : WithBot ℕ∞) ≤ _ at this
simp [WithBot.coe_le_coe] at this
change ((n + 1) : ℕ∞) ≤ (n : ℕ∞) at this
simp [ENat.add_one_le_iff] at this
lemma krullDim_eq_top_iff (R : Type _) [CommRing R] :
krullDim R = ↔ ∀ (n : ), ∃ I : PrimeSpectrum R, n ≤ height I := by
simp [eq_top_iff, le_krullDim_iff]
change (∀ (m : ), ∃ I, ((m : ℕ∞) : WithBot ℕ∞) ≤ height I) ↔ _
simp [WithBot.coe_le_coe]
/-- The Krull dimension of a local ring is the height of its maximal ideal. -/ /-- The Krull dimension of a local ring is the height of its maximal ideal. -/
lemma krullDim_eq_height [LocalRing R] : krullDim R = height (closedPoint R) := by lemma krullDim_eq_height [LocalRing R] : krullDim R = height (closedPoint R) := by

View file

@ -132,7 +132,7 @@ lemma ht_adjoin_x_eq_ht_add_one [Nontrivial R] (I : PrimeSpectrum R) : height I
apply hl.2 apply hl.2
exact hb exact hb
#check ( : ℕ∞)
/- /-
dim R + 1 ≤ dim R[X] dim R + 1 ≤ dim R[X]
-/ -/
@ -142,12 +142,26 @@ lemma dim_le_dim_polynomial_add_one [Nontrivial R] :
rw [hn] rw [hn]
change ↑(n + 1) ≤ krullDim R[X] change ↑(n + 1) ≤ krullDim R[X]
have := le_of_eq hn.symm have := le_of_eq hn.symm
rw [le_krullDim_iff'] at this ⊢ induction' n using ENat.recTopCoe with n
. change krullDim R = at hn
change ≤ krullDim R[X]
rw [krullDim_eq_top_iff] at hn
rw [top_le_iff, krullDim_eq_top_iff]
intro n
obtain ⟨I, hI⟩ := hn n
use adjoin_x I
calc n ≤ height I := hI
_ ≤ height I + 1 := le_self_add
_ ≤ height (adjoin_x I) := ht_adjoin_x_eq_ht_add_one I
change n ≤ krullDim R at this
change (n + 1 : ) ≤ krullDim R[X]
rw [le_krullDim_iff] at this ⊢
obtain ⟨I, hI⟩ := this obtain ⟨I, hI⟩ := this
use adjoin_x I use adjoin_x I
apply WithBot.coe_mono apply WithBot.coe_mono
calc n + 1 ≤ height I + 1 := by calc n + 1 ≤ height I + 1 := by
apply add_le_add_right apply add_le_add_right
change ((n : ℕ∞) : WithBot ℕ∞) ≤ (height I) at hI
rw [WithBot.coe_le_coe] at hI rw [WithBot.coe_le_coe] at hI
exact hI exact hI
_ ≤ height (adjoin_x I) := ht_adjoin_x_eq_ht_add_one I _ ≤ height (adjoin_x I) := ht_adjoin_x_eq_ht_add_one I