From 502cae808857735ebd27c842459fd21911a74cae Mon Sep 17 00:00:00 2001 From: Steve Awodey Date: Thu, 18 May 2017 16:45:28 -0400 Subject: [PATCH] exact couple small change --- algebra/exact_couple.hlean | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/algebra/exact_couple.hlean b/algebra/exact_couple.hlean index f3d9225..60744da 100644 --- a/algebra/exact_couple.hlean +++ b/algebra/exact_couple.hlean @@ -108,6 +108,13 @@ definition differential_is_differential {A B : AbGroup} (EC : exact_couple A B) section derived_couple +/- + A - i -> A + k ^ | + | v j + B ====== B +-/ + parameters {A B : AbGroup} (EC : exact_couple A B) local abbreviation i := exact_couple.i EC local abbreviation j := exact_couple.j EC @@ -131,11 +138,9 @@ definition SES_of_exact_couple_at_i : SES (ab_kernel i) A (ab_image i) := fapply ab_group_first_iso_thm i, end -definition kj_zero (a : A) : k (j a) = 1 := - begin - exact sorry - end - +definition kj_zero (a : A) : k (j a) = 1 := +is_exact.im_in_ker (exact_couple.exact_jk EC) a + definition j_factor : A →g (ab_kernel d) := begin fapply ab_hom_lift j, @@ -147,7 +152,6 @@ begin ... = 1 : to_respect_one, end - definition derived_couple_j : derived_couple_A EC →g derived_couple_B EC := begin exact sorry,