From 91931ca338e6f8ba54c44a6b6790350dc4b4950c Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Thu, 30 Mar 2017 15:02:14 -0400
Subject: [PATCH] generalize is_exact

---
 algebra/ses.hlean                   | 40 +++++++++++++----------------
 homotopy/cohomology.hlean           | 12 ---------
 homotopy/pushout.hlean              |  4 ---
 homotopy/spherical_fibrations.hlean |  2 +-
 move_to_lib.hlean                   | 18 +++++++++++++
 pointed.hlean                       |  2 +-
 6 files changed, 38 insertions(+), 40 deletions(-)

diff --git a/algebra/ses.hlean b/algebra/ses.hlean
index 22f06bf..5af0b09 100644
--- a/algebra/ses.hlean
+++ b/algebra/ses.hlean
@@ -3,7 +3,7 @@ Copyright (c) 2017 Egbert Rijke. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Egbert Rijke
 
-Basic facts about short exact sequences. 
+Basic facts about short exact sequences.
 
 At the moment, it only covers short exact sequences of abelian groups, but this should be extended to short exact sequences in any abelian category.
 -/
@@ -13,18 +13,14 @@ 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
 
-structure is_exact {A B C : AbGroup} (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) → image_subgroup f b)
-
 structure SES (A B C : AbGroup) :=
   ( f : A →g B)
   ( g : B →g C)
   ( Hf : is_embedding f)
   ( Hg : is_surjective g)
-  ( ex : is_exact f g)
+  ( ex : is_exact_ag 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)) := 
+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),
@@ -37,7 +33,7 @@ definition SES_of_inclusion {A B : AbGroup} (f : A →g B) (Hf : is_embedding f)
     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
+    exact rel_of_ab_qg_map_eq_one _ p
   end
 
 definition SES_of_subgroup {B : AbGroup} (S : subgroup_rel B) : SES (ab_subgroup S) B (quotient_ab_group S) :=
