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

new: Added some more theorems about ses

Browse source
This commit is contained in:
Sayantan Santra 2023-06-11 23:30:10 -07:00
parent 45c58bf041
commit 9bac6f9aad
Signed by: SinTan1729
GPG key ID: EB3E68BFBA25C85F
1 changed files with 7 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
comm_alg/resources.lean
View file

@ -65,7 +65,7 @@ variable (I : Ideal R)
open CategoryTheory CategoryTheory.Limits CategoryTheory.Preadditive open CategoryTheory CategoryTheory.Limits CategoryTheory.Preadditive
variable {𝒜 : Type _} [Category 𝒜] [Abelian 𝒜] 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
#check ShortExact f g #check ShortExact f g
@ -75,4 +75,9 @@ variable {A B C A': 𝒜} {f : A ⟶ B} {g : B ⟶ C}
#check LeftSplit f g #check LeftSplit f g
-- And there is a theorem that left split implies splitting -- And there is a theorem that left split implies splitting
#check LeftSplit.splitting #check LeftSplit.splitting
-- Similar things are there for RightSplit as well #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