From 947c28f00147380038595fb008bb426c9772077c Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Wed, 14 Jun 2023 23:51:46 -0700 Subject: [PATCH] Tried to avoid the finiteness condition on height P --- CommAlg/krull.lean | 9 +++- ...yantan(dim_eq_dim_polynomial_add_one).lean | 48 ++++++++++++------- 2 files changed, 39 insertions(+), 18 deletions(-) diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index 8da4d27..2b86416 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -4,6 +4,7 @@ import Mathlib.Order.Height import Mathlib.RingTheory.PrincipalIdealDomain import Mathlib.RingTheory.DedekindDomain.Basic import Mathlib.RingTheory.Ideal.Quotient +import Mathlib.RingTheory.Ideal.MinimalPrime import Mathlib.RingTheory.Localization.AtPrime import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic import Mathlib.Order.ConditionallyCompleteLattice.Basic @@ -270,8 +271,12 @@ lemma dim_le_one_of_pid [IsDomain R] [IsPrincipalIdealRing R] : krullDim R ≤ 1 lemma dim_le_dim_polynomial_add_one [Nontrivial R] : krullDim R + 1 ≤ krullDim (Polynomial R) := sorry -lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] : - krullDim R + 1 = krullDim (Polynomial R) := sorry +-- lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] : +-- krullDim R + 1 = krullDim (Polynomial R) := sorry + +lemma krull_height_theorem [Nontrivial R] [IsNoetherianRing R] (P: PrimeSpectrum R) (S: Finset R) + (h: P.asIdeal ∈ Ideal.minimalPrimes (Ideal.span S)) : height P ≤ S.card := by + sorry lemma dim_mvPolynomial [Field K] (n : ℕ) : krullDim (MvPolynomial (Fin n) K) = n := sorry diff --git a/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean b/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean index b321c4d..94c93e2 100644 --- a/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean +++ b/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean @@ -8,38 +8,54 @@ import Mathlib.RingTheory.Localization.AtPrime import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic import Mathlib.Order.ConditionallyCompleteLattice.Basic import Mathlib.Data.Set.Ncard +import CommAlg.krull namespace Ideal variable {R : Type _} [CommRing R] (I : PrimeSpectrum R) -noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < I} -noncomputable def krullDim (R : Type) [CommRing R] : WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height I -lemma height_def : height I = Set.chainHeight {J : PrimeSpectrum R | J < I} := rfl -lemma krullDim_def (R : Type) [CommRing R] : krullDim R = (⨆ (I : PrimeSpectrum R), height I : WithBot ℕ∞) := rfl -lemma krullDim_def' (R : Type) [CommRing R] : krullDim R = iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) := rfl +/-- +-- noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < I} +-- noncomputable def krullDim (R : Type) [CommRing R] : WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height I + +-- lemma height_def : height I = Set.chainHeight {J : PrimeSpectrum R | J < I} := rfl +-- lemma krullDim_def (R : Type) [CommRing R] : krullDim R = (⨆ (I : PrimeSpectrum R), height I : WithBot ℕ∞) := rfl +-- lemma krullDim_def' (R : Type) [CommRing R] : krullDim R = iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) := rfl noncomputable instance : CompleteLattice (WithBot (ℕ∞)) := WithBot.WithTop.completeLattice -lemma dim_le_dim_polynomial_add_one [Nontrivial R] : - krullDim R + 1 ≤ krullDim (Polynomial R) := sorry -- Others are working on it +-- lemma dim_le_dim_polynomial_add_one [Nontrivial R] : +-- krullDim R + 1 ≤ krullDim (Polynomial R) := sorry -- Others are working on it -lemma height_le_of_le {I J : PrimeSpectrum R} (I_le_J : I ≤ J) : height I ≤ height J := sorry -- Already done in main file +-- lemma height_le_of_le {I J : PrimeSpectrum R} (I_le_J : I ≤ J) : height I ≤ height J := sorry -- Already done in main file -lemma primeIdeal_finite_height_of_noetherianRing [Nontrivial R] [IsNoetherianRing R] (P: PrimeSpectrum R) : height P ≠ ⊤ := by - sorry +-- lemma primeIdeal_finite_height_of_noetherianRing [Nontrivial R] [IsNoetherianRing R] +-- (P: PrimeSpectrum R) : height P ≠ ⊤ := by +-- sorry +--/ -lemma exist_elts_MinimalOver_of_primeIdeal_of_noetherianRing [Nontrivial R] [IsNoetherianRing R] (P: PrimeSpectrum R) : +lemma exist_elts_MinimalOver_of_primeIdeal_of_noetherianRing [Nontrivial R] [IsNoetherianRing R] + (P: PrimeSpectrum R) (h : height P < ⊤) : ∃S : Set R, Set.ncard s = height P ∧ P.asIdeal ∈ Ideal.minimalPrimes (Ideal.span S) := by sorry -lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] : +lemma dim_eq_dim_polynomial_add_one [h1: Nontrivial R] [IsNoetherianRing R] : krullDim R + 1 = krullDim (Polynomial R) := by rw [le_antisymm_iff] constructor · exact dim_le_dim_polynomial_add_one - · unfold krullDim - have htPBdd : ∀ (P : PrimeSpectrum (Polynomial R)), (height P : WithBot ℕ∞) ≤ (⨆ (I : PrimeSpectrum R), ↑(height I + 1)) := by + · by_cases krullDim R = ⊤ + calc + krullDim (Polynomial R) ≤ ⊤ := le_top + _ ≤ krullDim R := top_le_iff.mpr h + _ ≤ krullDim R + 1 := by + apply le_of_eq + rw [h] + rfl + have h:= Ne.lt_top h + unfold krullDim + have htPBdd : ∀ (P : PrimeSpectrum (Polynomial R)), (height P : WithBot ℕ∞) + ≤ (⨆ (I : PrimeSpectrum R), ↑(height I + 1)) := by intro P have : ∃ (I : PrimeSpectrum R), (height P : WithBot ℕ∞) ≤ ↑(height I + 1) := by have : ∃ M, Ideal.IsMaximal M ∧ P.asIdeal ≤ M := by @@ -53,7 +69,6 @@ lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] : simp only [WithBot.coe_le_coe] have : ∃ (I : PrimeSpectrum R), height P' ≤ height I + 1 := by -- Prime avoidance is called subset_union_prime - sorry obtain ⟨I, h⟩ := this use I @@ -62,7 +77,8 @@ lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] : have : (↑(height I + 1) : WithBot ℕ∞) ≤ ⨆ (I : PrimeSpectrum R), ↑(height I + 1) := by apply @le_iSup (WithBot ℕ∞) _ _ _ I 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 := fun P ↦ (by apply add_le_add_right (@le_iSup (WithBot ℕ∞) _ _ _ P) 1) apply iSup_le