From 7ee38d255cc7a42e66265b339a92262a041594d7 Mon Sep 17 00:00:00 2001 From: Steve Awodey Date: Thu, 18 May 2017 17:54:13 -0400 Subject: [PATCH] left square --- algebra/exact_couple.hlean | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/algebra/exact_couple.hlean b/algebra/exact_couple.hlean index 4de244f..3dcd5d8 100644 --- a/algebra/exact_couple.hlean +++ b/algebra/exact_couple.hlean @@ -121,6 +121,7 @@ section derived_couple local abbreviation k := exact_couple.k EC local abbreviation d := differential EC local abbreviation H := differential_is_differential EC + -- local abbreviation u := exact_couple.i (SES_of_differential d H) definition derived_couple_A : AbGroup := ab_subgroup (image_subgroup i) @@ -172,7 +173,16 @@ definition subgroup_iso_exact_at_A_triangle : ab_kernel_incl i ~ ab_image_incl k induction EC, induction exact_ki, exact im_in_ker b, end -definition +definition subgroup_homom_ker_to_im : ab_kernel i →g ab_image d := + (image_homomorphism k j) ∘g subgroup_iso_exact_at_A +open eq +definition left_square_derived_ses : j_factor ∘g (ab_kernel_incl i) ~ (SES.f (SES_of_differential d H)) ∘g subgroup_homom_ker_to_im := + begin + intro x, + fapply subtype_eq, + refine sorry --(ap (j_factor) subgroup_iso_exact_at_A_triangle) ⬝ _, + end + definition derived_couple_j : derived_couple_A EC →g derived_couple_B EC := begin exact sorry,