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

276 lines
10 KiB
Text
Raw Normal View History

2023-06-11 23:41:21 -05:00
import Mathlib.RingTheory.Ideal.Basic
2023-06-13 19:21:42 -05:00
import Mathlib.RingTheory.Ideal.Operations
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-12 16:14:39 -05:00
import Mathlib.AlgebraicGeometry.PrimeSpectrum.Maximal
2023-06-13 19:21:42 -05:00
import Mathlib.AlgebraicGeometry.PrimeSpectrum.Noetherian
2023-06-12 16:14:39 -05:00
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-13 19:21:42 -05:00
import Mathlib.RingTheory.Finiteness
2023-06-14 15:09:23 -05:00
import Mathlib.Util.PiNotation
2023-06-16 16:37:06 -05:00
import Mathlib.RingTheory.Ideal.MinimalPrime
2023-06-15 22:45:29 -05:00
import CommAlg.krull
2023-06-14 15:09:23 -05:00
open PiNotation
2023-06-11 23:41:21 -05:00
2023-06-13 19:21:42 -05:00
namespace Ideal
2023-06-12 12:13:44 -05:00
2023-06-13 19:21:42 -05:00
variable (R : Type _) [CommRing R] (P : PrimeSpectrum R)
2023-06-12 16:14:39 -05:00
2023-06-15 22:45:29 -05:00
-- noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < P}
2023-06-12 16:14:39 -05:00
2023-06-15 22:45:29 -05:00
-- noncomputable def krullDim (R : Type) [CommRing R] :
-- WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height R I
2023-06-12 16:32:20 -05:00
2023-06-14 15:09:23 -05:00
--variable {R}
2023-06-13 19:21: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
2023-06-12 12:13:44 -05:00
2023-06-13 19:21:42 -05:00
-- Stacks Definition 10.32.1: An ideal is locally nilpotent
-- if every element is nilpotent
2023-06-14 15:09:23 -05:00
class IsLocallyNilpotent {R : Type _} [CommRing R] (I : Ideal R) : Prop :=
2023-06-13 19:21:42 -05:00
h : ∀ x ∈ I, IsNilpotent x
#check Ideal.IsLocallyNilpotent
end Ideal
2023-06-12 12:13:44 -05:00
2023-06-16 16:37:06 -05:00
def RingJacobson (R) [Ring R] := Ideal.jacobson (⊥ : Ideal R)
2023-06-12 16:14:39 -05:00
-- Repeats the definition of the length of a module by Monalisa
2023-06-13 19:21:42 -05:00
variable (R : Type _) [CommRing R] (I J : Ideal R)
2023-06-12 16:14:39 -05:00
variable (M : Type _) [AddCommMonoid M] [Module R M]
2023-06-13 19:21:42 -05:00
-- change the definition of length of a module
namespace Module
2023-06-12 22:48:42 -05:00
noncomputable def length := Set.chainHeight {M' : Submodule R M | M' < }
2023-06-13 19:21:42 -05:00
end Module
2023-06-12 16:14:39 -05:00
2023-06-13 19:21:42 -05:00
-- Stacks Lemma 10.31.5: R is Noetherian iff Spec(R) is a Noetherian space
example [IsNoetherianRing R] :
TopologicalSpace.NoetherianSpace (PrimeSpectrum R) :=
inferInstance
2023-06-11 23:41:21 -05:00
2023-06-13 19:21:42 -05:00
instance ring_Noetherian_of_spec_Noetherian
[TopologicalSpace.NoetherianSpace (PrimeSpectrum R)] :
IsNoetherianRing R where
noetherian := by sorry
2023-06-12 16:14:39 -05:00
2023-06-13 19:21:42 -05:00
lemma ring_Noetherian_iff_spec_Noetherian : IsNoetherianRing R
↔ TopologicalSpace.NoetherianSpace (PrimeSpectrum R) := by
constructor
intro RisNoetherian
2023-06-15 22:45:29 -05:00
sorry
sorry
2023-06-13 19:21:42 -05:00
-- how do I apply an instance to prove one direction?
2023-06-12 22:03:43 -05:00
2023-06-15 23:34:38 -05:00
-- Stacks Lemma 5.9.2:
2023-06-13 19:21:42 -05:00
-- Use TopologicalSpace.NoetherianSpace.exists_finset_irreducible :
-- Every closed subset of a noetherian space is a finite union
-- of irreducible closed subsets.
2023-06-12 22:03:43 -05:00
2023-06-13 19:21:42 -05:00
-- Stacks Lemma 10.32.5: R Noetherian. I,J ideals.
-- If J ⊂ √I, then J ^ n ⊂ I for some n. In particular, locally nilpotent
-- and nilpotent are the same for Noetherian rings
lemma containment_radical_power_containment :
IsNoetherianRing R ∧ J ≤ Ideal.radical I → ∃ n : , J ^ n ≤ I := by
rintro ⟨RisNoetherian, containment⟩
rw [isNoetherianRing_iff_ideal_fg] at RisNoetherian
specialize RisNoetherian (Ideal.radical I)
2023-06-13 23:17:54 -05:00
-- rcases RisNoetherian with ⟨S, Sgenerates⟩
have containment2 : ∃ n : , (Ideal.radical I) ^ n ≤ I := by
apply Ideal.exists_radical_pow_le_of_fg I RisNoetherian
cases' containment2 with n containment2'
have containment3 : J ^ n ≤ (Ideal.radical I) ^ n := by
apply Ideal.pow_mono containment
use n
apply le_trans containment3 containment2'
-- The above can be proven using the following quicker theorem that is in the wrong place.
-- Ideal.exists_pow_le_of_le_radical_of_fG
2023-06-12 22:03:43 -05:00
2023-06-13 19:21:42 -05:00
2023-06-14 15:09:23 -05:00
-- Stacks Lemma 10.52.5: R → S is a ring map. M is an S-mod.
-- Then length_R M ≥ length_S M.
-- Stacks Lemma 10.52.5': equality holds if R → S is surjective.
2023-06-13 19:21:42 -05:00
-- Stacks Lemma 10.52.6: I is a maximal ideal and IM = 0. Then length of M is
2023-06-13 23:17:54 -05:00
-- the same as the dimension as a vector space over R/I,
2023-06-15 22:45:29 -05:00
-- lemma length_eq_dim_if_maximal_annihilates {I : Ideal R} [Ideal.IsMaximal I]
-- : I • ( : Submodule R M) = 0
-- → Module.length R M = Module.rank RI M(I • ( : Submodule R M)) := by sorry
2023-06-13 23:17:54 -05:00
-- Does lean know that M/IM is a R/I module?
2023-06-14 15:09:23 -05:00
-- Use 10.52.5
2023-06-13 19:21:42 -05:00
-- Stacks Lemma 10.52.8: I is a finitely generated maximal ideal of R.
-- M is a finite R-mod and I^nM=0. Then length of M is finite.
2023-06-14 15:09:23 -05:00
lemma power_zero_finite_length [Ideal.IsMaximal I] (h₁ : Ideal.FG I) [Module.Finite R M]
(h₂ : (∃ n : , (I ^ n) • ( : Submodule R M) = 0)) :
(∃ m : , Module.length R M ≤ m) := by sorry
-- intro IisFG IisMaximal MisFinite power
-- rcases power with ⟨n, npower⟩
2023-06-13 19:21:42 -05:00
-- how do I get a generating set?
2023-06-14 21:14:01 -05:00
open Finset
2023-06-13 19:21:42 -05:00
-- Stacks Lemma 10.53.3: R is Artinian iff R has finitely many maximal ideals
2023-06-14 15:09:23 -05:00
lemma Artinian_has_finite_max_ideal
[IsArtinianRing R] : Finite (MaximalSpectrum R) := by
by_contra infinite
simp only [not_finite_iff_infinite] at infinite
2023-06-14 21:14:01 -05:00
let m' : ↪ MaximalSpectrum R := Infinite.natEmbedding (MaximalSpectrum R)
have m'inj := m'.injective
let m'' : → Ideal R := fun n : ↦ ⨅ k ∈ range n, (m' k).asIdeal
2023-06-15 22:45:29 -05:00
-- let f : → MaximalSpectrum R := fun n : ↦ m' n
-- let F : (n : ) → Fin n → MaximalSpectrum R := fun n k ↦ m' k
have DCC : ∃ n : , ∀ k : , n ≤ k → m'' n = m'' k := by
apply IsArtinian.monotone_stabilizes {
toFun := m''
monotone' := sorry
}
cases' DCC with n DCCn
specialize DCCn (n+1)
specialize DCCn (Nat.le_succ n)
have containment1 : m'' n < (m' (n + 1)).asIdeal := by sorry
have : ∀ (j : ), (j ≠ n + 1) → ∃ x, x ∈ (m' j).asIdeal ∧ x ∉ (m' (n+1)).asIdeal := by
intro j jnotn
have notcontain : ¬ (m' j).asIdeal ≤ (m' (n+1)).asIdeal := by
-- apply Ideal.IsMaximal (m' j).asIdeal
sorry
2023-06-14 23:32:22 -05:00
sorry
2023-06-15 22:45:29 -05:00
sorry
-- have distinct : (m' j).asIdeal ≠ (m' (n+1)).asIdeal := by
-- intro h
-- apply Function.Injective.ne m'inj jnotn
-- exact MaximalSpectrum.ext _ _ h
-- simp
-- unfold
2023-06-13 19:21:42 -05:00
-- Stacks Lemma 10.53.4: R Artinian => Jacobson ideal of R is nilpotent
2023-06-15 22:45:29 -05:00
-- This is in mathlib: IsArtinianRing.isNilpotent_jacobson_bot
2023-06-12 22:03:43 -05:00
-- 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
2023-06-14 15:09:23 -05:00
abbrev Prod_of_localization :=
Π I : MaximalSpectrum R, Localization.AtPrime I.1
-- instance : CommRing (Prod_of_localization R) := by
-- unfold Prod_of_localization
-- infer_instance
def foo : Prod_of_localization R →+* R where
toFun := sorry
2023-06-15 23:34:38 -05:00
-- invFun := sorry
2023-06-16 16:37:06 -05:00
--left_inv := sorry
--right_inv := sorry
2023-06-14 15:09:23 -05:00
map_mul' := sorry
map_add' := sorry
def product_of_localization_at_maximal_ideal [Finite (MaximalSpectrum R)]
2023-06-16 16:37:06 -05:00
(h : Ideal.IsLocallyNilpotent (RingJacobson R)) :
R ≃+* Prod_of_localization R := by sorry
2023-06-12 16:14:39 -05:00
2023-06-13 19:21:42 -05:00
-- Stacks Lemma 10.53.6: R is Artinian iff R has finite length as an R-mod
lemma IsArtinian_iff_finite_length :
IsArtinianRing R ↔ (∃ n : , Module.length R R ≤ n) := by sorry
-- Lemma: if R has finite length as R-mod, then R is Noetherian
lemma finite_length_is_Noetherian :
(∃ n : , Module.length R R ≤ n) → IsNoetherianRing R := by sorry
-- Lemma: if R is Artinian then all the prime ideals are maximal
2023-06-14 15:09:23 -05:00
lemma primes_of_Artinian_are_maximal
[IsArtinianRing R] [Ideal.IsPrime I] : Ideal.IsMaximal I := by sorry
2023-06-13 19:21:42 -05:00
-- Lemma: Krull dimension of a ring is the supremum of height of maximal ideals
2023-06-16 16:37:06 -05:00
-- Lemma: X is an irreducible component of Spec(R) ↔ X = V(I) for I a minimal prime
lemma irred_comp_minmimal_prime (X) :
X ∈ irreducibleComponents (PrimeSpectrum R)
↔ ∃ (P : minimalPrimes R), X = PrimeSpectrum.zeroLocus P := by
sorry
-- Lemma: localization of Noetherian ring is Noetherian
-- lemma localization_of_Noetherian_at_prime [IsNoetherianRing R]
-- (atprime: Ideal.IsPrime I) :
-- IsNoetherianRing (Localization.AtPrime I) := by sorry
2023-06-13 19:21:42 -05:00
-- Stacks Lemma 10.60.5: R is Artinian iff R is Noetherian of dimension 0
2023-06-16 16:37:06 -05:00
lemma Artinian_if_dim_le_zero_Noetherian (R : Type _) [CommRing R] :
IsNoetherianRing R ∧ Ideal.krullDim R ≤ 0 → IsArtinianRing R := by
2023-06-15 23:34:38 -05:00
rintro ⟨RisNoetherian, dimzero⟩
rw [ring_Noetherian_iff_spec_Noetherian] at RisNoetherian
2023-06-16 16:37:06 -05:00
have := fun X => (irred_comp_minmimal_prime R X).mp
choose F hf using this
2023-06-15 23:34:38 -05:00
let Z := irreducibleComponents (PrimeSpectrum R)
2023-06-16 16:37:06 -05:00
-- have Zfinite : Set.Finite Z := by
2023-06-15 23:34:38 -05:00
-- apply TopologicalSpace.NoetherianSpace.finite_irreducibleComponents ?_
2023-06-16 16:37:06 -05:00
-- sorry
--let P := fun
rw [← ring_Noetherian_iff_spec_Noetherian] at RisNoetherian
have PrimeIsMaximal : ∀ X : Z, Ideal.IsMaximal (F X X.2).1 := by
intro X
have prime : Ideal.IsPrime (F X X.2).1 := (F X X.2).2.1.1
rw [Ideal.dim_le_zero_iff] at dimzero
exact dimzero ⟨_, prime⟩
have JacLocallyNil : Ideal.IsLocallyNilpotent (RingJacobson R) := by sorry
let Loc := fun X : Z ↦ Localization.AtPrime (F X.1 X.2).1
have LocNoetherian : ∀ X, IsNoetherianRing (Loc X) := by
intro X
2023-06-15 23:34:38 -05:00
sorry
2023-06-16 16:37:06 -05:00
-- apply IsLocalization.isNoetherianRing (F X.1 X.2).1 (Loc X) RisNoetherian
have Locdimzero : ∀ X, Ideal.krullDim (Loc X) ≤ 0 := by sorry
have powerannihilates : ∀ X, ∃ n : ,
((F X.1 X.2).1) ^ n • (: Submodule R (Loc X)) = 0 := by sorry
have LocFinitelength : ∀ X, ∃ n : , Module.length R (Loc X) ≤ n := by
intro X
have idealfg : Ideal.FG (F X.1 X.2).1 := by
rw [isNoetherianRing_iff_ideal_fg] at RisNoetherian
specialize RisNoetherian (F X.1 X.2).1
exact RisNoetherian
have modulefg : Module.Finite R (Loc X) := by sorry -- not sure if this is true
specialize PrimeIsMaximal X
specialize powerannihilates X
apply power_zero_finite_length R (F X.1 X.2).1 (Loc X) idealfg powerannihilates
have RingFinitelength : ∃ n : , Module.length R R ≤ n := by sorry
rw [IsArtinian_iff_finite_length]
exact RingFinitelength
lemma dim_le_zero_Noetherian_if_Artinian (R : Type _) [CommRing R] :
IsArtinianRing R → IsNoetherianRing R ∧ Ideal.krullDim R ≤ 0 := by
2023-06-13 19:21:42 -05:00
intro RisArtinian
constructor
apply finite_length_is_Noetherian
rwa [IsArtinian_iff_finite_length] at RisArtinian
2023-06-15 22:45:29 -05:00
rw [Ideal.dim_le_zero_iff]
intro I
apply primes_of_Artinian_are_maximal
2023-06-13 19:21:42 -05:00
2023-06-12 16:14:39 -05:00
2023-06-12 22:48:42 -05:00
2023-06-11 23:41:21 -05:00