From 313754ee2b92c99e5ed1a84070bcd5f9095bccd4 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Fri, 16 Jun 2017 17:06:04 -0400 Subject: [PATCH] completed definition of k prime --- algebra/exact_couple.hlean | 67 +++++++++++++++++++++++++++++++++++--- algebra/subgroup.hlean | 14 ++++++++ 2 files changed, 77 insertions(+), 4 deletions(-) diff --git a/algebra/exact_couple.hlean b/algebra/exact_couple.hlean index 2f495c8..ecbccc3 100644 --- a/algebra/exact_couple.hlean +++ b/algebra/exact_couple.hlean @@ -11,6 +11,18 @@ import algebra.group_theory hit.set_quotient types.sigma types.list types.sum .q open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum list trunc function group trunc equiv is_equiv +-- This definition needs to be moved to exactness.hlean. However we had trouble doing so. Please help. +definition iso_ker_im_of_exact {A B C : AbGroup} (f : A →g B) (g : B →g C) (E : is_exact f g) : ab_kernel g ≃g ab_image f := + begin + fapply ab_subgroup_iso, + intro a, + induction E, + exact ker_in_im a, + intro a b, induction b with q, induction q with b p, induction p, + induction E, + exact im_in_ker b, + end + definition is_differential {B : AbGroup} (d : B →g B) := Π(b:B), d (d b) = 1 definition image_subgroup_of_diff {B : AbGroup} (d : B →g B) (H : is_differential d) : subgroup_rel (ab_kernel d) := @@ -214,10 +226,57 @@ definition derived_couple_j_htpy : group_fun (derived_couple_j ∘g SES.g SES_of exact pr2 (center' (derived_couple_j_unique)), end -/-definition derived_couple_j : derived_couple_A EC →g derived_couple_B EC := +definition SES_im_i_trivial : SES trivial_ab_group derived_couple_A derived_couple_A := begin - exact sorry, --- refine (comm_gq_map (comm_kernel (boundary CC)) (image_subgroup_of_bd (boundary CC) (boundary_is_boundary CC))) ∘g _, - end-/ + fapply SES_of_isomorphism_right, + fapply isomorphism.refl, + end + +definition subgroup_iso_exact_kerj_imi : ab_kernel j ≃g ab_image i := + begin + fapply iso_ker_im_of_exact, + induction EC, + exact exact_ij, + end + +definition k_restrict_aux : ab_kernel d →g ab_kernel j := + begin + fapply ab_hom_lift_kernel, + exact k ∘g ab_kernel_incl d, + intro p, induction p with b p, exact p, + end + +definition k_restrict : ab_kernel d →g derived_couple_A := + subgroup_iso_exact_kerj_imi ∘g k_restrict_aux + +definition k_restrict_square_left : k_restrict ∘g (SES.f (SES_of_differential d H)) ~ λ x, 1 := + begin + intro x, + induction x with b' p, + induction p with q, + induction q with b p, + induction p, + fapply subtype_eq, + induction EC, + induction exact_jk, + fapply im_in_ker, + end + +definition derived_couple_k_unique : is_contr + (Σ hC, group_fun (hC ∘g SES.g (SES_of_differential d H)) ~ group_fun + (SES.g SES_im_i_trivial ∘g k_restrict)) + := +quotient_extend_unique_SES (SES_of_differential d H) (SES_im_i_trivial) (trivial_homomorphism (ab_image d) trivial_ab_group) (k_restrict) (k_restrict_square_left) + +definition derived_couple_k : derived_couple_B →g derived_couple_A := + begin + exact pr1 (center' (derived_couple_k_unique)), + end + +definition derived_couple_k_htpy : group_fun (derived_couple_k ∘g SES.g (SES_of_differential d H)) ~ group_fun + (SES.g (SES_im_i_trivial) ∘g k_restrict) := + begin + exact pr2 (center' (derived_couple_k_unique)), + end end derived_couple diff --git a/algebra/subgroup.hlean b/algebra/subgroup.hlean index dac59c2..bda2cbd 100644 --- a/algebra/subgroup.hlean +++ b/algebra/subgroup.hlean @@ -332,6 +332,20 @@ f = incl_of_subgroup K ∘g hom_lift f K Hyp := reflexivity end +definition ab_hom_lift_kernel [constructor] {A B C : AbGroup} (f : A →g B) (g : B →g C) (Hyp : Π (a : A), g (f a) = 1) : A →g ab_kernel g := + begin + fapply ab_hom_lift, + exact f, + intro a, + exact Hyp a, + end + +definition ab_hom_lift_kernel_factors {A B C : AbGroup} (f : A →g B) (g : B →g C) (Hyp : Π (a : A), g (f a) = 1) : +f = ab_kernel_incl g ∘g ab_hom_lift_kernel f g Hyp := + begin + fapply ab_hom_factors_through_lift, + end + definition image_lift [constructor] {G H : Group} (f : G →g H) : G →g image f := begin fapply hom_lift f,