From 6b46181b725d6ecfcc602df3f7ebf6242fa48c5a Mon Sep 17 00:00:00 2001 From: leopoldmayer Date: Mon, 12 Jun 2023 10:22:57 -0700 Subject: [PATCH] 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