Require Import Basics Types WildCat HSet Pointed.Core Pointed.pTrunc Pointed.pEquiv
  Modalities.ReflectiveSubuniverse Truncations.Core Truncations.SeparatedTrunc
  AbGroups Homotopy.ExactSequence
  AbSES.Core AbSES.Pullback AbSES.Pushout BaerSum Ext PullbackFiberSequence.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

(** * The contravariant six-term sequence of Ext *)

(** We construct the contravariant six-term exact sequence of Ext groups associated to any short exact sequence [A -> E -> B] and coefficient group [G]. The existence of this exact sequence follows from the final result in [PullbackFiberSequence]. However, with that definition it becomes a bit tricky to show that the connecting map is given by pushing out [E]. Instead, we give a direct proof.

  As an application, we use the six-term exact sequence to show that [Ext Z/n A] is isomorphic to [A/n], for nonzero natural numbers [n]. (See [ext_cyclic_ab].) *)

(** Exactness of [0 -> ab_hom B G -> ab_hom E G] follows from the rightmost map being an embedding. *)
Definition isexact_abses_sixterm_i `{Funext}
  {B A G : AbGroup} (E : AbSES B A)
  : IsExact (Tr (-1))
      (pconst : pUnit ->* ab_hom B G)
      (fmap10 (A:=Group^op) ab_hom (projection E) G).
H: Funext
B, A, G: AbGroup
E: AbSES B A
IsExact (Tr (-1)) (pconst : pUnit ->* ab_hom B G)
  (fmap10 ab_hom (projection E) G)
Proof.
H: Funext
B, A, G: AbGroup
E: AbSES B A
IsExact (Tr (-1)) (pconst : pUnit ->* ab_hom B G)
  (fmap10 ab_hom (projection E) G)
  apply isexact_purely_O.
H: Funext
B, A, G: AbGroup
E: AbSES B A
IsExact Identity.purely pconst
  (fmap10 ab_hom (projection E) G)
  rapply isexact_homotopic_i.
H: Funext
B, A, G: AbGroup
E: AbSES B A
pconst ==* ?Goal
H: Funext
B, A, G: AbGroup
E: AbSES B A
IsExact Identity.purely ?Goal
  (fmap10 ab_hom (projection E) G)
  2: apply iff_grp_isexact_isembedding.
H: Funext
B, A, G: AbGroup
E: AbSES B A
pconst ==* grp_trivial_rec (ab_hom B G)
H: Funext
B, A, G: AbGroup
E: AbSES B A
IsEmbedding (fmap10 ab_hom (projection E) G)
  1: by apply phomotopy_homotopy_hset.
H: Funext
B, A, G: AbGroup
E: AbSES B A
IsEmbedding (fmap10 ab_hom (projection E) G)
  exact _. (* [isembedding_precompose_surjection_ab] *)
Defined.

(** Exactness of [ab_hom B G -> ab_hom E G -> ab_hom A G]. One can also deduce this from [isexact_abses_pullback]. *)
Definition isexact_ext_contra_sixterm_ii `{Funext}
  {B A G : AbGroup} (E : AbSES B A)
  : IsExact (Tr (-1))
      (fmap10 (A:=Group^op) ab_hom (projection E) G)
      (fmap10 (A:=Group^op) ab_hom (inclusion E) G).
H: Funext
B, A, G: AbGroup
E: AbSES B A
IsExact (Tr (-1)) (fmap10 ab_hom (projection E) G)
  (fmap10 ab_hom (inclusion E) G)
Proof.
H: Funext
B, A, G: AbGroup
E: AbSES B A
IsExact (Tr (-1)) (fmap10 ab_hom (projection E) G)
  (fmap10 ab_hom (inclusion E) G)
  snrapply Build_IsExact.
H: Funext
B, A, G: AbGroup
E: AbSES B A
IsComplex (fmap10 ab_hom (projection E) G)
  (fmap10 ab_hom (inclusion E) G)
H: Funext
B, A, G: AbGroup
E: AbSES B A
IsConnMap (Tr (-1)) (cxfib ?cx_isexact)
  {
H: Funext
B, A, G: AbGroup
E: AbSES B A
IsComplex (fmap10 ab_hom (projection E) G)
  (fmap10 ab_hom (inclusion E) G) apply phomotopy_homotopy_hset; intro f.
H: Funext
B, A, G: AbGroup
E: AbSES B A
f: ab_hom B G
(fmap10 ab_hom (inclusion E) G
 o* fmap10 ab_hom (projection E) G) f = pconst f
    apply equiv_path_grouphomomorphism; intro b; cbn.
H: Funext
B, A, G: AbGroup
E: AbSES B A
f: ab_hom B G
b: A
f (projection E (inclusion E b)) = group_unit
    refine (ap f _ @ grp_homo_unit f).
H: Funext
B, A, G: AbGroup
E: AbSES B A
f: ab_hom B G
b: A
projection E (inclusion E b) = mon_unit
    apply isexact_inclusion_projection. }
H: Funext
B, A, G: AbGroup
E: AbSES B A
IsConnMap (Tr (-1))
  (cxfib
     (phomotopy_homotopy_hset
        ((fun f : ab_hom B G =>
          let X :=
            equiv_fun equiv_path_grouphomomorphism in
          X
            ((fun b : A =>
              ap f
                (let X0 :=
                   fun a : AbSES' B A => cx_isexact in
                 let X1 :=
                   fun a : AbSES' B A =>
                   pointed_fun (X0 a) in
                 X1 E b) @ grp_homo_unit f
              :
              (fmap10 ab_hom (inclusion E) G
               o* fmap10 ab_hom (projection E) G) f b =
              pconst f b)
             :
             (fmap10 ab_hom (inclusion E) G
              o* fmap10 ab_hom (projection E) G) f ==
             pconst f))
         :
         fmap10 ab_hom (inclusion E) G
         o* fmap10 ab_hom (projection E) G == pconst)))
  hnf.
H: Funext
B, A, G: AbGroup
E: AbSES B A
forall
b : pFiber.pfiber (fmap10 ab_hom (inclusion E) G),
IsConnected (Tr (-1))
  (hfiber
     (cxfib
        (phomotopy_homotopy_hset
           (fun f : ab_hom B G =>
            let X :=
              equiv_fun equiv_path_grouphomomorphism
              in
            X
              (fun b0 : A =>
               ap f
                 (let X0 :=
                    fun a : AbSES' B A => cx_isexact
                    in
                  let X1 :=
                    fun a : AbSES' B A =>
                    pointed_fun (X0 a) in
                  X1 E b0) @ grp_homo_unit f)))) b) intros [f q]; rapply contr_inhabited_hprop.
H: Funext
B, A, G: AbGroup
E: AbSES B A
f: ab_hom E G
q: fmap10 ab_hom (inclusion E) G f = pt
Tr (-1)
  (hfiber
     (cxfib
        (phomotopy_homotopy_hset
           (fun f : ab_hom B G =>
            let X :=
              equiv_fun equiv_path_grouphomomorphism
              in
            X
              (fun b : A =>
               ap f
                 (let X0 :=
                    fun a : AbSES' B A => cx_isexact
                    in
                  let X1 :=
                    fun a : AbSES' B A =>
                    pointed_fun (X0 a) in
                  X1 E b) @ grp_homo_unit f)))) (f; q))
  srefine (tr (_; _)).
