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_bot_iff

Browse source
This commit is contained in:
GTBarkley 2023-06-13 19:11:44 +00:00
parent 0291df2283
commit afeeeb506f
1 changed files with 32 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

40
CommAlg/grant.lean
View file

@ -52,10 +52,10 @@ open Ideal
-- chain of primes
#check height
-- lemma height_ge_iff {𝔭 : PrimeSpectrum R} {n : ℕ∞} :
-- height 𝔭 ≥ n ↔ := sorry
lemma lt_height_iff {𝔭 : PrimeSpectrum R} {n : ℕ∞} :
height 𝔭 > n ↔ ∃ c : List (PrimeSpectrum R), c ∈ {I : PrimeSpectrum R | I < 𝔭}.subchain ∧ c.length = n + 1 := sorry
lemma height_ge_iff' {𝔭 : PrimeSpectrum R} {n : ℕ∞} :
lemma lt_height_iff' {𝔭 : PrimeSpectrum R} {n : ℕ∞} :
height 𝔭 > n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by
rcases n with _ | n
. constructor <;> intro h <;> exfalso
@ -88,13 +88,37 @@ lemma krullDim_nonneg_of_nontrivial [Nontrivial R] : ∃ n : ℕ∞, Ideal.krull
lift (Ideal.krullDim R) to ℕ∞ using h with k
use k
lemma krullDim_le_iff' (R : Type _) [CommRing R] {n : WithBot ℕ∞} :
Ideal.krullDim R ≤ n ↔ (∀ c : List (PrimeSpectrum R), c.Chain' (· < ·) → c.length ≤ n + 1) := by
sorry
-- lemma krullDim_le_iff' (R : Type _) [CommRing R] {n : WithBot ℕ∞} :
-- Ideal.krullDim R ≤ n ↔ (∀ c : List (PrimeSpectrum R), c.Chain' (· < ·) → c.length ≤ n + 1) := by
-- sorry
lemma krullDim_ge_iff' (R : Type _) [CommRing R] {n : WithBot ℕ∞} :
Ideal.krullDim R ≥ n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ c.length = n + 1 := sorry
-- lemma krullDim_ge_iff' (R : Type _) [CommRing R] {n : WithBot ℕ∞} :
-- Ideal.krullDim R ≥ n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ c.length = n + 1 := sorry
lemma prime_elim_of_subsingleton (x : PrimeSpectrum R) [Subsingleton R] : False :=
x.1.ne_top_iff_one.1 x.2.1 <| Eq.substr (Subsingleton.elim 1 (0 : R)) x.1.zero_mem
lemma primeSpectrum_empty_iff : IsEmpty (PrimeSpectrum R) ↔ Subsingleton R := by
constructor
. contrapose
rw [not_isEmpty_iff, ←not_nontrivial_iff_subsingleton, not_not]
apply PrimeSpectrum.instNonemptyPrimeSpectrum
. intro h
by_contra hneg
rw [not_isEmpty_iff] at hneg
rcases hneg with ⟨a, ha⟩
exact prime_elim_of_subsingleton R ⟨a, ha⟩
lemma dim_eq_bot_iff : krullDim R = ⊥ ↔ Subsingleton R := by
unfold Ideal.krullDim
rw [←primeSpectrum_empty_iff, iSup_eq_bot]
constructor <;> intro h
. rw [←not_nonempty_iff]
rintro ⟨a, ha⟩
specialize h ⟨a, ha⟩
tauto
. rw [h.forall_iff]
trivial
#check (sorry : False)