Require Import Basics Types Truncations.Core.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Pointed.Core.
Require Import WildCat.Core Homotopy.ExactSequence.
Require Import AbGroups.AbelianGroup AbSES.Core AbGroups.Biproduct.

Local Open Scope pointed_scope.
Local Open Scope type_scope.
Local Open Scope mc_add_scope.

(** * The direct sum of short exact sequences *)

(** Biproducts of abelian groups preserve exactness. *)
Lemma ab_biprod_exact {A E B X F Y : AbGroup}
      (i : A $-> E) (p : E $-> B) `{ex0 : IsExact (Tr (-1)) _ _ _ i p}
      (j : X $-> F) (q : F $-> Y) `{ex1 : IsExact (Tr (-1)) _ _ _ j q}
  : IsExact (Tr (-1)) (functor_ab_biprod i j)
            (functor_ab_biprod p q).
A, E, B, X, F, Y: AbGroup
i: A $-> E
p: E $-> B
ex0: IsExact (Tr (-1)) i p
j: X $-> F
q: F $-> Y
ex1: IsExact (Tr (-1)) j q
IsExact (Tr (-1)) (functor_ab_biprod i j)
  (functor_ab_biprod p q)
Proof.
A, E, B, X, F, Y: AbGroup
i: A $-> E
p: E $-> B
ex0: IsExact (Tr (-1)) i p
j: X $-> F
q: F $-> Y
ex1: IsExact (Tr (-1)) j q
IsExact (Tr (-1)) (functor_ab_biprod i j)
  (functor_ab_biprod p q)
  snrapply Build_IsExact.
A, E, B, X, F, Y: AbGroup
i: A $-> E
p: E $-> B
ex0: IsExact (Tr (-1)) i p
j: X $-> F
q: F $-> Y
ex1: IsExact (Tr (-1)) j q
IsComplex (functor_ab_biprod i j)
  (functor_ab_biprod p q)
A, E, B, X, F, Y: AbGroup
i: A $-> E
p: E $-> B
ex0: IsExact (Tr (-1)) i p
j: X $-> F
q: F $-> Y
ex1: IsExact (Tr (-1)) j q
ReflectiveSubuniverse.IsConnMap (Tr (-1))
  (cxfib ?cx_isexact)
  -
A, E, B, X, F, Y: AbGroup
i: A $-> E
p: E $-> B
ex0: IsExact (Tr (-1)) i p
j: X $-> F
q: F $-> Y
ex1: IsExact (Tr (-1)) j q
IsComplex (functor_ab_biprod i j)
  (functor_ab_biprod p q) snrapply phomotopy_homotopy_hset.
A, E, B, X, F, Y: AbGroup
i: A $-> E
p: E $-> B
ex0: IsExact (Tr (-1)) i p
j: X $-> F
q: F $-> Y
ex1: IsExact (Tr (-1)) j q
IsHSet (ab_biprod B Y)
A, E, B, X, F, Y: AbGroup
i: A $-> E
p: E $-> B
ex0: IsExact (Tr (-1)) i p
j: X $-> F
q: F $-> Y
ex1: IsExact (Tr (-1)) j q
functor_ab_biprod p q o* functor_ab_biprod i j ==
pconst
    1: exact _.
A, E, B, X, F, Y: AbGroup
i: A $-> E
p: E $-> B
ex0: IsExact (Tr (-1)) i p
j: X $-> F
q: F $-> Y
ex1: IsExact (Tr (-1)) j q
functor_ab_biprod p q o* functor_ab_biprod i j ==
pconst
    intro x; apply path_prod; cbn.
A, E, B, X, F, Y: AbGroup
i: A $-> E
p: E $-> B
ex0: IsExact (Tr (-1)) i p
j: X $-> F
q: F $-> Y
ex1: IsExact (Tr (-1)) j q
x: ab_biprod A X
p (i (fst x)) = mon_unit
A, E, B, X, F, Y: AbGroup
i: A $-> E
p: E $-> B
ex0: IsExact (Tr (-1)) i p
j: X $-> F
q: F $-> Y
ex1: IsExact (Tr (-1)) j q
x: ab_biprod A X
q (j (snd x)) = mon_unit
    +
