michael/Spectral
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

started on derived couple

Browse source
This commit is contained in:
Steve Awodey 2017-04-07 15:05:10 -04:00
parent f76e665dd3
commit 200885ad21
1 changed files with 8 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
algebra/exact_couple.hlean
View file

@ -26,6 +26,14 @@ definition image_subgroup_of_diff {B : AbGroup} (d : B →g B) (H : is_different
definition homology {B : AbGroup} (d : B →g B) (H : is_differential d) : AbGroup := definition homology {B : AbGroup} (d : B →g B) (H : is_differential d) : AbGroup :=
@quotient_ab_group (ab_kernel d) (image_subgroup_of_diff d H) @quotient_ab_group (ab_kernel d) (image_subgroup_of_diff d H)
definition SES_of_differential {B : AbGroup} (d : B →g B) (H : is_differential d) : SES (ab_image d) (ab_kernel d) (homology d H) :=
begin
fapply SES.mk,
sorry,
-- use the more general fact that a subgroup inclusion is a group homomorphism
-- maybe use SES_of_subgroup?
end
structure exact_couple (A B : AbGroup) : Type := structure exact_couple (A B : AbGroup) : Type :=
( i : A →g A) (j : A →g B) (k : B →g A) ( i : A →g A) (j : A →g B) (k : B →g A)
( exact_ij : is_exact i j) ( exact_ij : is_exact i j)