SinTan1729/comm_alg
1
0
Fork 0
mirror of https://github.com/GTBarkley/comm_alg.git synced 2024-10-16 11:37:05 -05:00
Code Issues Projects Releases Packages Wiki Activity

Completed polynomial_over_field_dim_one

Browse source
This commit is contained in:
Sayantan Santra 2023-06-16 11:11:13 -07:00
parent 3cf5665126
commit efbeadc4ce
Signed by: SinTan1729
GPG key ID: EB3E68BFBA25C85F
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
CommAlg/sayantan(poly_over_field).lean
View file

@ -7,7 +7,7 @@ import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
namespace Ideal
private lemma singleton_chainHeight_one {α : Type} [Preorder α] [Bot α] : Set.chainHeight {(⊥ : α)} ≤ 1 := by
private lemma singleton_bot_chainHeight_one {α : Type} [Preorder α] [Bot α] : Set.chainHeight {(⊥ : α)} ≤ 1 := by
unfold Set.chainHeight
simp only [iSup_le_iff, Nat.cast_le_one]
intro L h
@ -67,7 +67,7 @@ lemma polynomial_over_field_dim_one {K : Type} [Nontrivial K] [Field K] : krullD
unfold height
rw [sngletn]
simp only [WithBot.coe_le_one, ge_iff_le]
exact singleton_chainHeight_one
exact singleton_bot_chainHeight_one
· suffices : ∃I : PrimeSpectrum (Polynomial K), 1 ≤ (height I : WithBot ℕ∞)
· obtain ⟨I, h⟩ := this
have : (height I : WithBot ℕ∞) ≤ ⨆ (I : PrimeSpectrum (Polynomial K)), ↑(height I) := by