A, E, B, X, F, Y: AbGroup
i: A $-> E
p: E $-> B
ex0: IsExact (Tr (-1)) i p
j: X $-> F
q: F $-> Y
ex1: IsExact (Tr (-1)) j q
x: ab_biprod A X
p (i (fst x)) = mon_unit apply ex0.
    +
A, E, B, X, F, Y: AbGroup
i: A $-> E
p: E $-> B
ex0: IsExact (Tr (-1)) i p
j: X $-> F
q: F $-> Y
ex1: IsExact (Tr (-1)) j q
x: ab_biprod A X
q (j (snd x)) = mon_unit apply ex1.
  -
A, E, B, X, F, Y: AbGroup
i: A $-> E
p: E $-> B
ex0: IsExact (Tr (-1)) i p
j: X $-> F
q: F $-> Y
ex1: IsExact (Tr (-1)) j q
ReflectiveSubuniverse.IsConnMap (Tr (-1))
  (cxfib
     (phomotopy_homotopy_hset
        ((fun x : ab_biprod A X =>
          path_prod
            ((functor_ab_biprod p q
              o* functor_ab_biprod i j) x) (pconst x)
            ((let X0 := cx_isexact in
              let X1 := pointed_fun X0 in X1 (fst x))
             :
             fst
               ((functor_ab_biprod p q
                 o* functor_ab_biprod i j) x) =
             fst (pconst x))
            ((let X0 := cx_isexact in
              let X1 := pointed_fun X0 in X1 (snd x))
             :
             snd
               ((functor_ab_biprod p q
                 o* functor_ab_biprod i j) x) =
             snd (pconst x)))
         :
         functor_ab_biprod p q
         o* functor_ab_biprod i j == pconst))) intros [[e f] u]; cbn.
A, E, B, X, F, Y: AbGroup
i: A $-> E
p: E $-> B
ex0: IsExact (Tr (-1)) i p
j: X $-> F
q: F $-> Y
ex1: IsExact (Tr (-1)) j q
e: E
f: F
u: functor_ab_biprod p q (e, f) = pt
ReflectiveSubuniverse.IsConnected (Tr (-1))
  (hfiber
     (fun x : A * X =>
      ((i (fst x), j (snd x));
      path_prod (p (i (fst x)), q (j (snd x)))
        (mon_unit, mon_unit) (cx_isexact (fst x))
        (cx_isexact (snd x)))) ((e, f); u))
    rapply contr_inhabited_hprop.
A, E, B, X, F, Y: AbGroup
i: A $-> E
p: E $-> B
ex0: IsExact (Tr (-1)) i p
j: X $-> F
q: F $-> Y
ex1: IsExact (Tr (-1)) j q
e: E
f: F
u: functor_ab_biprod p q (e, f) = pt
Tr (-1)
  (hfiber
     (fun x : A * X =>
      ((i (fst x), j (snd x));
      path_prod (p (i (fst x)), q (j (snd x)))
        (mon_unit, mon_unit) (cx_isexact (fst x))
        (cx_isexact (snd x)))) ((e, f); u))
    pose (U := (equiv_path_prod _ _)^-1 u); cbn in U.
A, E, B, X, F, Y: AbGroup
i: A $-> E
p: E $-> B
ex0: IsExact (Tr (-1)) i p
j: X $-> F
q: F $-> Y
ex1: IsExact (Tr (-1)) j q
e: E
f: F
u: functor_ab_biprod p q (e, f) = pt
U:= (ap fst u, ap snd u): (p e = mon_unit) * (q f = mon_unit)
Tr (-1)
  (hfiber
     (fun x : A * X =>
      ((i (fst x), j (snd x));
      path_prod (p (i (fst x)), q (j (snd x)))
        (mon_unit, mon_unit) (cx_isexact (fst x))
        (cx_isexact (snd x)))) ((e, f); u))
    pose proof (a := isexact_preimage _ i p e (fst U)).
