comm_alg/CommAlg/sameer(artinian-rings).lean
2023-06-15 10:26:31 -07:00

79 lines
2.8 KiB
Text
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

import Mathlib.RingTheory.Ideal.Basic
import Mathlib.RingTheory.Noetherian
import Mathlib.RingTheory.Artinian
import Mathlib.RingTheory.Ideal.Quotient
import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
import Mathlib.RingTheory.DedekindDomain.DVR
lemma FieldisArtinian (R : Type _) [CommRing R] (h : IsField R) :
IsArtinianRing R := by
let inst := h.toField
rw [isArtinianRing_iff, isArtinian_iff_wellFounded]
apply WellFounded.intro
intro I
constructor
intro J hJI
constructor
intro K hKJ
exfalso
rcases Ideal.eq_bot_or_top J with rfl | rfl
. exact not_lt_bot hKJ
. exact not_top_lt hJI
lemma ArtinianDomainIsField (R : Type _) [CommRing R] [IsDomain R]
(IsArt : IsArtinianRing R) : IsField (R) := by
-- Assume P is nonzero and R is Artinian
-- Localize at P; Then R_P is Artinian;
-- Assume R_P is not a field
-- Then Jacobson Radical of R_P is nilpotent so it's maximal ideal is nilpotent
-- Maximal ideal is zero since local ring is a domain
-- a contradiction since P is nonzero
-- Therefore, R is a field
have maxIdeal := Ideal.exists_maximal R
obtain ⟨m,hm⟩ := maxIdeal
have h:= Ideal.primeCompl_le_nonZeroDivisors m
have artRP : IsDomain _ := IsLocalization.isDomain_localization h
have h' : IsArtinianRing (Localization (Ideal.primeCompl m)) := inferInstance
have h' : IsNilpotent (Ideal.jacobson (⊥ : Ideal (Localization
(Ideal.primeCompl m)))):= IsArtinianRing.isNilpotent_jacobson_bot
have := LocalRing.jacobson_eq_maximalIdeal (⊥ : Ideal (Localization
(Ideal.primeCompl m))) bot_ne_top
rw [this] at h'
have := IsNilpotent.eq_zero h'
rw [Ideal.zero_eq_bot, ← LocalRing.isField_iff_maximalIdeal_eq] at this
by_contra h''
--by_cases h'' : m = ⊥
have := Ring.ne_bot_of_isMaximal_of_not_isField hm h''
have := IsLocalization.AtPrime.not_isField R this (Localization (Ideal.primeCompl m))
contradiction
#check Ideal.IsPrime
#check IsDomain
lemma isArtinianRing_of_quotient_of_artinian (R : Type _) [CommRing R]
(I : Ideal R) (IsArt : IsArtinianRing R) : IsArtinianRing (R I) :=
isArtinian_of_tower R (isArtinian_of_quotient_of_artinian R R I IsArt)
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 Artinian Domain
-- RP is a field by the above lemma
-- P is maximal
have : IsDomain (RP) := Ideal.Quotient.isDomain P
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