Merge pull request #60 from GTBarkley/main

syncing main to monalisa
This commit is contained in:
ah1112 2023-06-14 16:14:44 -04:00 committed by GitHub
commit 009f768db6
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
4 changed files with 79 additions and 50 deletions

View file

@ -15,6 +15,9 @@ import Mathlib.RingTheory.Localization.AtPrime
import Mathlib.Order.ConditionallyCompleteLattice.Basic
import Mathlib.Algebra.Ring.Pi
import Mathlib.RingTheory.Finiteness
import Mathlib.Util.PiNotation
open PiNotation
namespace Ideal
@ -26,6 +29,8 @@ noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J <
noncomputable def krullDim (R : Type) [CommRing R] :
WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height R I
--variable {R}
-- 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
@ -33,7 +38,7 @@ noncomputable def krullDim (R : Type) [CommRing R] :
-- Stacks Definition 10.32.1: An ideal is locally nilpotent
-- if every element is nilpotent
class IsLocallyNilpotent (I : Ideal R) : Prop :=
class IsLocallyNilpotent {R : Type _} [CommRing R] (I : Ideal R) : Prop :=
h : ∀ x ∈ I, IsNilpotent x
#check Ideal.IsLocallyNilpotent
end Ideal
@ -89,6 +94,10 @@ lemma containment_radical_power_containment :
-- Ideal.exists_pow_le_of_le_radical_of_fG
-- 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.
-- Stacks Lemma 10.52.6: I is a maximal ideal and IM = 0. Then length of M is
-- the same as the dimension as a vector space over R/I,
lemma length_eq_dim_if_maximal_annihilates {I : Ideal R} [Ideal.IsMaximal I]
@ -96,48 +105,53 @@ lemma length_eq_dim_if_maximal_annihilates {I : Ideal R} [Ideal.IsMaximal I]
→ Module.length R M = Module.rank RI M(I • ( : Submodule R M)) := by sorry
-- Does lean know that M/IM is a R/I module?
-- Use 10.52.5
-- 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.
lemma power_zero_finite_length : Ideal.FG I → Ideal.IsMaximal I → Module.Finite R M
(∃ n : , (I ^ n) • ( : Submodule R M) = 0)
(∃ m : , Module.length R M ≤ m) := by
intro IisFG IisMaximal MisFinite power
rcases power with ⟨n, npower⟩
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⟩
-- how do I get a generating set?
-- 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
lemma Artinian_has_finite_max_ideal
[IsArtinianRing R] : Finite (MaximalSpectrum R) := by
by_contra infinite
simp only [not_finite_iff_infinite] at infinite
-- Stacks Lemma 10.53.4: R Artinian => Jacobson ideal of R is nilpotent
lemma Jacobson_of_Artinian_is_nilpotent :
IsArtinianRing R → IsNilpotent (Ideal.jacobson ( : Ideal R)) := by sorry
lemma Jacobson_of_Artinian_is_nilpotent
[IsArtinianRing R] : IsNilpotent (Ideal.jacobson (⊥ : Ideal R)) := by
have J := Ideal.jacobson (⊥ : Ideal R)
-- 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
abbrev Prod_of_localization :=
Π I : MaximalSpectrum R, Localization.AtPrime I.1
-- lemma product_of_localization_at_maximal_ideal : Finite (MaximalSpectrum R)
-- ∧
-- instance : CommRing (Prod_of_localization R) := by
-- unfold Prod_of_localization
-- infer_instance
def foo : Prod_of_localization R →+* R where
toFun := sorry
invFun := sorry
left_inv := sorry
right_inv := sorry
map_mul' := sorry
map_add' := sorry
def jaydensRing : Type _ := sorry
-- ∀ I : MaximalSpectrum R, Localization.AtPrime R I
instance : CommRing jaydensRing := sorry -- this should come for free, don't even need to state it
def foo : jaydensRing ≃+* R where
toFun := _
invFun := _
left_inv := _
right_inv := _
map_mul' := _
map_add' := _
-- Ideal.IsLocallyNilpotent (Ideal.jacobson ( : Ideal R)) →
-- Pi.commRing (MaximalSpectrum R) Localization.AtPrime R I
-- := by sorry
-- Haven't finished this.
def product_of_localization_at_maximal_ideal [Finite (MaximalSpectrum R)]
(h : Ideal.IsLocallyNilpotent (Ideal.jacobson (⊥ : Ideal R))) :
Prod_of_localization R ≃+* R := by sorry
-- Stacks Lemma 10.53.6: R is Artinian iff R has finite length as an R-mod
lemma IsArtinian_iff_finite_length :
@ -148,8 +162,8 @@ 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
lemma primes_of_Artinian_are_maximal :
IsArtinianRing R → Ideal.IsPrime I → Ideal.IsMaximal I := by sorry
lemma primes_of_Artinian_are_maximal
[IsArtinianRing R] [Ideal.IsPrime I] : Ideal.IsMaximal I := by sorry
-- Lemma: Krull dimension of a ring is the supremum of height of maximal ideals

View file