A, E, B, X, F, Y: AbGroup
i: A $-> E
p: E $-> B
ex0: IsExact (Tr (-1)) i p
j: X $-> F
q: F $-> Y
ex1: IsExact (Tr (-1)) j q
e: E
f: F
u: functor_ab_biprod p q (e, f) = pt
U:= (ap fst u, ap snd u): (p e = mon_unit) * (q f = mon_unit)
a: Tr (-1) (hfiber i e)
Tr (-1)
  (hfiber
     (fun x : A * X =>
      ((i (fst x), j (snd x));
      path_prod (p (i (fst x)), q (j (snd x)))
        (mon_unit, mon_unit) (cx_isexact (fst x))
        (cx_isexact (snd x)))) ((e, f); u))
    pose proof (x := isexact_preimage _ j q f (snd U)).
A, E, B, X, F, Y: AbGroup
i: A $-> E
p: E $-> B
ex0: IsExact (Tr (-1)) i p
j: X $-> F
q: F $-> Y
ex1: IsExact (Tr (-1)) j q
e: E
f: F
u: functor_ab_biprod p q (e, f) = pt
U:= (ap fst u, ap snd u): (p e = mon_unit) * (q f = mon_unit)
a: Tr (-1) (hfiber i e)
x: Tr (-1) (hfiber j f)
Tr (-1)
  (hfiber
     (fun x : A * X =>
      ((i (fst x), j (snd x));
      path_prod (p (i (fst x)), q (j (snd x)))
        (mon_unit, mon_unit) (cx_isexact (fst x))
        (cx_isexact (snd x)))) ((e, f); u))
    strip_truncations; apply tr.
A, E, B, X, F, Y: AbGroup
i: A $-> E
p: E $-> B
ex0: IsExact (Tr (-1)) i p
j: X $-> F
q: F $-> Y
ex1: IsExact (Tr (-1)) j q
e: E
f: F
u: functor_ab_biprod p q (e, f) = pt
U:= (ap fst u, ap snd u): (p e = mon_unit) * (q f = mon_unit)
x: hfiber j f
a: hfiber i e
hfiber
  (fun x : A * X =>
   ((i (fst x), j (snd x));
   path_prod (p (i (fst x)), q (j (snd x)))
     (mon_unit, mon_unit) (cx_isexact (fst x))
     (cx_isexact (snd x)))) ((e, f); u)
    exists (ab_biprod_inl a.1 + ab_biprod_inr x.1); cbn.
A, E, B, X, F, Y: AbGroup
i: A $-> E
p: E $-> B
ex0: IsExact (Tr (-1)) i p
j: X $-> F
q: F $-> Y
ex1: IsExact (Tr (-1)) j q
e: E
f: F
u: functor_ab_biprod p q (e, f) = pt
U:= (ap fst u, ap snd u): (p e = mon_unit) * (q f = mon_unit)
x: hfiber j f
a: hfiber i e
((i (a.1 + group_unit), j (group_unit + x.1));
path_prod
  (p (i (a.1 + group_unit)), q (j (group_unit + x.1)))
  (mon_unit, mon_unit) (cx_isexact (a.1 + group_unit))
  (cx_isexact (group_unit + x.1))) = ((e, f); u)
    pose (IS := sg_set (ab_biprod B Y)). (* This hint speeds up the next line. *)
