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

added to resources

Browse source
This commit is contained in:
leopoldmayer 2023-06-11 21:03:13 -07:00
parent a8b295fa0e
commit 12fd019113
1 changed files with 13 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
comm_alg/resources.lean
View file

@ -9,6 +9,8 @@ import Mathlib.RingTheory.Noetherian
import Mathlib.RingTheory.Artinian import Mathlib.RingTheory.Artinian
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.AlgebraicGeometry.PrimeSpectrum.Basic
variable {R M : Type _} [CommRing R] [AddCommGroup M] [Module R M] variable {R M : Type _} [CommRing R] [AddCommGroup M] [Module R M]
@ -44,4 +46,14 @@ variable (I : Ideal R)
#check Polynomial R #check Polynomial R
--this is the polynomial ring with variables indexed by ℕ --this is the polynomial ring with variables indexed by ℕ
#check MvPolynomial ℕ R #check MvPolynomial ℕ R
--hopefully there's good communication between them --hopefully there's good communication between them
--There's a preliminary version of the going up theorem
#check Ideal.exists_ideal_over_prime_of_isIntegral
--Theorems relating primes of a ring to primes of its localization
#check PrimeSpectrum.localization_comap_injective
#check PrimeSpectrum.localization_comap_range
--Theorems relating primes of a ring to primes of a quotient
#check PrimeSpectrum.range_comap_of_surjective