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

found a bunch of good finite-type algebra lemmas

Browse source
This commit is contained in:
leopoldmayer 2023-06-12 10:22:57 -07:00
parent d9f67a1075
commit 6b46181b72
1 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
comm_alg/resources.lean
View file

@ -7,6 +7,7 @@ useful lemmas and definitions
import Mathlib.RingTheory.Ideal.Basic import Mathlib.RingTheory.Ideal.Basic
import Mathlib.RingTheory.Noetherian import Mathlib.RingTheory.Noetherian
import Mathlib.RingTheory.Artinian import Mathlib.RingTheory.Artinian
import Mathlib.RingTheory.FiniteType
import Mathlib.Order.Height import Mathlib.Order.Height
import Mathlib.RingTheory.MvPolynomial.Basic import Mathlib.RingTheory.MvPolynomial.Basic
import Mathlib.RingTheory.Ideal.Over import Mathlib.RingTheory.Ideal.Over
@ -59,6 +60,11 @@ variable (I : Ideal R)
--Theorems relating primes of a ring to primes of a quotient --Theorems relating primes of a ring to primes of a quotient
#check PrimeSpectrum.range_comap_of_surjective #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 -- 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 -- 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 -- of R-modules, A and C being FG implies that B is FG