A, E, B, X, F, Y: AbGroup
i: A $-> E
p: E $-> B
ex0: IsExact (Tr (-1)) i p
j: X $-> F
q: F $-> Y
ex1: IsExact (Tr (-1)) j q
e: E
f: F
u: functor_ab_biprod p q (e, f) = pt
U:= (ap fst u, ap snd u): (p e = mon_unit) * (q f = mon_unit)
x: hfiber j f
a: hfiber i e
IS:= sg_set (ab_biprod B Y): IsHSet (ab_biprod B Y)
((i (a.1 + group_unit), j (group_unit + x.1));
path_prod
  (p (i (a.1 + group_unit)), q (j (group_unit + x.1)))
  (mon_unit, mon_unit) (cx_isexact (a.1 + group_unit))
  (cx_isexact (group_unit + x.1))) = ((e, f); u)
    apply path_sigma_hprop; cbn.
A, E, B, X, F, Y: AbGroup
i: A $-> E
p: E $-> B
ex0: IsExact (Tr (-1)) i p
j: X $-> F
q: F $-> Y
ex1: IsExact (Tr (-1)) j q
e: E
f: F
u: functor_ab_biprod p q (e, f) = pt
U:= (ap fst u, ap snd u): (p e = mon_unit) * (q f = mon_unit)
x: hfiber j f
a: hfiber i e
IS:= sg_set (ab_biprod B Y): IsHSet (ab_biprod B Y)
(i (a.1 + group_unit), j (group_unit + x.1)) = (e, f)
    apply path_prod; cbn.
A, E, B, X, F, Y: AbGroup
i: A $-> E
p: E $-> B
ex0: IsExact (Tr (-1)) i p
j: X $-> F
q: F $-> Y
ex1: IsExact (Tr (-1)) j q
e: E
f: F
u: functor_ab_biprod p q (e, f) = pt
U:= (ap fst u, ap snd u): (p e = mon_unit) * (q f = mon_unit)
x: hfiber j f
a: hfiber i e
IS:= sg_set (ab_biprod B Y): IsHSet (ab_biprod B Y)
i (a.1 + group_unit) = e
A, E, B, X, F, Y: AbGroup
i: A $-> E
p: E $-> B
ex0: IsExact (Tr (-1)) i p
j: X $-> F
q: F $-> Y
ex1: IsExact (Tr (-1)) j q
e: E
f: F
u: functor_ab_biprod p q (e, f) = pt
U:= (ap fst u, ap snd u): (p e = mon_unit) * (q f = mon_unit)
x: hfiber j f
a: hfiber i e
IS:= sg_set (ab_biprod B Y): IsHSet (ab_biprod B Y)
j (group_unit + x.1) = f
    +
A, E, B, X, F, Y: AbGroup
i: A $-> E
p: E $-> B
ex0: IsExact (Tr (-1)) i p
j: X $-> F
q: F $-> Y
ex1: IsExact (Tr (-1)) j q
e: E
f: F
u: functor_ab_biprod p q (e, f) = pt
U:= (ap fst u, ap snd u): (p e = mon_unit) * (q f = mon_unit)
x: hfiber j f
a: hfiber i e
IS:= sg_set (ab_biprod B Y): IsHSet (ab_biprod B Y)
i (a.1 + group_unit) = e rewrite right_identity.
A, E, B, X, F, Y: AbGroup
i: A $-> E
p: E $-> B
ex0: IsExact (Tr (-1)) i p
j: X $-> F
q: F $-> Y
ex1: IsExact (Tr (-1)) j q
e: E
f: F
u: functor_ab_biprod p q (e, f) = pt
U:= (ap fst u, ap snd u): (p e = mon_unit) * (q f = mon_unit)
x: hfiber j f
a: hfiber i e
IS:= sg_set (ab_biprod B Y): IsHSet (ab_biprod B Y)
i a.1 = e
      exact a.2.
    +