H: Funext
B, A, G: AbGroup
E: AbSES B A
f: ab_hom E G
q: fmap10 ab_hom (inclusion E) G f = pt
ab_hom B G
H: Funext
B, A, G: AbGroup
E: AbSES B A
f: ab_hom E G
q: fmap10 ab_hom (inclusion E) G f = pt
(fun x : ab_hom B G =>
 cxfib
   (phomotopy_homotopy_hset
      (fun f : ab_hom B G =>
       let X := equiv_fun equiv_path_grouphomomorphism
         in
       X
         (fun b : A =>
          ap f
            (let X0 :=
               fun a : AbSES' B A => cx_isexact in
             let X1 :=
               fun a : AbSES' B A =>
               pointed_fun (X0 a) in
             X1 E b) @ grp_homo_unit f))) x = (f; q))
  ?proj1
  {
H: Funext
B, A, G: AbGroup
E: AbSES B A
f: ab_hom E G
q: fmap10 ab_hom (inclusion E) G f = pt
ab_hom B G refine (grp_homo_compose _
              (abses_cokernel_iso (inclusion E) (projection E))^-1$).
H: Funext
B, A, G: AbGroup
E: AbSES B A
f: ab_hom E G
q: fmap10 ab_hom (inclusion E) G f = pt
GroupHomomorphism (ab_cokernel (inclusion E)) G
    apply (quotient_abgroup_rec _ _ f).
H: Funext
B, A, G: AbGroup
E: AbSES B A
f: ab_hom E G
q: fmap10 ab_hom (inclusion E) G f = pt
forall n : E,
grp_image (inclusion E) n -> f n = mon_unit
    intros e; rapply Trunc_ind.
H: Funext
B, A, G: AbGroup
E: AbSES B A
f: ab_hom E G
q: fmap10 ab_hom (inclusion E) G f = pt
e: E
{a : A & inclusion E a = e} -> f e = mon_unit
    intros [b r].
H: Funext
B, A, G: AbGroup
E: AbSES B A
f: ab_hom E G
q: fmap10 ab_hom (inclusion E) G f = pt
e: E
b: A
r: inclusion E b = e
f e = mon_unit
    refine (ap f r^ @ _).
H: Funext
B, A, G: AbGroup
E: AbSES B A
f: ab_hom E G
q: fmap10 ab_hom (inclusion E) G f = pt
e: E
b: A
r: inclusion E b = e
f (inclusion E b) = mon_unit
    exact (equiv_path_grouphomomorphism^-1 q _). }
H: Funext
B, A, G: AbGroup
E: AbSES B A
f: ab_hom E G
q: fmap10 ab_hom (inclusion E) G f = pt
(fun x : ab_hom B G =>
 cxfib
   (phomotopy_homotopy_hset
      (fun f : ab_hom B G =>
       let X := equiv_fun equiv_path_grouphomomorphism
         in
       X
         (fun b : A =>
          ap f
            (let X0 :=
               fun a : AbSES' B A => cx_isexact in
             let X1 :=
               fun a : AbSES' B A =>
               pointed_fun (X0 a) in
             X1 E b) @ grp_homo_unit f))) x = (f; q))
  (grp_homo_compose
     (quotient_abgroup_rec (grp_image (inclusion E)) G
        f
        (fun e : E =>
         Trunc_ind
           (fun
              _ : Trunc (-1)
                    {a : A & inclusion E a = e} =>
            f e = mon_unit)
           (fun a : {a : A & inclusion E a = e} =>
            (fun (b : A) (r : inclusion E b = e) =>
             ap f r^ @
             equiv_path_grouphomomorphism^-1 q b) a.1
              a.2)))
     (abses_cokernel_iso (inclusion E) (projection E))^-1$)
  lazy beta.
H: Funext
B, A, G: AbGroup
E: AbSES B A
f: ab_hom E G
q: fmap10 ab_hom (inclusion E) G f = pt
cxfib
  (phomotopy_homotopy_hset
     (fun f : ab_hom B G =>
      let X := equiv_fun equiv_path_grouphomomorphism
        in
      X
        (fun b : A =>
         ap f
           (let X0 := fun a : AbSES' B A => cx_isexact
              in
            let X1 :=
              fun a : AbSES' B A => pointed_fun (X0 a)
              in
            X1 E b) @ grp_homo_unit f)))
  (grp_homo_compose
     (quotient_abgroup_rec (grp_image (inclusion E)) G
        f
        (fun e : E =>
         Trunc_ind
           (fun
              _ : Trunc (-1)
                    {a : A & inclusion E a = e} =>
            f e = mon_unit)
           (fun a : {a : A & inclusion E a = e} =>
            ap f (a.2)^ @
            equiv_path_grouphomomorphism^-1 q a.1)))
     (abses_cokernel_iso (inclusion E) (projection E))^-1$) =
(f; q)
  apply path_sigma_hprop.
H: Funext
B, A, G: AbGroup
E: AbSES B A
f: ab_hom E G
q: fmap10 ab_hom (inclusion E) G f = pt
(cxfib
   (phomotopy_homotopy_hset
      (fun f : ab_hom B G =>
       let X := equiv_fun equiv_path_grouphomomorphism
         in
       X
         (fun b : A =>
          ap f
            (let X0 :=
               fun a : AbSES' B A => cx_isexact in
             let X1 :=
               fun a : AbSES' B A =>
               pointed_fun (X0 a) in
             X1 E b) @ grp_homo_unit f)))
   (grp_homo_compose
      (quotient_abgroup_rec (grp_image (inclusion E))
         G f
         (fun e : E =>
          Trunc_ind
            (fun
               _ : Trunc (-1)
                     {a : A & inclusion E a = e} =>
             f e = mon_unit)
            (fun a : {a : A & inclusion E a = e} =>
             ap f (a.2)^ @
             equiv_path_grouphomomorphism^-1 q a.1)))
      (abses_cokernel_iso (inclusion E) (projection E))^-1$)).1 =
(f; q).1
  apply equiv_path_grouphomomorphism; unfold pr1.
H: Funext
B, A, G: AbGroup
E: AbSES B A
f: ab_hom E G
q: fmap10 ab_hom (inclusion E) G f = pt
(cxfib
   (phomotopy_homotopy_hset
      (fun f : ab_hom B G =>
       equiv_path_grouphomomorphism
         (fun b : A =>
          ap f (cx_isexact b) @ grp_homo_unit f)))
   (grp_homo_compose
      (quotient_abgroup_rec (grp_image (inclusion E))
         G f
         (fun e : E =>
          Trunc_ind
            (fun
               _ : Trunc (-1)
                     {a : A & inclusion E a = e} =>
             f e = mon_unit)
            (fun a : {a : A & inclusion E a = e} =>
             ap f (a.2)^ @
             equiv_path_grouphomomorphism^-1 q a.1)))
      (abses_cokernel_iso (inclusion E) (projection E))^-1$)).1 ==
f
  intro x.
H: Funext
B, A, G: AbGroup
E: AbSES B A
f: ab_hom E G
q: fmap10 ab_hom (inclusion E) G f = pt
x: E
(cxfib
   (phomotopy_homotopy_hset
      (fun f : ab_hom B G =>
       equiv_path_grouphomomorphism
         (fun b : A =>
          ap f (cx_isexact b) @ grp_homo_unit f)))
   (grp_homo_compose
      (quotient_abgroup_rec (grp_image (inclusion E))
         G f
         (fun e : E =>
          Trunc_ind
            (fun
               _ : Trunc (-1)
                     {a : A & inclusion E a = e} =>
             f e = mon_unit)
            (fun a : {a : A & inclusion E a = e} =>
             ap f (a.2)^ @
             equiv_path_grouphomomorphism^-1 q a.1)))
      (abses_cokernel_iso (inclusion E) (projection E))^-1$)).1
  x = f x
  exact (ap (quotient_abgroup_rec _ _ f _)
            (abses_cokernel_iso_inv_beta _ _ _)).
Defined.

(** *** Exactness of [ab_hom E G -> ab_hom A G -> Ext B G] *)

