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

Turn some simp into simp only

Browse source
This commit is contained in:
Sayantan Santra 2023-06-14 11:12:33 -07:00
parent 50515d9ed8
commit a2f481c7db
Signed by: SinTan1729
GPG key ID: EB3E68BFBA25C85F
2 changed files with 9 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
CommAlg/krull.lean
View file

@ -63,7 +63,7 @@ lemma krullDim_eq_height [LocalRing R] : krullDim R = height (closedPoint R) :=
apply height_le_of_le apply height_le_of_le
apply le_maximalIdeal apply le_maximalIdeal
exact I.2.1 exact I.2.1
. simp . simp only [height_le_krullDim]
#check height_le_krullDim #check height_le_krullDim
--some propositions that would be nice to be able to eventually --some propositions that would be nice to be able to eventually

11
CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean
View file

@ -42,16 +42,21 @@ lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] :
have PleP' : P ≤ P' := PleM have PleP' : P ≤ P' := PleM
have : height P ≤ height P' := height_le_of_le PleP' have : height P ≤ height P' := height_le_of_le PleP'
simp only [WithBot.coe_le_coe] simp only [WithBot.coe_le_coe]
sorry have : ∃ (I : PrimeSpectrum R), height P' ≤ height I + 1 := by
sorry
obtain ⟨I, h⟩ := this
use I
exact ge_trans h this
obtain ⟨I, IP⟩ := this obtain ⟨I, IP⟩ := this
have : (↑(height I + 1) : WithBot ℕ∞) ≤ ⨆ (I : PrimeSpectrum R), ↑(height I + 1) := by have : (↑(height I + 1) : WithBot ℕ∞) ≤ ⨆ (I : PrimeSpectrum R), ↑(height I + 1) := by
apply @le_iSup (WithBot ℕ∞) _ _ _ I apply @le_iSup (WithBot ℕ∞) _ _ _ I
apply ge_trans this IP exact ge_trans this IP
have oneOut : (⨆ (I : PrimeSpectrum R), (height I : WithBot ℕ∞) + 1) ≤ (⨆ (I : PrimeSpectrum R), ↑(height I)) + 1 := by have oneOut : (⨆ (I : PrimeSpectrum R), (height I : WithBot ℕ∞) + 1) ≤ (⨆ (I : PrimeSpectrum R), ↑(height I)) + 1 := by
have : ∀ P : PrimeSpectrum R, (height P : WithBot ℕ∞) + 1 ≤ (⨆ (I : PrimeSpectrum R), ↑(height I)) + 1 := have : ∀ P : PrimeSpectrum R, (height P : WithBot ℕ∞) + 1 ≤ (⨆ (I : PrimeSpectrum R), ↑(height I)) + 1 :=
fun P ↦ (by apply add_le_add_right (@le_iSup (WithBot ℕ∞) _ _ _ P) 1) fun P ↦ (by apply add_le_add_right (@le_iSup (WithBot ℕ∞) _ _ _ P) 1)
apply iSup_le apply iSup_le
apply this apply this
simp simp only [iSup_le_iff]
intro P intro P
exact ge_trans oneOut (htPBdd P) exact ge_trans oneOut (htPBdd P)