A, E, B, X, F, Y: AbGroup
i: A $-> E
p: E $-> B
ex0: IsExact (Tr (-1)) i p
j: X $-> F
q: F $-> Y
ex1: IsExact (Tr (-1)) j q
e: E
f: F
u: functor_ab_biprod p q (e, f) = pt
U:= (ap fst u, ap snd u): (p e = mon_unit) * (q f = mon_unit)
x: hfiber j f
a: hfiber i e
IS:= sg_set (ab_biprod B Y): IsHSet (ab_biprod B Y)
j (group_unit + x.1) = f rewrite left_identity.
A, E, B, X, F, Y: AbGroup
i: A $-> E
p: E $-> B
ex0: IsExact (Tr (-1)) i p
j: X $-> F
q: F $-> Y
ex1: IsExact (Tr (-1)) j q
e: E
f: F
u: functor_ab_biprod p q (e, f) = pt
U:= (ap fst u, ap snd u): (p e = mon_unit) * (q f = mon_unit)
x: hfiber j f
a: hfiber i e
IS:= sg_set (ab_biprod B Y): IsHSet (ab_biprod B Y)
j x.1 = f
      exact x.2.
Defined.

(** The pointwise direct sum of two short exact sequences. *)
Definition abses_direct_sum `{Funext} {B A B' A' : AbGroup} (E : AbSES B A) (F : AbSES B' A')
  : AbSES (ab_biprod B B') (ab_biprod A A')
  := Build_AbSES (ab_biprod E F)
                 (functor_ab_biprod (inclusion E) (inclusion F))
                 (functor_ab_biprod (projection E) (projection F))
                 (functor_ab_biprod_embedding _ _)
                 (functor_ab_biprod_surjection _ _)
                 (ab_biprod_exact _ _ _ _).

(** For any short exact sequences [E], [E'], [F], [F'], and morphisms [f : E -> E'] and [g : F -> F'] there is a morphism [E + F -> E' + F']. *)
Lemma functor_abses_directsum `{Funext} {A A' B B' C C' D D' : AbGroup}
      {E : AbSES B A} {E' : AbSES B' A'} {F : AbSES D C} {F' : AbSES D' C'}
      (f : AbSESMorphism E E') (g : AbSESMorphism F F')
  : AbSESMorphism (abses_direct_sum E F) (abses_direct_sum E' F').
H: Funext
A, A', B, B', C, C', D, D': AbGroup
E: AbSES B A
E': AbSES B' A'
F: AbSES D C
F': AbSES D' C'
f: AbSESMorphism E E'
g: AbSESMorphism F F'
AbSESMorphism (abses_direct_sum E F)
  (abses_direct_sum E' F')
Proof.
H: Funext
A, A', B, B', C, C', D, D': AbGroup
E: AbSES B A
E': AbSES B' A'
F: AbSES D C
F': AbSES D' C'
f: AbSESMorphism E E'
g: AbSESMorphism F F'
AbSESMorphism (abses_direct_sum E F)
  (abses_direct_sum E' F')
  snrapply Build_AbSESMorphism.
H: Funext
A, A', B, B', C, C', D, D': AbGroup
E: AbSES B A
E': AbSES B' A'
F: AbSES D C
F': AbSES D' C'
f: AbSESMorphism E E'
g: AbSESMorphism F F'
ab_biprod A C $-> ab_biprod A' C'
H: Funext
A, A', B, B', C, C', D, D': AbGroup
E: AbSES B A
E': AbSES B' A'
F: AbSES D C
F': AbSES D' C'
f: AbSESMorphism E E'
g: AbSESMorphism F F'
abses_direct_sum E F $-> abses_direct_sum E' F'
H: Funext
A, A', B, B', C, C', D, D': AbGroup
E: AbSES B A
E': AbSES B' A'
F: AbSES D C
F': AbSES D' C'
f: AbSESMorphism E E'
g: AbSESMorphism F F'
ab_biprod B D $-> ab_biprod B' D'
H: Funext
A, A', B, B', C, C', D, D': AbGroup
E: AbSES B A
E': AbSES B' A'
F: AbSES D C
F': AbSES D' C'
f: AbSESMorphism E E'
g: AbSESMorphism F F'
inclusion (abses_direct_sum E' F') $o ?component1 ==
?component2 $o inclusion (abses_direct_sum E F)
H: Funext
A, A', B, B', C, C', D, D': AbGroup
E: AbSES B A
E': AbSES B' A'
F: AbSES D C
F': AbSES D' C'
f: AbSESMorphism E E'
g: AbSESMorphism F F'
projection (abses_direct_sum E' F') $o ?component2 ==
?component3 $o projection (abses_direct_sum E F)
  +
