SinTan1729/comm_alg
1
0
Fork 0
mirror of https://github.com/GTBarkley/comm_alg.git synced 2024-12-26 07:38:36 -06:00
Code Issues Projects Releases Packages Wiki Activity

Merge pull request #69 from GTBarkley/jayden

Browse source 
more stuff
This commit is contained in:
Jidong Wang 2023-06-14 19:14:29 -07:00 committed by GitHub
commit b7aae64f76
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 18 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
CommAlg/jayden(krull-dim-zero).lean
View file

@ -19,7 +19,6 @@ import Mathlib.Util.PiNotation
open PiNotation open PiNotation
namespace Ideal namespace Ideal
variable (R : Type _) [CommRing R] (P : PrimeSpectrum R) variable (R : Type _) [CommRing R] (P : PrimeSpectrum R)
@ -116,13 +115,30 @@ lemma power_zero_finite_length [Ideal.IsMaximal I] (h₁ : Ideal.FG I) [Module.F
-- rcases power with ⟨n, npower⟩ -- rcases power with ⟨n, npower⟩
-- how do I get a generating set? -- how do I get a generating set?
open Finset
-- Stacks Lemma 10.53.3: R is Artinian iff R has finitely many maximal ideals -- Stacks Lemma 10.53.3: R is Artinian iff R has finitely many maximal ideals
lemma Artinian_has_finite_max_ideal lemma Artinian_has_finite_max_ideal
[IsArtinianRing R] : Finite (MaximalSpectrum R) := by [IsArtinianRing R] : Finite (MaximalSpectrum R) := by
by_contra infinite by_contra infinite
simp only [not_finite_iff_infinite] at infinite simp only [not_finite_iff_infinite] at infinite
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
have comaximal : ∀ i j : ℕ, i ≠ j → (m' i).asIdeal ⊔ (m' j).asIdeal =
(⊤ : Ideal R) := by
intro i j distinct
apply Ideal.IsMaximal.coprime_of_ne
sorry
sorry
-- by_contra equal
have : (m' i) ≠ (m' j) := by
exact Function.Injective.ne m'inj distinct
intro h
apply this
exact MaximalSpectrum.ext _ _ h
-- let g :`= Ideal.quotientInfRingEquivPiQuotient m' comaximal
-- Stacks Lemma 10.53.4: R Artinian => Jacobson ideal of R is nilpotent -- Stacks Lemma 10.53.4: R Artinian => Jacobson ideal of R is nilpotent
lemma Jacobson_of_Artinian_is_nilpotent lemma Jacobson_of_Artinian_is_nilpotent