mirror of
https://github.com/GTBarkley/comm_alg.git
synced 2024-12-26 07:38:36 -06:00
commit
165d598066
1 changed files with 9 additions and 5 deletions
|
@ -125,19 +125,23 @@ lemma Artinian_has_finite_max_ideal
|
||||||
let m' : ℕ ↪ MaximalSpectrum R := Infinite.natEmbedding (MaximalSpectrum R)
|
let m' : ℕ ↪ MaximalSpectrum R := Infinite.natEmbedding (MaximalSpectrum R)
|
||||||
have m'inj := m'.injective
|
have m'inj := m'.injective
|
||||||
let m'' : ℕ → Ideal R := fun n : ℕ ↦ ⨅ k ∈ range n, (m' k).asIdeal
|
let m'' : ℕ → Ideal R := fun n : ℕ ↦ ⨅ k ∈ range n, (m' k).asIdeal
|
||||||
|
let f : ℕ → Ideal R := fun n : ℕ ↦ (m' n).asIdeal
|
||||||
|
let F : Fin n → Ideal R := fun k ↦ (m' k).asIdeal
|
||||||
have comaximal : ∀ i j : ℕ, i ≠ j → (m' i).asIdeal ⊔ (m' j).asIdeal =
|
have comaximal : ∀ i j : ℕ, i ≠ j → (m' i).asIdeal ⊔ (m' j).asIdeal =
|
||||||
(⊤ : Ideal R) := by
|
(⊤ : Ideal R) := by
|
||||||
intro i j distinct
|
intro i j distinct
|
||||||
apply Ideal.IsMaximal.coprime_of_ne
|
apply Ideal.IsMaximal.coprime_of_ne
|
||||||
sorry
|
exact (m' i).IsMaximal
|
||||||
sorry
|
exact (m' j).IsMaximal
|
||||||
-- by_contra equal
|
|
||||||
have : (m' i) ≠ (m' j) := by
|
have : (m' i) ≠ (m' j) := by
|
||||||
exact Function.Injective.ne m'inj distinct
|
exact Function.Injective.ne m'inj distinct
|
||||||
intro h
|
intro h
|
||||||
apply this
|
apply this
|
||||||
exact MaximalSpectrum.ext _ _ h
|
exact MaximalSpectrum.ext _ _ h
|
||||||
-- let g :`= Ideal.quotientInfRingEquivPiQuotient m' comaximal
|
have ∀ n : ℕ, (R ⧸ ⨅ (i : Fin n), (F n) i) ≃+* ((i : Fin n) → R ⧸ (F n) i) := by
|
||||||
|
sorry
|
||||||
|
-- (let F : Fin n → Ideal R := fun k : Fin n ↦ (m' k).asIdeal)
|
||||||
|
-- let g := Ideal.quotientInfRingEquivPiQuotient f 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
|
||||||
|
@ -193,7 +197,7 @@ lemma dim_zero_Noetherian_iff_Artinian (R : Type _) [CommRing R] :
|
||||||
constructor
|
constructor
|
||||||
apply finite_length_is_Noetherian
|
apply finite_length_is_Noetherian
|
||||||
rwa [IsArtinian_iff_finite_length] at RisArtinian
|
rwa [IsArtinian_iff_finite_length] at RisArtinian
|
||||||
sorry
|
sorry -- can use Grant's lemma dim_eq_zero_iff
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
Loading…
Reference in a new issue