H: Funext
A, A', B, B', C, C', D, D': AbGroup
E: AbSES B A
E': AbSES B' A'
F: AbSES D C
F': AbSES D' C'
f: AbSESMorphism E E'
g: AbSESMorphism F F'
ab_biprod A C $-> ab_biprod A' C' exact (functor_ab_biprod (component1 f) (component1 g)).
  +
H: Funext
A, A', B, B', C, C', D, D': AbGroup
E: AbSES B A
E': AbSES B' A'
F: AbSES D C
F': AbSES D' C'
f: AbSESMorphism E E'
g: AbSESMorphism F F'
abses_direct_sum E F $-> abses_direct_sum E' F' exact (functor_ab_biprod (component2 f) (component2 g)).
  +
H: Funext
A, A', B, B', C, C', D, D': AbGroup
E: AbSES B A
E': AbSES B' A'
F: AbSES D C
F': AbSES D' C'
f: AbSESMorphism E E'
g: AbSESMorphism F F'
ab_biprod B D $-> ab_biprod B' D' exact (functor_ab_biprod (component3 f) (component3 g)).
  +
H: Funext
A, A', B, B', C, C', D, D': AbGroup
E: AbSES B A
E': AbSES B' A'
F: AbSES D C
F': AbSES D' C'
f: AbSESMorphism E E'
g: AbSESMorphism F F'
inclusion (abses_direct_sum E' F') $o
functor_ab_biprod (component1 f) (component1 g) ==
functor_ab_biprod (component2 f) (component2 g) $o
inclusion (abses_direct_sum E F) intro x.
H: Funext
A, A', B, B', C, C', D, D': AbGroup
E: AbSES B A
E': AbSES B' A'
F: AbSES D C
F': AbSES D' C'
f: AbSESMorphism E E'
g: AbSESMorphism F F'
x: ab_biprod A C
(inclusion (abses_direct_sum E' F') $o
 functor_ab_biprod (component1 f) (component1 g)) x =
(functor_ab_biprod (component2 f) (component2 g) $o
 inclusion (abses_direct_sum E F)) x
    apply path_prod; apply left_square.
  +
H: Funext
A, A', B, B', C, C', D, D': AbGroup
E: AbSES B A
E': AbSES B' A'
F: AbSES D C
F': AbSES D' C'
f: AbSESMorphism E E'
g: AbSESMorphism F F'
projection (abses_direct_sum E' F') $o
functor_ab_biprod (component2 f) (component2 g) ==
functor_ab_biprod (component3 f) (component3 g) $o
projection (abses_direct_sum E F) intro x.
H: Funext
A, A', B, B', C, C', D, D': AbGroup
E: AbSES B A
E': AbSES B' A'
F: AbSES D C
F': AbSES D' C'
f: AbSESMorphism E E'
g: AbSESMorphism F F'
x: abses_direct_sum E F
(projection (abses_direct_sum E' F') $o
 functor_ab_biprod (component2 f) (component2 g)) x =
(functor_ab_biprod (component3 f) (component3 g) $o
 projection (abses_direct_sum E F)) x
    apply path_prod; apply right_square.
Defined.

