From 8e7ddca721f0f3eb6eca2eb47ac6434ef9328e06 Mon Sep 17 00:00:00 2001 From: Sameer Savkar Date: Mon, 12 Jun 2023 10:34:51 -0700 Subject: [PATCH 1/2] created a new file --- .gitignore | 3 ++- comm_alg/sameer(artinian-rings).lean | 11 +++++++++++ 2 files changed, 13 insertions(+), 1 deletion(-) create mode 100644 comm_alg/sameer(artinian-rings).lean diff --git a/.gitignore b/.gitignore index e254e15..c666579 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,4 @@ /build /lake-packages/* -.DS_Store \ No newline at end of file +.DS_Store +.cache/ \ No newline at end of file diff --git a/comm_alg/sameer(artinian-rings).lean b/comm_alg/sameer(artinian-rings).lean new file mode 100644 index 0000000..aae0fd7 --- /dev/null +++ b/comm_alg/sameer(artinian-rings).lean @@ -0,0 +1,11 @@ +import Mathlib.RingTheory.Ideal.Basic +import Mathlib.RingTheory.Noetherian +import Mathlib.RingTheory.Artinian +import Mathlib.RingTheory.Ideal.Quotient +import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic + +lemma quotientRing_is_Artinian (R : Type _) (isArtinianRing R) (Ideal I) : IsArtinianRing R := by sorry + +lemma IsPrimeisMaximal (R : Type_) (isArtinianRing R) (Ideal I) : IsPrimeisMaximal R := by sorry + +-- Use Stacks project proof since it's broken into lemmas From cbb0c6ce7af913b76cccb7462528aa8d071cc0c5 Mon Sep 17 00:00:00 2001 From: Sameer Savkar Date: Mon, 12 Jun 2023 13:34:09 -0700 Subject: [PATCH 2/2] Defining lemmas --- comm_alg/sameer(artinian-rings).lean | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/comm_alg/sameer(artinian-rings).lean b/comm_alg/sameer(artinian-rings).lean index aae0fd7..381680b 100644 --- a/comm_alg/sameer(artinian-rings).lean +++ b/comm_alg/sameer(artinian-rings).lean @@ -4,8 +4,12 @@ import Mathlib.RingTheory.Artinian import Mathlib.RingTheory.Ideal.Quotient import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic -lemma quotientRing_is_Artinian (R : Type _) (isArtinianRing R) (Ideal I) : IsArtinianRing R := by sorry +lemma quotientRing_is_Artinian (R : Type _) [CommRing R] (I : Ideal R) (IsArt : IsArtinianRing R): +IsArtinianRing (R⧸I) := by sorry + +#check Ideal.IsPrime + +lemma IsPrimeMaximal (R : Type _) [CommRing R] (I : Ideal R) (IsArt : IsArtinianRing R) (isPrime : Ideal.IsPrime I) : Ideal.IsMaximal I := by sorry -lemma IsPrimeisMaximal (R : Type_) (isArtinianRing R) (Ideal I) : IsPrimeisMaximal R := by sorry -- Use Stacks project proof since it's broken into lemmas