From 12fd0191134b40681c263bf3fe1200f0a9f78752 Mon Sep 17 00:00:00 2001 From: leopoldmayer Date: Sun, 11 Jun 2023 21:03:13 -0700 Subject: [PATCH] added to resources --- comm_alg/resources.lean | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/comm_alg/resources.lean b/comm_alg/resources.lean index eae7c89..adcce3a 100644 --- a/comm_alg/resources.lean +++ b/comm_alg/resources.lean @@ -9,6 +9,8 @@ import Mathlib.RingTheory.Noetherian import Mathlib.RingTheory.Artinian import Mathlib.Order.Height 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] @@ -44,4 +46,14 @@ variable (I : Ideal R) #check Polynomial R --this is the polynomial ring with variables indexed by ℕ #check MvPolynomial ℕ R ---hopefully there's good communication between them \ No newline at end of file +--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 \ No newline at end of file