From e87c235e24950f5e5b8d2872677275716d4a261a Mon Sep 17 00:00:00 2001
From: Steve Awodey <sawodey@gmail.com>
Date: Thu, 10 Nov 2016 16:49:09 -0500
Subject: [PATCH] WIP on exact couple and basic group theory

---
 algebra/.#exact_couple.hlean |  1 -
 algebra/exact_couple.hlean   | 30 +++++++++++++++---------------
 algebra/quotient_group.hlean |  5 ++++-
 3 files changed, 19 insertions(+), 17 deletions(-)
 delete mode 120000 algebra/.#exact_couple.hlean

diff --git a/algebra/.#exact_couple.hlean b/algebra/.#exact_couple.hlean
deleted file mode 120000
index c4be726..0000000
--- a/algebra/.#exact_couple.hlean
+++ /dev/null
@@ -1 +0,0 @@
-Steve@steveawodeysAir.wv.cc.cmu.edu.255
\ No newline at end of file
diff --git a/algebra/exact_couple.hlean b/algebra/exact_couple.hlean
index d7efdde..68507ce 100644
--- a/algebra/exact_couple.hlean
+++ b/algebra/exact_couple.hlean
@@ -15,9 +15,9 @@ 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)  
 
-definition is_boundary {B : CommGroup} (d : B →g B) := Π(b:B), d (d b) = 1
+definition is_differential {B : CommGroup} (d : B →g B) := Π(b:B), d (d b) = 1
 
-definition image_subgroup_of_bd {B : CommGroup} (d : B →g B) (H : is_boundary d) : subgroup_rel (comm_kernel d) :=
+definition image_subgroup_of_diff {B : CommGroup} (d : B →g B) (H : is_differential d) : subgroup_rel (comm_kernel d) :=
   subgroup_rel_of_subgroup (image_subgroup d) (kernel_subgroup d)
   begin
     intro g p, 
@@ -27,8 +27,8 @@ definition image_subgroup_of_bd {B : CommGroup} (d : B →g B) (H : is_boundary
     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)
+definition homology {B : CommGroup} (d : B →g B) (H : is_differential d) : CommGroup := 
+  @quotient_comm_group (comm_kernel d) (image_subgroup_of_diff d H)
 
 structure exact_couple (A B : CommGroup) : Type :=
   ( i : A →g A) (j : A →g B) (k : B →g A)
@@ -36,12 +36,12 @@ 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 differential {A B : CommGroup} (EC : exact_couple A B) : B →g B := 
+  (exact_couple.j EC) ∘g (exact_couple.k EC)
 
-definition boundary_is_boundary {A B : CommGroup} (CC : exact_couple A B) : is_boundary (boundary CC) :=
+definition differential_is_differential {A B : CommGroup} (EC : exact_couple A B) : is_differential (differential EC) :=
   begin
-    induction CC, 
+    induction EC, 
     induction exact_jk, 
     intro b,
     exact (ap (group_fun j) (im_in_ker (group_fun k b))) ⬝ (respect_one j)
@@ -49,21 +49,21 @@ definition boundary_is_boundary {A B : CommGroup} (CC : exact_couple A B) : is_b
 
 section derived_couple
 
-  variables {A B : CommGroup} (CC : exact_couple A B) 
+  variables {A B : CommGroup} (EC : exact_couple A B) 
 
 definition derived_couple_A : CommGroup :=
-  comm_subgroup (image_subgroup (exact_couple.i CC))
+  comm_subgroup (image_subgroup (exact_couple.i EC))
 
 definition derived_couple_B : CommGroup :=
-  homology (boundary CC) (boundary_is_boundary CC)
+  homology (differential EC) (differential_is_differential EC)
 
-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_i : derived_couple_A EC →g derived_couple_A EC :=
+  (image_lift (exact_couple.i EC)) ∘g (image_incl (exact_couple.i EC))
 
-definition derived_couple_j : derived_couple_A CC →g derived_couple_B CC :=
+definition derived_couple_j : derived_couple_A EC →g derived_couple_B EC :=
   begin
+  exact sorry,
 --    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/quotient_group.hlean b/algebra/quotient_group.hlean
index ecdb1d0..0421e9f 100644
--- a/algebra/quotient_group.hlean
+++ b/algebra/quotient_group.hlean
@@ -248,7 +248,10 @@ definition comm_group_first_iso_thm (A B : CommGroup) (f : A →g B) : quotient_
     fapply image_lift,
     intro a,
     intro k,
-    fapply comm_gq_map_eq_one  (f a),
+    fapply image_incl_eq_one,
+    exact k,
+    exact sorry,
+    -- show that the above map is injective and surjective.
   end  
 
     /- set generating normal subgroup -/