From 3b13474cec8bf6de0de201bd8de51149a348848c Mon Sep 17 00:00:00 2001 From: poincare-duality Date: Mon, 12 Jun 2023 10:13:44 -0700 Subject: [PATCH] add lemmas --- comm_alg/jayden(krull-dim-zero).lean | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) diff --git a/comm_alg/jayden(krull-dim-zero).lean b/comm_alg/jayden(krull-dim-zero).lean index 0e9b32f..7be91c5 100644 --- a/comm_alg/jayden(krull-dim-zero).lean +++ b/comm_alg/jayden(krull-dim-zero).lean @@ -1,12 +1,25 @@ import Mathlib.RingTheory.Ideal.Basic import Mathlib.RingTheory.Noetherian +import Mathlib.Order.KrullDimension import Mathlib.RingTheory.Artinian import Mathlib.RingTheory.Ideal.Quotient import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic -lemma dim_zero_Noetherian_is_Artinian (R : Type _) (IsNoetherianRing R) (krull_dim R = 0) : IsArtinianRing R := by sorry +variable {R : Type _} [CommRing R] --- Use Stacks project proof since it's broken into lemmas +-- Repeats the definition by Monalisa +noncomputable def length : krullDim (Submodule _ _) + + +-- The following is Stacks Lemma 10.60.5 +lemma dim_zero_Noetherian_iff_Artinian (R : Type _) [CommRing R] : + IsNoetherianRing R ∧ krull_dim R = 0 ↔ IsArtinianRing R := by + sorry + +#check IsNoetherianRing + +-- The following is Stacks Lemma 10.53.6 +lemma IsArtinian_iff_finite_length : IsArtinianRing R ↔ ∃ n : ℕ, length R R ≤ n := by sorry