mirror of
https://github.com/GTBarkley/comm_alg.git
synced 2024-12-25 23:28:36 -06:00
commit
a15c96e7b3
1 changed files with 40 additions and 19 deletions
|
@ -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
|
||||
|
||||
|
||||
|
||||
|
|
Loading…
Reference in a new issue