diff --git a/CommAlg/grant.lean b/CommAlg/grant.lean index 2f3c634..2261f25 100644 --- a/CommAlg/grant.lean +++ b/CommAlg/grant.lean @@ -17,6 +17,8 @@ import CommAlg.krull #check JordanHolderLattice +section Chains + variable {α : Type _} [Preorder α] (s : Set α) def finFun_to_list {n : ℕ} : (Fin n → α) → List α := by sorry @@ -26,7 +28,6 @@ def series_to_chain : StrictSeries s → s.subchain ⟨ finFun_to_list (fun x => toFun x), sorry⟩ - -- there should be a coercion from WithTop ℕ to WithBot (WithTop ℕ) but it doesn't seem to work -- it looks like this might be because someone changed the instance from CoeCT to Coe during the port -- actually it looks like we can coerce to WithBot (ℕ∞) fine @@ -40,15 +41,62 @@ lemma twoHeights : s ≠ ∅ → (some (Set.chainHeight s) : WithBot (WithTop -- norm_cast sorry +end Chains + +section Krull + +variable (R : Type _) [CommRing R] (M : Type _) [AddCommGroup M] [Module R M] + open Ideal -lemma krullDim_le_iff' (R : Type _) [CommRing R] : +-- chain of primes +#check height + +-- lemma height_ge_iff {𝔭 : PrimeSpectrum R} {n : ℕ∞} : +-- height 𝔭 ≥ n ↔ := sorry + +lemma height_ge_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 + . -- change ∃c, _ ∧ _ ∧ ((List.length c : ℕ∞) = ⊤ + 1) at h + -- rw [WithTop.top_add] at h + 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 → 𝔮 < 𝔭) ∧ _) ↔ _ + have h := fun (c : List (PrimeSpectrum R)) => (@WithTop.coe_eq_coe _ (List.length c) n) + constructor <;> rintro ⟨c, hc⟩ <;> use c --<;> tauto--<;> exact ⟨hc.1, by tauto⟩ + . --rw [and_assoc] + -- show _ ∧ _ ∧ _ + --exact ⟨hc.1, _⟩ + tauto + . change _ ∧ _ ∧ (List.length c : ℕ∞) = n + 1 at hc + norm_cast at hc + tauto + +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] : +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 - +#check (sorry : False) +#check (sorryAx) +#check (4 : WithBot ℕ∞) +#check List.sum -- #check ((4 : ℕ∞) : WithBot (WithTop ℕ)) -#check ( (Set.chainHeight s) : WithBot (ℕ∞)) \ No newline at end of file +-- #check ( (Set.chainHeight s) : WithBot (ℕ∞)) + +variable (P : PrimeSpectrum R) + +#check {J | J < P}.le_chainHeight_iff (n := 4) diff --git a/CommAlg/jayden(krull-dim-zero).lean b/CommAlg/jayden(krull-dim-zero).lean index 0646bcb..3651102 100644 --- a/CommAlg/jayden(krull-dim-zero).lean +++ b/CommAlg/jayden(krull-dim-zero).lean @@ -4,15 +4,16 @@ import Mathlib.RingTheory.Noetherian import Mathlib.Order.KrullDimension import Mathlib.RingTheory.Artinian import Mathlib.RingTheory.Ideal.Quotient +import Mathlib.RingTheory.Nilpotent import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic - import Mathlib.AlgebraicGeometry.PrimeSpectrum.Maximal import Mathlib.Data.Finite.Defs - import Mathlib.Order.Height import Mathlib.RingTheory.DedekindDomain.Basic import Mathlib.RingTheory.Localization.AtPrime import Mathlib.Order.ConditionallyCompleteLattice.Basic +import Mathlib.Algebra.Ring.Pi +import Mathlib.Topology.NoetherianSpace -- copy from krull.lean; the name of Krull dimension for rings is changed to krullDim' since krullDim already exists in the librrary namespace Ideal @@ -26,21 +27,9 @@ noncomputable def krullDim' (R : Type) [CommRing R] : WithBot ℕ∞ := ⨆ (I : -- Stacks Lemma 10.60.5: R is Artinian iff R is Noetherian of dimension 0 lemma dim_zero_Noetherian_iff_Artinian (R : Type _) [CommRing R] : - IsNoetherianRing R ∧ krullDim' R = 0 ↔ IsArtinianRing R := by + IsNoetherianRing R ∧ krullDim' R = 0 ↔ IsArtinianRing R := by sorry -variable {R : Type _} [CommRing R] - --- Repeats the definition by Monalisa -noncomputable def length : krullDim (Submodule _ _) - - --- The following is Stacks Lemma 10.60.5 -lemma dim_zero_Noetherian_iff_Artinian (R : Type _) [CommRing R] : - IsNoetherianRing R ∧ krull_dim R = 0 ↔ IsArtinianRing R := by - - sorry - #check IsNoetherianRing #check krullDim @@ -48,7 +37,8 @@ lemma dim_zero_Noetherian_iff_Artinian (R : Type _) [CommRing R] : -- Repeats the definition of the length of a module by Monalisa variable (M : Type _) [AddCommMonoid M] [Module R M] -noncomputable def length := krullDim (Submodule R M) +-- change the definition of length +noncomputable def length := Set.chainHeight {M' : Submodule R M | M' < ⊤} #check length -- Stacks Lemma 10.53.6: R is Artinian iff R has finite length as an R-mod @@ -58,9 +48,42 @@ lemma IsArtinian_iff_finite_length : IsArtinianRing R ↔ ∃ n : ℕ, length R lemma IsArtinian_iff_finite_max_ideal : IsArtinianRing R ↔ Finite (MaximalSpectrum R) := by sorry -- Stacks Lemma 10.53.4: R Artinian => Jacobson ideal of R is nilpotent -lemma Jacobson_of_Artinian_is_nilpotent : Is +lemma Jacobson_of_Artinian_is_nilpotent : IsArtinianRing R → IsNilpotent (Ideal.jacobson (⊤ : Ideal R)) := by sorry +-- Stacks Definition 10.32.1: An ideal is locally nilpotent +-- if every element is nilpotent +namespace Ideal +class IsLocallyNilpotent (I : Ideal R) : Prop := + h : ∀ x ∈ I, IsNilpotent x + +end Ideal + +#check Ideal.IsLocallyNilpotent + +-- Stacks Lemma 10.53.5: If R has finitely many maximal ideals and +-- locally nilpotent Jacobson radical, then R is the product of its localizations at +-- its maximal ideals. Also, all primes are maximal + +lemma product_of_localization_at_maximal_ideal : Finite (MaximalSpectrum R) + ∧ Ideal.IsLocallyNilpotent (Ideal.jacobson (⊤ : Ideal R)) → Pi.commRing (MaximalSpectrum R) Localization.AtPrime R I + := by sorry +-- Haven't finished this. + +-- Stacks Lemma 10.31.5: R is Noetherian iff Spec(R) is a Noetherian space +lemma ring_Noetherian_iff_spec_Noetherian : IsNoetherianRing R + ↔ TopologicalSpace.NoetherianSpace (PrimeSpectrum R) := by sorry +-- Use TopologicalSpace.NoetherianSpace.exists_finset_irreducible : +-- Every closed subset of a noetherian space is a finite union +-- of irreducible closed subsets. + + +-- Stacks Lemma 10.26.1 (Should already exists) +-- (1) The closure of a prime P is V(P) +-- (2) the irreducible closed subsets are V(P) for P prime +-- (3) the irreducible components are V(P) for P minimal prime + +-- Stacks Lemma 10.32.5: R Noetherian. I,J ideals. If J ⊂ √I, then J ^ n ⊂ I for some n -- how to use namespace @@ -70,8 +93,6 @@ end something open something --- The following is Stacks Lemma 10.53.6 -lemma IsArtinian_iff_finite_length : IsArtinianRing R ↔ ∃ n : ℕ, length R R ≤ n := by sorry