(** If a pushout [abses_pushout alpha E] is trivial, then [alpha] factors through [inclusion E]. *)
Lemma abses_pushout_trivial_factors_inclusion `{Univalence}
  {B A A' : AbGroup} (alpha : A $-> A') (E : AbSES B A)
  : abses_pushout alpha E = pt -> exists phi, alpha = phi $o inclusion E.
H: Univalence
B, A, A': AbGroup
alpha: A $-> A'
E: AbSES B A
abses_pushout alpha E = pt ->
{phi : E $-> A' & alpha = phi $o inclusion E}
Proof.
H: Univalence
B, A, A': AbGroup
alpha: A $-> A'
E: AbSES B A
abses_pushout alpha E = pt ->
{phi : E $-> A' & alpha = phi $o inclusion E}
  equiv_intros (equiv_path_abses (E:=abses_pushout alpha E) (F:=pt)) p.
H: Univalence
B, A, A': AbGroup
alpha: A $-> A'
E: AbSES B A
p: abses_path_data (abses_pushout alpha E) pt
{phi : E $-> A' & alpha = phi $o inclusion E}
  destruct p as [phi [p q]].
H: Univalence
B, A, A': AbGroup
alpha: A $-> A'
E: AbSES B A
phi: GroupHomomorphism (abses_pushout alpha E) pt
p: phi $o inclusion (abses_pushout alpha E) ==
inclusion pt
q: projection (abses_pushout alpha E) ==
projection pt $o phi
{phi : E $-> A' & alpha = phi $o inclusion E}
  exists (ab_biprod_pr1 $o phi $o ab_pushout_inr).
H: Univalence
B, A, A': AbGroup
alpha: A $-> A'
E: AbSES B A
phi: GroupHomomorphism (abses_pushout alpha E) pt
p: phi $o inclusion (abses_pushout alpha E) ==
inclusion pt
q: projection (abses_pushout alpha E) ==
projection pt $o phi
alpha =
ab_biprod_pr1 $o phi $o ab_pushout_inr $o inclusion E
  apply equiv_path_grouphomomorphism; intro a.
H: Univalence
B, A, A': AbGroup
alpha: A $-> A'
E: AbSES B A
phi: GroupHomomorphism (abses_pushout alpha E) pt
p: phi $o inclusion (abses_pushout alpha E) ==
inclusion pt
q: projection (abses_pushout alpha E) ==
projection pt $o phi
a: A
alpha a =
(ab_biprod_pr1 $o phi $o ab_pushout_inr $o inclusion E)
  a
  (* We embed into the biproduct and prove equality there. *)
  apply (isinj_embedding (@ab_biprod_inl A' B) _).
H: Univalence
B, A, A': AbGroup
alpha: A $-> A'
E: AbSES B A
phi: GroupHomomorphism (abses_pushout alpha E) pt
p: phi $o inclusion (abses_pushout alpha E) ==
inclusion pt
q: projection (abses_pushout alpha E) ==
projection pt $o phi
a: A
ab_biprod_inl (alpha a) =
ab_biprod_inl
  ((ab_biprod_pr1 $o phi $o ab_pushout_inr $o
    inclusion E) a)
  refine ((p (alpha a))^ @ _).
H: Univalence
B, A, A': AbGroup
alpha: A $-> A'
E: AbSES B A
phi: GroupHomomorphism (abses_pushout alpha E) pt
p: phi $o inclusion (abses_pushout alpha E) ==
inclusion pt
q: projection (abses_pushout alpha E) ==
projection pt $o phi
a: A
(phi $o inclusion (abses_pushout alpha E)) (alpha a) =
ab_biprod_inl
  ((ab_biprod_pr1 $o phi $o ab_pushout_inr $o
    inclusion E) a)
  refine (ap phi _ @ _).
H: Univalence
B, A, A': AbGroup
alpha: A $-> A'
E: AbSES B A
phi: GroupHomomorphism (abses_pushout alpha E) pt
p: phi $o inclusion (abses_pushout alpha E) ==
inclusion pt
q: projection (abses_pushout alpha E) ==
projection pt $o phi
a: A
inclusion (abses_pushout alpha E) (alpha a) = ?Goal
H: Univalence
B, A, A': AbGroup
alpha: A $-> A'
E: AbSES B A
phi: GroupHomomorphism (abses_pushout alpha E) pt
p: phi $o inclusion (abses_pushout alpha E) ==
inclusion pt
q: projection (abses_pushout alpha E) ==
projection pt $o phi
a: A
phi ?Goal =
ab_biprod_inl
  ((ab_biprod_pr1 $o phi $o ab_pushout_inr $o
    inclusion E) a)
  1: exact (left_square (abses_pushout_morphism E alpha) a).
H: Univalence
B, A, A': AbGroup
alpha: A $-> A'
E: AbSES B A
phi: GroupHomomorphism (abses_pushout alpha E) pt
p: phi $o inclusion (abses_pushout alpha E) ==
inclusion pt
q: projection (abses_pushout alpha E) ==
projection pt $o phi
a: A
phi
  ((component2 (abses_pushout_morphism E alpha) $o
    inclusion E) a) =
ab_biprod_inl
  ((ab_biprod_pr1 $o phi $o ab_pushout_inr $o
    inclusion E) a)
  apply (path_prod' idpath).
H: Univalence
B, A, A': AbGroup
alpha: A $-> A'
E: AbSES B A
phi: GroupHomomorphism (abses_pushout alpha E) pt
p: phi $o inclusion (abses_pushout alpha E) ==
inclusion pt
q: projection (abses_pushout alpha E) ==
projection pt $o phi
a: A
snd
  (phi
     ((component2 (abses_pushout_morphism E alpha) $o
       inclusion E) a)) =
grp_homo_const
  ((ab_biprod_pr1 $o phi $o ab_pushout_inr $o
    inclusion E) a)
  refine ((q _)^ @ _).
H: Univalence
B, A, A': AbGroup
alpha: A $-> A'
E: AbSES B A
phi: GroupHomomorphism (abses_pushout alpha E) pt
p: phi $o inclusion (abses_pushout alpha E) ==
inclusion pt
q: projection (abses_pushout alpha E) ==
projection pt $o phi
a: A
projection (abses_pushout alpha E)
  ((component2 (abses_pushout_morphism E alpha) $o
    inclusion E) a) =
grp_homo_const
  ((ab_biprod_pr1 $o phi $o ab_pushout_inr $o
    inclusion E) a)
  refine (right_square (abses_pushout_morphism E alpha) _ @ _); cbn.
H: Univalence
B, A, A': AbGroup
alpha: A $-> A'
E: AbSES B A
phi: GroupHomomorphism (abses_pushout alpha E) pt
p: phi $o inclusion (abses_pushout alpha E) ==
inclusion pt
q: projection (abses_pushout alpha E) ==
projection pt $o phi
a: A
projection E (inclusion E a) = group_unit
  apply isexact_inclusion_projection.
Defined.

Global Instance isexact_ext_contra_sixterm_iii@{u v +} `{Univalence}
  {B A G : AbGroup@{u}} (E : AbSES@{u v} B A)
  : IsExact (Tr (-1))
      (fmap10 (A:=Group^op) ab_hom (inclusion E) G)
      (abses_pushout_ext E).
H: Univalence
B, A, G: AbGroup
E: AbSES B A
IsExact (Tr (-1)) (fmap10 ab_hom (inclusion E) G)
  (abses_pushout_ext E)
Proof.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
IsExact (Tr (-1)) (fmap10 ab_hom (inclusion E) G)
  (abses_pushout_ext E)
  snrapply Build_IsExact.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
IsComplex (fmap10 ab_hom (inclusion E) G)
  (abses_pushout_ext E)
H: Univalence
B, A, G: AbGroup
E: AbSES B A
IsConnMap (Tr (-1)) (cxfib ?cx_isexact)
  -
H: Univalence
B, A, G: AbGroup
E: AbSES B A
IsComplex (fmap10 ab_hom (inclusion E) G)
  (abses_pushout_ext E) apply phomotopy_homotopy_hset; intro g; cbn.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
g: ab_hom E G
tr
  (abses_pushout (grp_homo_compose g (inclusion E)) E) =
tr ispointed_abses
    (* this equation holds purely *)
    apply (ap tr@{v}).
H: Univalence
B, A, G: AbGroup
E: AbSES B A
g: ab_hom E G
abses_pushout (grp_homo_compose g (inclusion E)) E =
ispointed_abses
    refine (abses_pushout_compose _ _ _ @ ap _ _ @ _).
H: Univalence
B, A, G: AbGroup
E: AbSES B A
g: ab_hom E G
abses_pushout (inclusion E) E = ?Goal
H: Univalence
B, A, G: AbGroup
E: AbSES B A
g: ab_hom E G
abses_pushout g ?Goal = ispointed_abses
    1: apply abses_pushout_inclusion.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
g: ab_hom E G
abses_pushout g pt = ispointed_abses
    apply abses_pushout_point.
  -
