From 159ea323abbf1f398924823ea6e3fbf1418ff1e1 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Thu, 16 Feb 2017 22:26:06 -0500 Subject: [PATCH] SES_hom extension lemma --- algebra/exact_couple.hlean | 98 ++++++++++++++++++++++++++++++------ algebra/quotient_group.hlean | 10 ++++ algebra/subgroup.hlean | 17 +++++++ 3 files changed, 111 insertions(+), 14 deletions(-) diff --git a/algebra/exact_couple.hlean b/algebra/exact_couple.hlean index 63ae837..b3dfb5a 100644 --- a/algebra/exact_couple.hlean +++ b/algebra/exact_couple.hlean @@ -9,7 +9,7 @@ Exact couple, derived couples, and so on import algebra.group_theory hit.set_quotient types.sigma types.list types.sum .quotient_group .subgroup open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum list trunc function group trunc - equiv + equiv is_equiv structure is_exact {A B C : AbGroup} (f : A →g B) (g : B →g C) := ( im_in_ker : Π(a:A), g (f a) = 1) @@ -22,6 +22,34 @@ structure SES (A B C : AbGroup) := ( Hg : is_surjective g) ( ex : is_exact f g) +definition SES_of_inclusion {A B : AbGroup} (f : A →g B) (Hf : is_embedding f) : SES A B (quotient_ab_group (image_subgroup f)) := + begin + have Hg : is_surjective (ab_qg_map (image_subgroup f)), + from is_surjective_ab_qg_map (image_subgroup f), + fapply SES.mk, + exact f, + exact ab_qg_map (image_subgroup f), + exact Hf, + exact Hg, + fapply is_exact.mk, + intro a, + fapply qg_map_eq_one, fapply tr, fapply fiber.mk, exact a, reflexivity, + intro b, intro p, + fapply rel_of_ab_qg_map_eq_one, assumption + end + +definition SES_of_surjective_map {B C : AbGroup} (g : B →g C) (Hg : is_surjective g) : SES (ab_kernel g) B C := + begin + fapply SES.mk, + exact ab_kernel_incl g, + exact g, + exact is_embedding_ab_kernel_incl g, + exact Hg, + fapply is_exact.mk, + intro a, induction a with a p, exact p, + intro b p, fapply tr, fapply fiber.mk, fapply sigma.mk, exact b, exact p, reflexivity, + end + structure hom_SES {A B C A' B' C' : AbGroup} (ses : SES A B C) (ses' : SES A' B' C') := ( hA : A →g A') ( hB : B →g B') @@ -37,34 +65,76 @@ structure hom_SES {A B C A' B' C' : AbGroup} (ses : SES A B C) (ses' : SES A' B' -- definition pre_right_extend_SES (to separate the following definition and replace C with B/A) -definition right_extend_SES {A B C A' B' C' : AbGroup} - (ses : SES A B C) (ses' : SES A' B' C') - (hA : A →g A') (hB : B →g B') (htpy1 : hB ∘g (SES.f ses) ~ (SES.f ses') ∘g hA) : C →g C' := +definition quotient_codomain_SES {A B C : AbGroup} (ses : SES A B C) : quotient_ab_group (kernel_subgroup (SES.g ses)) ≃g C := begin - refine _ ∘g (codomain_surjection_is_quotient (SES.g ses) (SES.Hg ses))⁻¹ᵍ, - refine (codomain_surjection_is_quotient (SES.g ses') (SES.Hg ses')) ∘g _, - fapply ab_group_quotient_homomorphism B B' (kernel_subgroup (SES.g ses)) (kernel_subgroup (SES.g ses')) hB, + exact (codomain_surjection_is_quotient (SES.g ses) (SES.Hg ses)) + end + +definition quotient_triangle_SES {A B C : AbGroup} (ses : SES A B C) : (quotient_codomain_SES ses) ∘g (ab_qg_map (kernel_subgroup (SES.g ses))) ~ (SES.g ses) := + begin + reflexivity + end + +section short_exact_sequences + parameters {A B C A' B' C' : AbGroup} + (ses : SES A B C) (ses' : SES A' B' C') + (hA : A →g A') (hB : B →g B') (htpy1 : hB ∘g (SES.f ses) ~ (SES.f ses') ∘g hA) + + local abbreviation f := SES.f ses + local abbreviation g := SES.g ses + local abbreviation ex := SES.ex ses + local abbreviation q := ab_qg_map (kernel_subgroup g) + local abbreviation f' := SES.f ses' + local abbreviation g' := SES.g ses' + local abbreviation ex' := SES.ex ses' + local abbreviation q' := ab_qg_map (kernel_subgroup g') + local abbreviation α := quotient_codomain_SES ses + local abbreviation α' := quotient_codomain_SES ses' + + include htpy1 + + -- We define a group homomorphism B/ker(g) →g B'/ker(g'), keeping in mind that ker(g)=A and ker(g')=A'. +definition quotient_extend_SES : quotient_ab_group (kernel_subgroup g) →g quotient_ab_group (kernel_subgroup g') := + begin + fapply ab_group_quotient_homomorphism B B' (kernel_subgroup g) (kernel_subgroup g') hB, intro b, intro K, - have k : trunctype.carrier (image_subgroup (SES.f ses) b), from is_exact.ker_in_im (SES.ex ses) b K, + have k : trunctype.carrier (image_subgroup f b), from is_exact.ker_in_im ex b K, induction k, induction a with a p, rewrite [p⁻¹], rewrite [htpy1 a], - fapply is_exact.im_in_ker (SES.ex ses') (hA a), + fapply is_exact.im_in_ker ex' (hA a) end -definition right_extend_hom_SES {A B C A' B' C' : AbGroup} - (ses : SES A B C) (ses' : SES A' B' C') - (hA : A →g A') (hB : B →g B') (htpy1 : hB ∘g (SES.f ses) ~ (SES.f ses') ∘g hA) : hom_SES ses ses' := + local abbreviation k := quotient_extend_SES + +definition quotient_extend_SES_square : k ∘g (ab_qg_map (kernel_subgroup g)) ~ (ab_qg_map (kernel_subgroup g')) ∘g hB := + begin + fapply quotient_group_compute + end + +definition right_extend_SES : C →g C' := + α' ∘g k ∘g α⁻¹ᵍ + +local abbreviation hC := right_extend_SES + +definition right_extend_hom_SES : hom_SES ses ses' := begin fapply hom_SES.mk, exact hA, exact hB, - exact right_extend_SES ses ses' hA hB htpy1, + exact hC, exact htpy1, - exact sorry -- fapply quotient_group_compute, + exact calc + hC ∘g g ~ hC ∘g α ∘g q : by reflexivity + ... ~ α' ∘g k ∘g α⁻¹ᵍ ∘g α ∘g q : by reflexivity + ... ~ α' ∘g k ∘g q : by exact hwhisker_left (α' ∘g k) (hwhisker_right q (left_inv α)) + ... ~ α' ∘g q' ∘g hB : by exact hwhisker_left α' (quotient_extend_SES_square) + ... ~ g' ∘g hB : by reflexivity end +end short_exact_sequences + 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) := diff --git a/algebra/quotient_group.hlean b/algebra/quotient_group.hlean index 4177481..8bba373 100644 --- a/algebra/quotient_group.hlean +++ b/algebra/quotient_group.hlean @@ -195,6 +195,16 @@ namespace group apply rel_of_eq _ H end + definition rel_of_ab_qg_map_eq_one {K : subgroup_rel A} (a :A) (H : ab_qg_map K a = 1) : K a := + begin + have e : (a * 1⁻¹ = a), + from calc + a * 1⁻¹ = a * 1 : one_inv + ... = a : mul_one, + rewrite (inverse e), + apply rel_of_eq _ H + end + definition quotient_group_elim_fun [unfold 6] (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) (g : quotient_group N) : G' := begin diff --git a/algebra/subgroup.hlean b/algebra/subgroup.hlean index 088ca44..1ed1376 100644 --- a/algebra/subgroup.hlean +++ b/algebra/subgroup.hlean @@ -241,6 +241,23 @@ namespace group intro g h, reflexivity end + definition is_embedding_incl_of_subgroup {G : Group} (H : subgroup_rel G) : is_embedding (incl_of_subgroup H) := + begin + fapply function.is_embedding_of_is_injective, + intro h h', + fapply subtype_eq + end + + definition ab_kernel_incl {G H : AbGroup} (f : G →g H) : ab_kernel f →g G := + begin + fapply incl_of_subgroup, + end + + definition is_embedding_ab_kernel_incl {G H : AbGroup} (f : G →g H) : is_embedding (ab_kernel_incl f) := + begin + fapply is_embedding_incl_of_subgroup, + end + definition subgroup_rel_of_subgroup {G : Group} (H1 H2 : subgroup_rel G) (hyp : Π (g : G), subgroup_rel.R H1 g → subgroup_rel.R H2 g) : subgroup_rel (subgroup H2) := subgroup_rel.mk -- definition of the subset