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

exact couple still

Browse source
This commit is contained in:
Steve Awodey 2017-04-27 18:07:30 -04:00
parent 6e13cb9dad
commit cefdc8f4e7
1 changed files with 27 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
algebra/exact_couple.hlean
View file

@ -32,13 +32,37 @@ definition diff_im_in_ker {B : AbGroup} (d : B →g B) (H : is_differential d) :
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 homology_ugly {B : AbGroup} (d : B →g B) (H : is_differential d) : AbGroup :=
(quotient_ab_group (image_subgroup (ab_subgroup_of_subgroup_incl (diff_im_in_ker d H))))
definition SES_of_differential {B : AbGroup} (d : B →g B) (H : is_differential d) : SES (ab_image d) (ab_kernel d) (quotient_ab_group (image_subgroup (ab_subgroup_of_subgroup_incl (diff_im_in_ker d H)))) := definition homology_iso_ugly {B : AbGroup} (d : B →g B) (H : is_differential d) : (homology d H) ≃g (homology_ugly d H) :=
begin begin
rexact SES_of_inclusion (ab_subgroup_of_subgroup_incl (diff_im_in_ker d H)) (is_embedding_ab_subgroup_of_subgroup_incl (diff_im_in_ker d H)), -- fapply quotientgroupiso ...
exact sorry
end end
definition SES_iso_C {A B C C' : AbGroup} (ses : SES A B C) (k : C ≃g C') : SES A B C' :=
begin
fapply SES.mk,
exact SES.f ses,
exact k ∘g SES.g ses,
exact SES.Hf ses,
fapply @is_surjective_compose _ _ _ k (SES.g ses),
exact is_surjective_of_is_equiv k,
exact SES.Hg ses,
fapply is_exact.mk,
repeat exact sorry
end
definition SES_of_differential_ugly {B : AbGroup} (d : B →g B) (H : is_differential d) : SES (ab_image d) (ab_kernel d) (homology_ugly d H) :=
begin
exact SES_of_inclusion (ab_subgroup_of_subgroup_incl (diff_im_in_ker d H)) (is_embedding_ab_subgroup_of_subgroup_incl (diff_im_in_ker d H)),
end
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
exact SES_of_inclusion (ab_subgroup_of_subgroup_incl (diff_im_in_ker d H)) (is_embedding_ab_subgroup_of_subgroup_incl (diff_im_in_ker d H)),
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)