(** For any short exact sequence [E], there is a morphism [E -> abses_direct_sum E E], where each component is ab_diagonal. *)
Definition abses_diagonal `{Funext} {A B : AbGroup} (E : AbSES B A)
  : AbSESMorphism E (abses_direct_sum E E).
H: Funext
A, B: AbGroup
E: AbSES B A
AbSESMorphism E (abses_direct_sum E E)
Proof.
H: Funext
A, B: AbGroup
E: AbSES B A
AbSESMorphism E (abses_direct_sum E E)
  snrapply Build_AbSESMorphism.
H: Funext
A, B: AbGroup
E: AbSES B A
A $-> ab_biprod A A
H: Funext
A, B: AbGroup
E: AbSES B A
E $-> abses_direct_sum E E
H: Funext
A, B: AbGroup
E: AbSES B A
B $-> ab_biprod B B
H: Funext
A, B: AbGroup
E: AbSES B A
inclusion (abses_direct_sum E E) $o ?component1 ==
?component2 $o inclusion E
H: Funext
A, B: AbGroup
E: AbSES B A
projection (abses_direct_sum E E) $o ?component2 ==
?component3 $o projection E
  1,2,3: exact ab_diagonal.
H: Funext
A, B: AbGroup
E: AbSES B A
inclusion (abses_direct_sum E E) $o ab_diagonal ==
ab_diagonal $o inclusion E
H: Funext
A, B: AbGroup
E: AbSES B A
projection (abses_direct_sum E E) $o ab_diagonal ==
ab_diagonal $o projection E
  all: reflexivity.
Defined.

(** For any short exact sequence [E], there is dually a morphism [abses_direct_sum E E -> E], with each component being the codiagonal. *)
Definition abses_codiagonal `{Funext} {A B : AbGroup} (E : AbSES B A)
  : AbSESMorphism (abses_direct_sum E E) E.
H: Funext
A, B: AbGroup
E: AbSES B A
AbSESMorphism (abses_direct_sum E E) E
Proof.
H: Funext
A, B: AbGroup
E: AbSES B A
AbSESMorphism (abses_direct_sum E E) E
  snrapply Build_AbSESMorphism.
H: Funext
A, B: AbGroup
E: AbSES B A
ab_biprod A A $-> A
H: Funext
A, B: AbGroup
E: AbSES B A
abses_direct_sum E E $-> E
H: Funext
A, B: AbGroup
E: AbSES B A
ab_biprod B B $-> B
H: Funext
A, B: AbGroup
E: AbSES B A
inclusion E $o ?component1 ==
?component2 $o inclusion (abses_direct_sum E E)
H: Funext
A, B: AbGroup
E: AbSES B A
projection E $o ?component2 ==
?component3 $o projection (abses_direct_sum E E)
  1,2,3: exact ab_codiagonal.
H: Funext
A, B: AbGroup
E: AbSES B A
inclusion E $o ab_codiagonal ==
ab_codiagonal $o inclusion (abses_direct_sum E E)
H: Funext
A, B: AbGroup
E: AbSES B A
projection E $o ab_codiagonal ==
ab_codiagonal $o projection (abses_direct_sum E E)
  all: intro x; cbn; apply grp_homo_op.
Defined.

