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

Merge pull request #19 from GTBarkley/sayantan

Browse source 
new: Added some more theorems about ses
This commit is contained in:
Sayantan Santra 2023-06-12 01:36:53 -05:00 committed by GitHub
commit a157174c65
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
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