From 6b46181b725d6ecfcc602df3f7ebf6242fa48c5a Mon Sep 17 00:00:00 2001 From: leopoldmayer Date: Mon, 12 Jun 2023 10:22:57 -0700 Subject: [PATCH 1/2] found a bunch of good finite-type algebra lemmas --- comm_alg/resources.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/comm_alg/resources.lean b/comm_alg/resources.lean index bb30ae3..2d5d227 100644 --- a/comm_alg/resources.lean +++ b/comm_alg/resources.lean @@ -7,6 +7,7 @@ useful lemmas and definitions import Mathlib.RingTheory.Ideal.Basic import Mathlib.RingTheory.Noetherian import Mathlib.RingTheory.Artinian +import Mathlib.RingTheory.FiniteType import Mathlib.Order.Height import Mathlib.RingTheory.MvPolynomial.Basic import Mathlib.RingTheory.Ideal.Over @@ -59,6 +60,11 @@ variable (I : Ideal R) --Theorems relating primes of a ring to primes of a quotient #check PrimeSpectrum.range_comap_of_surjective +--There's a lot of theorems about finite-type algebras +#check Algebra.FiniteType.polynomial +#check Algebra.FiniteType.mvPolynomial +#check Algebra.FiniteType.of_surjective + -- There is a notion of short exact sequences but the number of theorems are lacking -- For example, I couldn't find anything saying that for a ses 0 -> A -> B -> C -> 0 -- of R-modules, A and C being FG implies that B is FG From fd5bd05f0109488dd5eb4d4c85c957654c01d41b Mon Sep 17 00:00:00 2001 From: leopoldmayer Date: Mon, 12 Jun 2023 13:03:35 -0700 Subject: [PATCH 2/2] golf, added dim_eq_bot_iff --- CommAlg/krull.lean | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index 1bd2829..228f0b1 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -1,4 +1,5 @@ -import Mathlib.RingTheory.Ideal.Basic +import Mathlib.RingTheory.Ideal.Operations +import Mathlib.RingTheory.FiniteType import Mathlib.Order.Height import Mathlib.RingTheory.PrincipalIdealDomain import Mathlib.RingTheory.DedekindDomain.Basic @@ -33,11 +34,12 @@ noncomputable instance : CompleteLattice (WithBot (ℕ∞)) := WithBot.WithTop.c lemma krullDim_le_iff (R : Type) [CommRing R] (n : ℕ) : iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) ≤ n ↔ - ∀ I : PrimeSpectrum R, (height I : WithBot ℕ∞) ≤ ↑n := by - convert @iSup_le_iff (WithBot ℕ∞) (PrimeSpectrum R) inferInstance _ (↑n) + ∀ I : PrimeSpectrum R, (height I : WithBot ℕ∞) ≤ ↑n := iSup_le_iff (α := WithBot ℕ∞) --some propositions that would be nice to be able to eventually +lemma dim_eq_bot_iff : krullDim R = ⊥ ↔ Subsingleton R := sorry + lemma dim_eq_zero_iff_field [IsDomain R] : krullDim R = 0 ↔ IsField R := by sorry #check Ring.DimensionLEOne