From cefdc8f4e7b1e2b3116187268bcb43578322cb62 Mon Sep 17 00:00:00 2001 From: Steve Awodey Date: Thu, 27 Apr 2017 18:07:30 -0400 Subject: [PATCH] exact couple still --- algebra/exact_couple.hlean | 30 +++++++++++++++++++++++++++--- 1 file changed, 27 insertions(+), 3 deletions(-) diff --git a/algebra/exact_couple.hlean b/algebra/exact_couple.hlean index 0cf6d8f..4a6726c 100644 --- a/algebra/exact_couple.hlean +++ b/algebra/exact_couple.hlean @@ -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 := @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 - 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 + +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 := ( i : A →g A) (j : A →g B) (k : B →g A)