comm_alg/CommAlg/jayden(krull-dim-zero).lean

101 lines
3.5 KiB
Text
Raw Normal View History

2023-06-11 23:41:21 -05:00
import Mathlib.RingTheory.Ideal.Basic
2023-06-12 16:14:39 -05:00
import Mathlib.RingTheory.JacobsonIdeal
2023-06-11 23:41:21 -05:00
import Mathlib.RingTheory.Noetherian
2023-06-12 12:13:44 -05:00
import Mathlib.Order.KrullDimension
2023-06-11 23:41:21 -05:00
import Mathlib.RingTheory.Artinian
import Mathlib.RingTheory.Ideal.Quotient
2023-06-12 22:03:43 -05:00
import Mathlib.RingTheory.Nilpotent
2023-06-11 23:41:21 -05:00
import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
2023-06-12 16:14:39 -05:00
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
2023-06-12 22:03:43 -05:00
import Mathlib.Algebra.Ring.Pi
2023-06-12 22:48:42 -05:00
import Mathlib.Topology.NoetherianSpace
2023-06-11 23:41:21 -05:00
2023-06-12 16:14:39 -05:00
-- copy from krull.lean; the name of Krull dimension for rings is changed to krullDim' since krullDim already exists in the librrary
namespace Ideal
2023-06-12 12:13:44 -05:00
2023-06-12 16:14:39 -05:00
variable (R : Type _) [CommRing R] (I : PrimeSpectrum R)
2023-06-12 12:13:44 -05:00
2023-06-12 16:14:39 -05:00
noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < I}
noncomputable def krullDim' (R : Type) [CommRing R] : WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height R I
-- copy ends
-- Stacks Lemma 10.60.5: R is Artinian iff R is Noetherian of dimension 0
2023-06-12 12:13:44 -05:00
lemma dim_zero_Noetherian_iff_Artinian (R : Type _) [CommRing R] :
2023-06-12 22:03:43 -05:00
IsNoetherianRing R ∧ krullDim' R = 0 ↔ IsArtinianRing R := by sorry
2023-06-12 16:32:20 -05:00
2023-06-12 12:13:44 -05:00
#check IsNoetherianRing
2023-06-12 16:14:39 -05:00
#check krullDim
-- Repeats the definition of the length of a module by Monalisa
variable (M : Type _) [AddCommMonoid M] [Module R M]
2023-06-12 22:48:42 -05:00
-- change the definition of length
noncomputable def length := Set.chainHeight {M' : Submodule R M | M' < }
2023-06-12 16:14:39 -05:00
#check length
-- Stacks Lemma 10.53.6: R is Artinian iff R has finite length as an R-mod
2023-06-12 12:13:44 -05:00
lemma IsArtinian_iff_finite_length : IsArtinianRing R ↔ ∃ n : , length R R ≤ n := by sorry
2023-06-11 23:41:21 -05:00
2023-06-12 16:14:39 -05:00
-- Stacks Lemma 10.53.3: R is Artinian iff R has finitely many maximal ideals
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
2023-06-12 22:03:43 -05:00
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)
2023-06-12 22:48:42 -05:00
∧ Ideal.IsLocallyNilpotent (Ideal.jacobson ( : Ideal R)) → Pi.commRing (MaximalSpectrum R) Localization.AtPrime R I
:= by sorry
-- Haven't finished this.
2023-06-12 16:14:39 -05:00
2023-06-12 22:48:42 -05:00
-- 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.
2023-06-12 16:14:39 -05:00
2023-06-12 22:48:42 -05:00
-- 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
2023-06-12 16:14:39 -05:00
-- how to use namespace
2023-06-11 23:41:21 -05:00
2023-06-12 16:14:39 -05:00
namespace something
2023-06-11 23:41:21 -05:00
2023-06-12 16:14:39 -05:00
end something
2023-06-11 23:41:21 -05:00
2023-06-12 16:14:39 -05:00
open something
2023-06-11 23:41:21 -05:00