H: Univalence
B, A, G: AbGroup
E: AbSES B A
IsConnMap (Tr (-1))
  (cxfib
     (phomotopy_homotopy_hset
        ((fun g : ab_hom E G =>
          ap tr
            ((abses_pushout_compose (inclusion E) g E @
              ap (abses_pushout g)
                (abses_pushout_inclusion E)) @
             abses_pushout_point g)
          :
          (abses_pushout_ext E
           o* fmap10 ab_hom (inclusion E) G) g =
          pconst g)
         :
         abses_pushout_ext E
         o* fmap10 ab_hom (inclusion E) G == pconst))) intros [F p].
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: ab_hom A G
p: abses_pushout_ext E F = pt
IsConnected (Tr (-1))
  (hfiber
     (cxfib
        (phomotopy_homotopy_hset
           (fun g : ab_hom E G =>
            ap tr
              ((abses_pushout_compose (inclusion E) g
                  E @
                ap (abses_pushout g)
                  (abses_pushout_inclusion E)) @
               abses_pushout_point g)))) (F; p))
    (* since we are proving a proposition, we may convert [p] to an actual path *)
    pose proof (p' := (equiv_path_Tr _ _)^-1 p).
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: ab_hom A G
p: abses_pushout_ext E F = pt
p': Tr (-1)
  (fmap
     ((AbSES' : AbGroup^op -> AbGroup -> Type) B)
     F E = pt)
IsConnected (Tr (-1))
  (hfiber
     (cxfib
        (phomotopy_homotopy_hset
           (fun g : ab_hom E G =>
            ap tr
              ((abses_pushout_compose (inclusion E) g
                  E @
                ap (abses_pushout g)
                  (abses_pushout_inclusion E)) @
               abses_pushout_point g)))) (F; p))
    (* slightly faster than [strip_truncations]: *)
    revert p'; apply Trunc_rec; intro p'.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: ab_hom A G
p: abses_pushout_ext E F = pt
p': fmap ((AbSES' : AbGroup^op -> AbGroup -> Type) B)
  F E = pt
IsConnected (Tr (-1))
  (hfiber
     (cxfib
        (phomotopy_homotopy_hset
           (fun g : ab_hom E G =>
            ap tr
              ((abses_pushout_compose (inclusion E) g
                  E @
                ap (abses_pushout g)
                  (abses_pushout_inclusion E)) @
               abses_pushout_point g)))) (F; p))
    rapply contr_inhabited_hprop; apply tr.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: ab_hom A G
p: abses_pushout_ext E F = pt
p': fmap ((AbSES' : AbGroup^op -> AbGroup -> Type) B)
  F E = pt
hfiber
  (cxfib
     (phomotopy_homotopy_hset
        (fun g : ab_hom E G =>
         ap tr
           ((abses_pushout_compose (inclusion E) g E @
             ap (abses_pushout g)
               (abses_pushout_inclusion E)) @
            abses_pushout_point g)))) (F; p)
    (* now we construct a preimage *)
    pose (g := abses_pushout_trivial_factors_inclusion _ E p');
      destruct g as [g k].
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: ab_hom A G
p: abses_pushout_ext E F = pt
p': fmap ((AbSES' : AbGroup^op -> AbGroup -> Type) B)
  F E = pt
g: E $-> G
k: F = g $o inclusion E
hfiber
  (cxfib
     (phomotopy_homotopy_hset
        (fun g : ab_hom E G =>
         ap tr
           ((abses_pushout_compose (inclusion E) g E @
             ap (abses_pushout g)
               (abses_pushout_inclusion E)) @
            abses_pushout_point g)))) (F; p)
    exists g.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: ab_hom A G
p: abses_pushout_ext E F = pt
p': fmap ((AbSES' : AbGroup^op -> AbGroup -> Type) B)
  F E = pt
g: E $-> G
k: F = g $o inclusion E
cxfib
  (phomotopy_homotopy_hset
     (fun g : ab_hom E G =>
      ap tr
        ((abses_pushout_compose (inclusion E) g E @
          ap (abses_pushout g)
            (abses_pushout_inclusion E)) @
         abses_pushout_point g))) g = (F; p)
    apply path_sigma_hprop; cbn.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: ab_hom A G
p: abses_pushout_ext E F = pt
p': fmap ((AbSES' : AbGroup^op -> AbGroup -> Type) B)
  F E = pt
g: E $-> G
k: F = g $o inclusion E
grp_homo_compose g (inclusion E) = F
    exact k^.
Defined.

(** *** Exactness of [ab_hom A G -> Ext1 B G -> Ext1 E G]. *)