@@ -73,7 +69,7 @@ definition SES_of_homomorphism {A B : AbGroup} (f : A →g B) : SES (ab_kernel f
     exact is_surjective_image_lift f,
     fapply is_exact.mk,
     intro a, induction a with a p, fapply subtype_eq, exact p,
-    intro a p, fapply tr, fapply fiber.mk, fapply sigma.mk, exact a, 
+    intro a p, fapply tr, fapply fiber.mk, fapply sigma.mk, exact a,
     exact calc
       f a = image_incl f (image_lift f a) : by exact homotopy_of_eq (ap group_fun (image_factor f)) a
       ... = image_incl f 1 : ap (image_incl f) p
@@ -90,10 +86,10 @@ definition SES_of_isomorphism_right {B C : AbGroup} (g : B ≃g C) : SES trivial
     fapply is_surjective_of_is_equiv,
     fapply is_exact.mk,
     intro a, induction a, fapply respect_one,
-    intro b p, 
+    intro b p,
     have q : g b = g 1,
-    from p ⬝ (respect_one g)⁻¹, 
-    note r := eq_of_fn_eq_fn (equiv_of_isomorphism g) q, 
+    from p ⬝ (respect_one g)⁻¹,
+    note r := eq_of_fn_eq_fn (equiv_of_isomorphism g) q,
     fapply tr, fapply fiber.mk, exact unit.star, rewrite r,
   end
 
@@ -113,10 +109,10 @@ parameters {A B C : AbGroup} (ses : SES A B C)
   local abbreviation q := ab_qg_map (kernel_subgroup g)
   local abbreviation B_mod_A := quotient_ab_group (kernel_subgroup g)
 
---definition quotient_SES {A B C : AbGroup} (ses : SES A B C) : 
+--definition quotient_SES {A B C : AbGroup} (ses : SES A B C) :
 --  quotient_ab_group (image_subgroup (SES.f ses)) ≃g C :=
 --  begin
---    fapply ab_group_first_iso_thm B C (SES.g ses), 
+--    fapply ab_group_first_iso_thm B C (SES.g ses),
 --  end
 
 -- definition pre_right_extend_SES (to separate the following definition and replace C with B/A)
@@ -137,7 +133,7 @@ definition quotient_triangle_extend_SES {C': AbGroup} (k : B →g C') :
   (Σ (h : C →g C'), h ∘g g ~ k) ≃ (Σ (h' : B_mod_A →g C'), h' ∘g q ~ k) :=
   begin
     fapply equiv.mk,
-    intro pair, induction pair with h H, 
+    intro pair, induction pair with h H,
     fapply sigma.mk, exact h ∘g α, intro b,
     exact H b,
     fapply adjointify,
@@ -153,8 +149,8 @@ definition quotient_triangle_extend_SES {C': AbGroup} (k : B →g C') :
     esimp, fapply is_prop.elimo, fapply pi.is_trunc_pi, intro a, fapply is_trunc_eq,
   end
 
-  parameters {A' B' C' : AbGroup} 
-  (ses' : SES A' B' C')  
+  parameters {A' B' C' : AbGroup}
+  (ses' : SES A' B' C')
   (hA : A →g A') (hB : B →g B') (htpy1 : hB ∘g f ~ (SES.f ses') ∘g hA)
 
   local abbreviation f' := SES.f ses'
@@ -162,12 +158,12 @@ definition quotient_triangle_extend_SES {C': AbGroup} (k : B →g C') :
   local abbreviation ex' := SES.ex ses'
   local abbreviation q' := ab_qg_map (kernel_subgroup g')
   local abbreviation α' := quotient_codomain_SES
-  
+
   include htpy1
 
-  definition quotient_extend_unique_SES : is_contr (Σ (hC : C →g C'), hC ∘g g ~ g' ∘g hB) := 
+  definition quotient_extend_unique_SES : is_contr (Σ (hC : C →g C'), hC ∘g g ~ g' ∘g hB) :=
   begin
-    fapply @(is_trunc_equiv_closed_rev _ (quotient_triangle_extend_SES (g' ∘g hB))), 
+    fapply @(is_trunc_equiv_closed_rev _ (quotient_triangle_extend_SES (g' ∘g hB))),
     fapply ab_qg_universal_property,
     intro b, intro K,
     have k : trunctype.carrier (image_subgroup f b), from is_exact.ker_in_im ex b K,
@@ -198,7 +194,7 @@ definition quotient_extend_SES_square : k ∘g (ab_qg_map (kernel_subgroup g)) ~
     fapply quotient_group_compute
   end
 
-definition right_extend_SES  : C →g C' := 
+definition right_extend_SES  : C →g C' :=
   α' ∘g k ∘g α⁻¹ᵍ
 
 local abbreviation hC := right_extend_SES
@@ -229,7 +225,7 @@ definition right_extend_SES_unique_map (hC' : C →g C') (htpy2' : hC' ∘g g ~
   begin
     exact calc
       hC ~ α' ∘g k ∘g α⁻¹ᵍ : by reflexivity
-     ... ~ α' ∘g α'⁻¹ᵍ ∘g hC' ∘g α ∘g α⁻¹ᵍ : 
+     ... ~ α' ∘g α'⁻¹ᵍ ∘g hC' ∘g α ∘g α⁻¹ᵍ :
      ... ~ hC' ∘g α ∘g α⁻¹ᵍ : _
      ... ~ hC' : _
   end
diff --git a/homotopy/cohomology.hlean b/homotopy/cohomology.hlean
index 4fc57e2..5326a17 100644
--- a/homotopy/cohomology.hlean
+++ b/homotopy/cohomology.hlean
@@ -11,18 +11,6 @@ import .spectrum .EM ..algebra.arrow_group .fwedge ..choice .pushout ..move_to_l
 open eq spectrum int trunc pointed EM group algebra circle sphere nat EM.ops equiv susp is_trunc
      function fwedge cofiber bool lift sigma is_equiv choice pushout algebra unit pi
 
--- TODO: move
-structure is_exact {A B : Type} {C : Type*} (f : A → B) (g : B → C) :=
-  ( im_in_ker : Π(a:A), g (f a) = pt)
-  ( ker_in_im : Π(b:B), (g b = pt) → image f b)
-
-definition is_exact_g {A B C : Group} (f : A →g B) (g : B →g C) :=
-is_exact f g
-
-definition is_exact_g.mk {A B C : Group} {f : A →g B} {g : B →g C}
-  (H₁ : Πa, g (f a) = 1) (H₂ : Πb, g b = 1 → image f b) : is_exact_g f g :=
-is_exact.mk H₁ H₂
-
 definition is_exact_trunc_functor {A B : Type} {C : Type*} {f : A → B} {g : B → C}
   (H : is_exact_t f g) : @is_exact _ _ (ptrunc 0 C) (trunc_functor 0 f) (trunc_functor 0 g) :=
 begin
diff --git a/homotopy/pushout.hlean b/homotopy/pushout.hlean
index af83bc4..bf4a9d7 100644
--- a/homotopy/pushout.hlean
+++ b/homotopy/pushout.hlean
@@ -464,10 +464,6 @@ namespace pushout
 
   /- universal property of cofiber -/
 
-  structure is_exact_t {A B : Type} {C : Type*} (f : A → B) (g : B → C) :=
-  ( im_in_ker : Π(a:A), g (f a) = pt)
-  ( ker_in_im : Π(b:B), (g b = pt) → fiber f b)
-
   definition cofiber_exact_1 {X Y Z : Type*} (f : X →* Y) (g : pcofiber f →* Z) :
     (g ∘* pcod f) ∘* f ~* pconst X Z :=
   !passoc ⬝* pwhisker_left _ !pcod_pcompose ⬝* !pcompose_pconst
diff --git a/homotopy/spherical_fibrations.hlean b/homotopy/spherical_fibrations.hlean
index a53c6ea..6c81560 100644
--- a/homotopy/spherical_fibrations.hlean
+++ b/homotopy/spherical_fibrations.hlean
@@ -59,7 +59,7 @@ namespace spherical_fibrations
   begin
     intro X, cases X with X p,
     apply sigma.mk (psusp X), induction p with f, apply tr,
-    apply susp.psusp_equiv f
+    apply susp.psusp_pequiv f
   end
 
   definition BF_of_BG {n : ℕ} : BG n → BF n :=
diff --git a/move_to_lib.hlean b/move_to_lib.hlean
index f33b397..3bd5d09 100644
--- a/move_to_lib.hlean
+++ b/move_to_lib.hlean
@@ -8,6 +8,24 @@ open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc
 definition add_comm_right {A : Type} [add_comm_semigroup A] (n m k : A) : n + m + k = n + k + m :=
 !add.assoc ⬝ ap (add n) !add.comm ⬝ !add.assoc⁻¹
 
+structure is_exact_t {A B : Type} {C : Type*} (f : A → B) (g : B → C) :=
+  ( im_in_ker : Π(a:A), g (f a) = pt)
+  ( ker_in_im : Π(b:B), (g b = pt) → fiber f b)
+
+structure is_exact {A B : Type} {C : Type*} (f : A → B) (g : B → C) :=
+  ( im_in_ker : Π(a:A), g (f a) = pt)
+  ( ker_in_im : Π(b:B), (g b = pt) → image f b)
+
+definition is_exact_g {A B C : Group} (f : A →g B) (g : B →g C) :=
+is_exact f g
+
+definition is_exact_ag {A B C : AbGroup} (f : A →g B) (g : B →g C) :=
+is_exact f g
+
+definition is_exact_g.mk {A B C : Group} {f : A →g B} {g : B →g C}
+  (H₁ : Πa, g (f a) = 1) (H₂ : Πb, g b = 1 → image f b) : is_exact_g f g :=
+is_exact.mk H₁ H₂
+
 namespace algebra
   definition inf_group_loopn (n : ℕ) (A : Type*) [H : is_succ n] : inf_group (Ω[n] A) :=
   by induction H; exact _
diff --git a/pointed.hlean b/pointed.hlean
index 33dc9c0..9faf663 100644
--- a/pointed.hlean
+++ b/pointed.hlean
@@ -930,7 +930,7 @@ namespace pointed
             (ppcompose_left_loop_phomotopy' (pmap_of_map f x₀) !pconst) :=
   begin
     fapply phomotopy.mk,
-    { esimp, esimp [pmap_eq_equiv], intro p,
+    { esimp, intro p,
      refine _ ⬝ ap011 (λx y, phomotopy_of_eq (ap1_gen _ x y _))
                  proof !eq_of_phomotopy_refl⁻¹ qed proof !eq_of_phomotopy_refl⁻¹ qed,
      refine _ ⬝ ap phomotopy_of_eq !ap1_gen_idp_left⁻¹,