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

Merge pull request #21 from GTBarkley/jayden

Browse source 
add lemmas
This commit is contained in:
Jidong Wang 2023-06-12 10:14:26 -07:00 committed by GitHub
commit 3fac57ad02
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 15 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
comm_alg/jayden(krull-dim-zero).lean
View file

@ -1,12 +1,25 @@
import Mathlib.RingTheory.Ideal.Basic import Mathlib.RingTheory.Ideal.Basic
import Mathlib.RingTheory.Noetherian import Mathlib.RingTheory.Noetherian
import Mathlib.Order.KrullDimension
import Mathlib.RingTheory.Artinian import Mathlib.RingTheory.Artinian
import Mathlib.RingTheory.Ideal.Quotient import Mathlib.RingTheory.Ideal.Quotient
import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic 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