From 41922be785ca3dceecac7ceb95c7d8bb9ffefbc6 Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Sun, 11 Jun 2023 21:18:21 -0700 Subject: [PATCH] new: Added some definitions about short exact sequences --- comm_alg/resources.lean | 21 ++++++++++++++++++++- 1 file changed, 20 insertions(+), 1 deletion(-) diff --git a/comm_alg/resources.lean b/comm_alg/resources.lean index adcce3a..5fbc3d6 100644 --- a/comm_alg/resources.lean +++ b/comm_alg/resources.lean @@ -11,6 +11,7 @@ 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] @@ -56,4 +57,22 @@ variable (I : Ideal R) #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 +#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 A': 𝒜} {f : A ⟶ B} {g : B ⟶ C} + +#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 +-- Similar things are there for RightSplit as well \ No newline at end of file