(** We construct a morphism which witnesses exactness. *)
Definition isexact_ext_contra_sixterm_iv_mor `{Univalence}
  {B A G : AbGroup} (E : AbSES B A)
  (F : AbSES B G) (p : abses_pullback (projection E) F = pt)
  : AbSESMorphism E F.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
AbSESMorphism E F
Proof.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
AbSESMorphism E F
  pose (p' := equiv_path_abses^-1 p^);
    destruct p' as [p' [pl pr]].
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
p': GroupHomomorphism pt
  (abses_pullback (projection E) F)
pl: p' $o inclusion pt ==
inclusion (abses_pullback (projection E) F)
pr: projection pt ==
projection (abses_pullback (projection E) F) $o
p'
AbSESMorphism E F
  srefine (Build_AbSESMorphism _ _ grp_homo_id _ _).
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
p': GroupHomomorphism pt
  (abses_pullback (projection E) F)
pl: p' $o inclusion pt ==
inclusion (abses_pullback (projection E) F)
pr: projection pt ==
projection (abses_pullback (projection E) F) $o
p'
A $-> G
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
p': GroupHomomorphism pt
  (abses_pullback (projection E) F)
pl: p' $o inclusion pt ==
inclusion (abses_pullback (projection E) F)
pr: projection pt ==
projection (abses_pullback (projection E) F) $o
p'
E $-> F
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
p': GroupHomomorphism pt
  (abses_pullback (projection E) F)
pl: p' $o inclusion pt ==
inclusion (abses_pullback (projection E) F)
pr: projection pt ==
projection (abses_pullback (projection E) F) $o
p'
inclusion F $o ?component1 ==
?component2 $o inclusion E
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
p': GroupHomomorphism pt
  (abses_pullback (projection E) F)
pl: p' $o inclusion pt ==
inclusion (abses_pullback (projection E) F)
pr: projection pt ==
projection (abses_pullback (projection E) F) $o
p'
projection F $o ?component2 ==
grp_homo_id $o projection E
  -
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
p': GroupHomomorphism pt
  (abses_pullback (projection E) F)
pl: p' $o inclusion pt ==
inclusion (abses_pullback (projection E) F)
pr: projection pt ==
projection (abses_pullback (projection E) F) $o
p'
A $-> G refine (grp_homo_compose
              (grp_iso_inverse
                 (abses_kernel_iso (inclusion F) (projection F))) _).
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
p': GroupHomomorphism pt
  (abses_pullback (projection E) F)
pl: p' $o inclusion pt ==
inclusion (abses_pullback (projection E) F)
pr: projection pt ==
projection (abses_pullback (projection E) F) $o
p'
GroupHomomorphism A (ab_kernel (projection F))
    (* now it's easy to construct map into the kernel *)
    snrapply grp_kernel_corec.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
p': GroupHomomorphism pt
  (abses_pullback (projection E) F)
pl: p' $o inclusion pt ==
inclusion (abses_pullback (projection E) F)
pr: projection pt ==
projection (abses_pullback (projection E) F) $o
p'
A $-> F
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
p': GroupHomomorphism pt
  (abses_pullback (projection E) F)
pl: p' $o inclusion pt ==
inclusion (abses_pullback (projection E) F)
pr: projection pt ==
projection (abses_pullback (projection E) F) $o
p'
projection F $o ?g == grp_homo_const
    1: exact (grp_pullback_pr1 _ _ $o p' $o ab_biprod_inr $o inclusion E).
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
p': GroupHomomorphism pt
  (abses_pullback (projection E) F)
pl: p' $o inclusion pt ==
inclusion (abses_pullback (projection E) F)
pr: projection pt ==
projection (abses_pullback (projection E) F) $o
p'
projection F $o
(grp_pullback_pr1 (projection F) (projection E) $o p' $o
 ab_biprod_inr $o inclusion E) == grp_homo_const
    intro x.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
p': GroupHomomorphism pt
  (abses_pullback (projection E) F)
pl: p' $o inclusion pt ==
inclusion (abses_pullback (projection E) F)
pr: projection pt ==
projection (abses_pullback (projection E) F) $o
p'
x: A
(projection F $o
 (grp_pullback_pr1 (projection F) (projection E) $o p' $o
  ab_biprod_inr $o inclusion E)) x = grp_homo_const x
    refine (right_square (abses_pullback_morphism F _) _ @ _).
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
p': GroupHomomorphism pt
  (abses_pullback (projection E) F)
pl: p' $o inclusion pt ==
inclusion (abses_pullback (projection E) F)
pr: projection pt ==
projection (abses_pullback (projection E) F) $o
p'
x: A
(component3 (abses_pullback_morphism F (projection E)) $o
 projection (abses_pullback (projection E) F))
  (p' (ab_biprod_inr (inclusion E x))) =
grp_homo_const x
    refine (ap (projection E) (pr _)^ @ _); cbn.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
p': GroupHomomorphism pt
  (abses_pullback (projection E) F)
pl: p' $o inclusion pt ==
inclusion (abses_pullback (projection E) F)
pr: projection pt ==
projection (abses_pullback (projection E) F) $o
p'
x: A
projection E (inclusion E x) = group_unit
    apply isexact_inclusion_projection.
  -
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
p': GroupHomomorphism pt
  (abses_pullback (projection E) F)
pl: p' $o inclusion pt ==
inclusion (abses_pullback (projection E) F)
pr: projection pt ==
projection (abses_pullback (projection E) F) $o
p'
E $-> F exact (grp_pullback_pr1 _ _ $o p' $o ab_biprod_inr).
  -
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
p': GroupHomomorphism pt
  (abses_pullback (projection E) F)
pl: p' $o inclusion pt ==
inclusion (abses_pullback (projection E) F)
pr: projection pt ==
projection (abses_pullback (projection E) F) $o
p'
inclusion F $o
grp_homo_compose
  (grp_iso_inverse
     (abses_kernel_iso (inclusion F) (projection F)))
  (grp_kernel_corec
     (grp_pullback_pr1 (projection F) (projection E) $o
      p' $o ab_biprod_inr $o inclusion E)
     ((fun x : A =>
       right_square
         (abses_pullback_morphism F (projection E))
         (p' (ab_biprod_inr (inclusion E x))) @
       (ap (projection E)
          (pr (ab_biprod_inr (inclusion E x)))^ @
        ((let X := fun a : AbSES' B A => cx_isexact in
          let X0 :=
            fun a : AbSES' B A => pointed_fun (X a) in
          X0 E x)
         :
         projection E
           (projection pt
              (ab_biprod_inr (inclusion E x))) =
         grp_homo_const x)))
      :
      projection F $o
      (grp_pullback_pr1 (projection F) (projection E) $o
       p' $o ab_biprod_inr $o inclusion E) ==
      grp_homo_const)) ==
grp_pullback_pr1 (projection F) (projection E) $o p' $o
ab_biprod_inr $o inclusion E intro a.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
p': GroupHomomorphism pt
  (abses_pullback (projection E) F)
pl: p' $o inclusion pt ==
inclusion (abses_pullback (projection E) F)
pr: projection pt ==
projection (abses_pullback (projection E) F) $o
p'
a: A
(inclusion F $o
 grp_homo_compose
   (grp_iso_inverse
      (abses_kernel_iso (inclusion F) (projection F)))
   (grp_kernel_corec
      (grp_pullback_pr1 (projection F) (projection E) $o
       p' $o ab_biprod_inr $o inclusion E)
      (fun x : A =>
       right_square
         (abses_pullback_morphism F (projection E))
         (p' (ab_biprod_inr (inclusion E x))) @
       (ap (projection E)
          (pr (ab_biprod_inr (inclusion E x)))^ @
        (let X := fun a : AbSES' B A => cx_isexact in
         let X0 :=
           fun a : AbSES' B A => pointed_fun (X a) in
         X0 E x))))) a =
(grp_pullback_pr1 (projection F) (projection E) $o p' $o
 ab_biprod_inr $o inclusion E) a
    nrapply abses_kernel_iso_inv_beta.
  -
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
p': GroupHomomorphism pt
  (abses_pullback (projection E) F)
pl: p' $o inclusion pt ==
inclusion (abses_pullback (projection E) F)
pr: projection pt ==
projection (abses_pullback (projection E) F) $o
p'
projection F $o
(grp_pullback_pr1 (projection F) (projection E) $o p' $o
 ab_biprod_inr) == grp_homo_id $o projection E intro e.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
p': GroupHomomorphism pt
  (abses_pullback (projection E) F)
pl: p' $o inclusion pt ==
inclusion (abses_pullback (projection E) F)
pr: projection pt ==
projection (abses_pullback (projection E) F) $o
p'
e: E
(projection F $o
 (grp_pullback_pr1 (projection F) (projection E) $o p' $o
  ab_biprod_inr)) e = (grp_homo_id $o projection E) e
    refine (right_square (abses_pullback_morphism F _) _
              @ ap (projection E) _).
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
p': GroupHomomorphism pt
  (abses_pullback (projection E) F)
pl: p' $o inclusion pt ==
inclusion (abses_pullback (projection E) F)
pr: projection pt ==
projection (abses_pullback (projection E) F) $o
p'
e: E
projection (abses_pullback (projection E) F)
  (p' (ab_biprod_inr e)) = e
    exact (pr _)^.
Defined.

Global Instance isexact_ext_contra_sixterm_iv `{Univalence}
  {B A G : AbGroup@{u}} (E : AbSES@{u v} B A)
  : IsExact (Tr (-1)) (abses_pushout_ext E)
      (fmap (pTr 0) (abses_pullback_pmap (A:=G) (projection E))).
H: Univalence
B, A, G: AbGroup
E: AbSES B A
IsExact (Tr (-1)) (abses_pushout_ext E)
  (fmap (pTr 0) (abses_pullback_pmap (projection E)))
Proof.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
IsExact (Tr (-1)) (abses_pushout_ext E)
  (fmap (pTr 0) (abses_pullback_pmap (projection E)))
  snrapply Build_IsExact.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
IsComplex (abses_pushout_ext E)
  (fmap (pTr 0) (abses_pullback_pmap (projection E)))
H: Univalence
B, A, G: AbGroup
E: AbSES B A
IsConnMap (Tr (-1)) (cxfib ?cx_isexact)
  -
H: Univalence
B, A, G: AbGroup
E: AbSES B A
IsComplex (abses_pushout_ext E)
  (fmap (pTr 0) (abses_pullback_pmap (projection E))) apply phomotopy_homotopy_hset; intro g; cbn.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
g: ab_hom A G
tr (abses_pullback (projection E) (abses_pushout g E)) =
tr ispointed_abses
    (* this equation holds purely *)
    apply (ap tr@{v}).
H: Univalence
B, A, G: AbGroup
E: AbSES B A
g: ab_hom A G
abses_pullback (projection E) (abses_pushout g E) =
ispointed_abses
    refine ((abses_pushout_pullback_reorder _ _ _)^
              @ ap _ _ @ _).
H: Univalence
B, A, G: AbGroup
E: AbSES B A
g: ab_hom A G
abses_pullback (projection E) E = ?Goal
H: Univalence
B, A, G: AbGroup
E: AbSES B A
g: ab_hom A G
abses_pushout g ?Goal = ispointed_abses
    1: exact (abses_pullback_projection _)^.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
g: ab_hom A G
abses_pushout g pt = ispointed_abses
    apply abses_pushout_point.
  (* since we are proving a proposition, we may convert [p] to an actual path *)
  -
H: Univalence
B, A, G: AbGroup
E: AbSES B A
IsConnMap (Tr (-1))
  (cxfib
     (phomotopy_homotopy_hset
        ((fun g : ab_hom A G =>
          ap tr
            (((abses_pushout_pullback_reorder E g
                 (projection E))^ @
              ap (abses_pushout g)
                (abses_pullback_projection E)^) @
             abses_pushout_point g)
          :
          (fmap (pTr 0)
             (abses_pullback_pmap (projection E))
           o* abses_pushout_ext E) g = pconst g)
         :
         fmap (pTr 0)
           (abses_pullback_pmap (projection E))
         o* abses_pushout_ext E == pconst))) intros [F p].
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: ab_ext B G
p: fmap (pTr 0) (abses_pullback_pmap (projection E))
  F = pt
IsConnected (Tr (-1))
  (hfiber
     (cxfib
        (phomotopy_homotopy_hset
           (fun g : ab_hom A G =>
            ap tr
              (((abses_pushout_pullback_reorder E g
                   (projection E))^ @
                ap (abses_pushout g)
                  (abses_pullback_projection E)^) @
               abses_pushout_point g)))) (F; p))
    revert dependent F; nrapply (Trunc_ind (n:=0) (A:=AbSES B G)).