(** There is always a morphism [abses_direct_sum E F -> abses_direct_sum F E] of short exact sequences, for any [E : AbSES B A] and [F : AbSES B' A']. *)
Definition abses_swap_morphism `{Funext} {A A' B B' : AbGroup}
           (E : AbSES B A) (F : AbSES B' A')
  : AbSESMorphism (abses_direct_sum E F) (abses_direct_sum F E).
H: Funext
A, A', B, B': AbGroup
E: AbSES B A
F: AbSES B' A'
AbSESMorphism (abses_direct_sum E F)
  (abses_direct_sum F E)
Proof.
H: Funext
A, A', B, B': AbGroup
E: AbSES B A
F: AbSES B' A'
AbSESMorphism (abses_direct_sum E F)
  (abses_direct_sum F E)
  snrapply Build_AbSESMorphism.
H: Funext
A, A', B, B': AbGroup
E: AbSES B A
F: AbSES B' A'
ab_biprod A A' $-> ab_biprod A' A
H: Funext
A, A', B, B': AbGroup
E: AbSES B A
F: AbSES B' A'
abses_direct_sum E F $-> abses_direct_sum F E
H: Funext
A, A', B, B': AbGroup
E: AbSES B A
F: AbSES B' A'
ab_biprod B B' $-> ab_biprod B' B
H: Funext
A, A', B, B': AbGroup
E: AbSES B A
F: AbSES B' A'
inclusion (abses_direct_sum F E) $o ?component1 ==
?component2 $o inclusion (abses_direct_sum E F)
H: Funext
A, A', B, B': AbGroup
E: AbSES B A
F: AbSES B' A'
projection (abses_direct_sum F E) $o ?component2 ==
?component3 $o projection (abses_direct_sum E F)
  1,2,3: exact direct_sum_swap.
H: Funext
A, A', B, B': AbGroup
E: AbSES B A
F: AbSES B' A'
inclusion (abses_direct_sum F E) $o direct_sum_swap ==
direct_sum_swap $o inclusion (abses_direct_sum E F)
H: Funext
A, A', B, B': AbGroup
E: AbSES B A
F: AbSES B' A'
projection (abses_direct_sum F E) $o direct_sum_swap ==
direct_sum_swap $o projection (abses_direct_sum E F)
  all: reflexivity.
Defined.

(** For [E, F, G : AbSES B A], there is a morphism [(E + F) + G -> (G + F) + E] induced by the above map, where [+] denotes [abses_direct_sum]. *)
Lemma abses_twist_directsum `{Funext} {A B : AbGroup} (E F G : AbSES B A)
  : AbSESMorphism (abses_direct_sum (abses_direct_sum E F) G)
                  (abses_direct_sum (abses_direct_sum G F) E).
H: Funext
A, B: AbGroup
E, F, G: AbSES B A
AbSESMorphism
  (abses_direct_sum (abses_direct_sum E F) G)
  (abses_direct_sum (abses_direct_sum G F) E)
Proof.
H: Funext
A, B: AbGroup
E, F, G: AbSES B A
AbSESMorphism
  (abses_direct_sum (abses_direct_sum E F) G)
  (abses_direct_sum (abses_direct_sum G F) E)
  snrapply Build_AbSESMorphism.
H: Funext
A, B: AbGroup
E, F, G: AbSES B A
ab_biprod (ab_biprod A A) A $->
ab_biprod (ab_biprod A A) A
H: Funext
A, B: AbGroup
E, F, G: AbSES B A
abses_direct_sum (abses_direct_sum E F) G $->
abses_direct_sum (abses_direct_sum G F) E
H: Funext
A, B: AbGroup
E, F, G: AbSES B A
ab_biprod (ab_biprod B B) B $->
ab_biprod (ab_biprod B B) B
H: Funext
A, B: AbGroup
E, F, G: AbSES B A
inclusion (abses_direct_sum (abses_direct_sum G F) E) $o
?component1 ==
?component2 $o
inclusion (abses_direct_sum (abses_direct_sum E F) G)
H: Funext
A, B: AbGroup
E, F, G: AbSES B A
projection (abses_direct_sum (abses_direct_sum G F) E) $o
?component2 ==
?component3 $o
projection (abses_direct_sum (abses_direct_sum E F) G)
  1,2,3: exact ab_biprod_twist.
H: Funext
A, B: AbGroup
E, F, G: AbSES B A
inclusion (abses_direct_sum (abses_direct_sum G F) E) $o
ab_biprod_twist ==
ab_biprod_twist $o
inclusion (abses_direct_sum (abses_direct_sum E F) G)
H: Funext
A, B: AbGroup
E, F, G: AbSES B A
projection (abses_direct_sum (abses_direct_sum G F) E) $o
ab_biprod_twist ==
ab_biprod_twist $o
projection (abses_direct_sum (abses_direct_sum E F) G)
  all: reflexivity.
Defined.