From 81e6c07f23c04e11019f75857b370ca6b50cd883 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Thu, 3 Nov 2016 16:42:12 -0400
Subject: [PATCH] progress on derived exact couples

---
 algebra/exact_couple.hlean | 61 +++++++++++++++++++++++++++-----------
 algebra/subgroup.hlean     | 33 +++++++++++++++++++++
 2 files changed, 77 insertions(+), 17 deletions(-)

diff --git a/algebra/exact_couple.hlean b/algebra/exact_couple.hlean
index 9b64c4e..d7efdde 100644
--- a/algebra/exact_couple.hlean
+++ b/algebra/exact_couple.hlean
@@ -6,29 +6,29 @@ Authors: Egbert Rijke
 Exact couple, derived couples, and so on
 -/
 
-import algebra.group_theory hit.set_quotient types.sigma types.list types.sum
+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
+open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum list trunc function group trunc
      equiv
 
-definition kernel.{l1} {A B : CommGroup.{l1}} (f : A →g B) : CommGroup.{l1} :=
-  begin
-    fapply CommGroup.mk,
-    { exact fiber f 1},
-    fapply comm_group.mk,
-    { intro x, induction x with a p, intro y, induction y with b q, fapply fiber.mk, exact a*b, rewrite respect_mul, rewrite p, rewrite q, apply mul_one},
-    { exact sorry },
-    { intros x y z, induction x with a p, induction y with b q, induction z with c r, esimp, exact sorry }, repeat exact sorry
-  end
-
 structure is_exact {A B C : CommGroup} (f : A →g B) (g : B →g C) :=
   ( im_in_ker : Π(a:A), g (f a) = 1)
-  ( ker_in_im : Π(b:B), (g b = 1) → Σ(a:A), f a = b)  
+  ( ker_in_im : Π(b:B), (g b = 1) → ∃(a:A), f a = b)  
 
-definition isBoundary {B : CommGroup} (d : B →g B) := Π(b:B), d b = 1
+definition is_boundary {B : CommGroup} (d : B →g B) := Π(b:B), d (d b) = 1
 
--- definition homology {B : CommGroup} (d : B →g B) (H : isBoundary d) := 
---   quotient_group (kernel d) (image d)
+definition image_subgroup_of_bd {B : CommGroup} (d : B →g B) (H : is_boundary d) : subgroup_rel (comm_kernel d) :=
+  subgroup_rel_of_subgroup (image_subgroup d) (kernel_subgroup d)
+  begin
+    intro g p, 
+    induction p with f, induction f with h p,
+    rewrite [p⁻¹], 
+    esimp,
+    exact H h 
+  end
+
+definition homology {B : CommGroup} (d : B →g B) (H : is_boundary d) : CommGroup := 
+  @quotient_comm_group (comm_kernel d) (image_subgroup_of_bd d H)
 
 structure exact_couple (A B : CommGroup) : Type :=
   ( i : A →g A) (j : A →g B) (k : B →g A)
@@ -36,7 +36,34 @@ structure exact_couple (A B : CommGroup) : Type :=
   ( exact_jk : is_exact j k)
   ( exact_ki : is_exact k i)
 
-definition boundary {A B : CommGroup} (CC : exact_couple A B) : B →g B := (exact_couple.j CC) ∘g (exact_couple.k CC)
+definition boundary {A B : CommGroup} (CC : exact_couple A B) : B →g B := 
+  (exact_couple.j CC) ∘g (exact_couple.k CC)
 
+definition boundary_is_boundary {A B : CommGroup} (CC : exact_couple A B) : is_boundary (boundary CC) :=
+  begin
+    induction CC, 
+    induction exact_jk, 
+    intro b,
+    exact (ap (group_fun j) (im_in_ker (group_fun k b))) ⬝ (respect_one j)
+  end
 
+section derived_couple
 
+  variables {A B : CommGroup} (CC : exact_couple A B) 
+
+definition derived_couple_A : CommGroup :=
+  comm_subgroup (image_subgroup (exact_couple.i CC))
+
+definition derived_couple_B : CommGroup :=
+  homology (boundary CC) (boundary_is_boundary CC)
+
+definition derived_couple_i : derived_couple_A CC →g derived_couple_A CC :=
+  (image_lift (exact_couple.i CC)) ∘g (image_incl (exact_couple.i CC))
+
+definition derived_couple_j : derived_couple_A CC →g derived_couple_B CC :=
+  begin
+--    refine (comm_gq_map (comm_kernel (boundary CC)) (image_subgroup_of_bd (boundary CC) (boundary_is_boundary CC))) ∘g _,
+  exact sorry
+  end
+
+end derived_couple
diff --git a/algebra/subgroup.hlean b/algebra/subgroup.hlean
index b2ae55b..2badfa2 100644
--- a/algebra/subgroup.hlean
+++ b/algebra/subgroup.hlean
@@ -232,6 +232,8 @@ namespace group
 
   definition kernel {G H : Group} (f : G →g H) : Group := subgroup (kernel_subgroup f)
 
+  definition comm_kernel {G H : CommGroup} (f : G →g H) : CommGroup := comm_subgroup (kernel_subgroup f)
+
   definition incl_of_subgroup [constructor] {G : Group} (H : subgroup_rel G) : subgroup H →g G :=
   begin
     fapply homomorphism.mk,
@@ -252,4 +254,35 @@ namespace group
       -- closed under inverses
     (λ h p, subgroup_respect_inv H1 p)
 
+  definition image {G H : Group} (f : G →g H) : Group :=
+    subgroup (image_subgroup f)
+
+  definition image_incl {G H : Group} (f : G →g H) : image f →g H :=
+    incl_of_subgroup (image_subgroup f)
+
+  definition hom_lift {G H : Group} (f : G →g H) (K : subgroup_rel H) (Hyp : Π (g : G), K (f g)) : G →g subgroup K :=
+  begin
+    fapply homomorphism.mk,
+    intro g,
+    fapply sigma.mk,
+    exact f g,
+    fapply Hyp,
+    intro g h, apply subtype_eq, esimp, apply respect_mul
+  end
+
+  definition image_lift {G H : Group} (f : G →g H) : G →g image f :=
+  begin
+    fapply hom_lift f,
+    intro g, 
+    apply tr,
+    fapply fiber.mk, 
+    exact g, reflexivity
+  end
+
+  definition image_factor {G H : Group} (f : G →g H) : f = (image_incl f) ∘g (image_lift f) :=
+  begin
+    fapply homomorphism_eq,
+    reflexivity
+  end
+
 end group