@ -63,7 +63,7 @@ lemma krullDim_eq_height [LocalRing R] : krullDim R = height (closedPoint R) :=
apply height_le_of_le
apply le_maximalIdeal
exact I.2.1
. simp
. simp only [height_le_krullDim]
#check height_le_krullDim
--some propositions that would be nice to be able to eventually
@ -135,7 +135,7 @@ lemma dim_field_eq_zero {K : Type _} [Field K] : krullDim K = 0 := by
unfold krullDim
simp [field_prime_height_zero]
lemma isField.dim_zero {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0) : IsField D := by
lemma domain_dim_zero.isField {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0) : IsField D := by
by_contra x
rw [Ring.not_isField_iff_exists_prime] at x
obtain ⟨P, ⟨h1, primeP⟩⟩ := x
@ -156,9 +156,9 @@ lemma isField.dim_zero {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0)
aesop
contradiction
lemma dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krullDim D = 0 ↔ IsField D := by
lemma domain_dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krullDim D = 0 ↔ IsField D := by
constructor
· exact isField.dim_zero
· exact domain_dim_zero.isField
· intro fieldD
let h : Field D := IsField.toField fieldD
exact dim_field_eq_zero
@ -226,7 +226,11 @@ lemma dim_le_dim_polynomial_add_one [Nontrivial R] :
lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] :
krullDim R + 1 = krullDim (Polynomial R) := sorry
lemma dim_mvPolynomial [Field K] (n : ) : krullDim (MvPolynomial (Fin n) K) = n := sorry
lemma height_eq_dim_localization :
height I = krullDim (Localization.AtPrime I.asIdeal) := sorry
lemma dim_quotient_le_dim : height I + krullDim (R I.asIdeal) ≤ krullDim R := sorry
lemma height_add_dim_quotient_le_dim : height I + krullDim (R I.asIdeal) ≤ krullDim R := sorry

View file

@ -6,7 +6,9 @@ import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
import Mathlib.RingTheory.DedekindDomain.DVR
lemma FieldisArtinian (R : Type _) [CommRing R] (IsField : ):= by sorry
lemma FieldisArtinian (R : Type _) [CommRing R] (h: IsField R) :
IsArtinianRing R := by sorry
lemma ArtinianDomainIsField (R : Type _) [CommRing R] [IsDomain R]
@ -47,8 +49,7 @@ lemma isArtinianRing_of_quotient_of_artinian (R : Type _) [CommRing R]
lemma IsPrimeMaximal (R : Type _) [CommRing R] (P : Ideal R)
(IsArt : IsArtinianRing R) (isPrime : Ideal.IsPrime P) : Ideal.IsMaximal P :=
by
-- if R is Artinian and P is prime then R/P is Integral Domain
-- which is Artinian Domain
-- if R is Artinian and P is prime then R/P is Artinian Domain
-- RP is a field by the above lemma
-- P is maximal
@ -56,13 +57,13 @@ by
have artRP : IsArtinianRing (RP) := by
exact isArtinianRing_of_quotient_of_artinian R P IsArt
have artRPField : IsField (RP) := by
exact ArtinianDomainIsField (RP) artRP
have h := Ideal.Quotient.maximal_of_isField P artRPField
exact h
-- Then R/I is Artinian
-- have' : IsArtinianRing R ∧ Ideal.IsPrime I → IsDomain (RI) := by
-- RI.IsArtinian → monotone_stabilizes_iff_artinian.RI
-- Use Stacks project proof since it's broken into lemmas

View file

@ -22,11 +22,7 @@ noncomputable instance : CompleteLattice (WithBot (ℕ∞)) := WithBot.WithTop.c
lemma dim_le_dim_polynomial_add_one [Nontrivial R] :
krullDim R + 1 ≤ krullDim (Polynomial R) := sorry -- Others are working on it
-- private lemma sum_succ_of_succ_sum {ι : Type} (a : ℕ∞) [inst : Nonempty ι] :
-- (⨆ (x : ι), a + 1) = (⨆ (x : ι), a) + 1 := by
-- have : a + 1 = (⨆ (x : ι), a) + 1 := by rw [ciSup_const]
-- have : a + 1 = (⨆ (x : ι), a + 1) := Eq.symm ciSup_const
-- simp
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 dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] :
krullDim R + 1 = krullDim (Polynomial R) := by
@ -37,16 +33,30 @@ lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] :
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
sorry
have : ∃ M, Ideal.IsMaximal M ∧ P.asIdeal ≤ M := by
apply exists_le_maximal
apply IsPrime.ne_top
apply P.IsPrime
obtain ⟨M, maxM, PleM⟩ := this
let P' : PrimeSpectrum (Polynomial R) := PrimeSpectrum.mk M (IsMaximal.isPrime maxM)
have PleP' : P ≤ P' := PleM
have : height P ≤ height P' := height_le_of_le PleP'
simp only [WithBot.coe_le_coe]
have : ∃ (I : PrimeSpectrum R), height P' ≤ height I + 1 := by
sorry
obtain ⟨I, h⟩ := this
use I
exact ge_trans h this
obtain ⟨I, IP⟩ := this
have : (↑(height I + 1) : WithBot ℕ∞) ≤ ⨆ (I : PrimeSpectrum R), ↑(height I + 1) := by
apply @le_iSup (WithBot ℕ∞) _ _ _ I
apply ge_trans this IP
exact ge_trans this IP
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
apply this
simp
simp only [iSup_le_iff]
intro P
exact ge_trans oneOut (htPBdd P)