Merge pull request #66 from GTBarkley/grant

characterized dim <= 0 via primes
This commit is contained in:
GTBarkley 2023-06-14 14:36:20 -07:00 committed by GitHub
commit bdcfc9d821
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 123 additions and 34 deletions

View file

@ -171,6 +171,48 @@ lemma dim_le_one_of_dimLEOne : Ring.DimensionLEOne R → krullDim R ≤ (1 :
apply (IsCoatom.lt_iff H.out).mp apply (IsCoatom.lt_iff H.out).mp
exact hc2 exact hc2
--refine Iff.mp radical_eq_top (?_ (id (Eq.symm hc3))) --refine Iff.mp radical_eq_top (?_ (id (Eq.symm hc3)))
lemma not_maximal_of_lt_prime {p : Ideal R} {q : Ideal R} (hq : IsPrime q) (h : p < q) : ¬IsMaximal p := by
intro hp
apply IsPrime.ne_top hq
apply (IsCoatom.lt_iff hp.out).mp
exact h
lemma dim_le_zero_iff : krullDim R ≤ 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal I.asIdeal := by
show ((_ : WithBot ℕ∞) ≤ (0 : )) ↔ _
rw [krullDim_le_iff R 0]
constructor <;> intro h I
. contrapose! h
have ⟨𝔪, h𝔪⟩ := I.asIdeal.exists_le_maximal (IsPrime.ne_top I.IsPrime)
let 𝔪p := (⟨𝔪, IsMaximal.isPrime h𝔪.1⟩ : PrimeSpectrum R)
have hstrct : I < 𝔪p := by
apply lt_of_le_of_ne h𝔪.2
intro hcontr
rw [hcontr] at h
exact h h𝔪.1
use 𝔪p
show (_ : WithBot ℕ∞) > (0 : ℕ∞)
rw [_root_.lt_height_iff'']
use [I]
constructor
. exact List.chain'_singleton _
. constructor
. intro I' hI'
simp at hI'
rwa [hI']
. simp
. contrapose! h
change (_ : WithBot ℕ∞) > (0 : ℕ∞) at h
rw [_root_.lt_height_iff''] at h
obtain ⟨c, _, hc2, hc3⟩ := h
norm_cast at hc3
rw [List.length_eq_one] at hc3
obtain ⟨𝔮, h𝔮⟩ := hc3
use 𝔮
specialize hc2 𝔮 (h𝔮 ▸ (List.mem_singleton.mpr rfl))
apply not_maximal_of_lt_prime _ I.IsPrime
exact hc2
end Krull end Krull
section iSupWithBot section iSupWithBot

View file

@ -65,6 +65,34 @@ lemma krullDim_eq_height [LocalRing R] : krullDim R = height (closedPoint R) :=
exact I.2.1 exact I.2.1
. simp only [height_le_krullDim] . simp only [height_le_krullDim]
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
. exact (not_le.mpr h) le_top
. tauto
have (m : ℕ∞) : m > some n ↔ m ≥ some (n + 1) := by
symm
show (n + 1 ≤ m ↔ _ )
apply ENat.add_one_le_iff
exact ENat.coe_ne_top _
rw [this]
unfold Ideal.height
show ((↑(n + 1):ℕ∞) ≤ _) ↔ ∃c, _ ∧ _ ∧ ((_ : WithTop ) = (_:ℕ∞))
rw [{J | J < 𝔭}.le_chainHeight_iff]
show (∃ c, (List.Chain' _ c ∧ ∀𝔮, 𝔮 ∈ c → 𝔮 < 𝔭) ∧ _) ↔ _
constructor <;> rintro ⟨c, hc⟩ <;> use c
. tauto
. change _ ∧ _ ∧ (List.length c : ℕ∞) = n + 1 at hc
norm_cast at hc
tauto
lemma lt_height_iff'' {𝔭 : PrimeSpectrum R} {n : ℕ∞} :
height 𝔭 > (n : WithBot ℕ∞) ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by
show (_ < _) ↔ _
rw [WithBot.coe_lt_coe]
exact lt_height_iff'
#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
@ -99,12 +127,58 @@ lemma krullDim_nonneg_of_nontrivial (R : Type _) [CommRing R] [Nontrivial R] :
lift (Ideal.krullDim R) to ℕ∞ using h with k lift (Ideal.krullDim R) to ℕ∞ using h with k
use k use k
lemma not_maximal_of_lt_prime {p : Ideal R} {q : Ideal R} (hq : IsPrime q) (h : p < q) : ¬IsMaximal p := by
intro hp
apply IsPrime.ne_top hq
apply (IsCoatom.lt_iff hp.out).mp
exact h
lemma dim_le_zero_iff : krullDim R ≤ 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal I.asIdeal := by
show ((_ : WithBot ℕ∞) ≤ (0 : )) ↔ _
rw [krullDim_le_iff R 0]
constructor <;> intro h I
. contrapose! h
have ⟨𝔪, h𝔪⟩ := I.asIdeal.exists_le_maximal (IsPrime.ne_top I.IsPrime)
let 𝔪p := (⟨𝔪, IsMaximal.isPrime h𝔪.1⟩ : PrimeSpectrum R)
have hstrct : I < 𝔪p := by
apply lt_of_le_of_ne h𝔪.2
intro hcontr
rw [hcontr] at h
exact h h𝔪.1
use 𝔪p
show (_ : WithBot ℕ∞) > (0 : ℕ∞)
rw [lt_height_iff'']
use [I]
constructor
. exact List.chain'_singleton _
. constructor
. intro I' hI'
simp at hI'
rwa [hI']
. simp
. contrapose! h
change (_ : WithBot ℕ∞) > (0 : ℕ∞) at h
rw [lt_height_iff''] at h
obtain ⟨c, _, hc2, hc3⟩ := h
norm_cast at hc3
rw [List.length_eq_one] at hc3
obtain ⟨𝔮, h𝔮⟩ := hc3
use 𝔮
specialize hc2 𝔮 (h𝔮 ▸ (List.mem_singleton.mpr rfl))
apply not_maximal_of_lt_prime I.IsPrime
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
@ -167,37 +241,10 @@ lemma domain_dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krull
-- This lemma is false! -- This lemma is false!
lemma dim_le_one_iff : krullDim R ≤ 1 ↔ Ring.DimensionLEOne R := sorry lemma dim_le_one_iff : krullDim R ≤ 1 ↔ Ring.DimensionLEOne R := sorry
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
. exact (not_le.mpr h) le_top
. tauto
have (m : ℕ∞) : m > some n ↔ m ≥ some (n + 1) := by
symm
show (n + 1 ≤ m ↔ _ )
apply ENat.add_one_le_iff
exact ENat.coe_ne_top _
rw [this]
unfold Ideal.height
show ((↑(n + 1):ℕ∞) ≤ _) ↔ ∃c, _ ∧ _ ∧ ((_ : WithTop ) = (_:ℕ∞))
rw [{J | J < 𝔭}.le_chainHeight_iff]
show (∃ c, (List.Chain' _ c ∧ ∀𝔮, 𝔮 ∈ c → 𝔮 < 𝔭) ∧ _) ↔ _
constructor <;> rintro ⟨c, hc⟩ <;> use c
. tauto
. change _ ∧ _ ∧ (List.length c : ℕ∞) = n + 1 at hc
norm_cast at hc
tauto
lemma lt_height_iff'' {𝔭 : PrimeSpectrum R} {n : ℕ∞} :
height 𝔭 > (n : WithBot ℕ∞) ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by
show (_ < _) ↔ _
rw [WithBot.coe_lt_coe]
exact lt_height_iff'
/-- The converse of this is false, because the definition of "dimension ≤ 1" in mathlib /-- The converse of this is false, because the definition of "dimension ≤ 1" in mathlib
applies only to dimension zero rings and domains of dimension 1. -/ applies only to dimension zero rings and domains of dimension 1. -/
lemma dim_le_one_of_dimLEOne : Ring.DimensionLEOne R → krullDim R ≤ (1 : ) := by lemma dim_le_one_of_dimLEOne : Ring.DimensionLEOne R → krullDim R ≤ 1 := by
show _ → ((_ : WithBot ℕ∞) ≤ (1 : ))
rw [krullDim_le_iff R 1] rw [krullDim_le_iff R 1]
intro H p intro H p
apply le_of_not_gt apply le_of_not_gt