From 9bac6f9aad370e7e9325672aba2e6a96c9c7fc52 Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Sun, 11 Jun 2023 23:30:10 -0700 Subject: [PATCH] new: Added some more theorems about ses --- comm_alg/resources.lean | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/comm_alg/resources.lean b/comm_alg/resources.lean index 5fbc3d6..bb30ae3 100644 --- a/comm_alg/resources.lean +++ b/comm_alg/resources.lean @@ -65,7 +65,7 @@ variable (I : Ideal R) open CategoryTheory CategoryTheory.Limits CategoryTheory.Preadditive variable {𝒜 : Type _} [Category 𝒜] [Abelian 𝒜] -variable {A B C A': 𝒜} {f : A ⟶ B} {g : B ⟶ C} +variable {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} {h : LeftSplit f g} {h' : RightSplit f g} #check ShortExact #check ShortExact f g @@ -75,4 +75,9 @@ variable {A B C A': 𝒜} {f : A ⟶ B} {g : B ⟶ C} #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 +#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