comm_alg/CommAlg/resources.lean
2023-06-12 17:47:09 +00:00

83 lines
2.6 KiB
Text
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

/-
We don't want to reinvent the wheel, but finding
things in Mathlib can be pretty annoying. This is
a temporary file intended to be a dumping ground for
useful lemmas and definitions
-/
import Mathlib.RingTheory.Ideal.Basic
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
import Mathlib.Algebra.Homology.ShortExact.Abelian
variable {R M : Type _} [CommRing R] [AddCommGroup M] [Module R M]
--ideals are defined
#check Ideal R
variable (I : Ideal R)
--as are prime and maximal (they are defined as typeclasses)
#check (I.IsPrime)
#check (I.IsMaximal)
--a module being Noetherian is also a class
#check IsNoetherian M
#check IsNoetherian I
--a ring is Noetherian if it is Noetherian as a module over itself
#check IsNoetherianRing R
--ditto for Artinian
#check IsArtinian M
#check IsArtinianRing R
--I can't find the theorem that an Artinian ring is noetherian. That could be a good
--thing to add at some point
--Here's the main defintion that will be helpful
#check Set.chainHeight
--this is the polynomial ring R[x]
#check Polynomial R
--this is the polynomial ring with variables indexed by
#check MvPolynomial R
--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
-- 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
open CategoryTheory CategoryTheory.Limits CategoryTheory.Preadditive
variable {𝒜 : Type _} [Category 𝒜] [Abelian 𝒜]
variable {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} {h : LeftSplit f g} {h' : RightSplit f g}
#check ShortExact
#check ShortExact f g
-- There are some notion of splitting as well
#check Splitting
#check LeftSplit
#check LeftSplit f g
-- And there is a theorem that left split implies splitting
#check LeftSplit.splitting
#check LeftSplit.splitting h
-- Similar things are there for RightSplit as well
#check RightSplit.splitting
#check RightSplit.splitting h'
-- There's also a theorem about ismorphisms between short exact sequences
#check isIso_of_shortExact_of_isIso_of_isIso