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

proved dim_eq_zero_iff

Browse source
This commit is contained in:
GTBarkley 2023-06-14 21:35:36 +00:00
parent 3c4cfeab65
commit 4690889149
1 changed files with 10 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
CommAlg/krull.lean
View file

@ -169,11 +169,16 @@ lemma dim_le_zero_iff : krullDim R ≤ 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal
exact hc2 exact hc2
lemma dim_eq_zero_iff [Nontrivial R] : krullDim R = 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal I.asIdeal := by lemma dim_eq_zero_iff [Nontrivial R] : krullDim R = 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal I.asIdeal := by
constructor <;> intro h rw [←dim_le_zero_iff]
. intro I obtain ⟨n, hn⟩ := krullDim_nonneg_of_nontrivial R
sorry have : n ≥ 0 := zero_le n
. sorry change _ ≤ _ at this
rw [←WithBot.coe_le_coe,←hn] at this
change (0 : WithBot ℕ∞) ≤ _ at this
constructor <;> intro h'
rw [h']
exact le_antisymm h' this
@[simp] @[simp]
lemma field_prime_bot {K: Type _} [Field K] (P : Ideal K) : IsPrime P ↔ P = ⊥ := by lemma field_prime_bot {K: Type _} [Field K] (P : Ideal K) : IsPrime P ↔ P = ⊥ := by
constructor constructor