H: Univalence
B, A, G: AbGroup
E: AbSES B A
forall aa : Trunc 0 (AbSES B G),
IsHSet
  (forall
   p : fmap (pTr 0)
         (abses_pullback_pmap (projection E)) aa = pt,
   IsConnected (Tr (-1))
     (hfiber
        (cxfib
           (phomotopy_homotopy_hset
              (fun g : ab_hom A G =>
               ap tr
                 (((abses_pushout_pullback_reorder E g
                      (projection E))^ @
                   ap (abses_pushout g)
                     (abses_pullback_projection E)^) @
                  abses_pushout_point g)))) (aa; p)))
H: Univalence
B, A, G: AbGroup
E: AbSES B A
forall (a : AbSES B G)
(p : fmap (pTr 0) (abses_pullback_pmap (projection E))
       (tr a) = pt),
IsConnected (Tr (-1))
  (hfiber
     (cxfib
        (phomotopy_homotopy_hset
           (fun g : ab_hom A G =>
            ap tr
              (((abses_pushout_pullback_reorder E g
                   (projection E))^ @
                ap (abses_pushout g)
                  (abses_pullback_projection E)^) @
               abses_pushout_point g)))) (tr a; p))
    (* [exact _.] works here, but is slow. *)
    {
H: Univalence
B, A, G: AbGroup
E: AbSES B A
forall aa : Trunc 0 (AbSES B G),
IsHSet
  (forall
   p : fmap (pTr 0)
         (abses_pullback_pmap (projection E)) aa = pt,
   IsConnected (Tr (-1))
     (hfiber
        (cxfib
           (phomotopy_homotopy_hset
              (fun g : ab_hom A G =>
               ap tr
                 (((abses_pushout_pullback_reorder E g
                      (projection E))^ @
                   ap (abses_pushout g)
                     (abses_pullback_projection E)^) @
                  abses_pushout_point g)))) (aa; p))) intro x; nrapply istrunc_forall.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
x: Trunc 0 (AbSES B G)
forall
a : fmap (pTr 0) (abses_pullback_pmap (projection E))
      x = pt,
IsHSet
  (IsConnected (Tr (-1))
     (hfiber
        (cxfib
           (phomotopy_homotopy_hset
              (fun g : ab_hom A G =>
               ap tr
                 (((abses_pushout_pullback_reorder E g
                      (projection E))^ @
                   ap (abses_pushout g)
                     (abses_pullback_projection E)^) @
                  abses_pushout_point g)))) (x; a)))
      intro y; rapply (istrunc_leq (trunc_index_leq_succ _)). }
H: Univalence
B, A, G: AbGroup
E: AbSES B A
forall (a : AbSES B G)
(p : fmap (pTr 0) (abses_pullback_pmap (projection E))
       (tr a) = pt),
IsConnected (Tr (-1))
  (hfiber
     (cxfib
        (phomotopy_homotopy_hset
           (fun g : ab_hom A G =>
            ap tr
              (((abses_pushout_pullback_reorder E g
                   (projection E))^ @
                ap (abses_pushout g)
                  (abses_pullback_projection E)^) @
               abses_pushout_point g)))) (tr a; p))
    intro F.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
forall
p : fmap (pTr 0) (abses_pullback_pmap (projection E))
      (tr F) = pt,
IsConnected (Tr (-1))
  (hfiber
     (cxfib
        (phomotopy_homotopy_hset
           (fun g : ab_hom A G =>
            ap tr
              (((abses_pushout_pullback_reorder E g
                   (projection E))^ @
                ap (abses_pushout g)
                  (abses_pullback_projection E)^) @
               abses_pushout_point g)))) (tr F; p))
    equiv_intros (equiv_path_Tr (n:=-1) (abses_pullback (projection E) F) pt) p.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: Tr (-1) (abses_pullback (projection E) F = pt)
IsConnected (Tr (-1))
  (hfiber
     (cxfib
        (phomotopy_homotopy_hset
           (fun g : ab_hom A G =>
            ap tr
              (((abses_pushout_pullback_reorder E g
                   (projection E))^ @
                ap (abses_pushout g)
                  (abses_pullback_projection E)^) @
               abses_pushout_point g))))
     (tr F;
     equiv_path_Tr (abses_pullback (projection E) F)
       pt p))
    strip_truncations.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
IsConnected (Tr (-1))
  (hfiber
     (cxfib
        (phomotopy_homotopy_hset
           (fun g : ab_hom A G =>
            ap tr
              (((abses_pushout_pullback_reorder E g
                   (projection E))^ @
                ap (abses_pushout g)
                  (abses_pullback_projection E)^) @
               abses_pushout_point g))))
     (tr F;
     equiv_path_Tr (abses_pullback (projection E) F)
       pt (tr p)))
    rapply contr_inhabited_hprop; apply tr.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
hfiber
  (cxfib
     (phomotopy_homotopy_hset
        (fun g : ab_hom A G =>
         ap tr
           (((abses_pushout_pullback_reorder E g
                (projection E))^ @
             ap (abses_pushout g)
               (abses_pullback_projection E)^) @
            abses_pushout_point g))))
  (tr F;
  equiv_path_Tr (abses_pullback (projection E) F) pt
    (tr p))
    pose (g := isexact_ext_contra_sixterm_iv_mor E F p).
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
g:= isexact_ext_contra_sixterm_iv_mor E F p: AbSESMorphism E F
hfiber
  (cxfib
     (phomotopy_homotopy_hset
        (fun g : ab_hom A G =>
         ap tr
           (((abses_pushout_pullback_reorder E g
                (projection E))^ @
             ap (abses_pushout g)
               (abses_pullback_projection E)^) @
            abses_pushout_point g))))
  (tr F;
  equiv_path_Tr (abses_pullback (projection E) F) pt
    (tr p))
    exists (component1 g).
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
g:= isexact_ext_contra_sixterm_iv_mor E F p: AbSESMorphism E F
cxfib
  (phomotopy_homotopy_hset
     (fun g : ab_hom A G =>
      ap tr
        (((abses_pushout_pullback_reorder E g
             (projection E))^ @
          ap (abses_pushout g)
            (abses_pullback_projection E)^) @
         abses_pushout_point g))) (component1 g) =
(tr F;
equiv_path_Tr (abses_pullback (projection E) F) pt
  (tr p))
    apply path_sigma_hprop, (ap tr).
