mirror of
https://github.com/GTBarkley/comm_alg.git
synced 2024-12-26 07:38:36 -06:00
79 lines
2.8 KiB
Text
79 lines
2.8 KiB
Text
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
|
||
-- R⧸P is a field by the above lemma
|
||
-- P is maximal
|
||
|
||
have : IsDomain (R⧸P) := Ideal.Quotient.isDomain P
|
||
have artRP : IsArtinianRing (R⧸P) := by
|
||
exact isArtinianRing_of_quotient_of_artinian R P IsArt
|
||
|
||
have artRPField : IsField (R⧸P) := by
|
||
exact ArtinianDomainIsField (R⧸P) artRP
|
||
|
||
have h := Ideal.Quotient.maximal_of_isField P artRPField
|
||
exact h
|
||
|
||
-- Then R/I is Artinian
|
||
-- have' : IsArtinianRing R ∧ Ideal.IsPrime I → IsDomain (R⧸I) := by
|
||
|
||
-- R⧸I.IsArtinian → monotone_stabilizes_iff_artinian.R⧸I
|