H: Univalence
B, A, G: AbGroup
E: AbSES B A
F: AbSES B G
p: abses_pullback (projection E) F = pt
g:= isexact_ext_contra_sixterm_iv_mor E F p: AbSESMorphism E F
fmap ((AbSES' : AbGroup^op -> AbGroup -> Type) B)
  (component1 g) E = F
    by rapply (abses_pushout_component3_id g).
Defined.

(** *** Exactness of [Ext B G -> Ext E G -> Ext A G] *)

(** This is an immediate consequence of [isexact_abses_pullback]. *)
Global Instance isexact_ext_contra_sixterm_v `{Univalence}
  {B A G : AbGroup} (E : AbSES B A)
  : IsExact (Tr (-1))
      (fmap (pTr 0) (abses_pullback_pmap (A:=G) (projection E)))
      (fmap (pTr 0) (abses_pullback_pmap (A:=G) (inclusion E))).
H: Univalence
B, A, G: AbGroup
E: AbSES B A
IsExact (Tr (-1))
  (fmap (pTr 0) (abses_pullback_pmap (projection E)))
  (fmap (pTr 0) (abses_pullback_pmap (inclusion E)))
Proof.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
IsExact (Tr (-1))
  (fmap (pTr 0) (abses_pullback_pmap (projection E)))
  (fmap (pTr 0) (abses_pullback_pmap (inclusion E)))
  rapply isexact_ptr.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
IsExact (Tr (-1)) (abses_pullback_pmap (projection E))
  (abses_pullback_pmap (inclusion E))
  rapply isexact_purely_O.
Defined.

(** *** [Ext Z/n A] is isomorphic to [A/n] *)

(** An easy consequence of the contravariant six-term exact sequence is that [Ext Z/n A] is isomorphic to the cokernel of the multiplication-by-n endomorphism [A -> A], for any abelian group [A]. This falls out of the six-term exact sequence associated to [Z -> Z -> Z/n] and projectivity of [Z]. A minor point is that the library does not currently contain a proof that multiplication by a nonzero natural number is a self-injection of [Z]. Thus we work directly with the assumption that [Z1_mul_nat n] is an embedding. *)

(** We define our own cyclic groups using [ab_cokernel_embedding] under the assumption that [Z1_mul_nat n] is an embedding. *)
Definition cyclic' `{Funext} (n : nat) `{IsEmbedding (Z1_mul_nat n)}
  : AbGroup := ab_cokernel_embedding (Z1_mul_nat n).

(** We first show that [ab_hom Z A -> ab_hom Z A -> Ext (cyclic n) A] is exact. We could inline the proof below, but factoring it out is faster. *)
Local Definition isexact_ext_cyclic_ab_iii@{u v w | u < v, v < w} `{Univalence}
  (n : nat) `{IsEmbedding (Z1_mul_nat n)} {A : AbGroup@{u}}
  : IsExact (Tr (-1))
      (fmap10 (A:=Group^op) ab_hom (Z1_mul_nat n) A)
      (abses_pushout_ext (abses_from_inclusion (Z1_mul_nat n)))
  := isexact_ext_contra_sixterm_iii
       (abses_from_inclusion (Z1_mul_nat n)).

(** We show exactness of [A -> A -> Ext Z/n A] where the first map is multiplication by [n], but considered in universe [v]. *)
Local Definition ext_cyclic_exact@{u v w} `{Univalence}
  (n : nat) `{IsEmbedding (Z1_mul_nat n)} {A : AbGroup@{u}}
  : IsExact@{v v v v v} (Tr (-1))
      (ab_mul_nat (A:=A) n)
      (abses_pushout_ext@{u w v} (abses_from_inclusion (Z1_mul_nat n))
         o* (pequiv_groupisomorphism (equiv_Z1_hom A))^-1*).
H: Univalence
n: nat
IsEmbedding0: IsEmbedding (Z1_mul_nat n)
A: AbGroup
IsExact (Tr (-1)) (ab_mul_nat n)
  (abses_pushout_ext
     (abses_from_inclusion (Z1_mul_nat n))
   o* (equiv_Z1_hom A)^-1*)
Proof.
H: Univalence
n: nat
IsEmbedding0: IsEmbedding (Z1_mul_nat n)
A: AbGroup
IsExact (Tr (-1)) (ab_mul_nat n)
  (abses_pushout_ext
     (abses_from_inclusion (Z1_mul_nat n))
   o* (equiv_Z1_hom A)^-1*)
  (* we first move [equiv_Z1_hom] across the total space *)
  apply moveL_isexact_equiv.
H: Univalence
n: nat
IsEmbedding0: IsEmbedding (Z1_mul_nat n)
A: AbGroup
IsExact (Tr (-1))
  ((equiv_Z1_hom A)^-1* o* ab_mul_nat n)
  (abses_pushout_ext
     (abses_from_inclusion (Z1_mul_nat n)))
  (* now we change the left map so as to apply exactness at iii from above *)
  snrapply (isexact_homotopic_i (Tr (-1))).
H: Univalence
n: nat
IsEmbedding0: IsEmbedding (Z1_mul_nat n)
A: AbGroup
A ->* ab_hom ab_Z1 A
H: Univalence
n: nat
IsEmbedding0: IsEmbedding (Z1_mul_nat n)
A: AbGroup
(equiv_Z1_hom A)^-1* o* ab_mul_nat n ==* ?i
H: Univalence
n: nat
IsEmbedding0: IsEmbedding (Z1_mul_nat n)
A: AbGroup
IsExact (Tr (-1)) ?i
  (abses_pushout_ext
     (abses_from_inclusion (Z1_mul_nat n)))
  1: exact (fmap10 (A:=Group^op) ab_hom (Z1_mul_nat n) A o*
              (pequiv_inverse
                 (pequiv_groupisomorphism (equiv_Z1_hom A)))).
H: Univalence
n: nat
IsEmbedding0: IsEmbedding (Z1_mul_nat n)
A: AbGroup
(equiv_Z1_hom A)^-1* o* ab_mul_nat n ==*
fmap10 ab_hom (Z1_mul_nat n) A
o* pequiv_inverse (equiv_Z1_hom A)
H: Univalence
n: nat
IsEmbedding0: IsEmbedding (Z1_mul_nat n)
A: AbGroup
IsExact (Tr (-1))
  (fmap10 ab_hom (Z1_mul_nat n) A
   o* pequiv_inverse (equiv_Z1_hom A))
  (abses_pushout_ext
     (abses_from_inclusion (Z1_mul_nat n)))
  -
H: Univalence
n: nat
IsEmbedding0: IsEmbedding (Z1_mul_nat n)
A: AbGroup
(equiv_Z1_hom A)^-1* o* ab_mul_nat n ==*
fmap10 ab_hom (Z1_mul_nat n) A
o* pequiv_inverse (equiv_Z1_hom A) apply phomotopy_homotopy_hset.
H: Univalence
n: nat
IsEmbedding0: IsEmbedding (Z1_mul_nat n)
A: AbGroup
(equiv_Z1_hom A)^-1* o* ab_mul_nat n ==
fmap10 ab_hom (Z1_mul_nat n) A
o* pequiv_inverse (equiv_Z1_hom A)
    rapply (equiv_ind (equiv_Z1_hom A)); intro f.
H: Univalence
n: nat
IsEmbedding0: IsEmbedding (Z1_mul_nat n)
A: AbGroup
f: ab_hom ab_Z1 A
((equiv_Z1_hom A)^-1* o* ab_mul_nat n)
  (equiv_Z1_hom A f) =
(fmap10 ab_hom (Z1_mul_nat n) A
 o* pequiv_inverse (equiv_Z1_hom A))
  (equiv_Z1_hom A f)
    refine (_ @ ap _ (eissect _ _)^).
H: Univalence
n: nat
IsEmbedding0: IsEmbedding (Z1_mul_nat n)
A: AbGroup
f: ab_hom ab_Z1 A
((equiv_Z1_hom A)^-1* o* ab_mul_nat n)
  (equiv_Z1_hom A f) =
fmap10 ab_hom (Z1_mul_nat n) A f
    apply moveR_equiv_V; symmetry.
H: Univalence
n: nat
IsEmbedding0: IsEmbedding (Z1_mul_nat n)
A: AbGroup
f: ab_hom ab_Z1 A
equiv_Z1_hom A (fmap10 ab_hom (Z1_mul_nat n) A f) =
ab_mul_nat n (equiv_Z1_hom A f)
    refine (ap f _ @ _).
H: Univalence
n: nat
IsEmbedding0: IsEmbedding (Z1_mul_nat n)
A: AbGroup
f: ab_hom ab_Z1 A
Z1_mul_nat n
  (freegroup_eta (FreeGroup.word_sing Unit (inl tt))) =
?Goal
H: Univalence
n: nat
IsEmbedding0: IsEmbedding (Z1_mul_nat n)
A: AbGroup
f: ab_hom ab_Z1 A
f ?Goal = ab_mul_nat n (equiv_Z1_hom A f)
    1: apply Z1_rec_beta.
H: Univalence
n: nat
IsEmbedding0: IsEmbedding (Z1_mul_nat n)
A: AbGroup
f: ab_hom ab_Z1 A
f (nat_to_Z1 n) = ab_mul_nat n (equiv_Z1_hom A f)
    exact (ab_mul_nat_homo f n Z1_gen).
  - (* we get rid of [equiv_Z1_hom] *)
H: Univalence
n: nat
IsEmbedding0: IsEmbedding (Z1_mul_nat n)
A: AbGroup
IsExact (Tr (-1))
  (fmap10 ab_hom (Z1_mul_nat n) A
   o* pequiv_inverse (equiv_Z1_hom A))
  (abses_pushout_ext
     (abses_from_inclusion (Z1_mul_nat n)))
    apply isexact_equiv_fiber.
H: Univalence
n: nat
IsEmbedding0: IsEmbedding (Z1_mul_nat n)
A: AbGroup
IsExact (Tr (-1)) (fmap10 ab_hom (Z1_mul_nat n) A)
  (abses_pushout_ext
     (abses_from_inclusion (Z1_mul_nat n)))
    apply isexact_ext_cyclic_ab_iii.
Defined.

(** The main result of this section. *)
Theorem ext_cyclic_ab@{u v w | u < v, v < w} `{Univalence}
  (n : nat) `{emb : IsEmbedding (Z1_mul_nat n)} {A : AbGroup@{u}}
  : ab_cokernel@{v w} (ab_mul_nat (A:=A) n)
      $<~> ab_ext@{u v} (cyclic'@{u v} n) A.
H: Univalence
n: nat
emb: IsEmbedding (Z1_mul_nat n)
A: AbGroup
ab_cokernel (ab_mul_nat n) $<~> ab_ext (cyclic' n) A
  (* We take a large cokernel in order to apply [abses_cokernel_iso]. *)
Proof.
H: Univalence
n: nat
emb: IsEmbedding (Z1_mul_nat n)
A: AbGroup
ab_cokernel (ab_mul_nat n) $<~> ab_ext (cyclic' n) A
  pose (E := abses_from_inclusion (Z1_mul_nat n)).
H: Univalence
n: nat
emb: IsEmbedding (Z1_mul_nat n)
A: AbGroup
E:= abses_from_inclusion (Z1_mul_nat n): AbSES
  (QuotientAbGroup ab_Z1
     (grp_image_embedding (Z1_mul_nat n))) ab_Z1
ab_cokernel (ab_mul_nat n) $<~> ab_ext (cyclic' n) A
  snrefine (abses_cokernel_iso (ab_mul_nat n) _).
H: Univalence
n: nat
emb: IsEmbedding (Z1_mul_nat n)
A: AbGroup
E:= abses_from_inclusion (Z1_mul_nat n): AbSES
  (QuotientAbGroup ab_Z1
     (grp_image_embedding (Z1_mul_nat n))) ab_Z1
GroupHomomorphism A (ab_ext (cyclic' n) A)
H: Univalence
n: nat
emb: IsEmbedding (Z1_mul_nat n)
A: AbGroup
E:= abses_from_inclusion (Z1_mul_nat n): AbSES
  (QuotientAbGroup ab_Z1
     (grp_image_embedding (Z1_mul_nat n))) ab_Z1
IsConnMap (Tr (-1)) ?g
H: Univalence
n: nat
emb: IsEmbedding (Z1_mul_nat n)
A: AbGroup
E:= abses_from_inclusion (Z1_mul_nat n): AbSES
  (QuotientAbGroup ab_Z1
     (grp_image_embedding (Z1_mul_nat n))) ab_Z1
IsExact (Tr (-1)) (ab_mul_nat n) ?g
  -
H: Univalence
n: nat
emb: IsEmbedding (Z1_mul_nat n)
A: AbGroup
E:= abses_from_inclusion (Z1_mul_nat n): AbSES
  (QuotientAbGroup ab_Z1
     (grp_image_embedding (Z1_mul_nat n))) ab_Z1
GroupHomomorphism A (ab_ext (cyclic' n) A) exact (grp_homo_compose
             (abses_pushout_ext E)
             (grp_iso_inverse (equiv_Z1_hom A))).
  -
H: Univalence
n: nat
emb: IsEmbedding (Z1_mul_nat n)
A: AbGroup
E:= abses_from_inclusion (Z1_mul_nat n): AbSES
  (QuotientAbGroup ab_Z1
     (grp_image_embedding (Z1_mul_nat n))) ab_Z1
IsConnMap (Tr (-1))
  (grp_homo_compose (abses_pushout_ext E)
     (grp_iso_inverse (equiv_Z1_hom A))) apply (conn_map_compose _ (grp_iso_inverse (equiv_Z1_hom A))).
H: Univalence
n: nat
emb: IsEmbedding (Z1_mul_nat n)
A: AbGroup
E:= abses_from_inclusion (Z1_mul_nat n): AbSES
  (QuotientAbGroup ab_Z1
     (grp_image_embedding (Z1_mul_nat n))) ab_Z1
IsConnMap (Tr (-1)) (grp_iso_inverse (equiv_Z1_hom A))
H: Univalence
n: nat
emb: IsEmbedding (Z1_mul_nat n)
A: AbGroup
E:= abses_from_inclusion (Z1_mul_nat n): AbSES
  (QuotientAbGroup ab_Z1
     (grp_image_embedding (Z1_mul_nat n))) ab_Z1
IsConnMap (Tr (-1)) (abses_pushout_ext E)
    1: rapply conn_map_isequiv.
H: Univalence
n: nat
emb: IsEmbedding (Z1_mul_nat n)
A: AbGroup
E:= abses_from_inclusion (Z1_mul_nat n): AbSES
  (QuotientAbGroup ab_Z1
     (grp_image_embedding (Z1_mul_nat n))) ab_Z1
IsConnMap (Tr (-1)) (abses_pushout_ext E)
    (* Coq knows that [Ext Z1 A] is contractible since [Z1] is projective, so exactness at spot iv gives us this: *)
    exact (isconnmap_O_isexact_base_contr _ _
             (fmap (pTr 0)
                (abses_pullback_pmap (A:=A)
                   (projection E)))).
  - (* we change [grp_homo_compose] to [o*] *)
H: Univalence
n: nat
emb: IsEmbedding (Z1_mul_nat n)
A: AbGroup
E:= abses_from_inclusion (Z1_mul_nat n): AbSES
  (QuotientAbGroup ab_Z1
     (grp_image_embedding (Z1_mul_nat n))) ab_Z1
IsExact (Tr (-1)) (ab_mul_nat n)
  (grp_homo_compose (abses_pushout_ext E)
     (grp_iso_inverse (equiv_Z1_hom A)))
    srapply isexact_homotopic_f.
H: Univalence
n: nat
emb: IsEmbedding (Z1_mul_nat n)
A: AbGroup
E:= abses_from_inclusion (Z1_mul_nat n): AbSES
  (QuotientAbGroup ab_Z1
     (grp_image_embedding (Z1_mul_nat n))) ab_Z1
A ->* ab_ext (cyclic' n) A
H: Univalence
n: nat
emb: IsEmbedding (Z1_mul_nat n)
A: AbGroup
E:= abses_from_inclusion (Z1_mul_nat n): AbSES
  (QuotientAbGroup ab_Z1
     (grp_image_embedding (Z1_mul_nat n))) ab_Z1
grp_homo_compose (abses_pushout_ext E)
  (grp_iso_inverse (equiv_Z1_hom A)) ==* ?f
H: Univalence
n: nat
emb: IsEmbedding (Z1_mul_nat n)
A: AbGroup
E:= abses_from_inclusion (Z1_mul_nat n): AbSES
  (QuotientAbGroup ab_Z1
     (grp_image_embedding (Z1_mul_nat n))) ab_Z1
IsExact (Tr (-1)) (ab_mul_nat n) ?f
    1: exact (abses_pushout_ext (abses_from_inclusion (Z1_mul_nat n))
                o* (pequiv_groupisomorphism (equiv_Z1_hom A))^-1*).
H: Univalence
n: nat
emb: IsEmbedding (Z1_mul_nat n)
A: AbGroup
E:= abses_from_inclusion (Z1_mul_nat n): AbSES
  (QuotientAbGroup ab_Z1
     (grp_image_embedding (Z1_mul_nat n))) ab_Z1
grp_homo_compose (abses_pushout_ext E)
  (grp_iso_inverse (equiv_Z1_hom A)) ==*
abses_pushout_ext
  (abses_from_inclusion (Z1_mul_nat n))
o* (equiv_Z1_hom A)^-1*
H: Univalence
n: nat
emb: IsEmbedding (Z1_mul_nat n)
A: AbGroup
E:= abses_from_inclusion (Z1_mul_nat n): AbSES
  (QuotientAbGroup ab_Z1
     (grp_image_embedding (Z1_mul_nat n))) ab_Z1
IsExact (Tr (-1)) (ab_mul_nat n)
  (abses_pushout_ext
     (abses_from_inclusion (Z1_mul_nat n))
   o* (equiv_Z1_hom A)^-1*)
    1: by apply phomotopy_homotopy_hset.
H: Univalence
n: nat
emb: IsEmbedding (Z1_mul_nat n)
A: AbGroup
E:= abses_from_inclusion (Z1_mul_nat n): AbSES
  (QuotientAbGroup ab_Z1
     (grp_image_embedding (Z1_mul_nat n))) ab_Z1
IsExact (Tr (-1)) (ab_mul_nat n)
  (abses_pushout_ext
     (abses_from_inclusion (Z1_mul_nat n))
   o* (equiv_Z1_hom A)^-1*)
    apply ext_cyclic_exact.
Defined.