BaerSum.v

Require Import Basics Types.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import WildCat Pointed.Core.
Require Import AbGroups.AbelianGroup AbGroups.Biproduct AbGroups.AbHom.
Require Import AbSES.Core AbSES.Pullback AbSES.Pushout AbSES.DirectSum.
Require Import Homotopy.HSpace.Core.

Local Open Scope mc_scope.
Local Open Scope mc_add_scope.

(** * The Baer sum of two short exact sequences, lemmas and consequences. *)

(** The Baer sum of two short exact sequences is obtained from the pointwise direct sum by pushing forward along the codiagonal and then pulling back along the diagonal. (Swapping the order of pushing forward and pulling back produces an isomorphic short exact sequence.) *)
Definition abses_baer_sum `{Univalence} {B A : AbGroup@{u}} (E F : AbSES B A)
  : AbSES B A
  := abses_pullback ab_diagonal (abses_pushout ab_codiagonal (abses_direct_sum E F)).


(** ** [AbSES'] is a bifunctor *)

(** Given a morphism [f] of short exact sequences, the pushout of the domain along [f_1] equals the pullback of the codomain along [f_3]. *)
Lemma abses_pushout_is_pullback' `{Univalence} {A A' B B' : AbGroup@{u}}
      {E : AbSES B A} {E' : AbSES B' A'} (f : AbSESMorphism E E')
  : abses_pushout (component1 f) E $== abses_pullback (component3 f) E'.H: Univalence
A, A', B, B': AbGroup
E: AbSES B A
E': AbSES B' A'
f: AbSESMorphism E E'
abses_pushout (component1 f) E $==
abses_pullback (component3 f) E'
Proof.H: Univalence
A, A', B, B': AbGroup
E: AbSES B A
E': AbSES B' A'
f: AbSESMorphism E E'
abses_pushout (component1 f) E $==
abses_pullback (component3 f) E'
  (* The morphism [f : E -> E'] factors as [E -> f_1 E -> E'], where the first map is the map defining the pushout [f_1 E] and the second map is denoted [abses_pushout_morphism_rec f] below.  This second map is the identity on the first component, so it presents its domain as the pullback of [E'] along [f_3]. *)
  exact (abses_pullback_component1_id' (abses_pushout_morphism_rec f) (fun _ => idpath)).
Defined.

(** Given a morphism [f] of short exact sequences, the pushout of the domain along [f_1] equals the pullback of the codomain along [f_3]. *)
Definition abses_pushout_is_pullback `{Univalence} {A A' B B' : AbGroup}
      {E : AbSES B A} {E' : AbSES B' A'} (f : AbSESMorphism E E')
  : abses_pushout (component1 f) E = abses_pullback (component3 f) E'
  := equiv_path_abses_iso (abses_pushout_is_pullback' f).

Definition abses_pushout_pullback_reorder' `{Univalence} {A A' B B' : AbGroup}
  (E : AbSES B A) (f : A $-> A') (g : B' $-> B)
  : abses_pushout f (abses_pullback g E) $== abses_pullback g (abses_pushout f E).H: Univalence
A, A', B, B': AbGroup
E: AbSES B A
f: A $-> A'
g: B' $-> B
abses_pushout f (abses_pullback g E) $==
abses_pullback g (abses_pushout f E)
Proof.H: Univalence
A, A', B, B': AbGroup
E: AbSES B A
f: A $-> A'
g: B' $-> B
abses_pushout f (abses_pullback g E) $==
abses_pullback g (abses_pushout f E)
  (* There are morphisms [Eg -> E] and [E -> fE] by definition of the pullback and pushout. We define [F : Eg -> fE] to be the composite. Its first and third components are [f o id] and [id o g]. *)
  pose (F := absesmorphism_compose (abses_pushout_morphism E f) (abses_pullback_morphism E g)).H: Univalence
A, A', B, B': AbGroup
E: AbSES B A
f: A $-> A'
g: B' $-> B
F:= absesmorphism_compose (abses_pushout_morphism E f)
  (abses_pullback_morphism E g): AbSESMorphism (abses_pullback g E)
  (abses_pushout f E)
abses_pushout f (abses_pullback g E) $==
abses_pullback g (abses_pushout f E)
  (* We change [F] to a morphism that is the same except that the first and third components are [f] and [g]. Then [abses_pushout_is_pullback] shows that the pushout of [Eg] along [f] is equal to the pullback of [fE] along [g]. *)
  refine (abses_pushout_is_pullback' (Build_AbSESMorphism f (component2 F) g _ _)); apply F.
Defined.

(** This is the statement that [AbSES'] is a bifunctor, but we state it separately because Coq is slow to unify [IsBifunctor AbSES'] against goals written in this form. *)
Definition abses_pushout_pullback_reorder `{Univalence} {A A' B B' : AbGroup}
  (E : AbSES B A) (f : A $-> A') (g : B' $-> B)
  : abses_pushout f (abses_pullback g E) = abses_pullback g (abses_pushout f E).H: Univalence
A, A', B, B': AbGroup
E: AbSES B A
f: A $-> A'
g: B' $-> B
abses_pushout f (abses_pullback g E) =
abses_pullback g (abses_pushout f E)
Proof.H: Univalence
A, A', B, B': AbGroup
E: AbSES B A
f: A $-> A'
g: B' $-> B
abses_pushout f (abses_pullback g E) =
abses_pullback g (abses_pushout f E)
  apply equiv_path_abses_iso.H: Univalence
A, A', B, B': AbGroup
E: AbSES B A
f: A $-> A'
g: B' $-> B
abses_path_data_iso
  (abses_pushout f (abses_pullback g E))
  (abses_pullback g (abses_pushout f E))
  apply abses_pushout_pullback_reorder'.
Defined.

Instance is0bifunctor_abses' `{Univalence}
  : Is0Bifunctor (AbSES' : AbGroup^op -> AbGroup -> Type)
  := Build_Is0Bifunctor'' _.

Instance is1bifunctor_abses' `{Univalence}
  : Is1Bifunctor (AbSES' : AbGroup^op -> AbGroup -> Type).H: Univalence
Is1Bifunctor (AbSES' : AbGroup^op -> AbGroup -> Type)
Proof.H: Univalence
Is1Bifunctor (AbSES' : AbGroup^op -> AbGroup -> Type)
  snapply Build_Is1Bifunctor''.H: Univalence
forall a : AbGroup^op, Is1Functor (AbSES' a)
H: Univalence
forall b : AbGroup, Is1Functor (flip AbSES' b)
H: Univalence
forall (a0 a1 : AbGroup^op) (f : a0 $-> a1)
(b0 b1 : AbGroup) (g : b0 $-> b1),
fmap01 AbSES' a1 g $o fmap10 AbSES' f b0 $==
fmap10 AbSES' f b1 $o fmap01 AbSES' a0 g
  1,2: exact _.H: Univalence
forall (a0 a1 : AbGroup^op) (f : a0 $-> a1)
(b0 b1 : AbGroup) (g : b0 $-> b1),
fmap01 AbSES' a1 g $o fmap10 AbSES' f b0 $==
fmap10 AbSES' f b1 $o fmap01 AbSES' a0 g
  intros ? ? g ? ? f E; cbn.H: Univalence
a0, a1: AbGroup^op
g: a0 $-> a1
b0, b1: AbGroup
f: b0 $-> b1
E: AbSES' a0 b0
abses_pushout f (abses_pullback g E) =
abses_pullback g (abses_pushout f E)
  exact (abses_pushout_pullback_reorder E f g).
Defined.

(** Given a short exact sequence [A -> E -> B] and maps [f : A -> A'], [g : B' -> B], we can change the order of pushing out along [f] and pulling back along [g]. *)
Lemma abses_reorder_pullback_pushout `{Univalence} {A A' B B' : AbGroup}
      (E : AbSES B A) (f : A $-> A') (g : B' $-> B)
  : abses_pushout f (abses_pullback g E) = abses_pullback g (abses_pushout f E).H: Univalence
A, A', B, B': AbGroup
E: AbSES B A
f: A $-> A'
g: B' $-> B
abses_pushout f (abses_pullback g E) =
abses_pullback g (abses_pushout f E)
Proof.H: Univalence
A, A', B, B': AbGroup
E: AbSES B A
f: A $-> A'
g: B' $-> B
abses_pushout f (abses_pullback g E) =
abses_pullback g (abses_pushout f E)
  (* There are morphisms [Eg -> E] and [E -> fE] by definition of the pullback and pushout. We define [F : Eg -> fE] to be the composite. Its first and third components are [f o id] and [id o g]. *)
  pose (F := absesmorphism_compose (abses_pushout_morphism E f) (abses_pullback_morphism E g)).H: Univalence
A, A', B, B': AbGroup
E: AbSES B A
f: A $-> A'
g: B' $-> B
F:= absesmorphism_compose (abses_pushout_morphism E f)
  (abses_pullback_morphism E g): AbSESMorphism (abses_pullback g E)
  (abses_pushout f E)
abses_pushout f (abses_pullback g E) =
abses_pullback g (abses_pushout f E)
  (* We change [F] to a morphism that is the same except that the first and third components are [f] and [g]. Then [abses_pushout_is_pullback] shows that the pushout of [Eg] along [f] is equal to the pullback of [fE] along [g]. *)
  refine (abses_pushout_is_pullback (Build_AbSESMorphism f (component2 F) g _ _)); apply F.
Defined.

(** The Baer sum distributes over pullbacks. *)
Lemma baer_sum_distributive_pullbacks `{Univalence} {A B B' : AbGroup}
  {E : AbSES B A} (f g : ab_hom B' B)
  : abses_pullback (f + g) E = abses_baer_sum (abses_pullback f E) (abses_pullback g E).H: Univalence
A, B, B': AbGroup
E: AbSES B A
f, g: ab_hom B' B
abses_pullback (f + g) E =
abses_baer_sum (abses_pullback f E)
  (abses_pullback g E)
Proof.H: Univalence
A, B, B': AbGroup
E: AbSES B A
f, g: ab_hom B' B
abses_pullback (f + g) E =
abses_baer_sum (abses_pullback f E)
  (abses_pullback g E)
  unfold abses_baer_sum.H: Univalence
A, B, B': AbGroup
E: AbSES B A
f, g: ab_hom B' B
abses_pullback (f + g) E =
abses_pullback ab_diagonal
  (abses_pushout ab_codiagonal
     (abses_direct_sum (abses_pullback f E)
        (abses_pullback g E)))
  refine ((abses_pullback_compose (B1:=ab_biprod B B) _ _ E)^ @ _).H: Univalence
A, B, B': AbGroup
E: AbSES B A
f, g: ab_hom B' B
abses_pullback (grp_prod_corec f g)
  (abses_pullback ab_codiagonal E) =
abses_pullback ab_diagonal
  (abses_pushout ab_codiagonal
     (abses_direct_sum (abses_pullback f E)
        (abses_pullback g E)))
  refine (ap (abses_pullback _) (abses_pushout_is_pullback (abses_codiagonal E))^ @ _).H: Univalence
A, B, B': AbGroup
E: AbSES B A
f, g: ab_hom B' B
abses_pullback (grp_prod_corec f g)
  (abses_pushout (component1 (abses_codiagonal E))
     (abses_direct_sum E E)) =
abses_pullback ab_diagonal
  (abses_pushout ab_codiagonal
     (abses_direct_sum (abses_pullback f E)
        (abses_pullback g E)))
  unfold abses_codiagonal, component1.H: Univalence
A, B, B': AbGroup
E: AbSES B A
f, g: ab_hom B' B
abses_pullback (grp_prod_corec f g)
  (abses_pushout ab_codiagonal (abses_direct_sum E E)) =
abses_pullback ab_diagonal
  (abses_pushout ab_codiagonal
     (abses_direct_sum (abses_pullback f E)
        (abses_pullback g E)))
  refine (_^ @ _ @ _).H: Univalence
A, B, B': AbGroup
E: AbSES B A
f, g: ab_hom B' B
?Goal0 =
abses_pullback (grp_prod_corec f g)
  (abses_pushout ab_codiagonal (abses_direct_sum E E))
H: Univalence
A, B, B': AbGroup
E: AbSES B A
f, g: ab_hom B' B
?Goal0 = ?Goal
H: Univalence
A, B, B': AbGroup
E: AbSES B A
f, g: ab_hom B' B
?Goal =
abses_pullback ab_diagonal
  (abses_pushout ab_codiagonal
     (abses_direct_sum (abses_pullback f E)
        (abses_pullback g E)))
  1,3: apply abses_reorder_pullback_pushout.H: Univalence
A, B, B': AbGroup
E: AbSES B A
f, g: ab_hom B' B
abses_pushout ab_codiagonal
  (abses_pullback (grp_prod_corec f g)
     (abses_direct_sum E E)) =
abses_pushout ab_codiagonal
  (abses_pullback ab_diagonal
     (abses_direct_sum (abses_pullback f E)
        (abses_pullback g E)))
  refine (ap (abses_pushout _) _).H: Univalence
A, B, B': AbGroup
E: AbSES B A
f, g: ab_hom B' B
abses_pullback (grp_prod_corec f g)
  (abses_direct_sum E E) =
abses_pullback ab_diagonal
  (abses_direct_sum (abses_pullback f E)
     (abses_pullback g E))
  refine (ap (fun h => abses_pullback h _) (ab_biprod_corec_diagonal _ _) @ _).H: Univalence
A, B, B': AbGroup
E: AbSES B A
f, g: ab_hom B' B
abses_pullback (functor_ab_biprod f g $o ab_diagonal)
  (abses_direct_sum E E) =
abses_pullback ab_diagonal
  (abses_direct_sum (abses_pullback f E)
     (abses_pullback g E))
  refine ((abses_pullback_compose _ _ (abses_direct_sum E E))^ @ _).H: Univalence
A, B, B': AbGroup
E: AbSES B A
f, g: ab_hom B' B
abses_pullback ab_diagonal
  (abses_pullback (functor_ab_biprod f g)
     (abses_direct_sum E E)) =
abses_pullback ab_diagonal
  (abses_direct_sum (abses_pullback f E)
     (abses_pullback g E))
  exact (ap (abses_pullback _) (abses_directsum_distributive_pullbacks f g)).
Defined.

(** The Baer sum is commutative. *)
Lemma baer_sum_commutative `{Univalence} {A B : AbGroup} (E F : AbSES B A)
  : abses_baer_sum E F = abses_baer_sum F E.H: Univalence
A, B: AbGroup
E, F: AbSES B A
abses_baer_sum E F = abses_baer_sum F E
Proof.H: Univalence
A, B: AbGroup
E, F: AbSES B A
abses_baer_sum E F = abses_baer_sum F E
  unfold abses_baer_sum.H: Univalence
A, B: AbGroup
E, F: AbSES B A
abses_pullback ab_diagonal
  (abses_pushout ab_codiagonal (abses_direct_sum E F)) =
abses_pullback ab_diagonal
  (abses_pushout ab_codiagonal (abses_direct_sum F E))
  (* The next line uses that [direct_sum_swap $o ab_diagonal] is definitionally equal to [ab_diagonal]: *)
  refine (_ @ abses_pullback_compose ab_diagonal direct_sum_swap _).H: Univalence
A, B: AbGroup
E, F: AbSES B A
abses_pullback ab_diagonal
  (abses_pushout ab_codiagonal (abses_direct_sum E F)) =
abses_pullback ab_diagonal
  (abses_pullback direct_sum_swap
     (abses_pushout ab_codiagonal
        (abses_direct_sum F E)))
  refine (ap (abses_pullback ab_diagonal) _).H: Univalence
A, B: AbGroup
E, F: AbSES B A
abses_pushout ab_codiagonal (abses_direct_sum E F) =
abses_pullback direct_sum_swap
  (abses_pushout ab_codiagonal (abses_direct_sum F E))
  refine (ap (fun f => abses_pushout f _) ab_codiagonal_swap^ @ _).H: Univalence
A, B: AbGroup
E, F: AbSES B A
abses_pushout (ab_codiagonal $o direct_sum_swap)
  (abses_direct_sum E F) =
abses_pullback direct_sum_swap
  (abses_pushout ab_codiagonal (abses_direct_sum F E))
  refine ((abses_pushout_compose _ _ _) @ _).H: Univalence
A, B: AbGroup
E, F: AbSES B A
abses_pushout ab_codiagonal
  (abses_pushout direct_sum_swap
     (abses_direct_sum E F)) =
abses_pullback direct_sum_swap
  (abses_pushout ab_codiagonal (abses_direct_sum F E))
  refine (ap _ (abses_pushout_is_pullback (abses_swap_morphism E F)) @ _).H: Univalence
A, B: AbGroup
E, F: AbSES B A
abses_pushout ab_codiagonal
  (abses_pullback
     (component3 (abses_swap_morphism E F))
     (abses_direct_sum F E)) =
abses_pullback direct_sum_swap
  (abses_pushout ab_codiagonal (abses_direct_sum F E))
  unfold abses_swap_morphism, component3.H: Univalence
A, B: AbGroup
E, F: AbSES B A
abses_pushout ab_codiagonal
  (abses_pullback direct_sum_swap
     (abses_direct_sum F E)) =
abses_pullback direct_sum_swap
  (abses_pushout ab_codiagonal (abses_direct_sum F E))
  apply abses_pushout_pullback_reorder.
Defined.

(** The right unit law for the Baer sum says that for all [E : AbSES B A], [E + E_0 = E], where [E_0] is the split short exact sequence. *)
Lemma baer_sum_unit_r `{Univalence} {A B : AbGroup} (E : AbSES B A)
  : abses_baer_sum E (point (AbSES B A)) = E.H: Univalence
A, B: AbGroup
E: AbSES B A
abses_baer_sum E (point (AbSES B A)) = E
Proof.H: Univalence
A, B: AbGroup
E: AbSES B A
abses_baer_sum E (point (AbSES B A)) = E
  refine (ap (abses_baer_sum E) _ @ _).H: Univalence
A, B: AbGroup
E: AbSES B A
point (AbSES B A) = ?Goal
H: Univalence
A, B: AbGroup
E: AbSES B A
abses_baer_sum E ?Goal = E
  -H: Univalence
A, B: AbGroup
E: AbSES B A
point (AbSES B A) = ?Goal exact (abses_pullback_const E).
  -H: Univalence
A, B: AbGroup
E: AbSES B A
abses_baer_sum E (abses_pullback grp_homo_const E) = E refine (ap (fun F => abses_baer_sum F (abses_pullback grp_homo_const E)) (abses_pullback_id E)^ @ _).H: Univalence
A, B: AbGroup
E: AbSES B A
abses_baer_sum (abses_pullback grp_homo_id E)
  (abses_pullback grp_homo_const E) = E
    refine ((baer_sum_distributive_pullbacks grp_homo_id grp_homo_const)^ @ _).H: Univalence
A, B: AbGroup
E: AbSES B A
abses_pullback (grp_homo_id + grp_homo_const) E = E
    refine (ap (fun f => abses_pullback f E) (grp_unit_r (G := ab_hom _ _) _) @ _).H: Univalence
A, B: AbGroup
E: AbSES B A
abses_pullback grp_homo_id E = E
    apply abses_pullback_id.
Defined.

(** The left unit law for the Baer sum is analogous. *)
Definition baer_sum_unit_l `{Univalence} {A B : AbGroup} (E : AbSES B A)
  : abses_baer_sum (point (AbSES B A)) E = E
  := baer_sum_commutative _ _ @ baer_sum_unit_r _.

(** For any [E : AbSES B A], the pullback of [E] along [-id_B] acts as an additive inverse for [E] with respect to the Baer sum. *)
Lemma baer_sum_inverse_l `{Univalence} {A B : AbGroup} (E : AbSES B A)
  : abses_baer_sum E (abses_pullback (- grp_homo_id) E) = point (AbSES B A).H: Univalence
A, B: AbGroup
E: AbSES B A
abses_baer_sum E (abses_pullback (- grp_homo_id) E) =
point (AbSES B A)
Proof.H: Univalence
A, B: AbGroup
E: AbSES B A
abses_baer_sum E (abses_pullback (- grp_homo_id) E) =
point (AbSES B A)
  refine (ap (fun F => abses_baer_sum F (abses_pullback _ E)) (abses_pullback_id E)^ @ _).H: Univalence
A, B: AbGroup
E: AbSES B A
abses_baer_sum (abses_pullback grp_homo_id E)
  (abses_pullback (- grp_homo_id) E) =
point (AbSES B A)
  refine ((baer_sum_distributive_pullbacks grp_homo_id (-grp_homo_id))^ @ _).H: Univalence
A, B: AbGroup
E: AbSES B A
abses_pullback (grp_homo_id - grp_homo_id) E =
point (AbSES B A)
  refine (ap (fun f => abses_pullback f _) (grp_inv_r (G := ab_hom _ _) _) @ _).H: Univalence
A, B: AbGroup
E: AbSES B A
abses_pullback 0 E = point (AbSES B A)
  symmetry; apply abses_pullback_const.
Defined.

(** The right inverse law follows by commutativity. *)
Definition baer_sum_inverse_r `{Univalence} {A B : AbGroup} (E : AbSES B A)
  : abses_baer_sum (abses_pullback (-grp_homo_id) E) E = point (AbSES B A)
  := baer_sum_commutative _ _ @ baer_sum_inverse_l _.

(** The Baer sum distributes over pushouts. *)
Lemma baer_sum_distributive_pushouts `{Univalence}
      {A A' B : AbGroup} {E : AbSES B A'} (f g : ab_hom A' A)
  : abses_pushout (f + g) E = abses_baer_sum (abses_pushout f E) (abses_pushout g E).H: Univalence
A, A', B: AbGroup
E: AbSES B A'
f, g: ab_hom A' A
abses_pushout (f + g) E =
abses_baer_sum (abses_pushout f E) (abses_pushout g E)
Proof.H: Univalence
A, A', B: AbGroup
E: AbSES B A'
f, g: ab_hom A' A
abses_pushout (f + g) E =
abses_baer_sum (abses_pushout f E) (abses_pushout g E)
  unfold abses_baer_sum.H: Univalence
A, A', B: AbGroup
E: AbSES B A'
f, g: ab_hom A' A
abses_pushout (f + g) E =
abses_pullback ab_diagonal
  (abses_pushout ab_codiagonal
     (abses_direct_sum (abses_pushout f E)
        (abses_pushout g E)))
  refine (abses_pushout_compose (A1 := ab_biprod A A) _ _ E @ _).H: Univalence
A, A', B: AbGroup
E: AbSES B A'
f, g: ab_hom A' A
abses_pushout ab_codiagonal
  (abses_pushout (grp_prod_corec f g) E) =
abses_pullback ab_diagonal
  (abses_pushout ab_codiagonal
     (abses_direct_sum (abses_pushout f E)
        (abses_pushout g E)))
  refine (_ @ abses_pushout_pullback_reorder _ _ _).H: Univalence
A, A', B: AbGroup
E: AbSES B A'
f, g: ab_hom A' A
abses_pushout ab_codiagonal
  (abses_pushout (grp_prod_corec f g) E) =
abses_pushout ab_codiagonal
  (abses_pullback ab_diagonal
     (abses_direct_sum (abses_pushout f E)
        (abses_pushout g E)))
  refine (ap (abses_pushout ab_codiagonal) _).H: Univalence
A, A', B: AbGroup
E: AbSES B A'
f, g: ab_hom A' A
abses_pushout (grp_prod_corec f g) E =
abses_pullback ab_diagonal
  (abses_direct_sum (abses_pushout f E)
     (abses_pushout g E))
  refine (ap (fun f => abses_pushout f E) (ab_biprod_corec_diagonal f g) @ _).H: Univalence
A, A', B: AbGroup
E: AbSES B A'
f, g: ab_hom A' A
abses_pushout (functor_ab_biprod f g $o ab_diagonal) E =
abses_pullback ab_diagonal
  (abses_direct_sum (abses_pushout f E)
     (abses_pushout g E))
  refine (abses_pushout_compose _ _ E @ _).H: Univalence
A, A', B: AbGroup
E: AbSES B A'
f, g: ab_hom A' A
abses_pushout (functor_ab_biprod f g)
  (abses_pushout ab_diagonal E) =
abses_pullback ab_diagonal
  (abses_direct_sum (abses_pushout f E)
     (abses_pushout g E))
  refine (ap (abses_pushout _) (abses_pushout_is_pullback (abses_diagonal E)) @ _).H: Univalence
A, A', B: AbGroup
E: AbSES B A'
f, g: ab_hom A' A
abses_pushout (functor_ab_biprod f g)
  (abses_pullback (component3 (abses_diagonal E))
     (abses_direct_sum E E)) =
abses_pullback ab_diagonal
  (abses_direct_sum (abses_pushout f E)
     (abses_pushout g E))
  refine (abses_pushout_pullback_reorder _ _ _ @ _).H: Univalence
A, A', B: AbGroup
E: AbSES B A'
f, g: ab_hom A' A
abses_pullback (component3 (abses_diagonal E))
  (abses_pushout (functor_ab_biprod f g)
     (abses_direct_sum E E)) =
abses_pullback ab_diagonal
  (abses_direct_sum (abses_pushout f E)
     (abses_pushout g E))
  exact (ap (abses_pullback _) (abses_directsum_distributive_pushouts f g)).
Defined.

(** Our next goal is to prove that the Baer sum is associative.  Rather than showing this directly, we first prove [baer_sum_twist], which says that [abses_baer_sum (abses_baer_sum E F) G = abses_baer_sum (abses_baer_sum G F) E].  The proof of this mimics the proof of commutativity above.  Then we prove associativity by combining this with commutativity. *)

(** The trinary Baer sum of three short exact sequences. *)
Definition abses_trinary_baer_sum `{Univalence}
  {A B : AbGroup@{u}} (E F G : AbSES B A)
  : AbSES B A
  := abses_pullback ab_triagonal
       (abses_pushout ab_cotriagonal
          (abses_direct_sum (abses_direct_sum E F) G)).

(** For [E, F, G : AbSES B A], the Baer sum of [E], [F] and [G] (associated left) is equal to the trinary Baer sum of [E], [F] and [G]. *)
Lemma baer_sum_is_trinary `{Univalence} {A B : AbGroup@{u}} (E F G : AbSES B A)
  : abses_baer_sum (abses_baer_sum E F) G = abses_trinary_baer_sum E F G.H: Univalence
A, B: AbGroup
E, F, G: AbSES B A
abses_baer_sum (abses_baer_sum E F) G =
abses_trinary_baer_sum E F G
Proof.H: Univalence
A, B: AbGroup
E, F, G: AbSES B A
abses_baer_sum (abses_baer_sum E F) G =
abses_trinary_baer_sum E F G
  unfold abses_baer_sum, abses_trinary_baer_sum, ab_triagonal, ab_cotriagonal.H: Univalence
A, B: AbGroup
E, F, G: AbSES B A
abses_pullback ab_diagonal
  (abses_pushout ab_codiagonal
     (abses_direct_sum
        (abses_pullback ab_diagonal
           (abses_pushout ab_codiagonal
              (abses_direct_sum E F))) G)) =
abses_pullback
  (functor_ab_biprod ab_diagonal grp_homo_id $o
   ab_diagonal)
  (abses_pushout
     (ab_codiagonal $o
      functor_ab_biprod ab_codiagonal grp_homo_id)
     (abses_direct_sum (abses_direct_sum E F) G))
  refine (ap (abses_pullback _ o abses_pushout _) _^ @ _).H: Univalence
A, B: AbGroup
E, F, G: AbSES B A
?Goal =
abses_direct_sum
  (abses_pullback ab_diagonal
     (abses_pushout ab_codiagonal
        (abses_direct_sum E F))) G
H: Univalence
A, B: AbGroup
E, F, G: AbSES B A
abses_pullback ab_diagonal
  (abses_pushout ab_codiagonal ?Goal) =
abses_pullback
  (functor_ab_biprod ab_diagonal grp_homo_id $o
   ab_diagonal)
  (abses_pushout
     (ab_codiagonal $o
      functor_ab_biprod ab_codiagonal grp_homo_id)
     (abses_direct_sum (abses_direct_sum E F) G))
  -H: Univalence
A, B: AbGroup
E, F, G: AbSES B A
?Goal =
abses_direct_sum
  (abses_pullback ab_diagonal
     (abses_pushout ab_codiagonal
        (abses_direct_sum E F))) G refine (_ @ ap (abses_direct_sum _) (abses_pullback_id G)).H: Univalence
A, B: AbGroup
E, F, G: AbSES B A
?Goal =
abses_direct_sum
  (abses_pullback ab_diagonal
     (abses_pushout ab_codiagonal
        (abses_direct_sum E F)))
  (abses_pullback grp_homo_id G)
    refine (_ @ abses_directsum_distributive_pullbacks _ _).H: Univalence
A, B: AbGroup
E, F, G: AbSES B A
?Goal =
abses_pullback
  (functor_ab_biprod ab_diagonal grp_homo_id)
  (abses_direct_sum
     (abses_pushout ab_codiagonal
        (abses_direct_sum E F)) G)
    refine (ap (abses_pullback _) _).H: Univalence
A, B: AbGroup
E, F, G: AbSES B A
?Goal0 =
abses_direct_sum
  (abses_pushout ab_codiagonal (abses_direct_sum E F))
  G
    refine (_ @ ap (abses_direct_sum _) (abses_pushout_id G)).H: Univalence
A, B: AbGroup
E, F, G: AbSES B A
?Goal0 =
abses_direct_sum
  (abses_pushout ab_codiagonal (abses_direct_sum E F))
  (abses_pushout grp_homo_id G)
    apply abses_directsum_distributive_pushouts.
  -H: Univalence
A, B: AbGroup
E, F, G: AbSES B A
abses_pullback ab_diagonal
  (abses_pushout ab_codiagonal
     (abses_pullback
        (functor_ab_biprod ab_diagonal grp_homo_id)
        (abses_pushout
           (functor_ab_biprod ab_codiagonal
              grp_homo_id)
           (abses_direct_sum (abses_direct_sum E F) G)))) =
abses_pullback
  (functor_ab_biprod ab_diagonal grp_homo_id $o
   ab_diagonal)
  (abses_pushout
     (ab_codiagonal $o
      functor_ab_biprod ab_codiagonal grp_homo_id)
     (abses_direct_sum (abses_direct_sum E F) G)) refine (ap (abses_pullback _) (abses_pushout_pullback_reorder _ _ _) @ _).H: Univalence
A, B: AbGroup
E, F, G: AbSES B A
abses_pullback ab_diagonal
  (abses_pullback
     (functor_ab_biprod ab_diagonal grp_homo_id)
     (abses_pushout ab_codiagonal
        (abses_pushout
           (functor_ab_biprod ab_codiagonal
              grp_homo_id)
           (abses_direct_sum (abses_direct_sum E F) G)))) =
abses_pullback
  (functor_ab_biprod ab_diagonal grp_homo_id $o
   ab_diagonal)
  (abses_pushout
     (ab_codiagonal $o
      functor_ab_biprod ab_codiagonal grp_homo_id)
     (abses_direct_sum (abses_direct_sum E F) G))
    refine (abses_pullback_compose _ _ _ @ _).H: Univalence
A, B: AbGroup
E, F, G: AbSES B A
abses_pullback
  (functor_ab_biprod ab_diagonal grp_homo_id $o
   ab_diagonal)
  (abses_pushout ab_codiagonal
     (abses_pushout
        (functor_ab_biprod ab_codiagonal grp_homo_id)
        (abses_direct_sum (abses_direct_sum E F) G))) =
abses_pullback
  (functor_ab_biprod ab_diagonal grp_homo_id $o
   ab_diagonal)
  (abses_pushout
     (ab_codiagonal $o
      functor_ab_biprod ab_codiagonal grp_homo_id)
     (abses_direct_sum (abses_direct_sum E F) G))
    refine (ap (abses_pullback _) _^).H: Univalence
A, B: AbGroup
E, F, G: AbSES B A
abses_pushout
  (ab_codiagonal $o
   functor_ab_biprod ab_codiagonal grp_homo_id)
  (abses_direct_sum (abses_direct_sum E F) G) =
abses_pushout ab_codiagonal
  (abses_pushout
     (functor_ab_biprod ab_codiagonal grp_homo_id)
     (abses_direct_sum (abses_direct_sum E F) G))
    apply abses_pushout_compose.
Defined.

(** For [E, F, G : AbSES B A], we can "twist" the order of the trinary Baer sum as follows. *)
Lemma twist_trinary_baer_sum `{Univalence}
  {A B : AbGroup@{u}} (E F G : AbSES B A)
  : abses_trinary_baer_sum E F G = abses_trinary_baer_sum G F E.H: Univalence
A, B: AbGroup
E, F, G: AbSES B A
abses_trinary_baer_sum E F G =
abses_trinary_baer_sum G F E
Proof.H: Univalence
A, B: AbGroup
E, F, G: AbSES B A
abses_trinary_baer_sum E F G =
abses_trinary_baer_sum G F E
  unfold abses_trinary_baer_sum.H: Univalence
A, B: AbGroup
E, F, G: AbSES B A
abses_pullback ab_triagonal
  (abses_pushout ab_cotriagonal
     (abses_direct_sum (abses_direct_sum E F) G)) =
abses_pullback ab_triagonal
  (abses_pushout ab_cotriagonal
     (abses_direct_sum (abses_direct_sum G F) E))
  (* The next line uses the fact that [ab_triagonal] is definitionally equal to [ab_biprod_twist $o ab_triagonal]: *)
  refine (_ @ abses_pullback_compose ab_triagonal ab_biprod_twist _).H: Univalence
A, B: AbGroup
E, F, G: AbSES B A
abses_pullback ab_triagonal
  (abses_pushout ab_cotriagonal
     (abses_direct_sum (abses_direct_sum E F) G)) =
abses_pullback ab_triagonal
  (abses_pullback ab_biprod_twist
     (abses_pushout ab_cotriagonal
        (abses_direct_sum (abses_direct_sum G F) E)))
  refine (ap (abses_pullback _) _).H: Univalence
A, B: AbGroup
E, F, G: AbSES B A
abses_pushout ab_cotriagonal
  (abses_direct_sum (abses_direct_sum E F) G) =
abses_pullback ab_biprod_twist
  (abses_pushout ab_cotriagonal
     (abses_direct_sum (abses_direct_sum G F) E))
  refine (ap (fun f => abses_pushout f _) ab_cotriagonal_twist^ @ _).H: Univalence
A, B: AbGroup
E, F, G: AbSES B A
abses_pushout (ab_cotriagonal $o ab_biprod_twist)
  (abses_direct_sum (abses_direct_sum E F) G) =
abses_pullback ab_biprod_twist
  (abses_pushout ab_cotriagonal
     (abses_direct_sum (abses_direct_sum G F) E))
  refine (abses_pushout_compose _ _ _ @ _).H: Univalence
A, B: AbGroup
E, F, G: AbSES B A
abses_pushout ab_cotriagonal
  (abses_pushout ab_biprod_twist
     (abses_direct_sum (abses_direct_sum E F) G)) =
abses_pullback ab_biprod_twist
  (abses_pushout ab_cotriagonal
     (abses_direct_sum (abses_direct_sum G F) E))
  refine (ap _ (abses_pushout_is_pullback (abses_twist_directsum E F G)) @ _).H: Univalence
A, B: AbGroup
E, F, G: AbSES B A
abses_pushout ab_cotriagonal
  (abses_pullback
     (component3 (abses_twist_directsum E F G))
     (abses_direct_sum (abses_direct_sum G F) E)) =
abses_pullback ab_biprod_twist
  (abses_pushout ab_cotriagonal
     (abses_direct_sum (abses_direct_sum G F) E))
  unfold abses_twist_directsum, component3.H: Univalence
A, B: AbGroup
E, F, G: AbSES B A
abses_pushout ab_cotriagonal
  (abses_pullback ab_biprod_twist
     (abses_direct_sum (abses_direct_sum G F) E)) =
abses_pullback ab_biprod_twist
  (abses_pushout ab_cotriagonal
     (abses_direct_sum (abses_direct_sum G F) E))
  exact (abses_pushout_pullback_reorder _ _ _).
Defined.

(** It now follows that we can twist the order of the summands in the Baer sum. *)
Lemma baer_sum_twist `{Univalence} {A B : AbGroup@{u}} (E F G : AbSES B A)
  : abses_baer_sum (abses_baer_sum E F) G = abses_baer_sum (abses_baer_sum G F) E.H: Univalence
A, B: AbGroup
E, F, G: AbSES B A
abses_baer_sum (abses_baer_sum E F) G =
abses_baer_sum (abses_baer_sum G F) E
Proof.H: Univalence
A, B: AbGroup
E, F, G: AbSES B A
abses_baer_sum (abses_baer_sum E F) G =
abses_baer_sum (abses_baer_sum G F) E
  refine ((baer_sum_is_trinary E F G) @ _ @ (baer_sum_is_trinary G F E)^).H: Univalence
A, B: AbGroup
E, F, G: AbSES B A
abses_trinary_baer_sum E F G =
abses_trinary_baer_sum G F E
  apply twist_trinary_baer_sum.
Defined.

(** From these results, it finally follows that the Baer sum is associative. *)
Lemma baer_sum_associative `{Univalence}
  {A B : AbGroup@{u}} (E F G : AbSES B A)
  : abses_baer_sum (abses_baer_sum E F) G = abses_baer_sum E (abses_baer_sum F G).H: Univalence
A, B: AbGroup
E, F, G: AbSES B A
abses_baer_sum (abses_baer_sum E F) G =
abses_baer_sum E (abses_baer_sum F G)
Proof.H: Univalence
A, B: AbGroup
E, F, G: AbSES B A
abses_baer_sum (abses_baer_sum E F) G =
abses_baer_sum E (abses_baer_sum F G)
  refine ((baer_sum_twist _ _ _)^ @ _).H: Univalence
A, B: AbGroup
E, F, G: AbSES B A
abses_baer_sum (abses_baer_sum G F) E =
abses_baer_sum E (abses_baer_sum F G)
  refine (baer_sum_commutative _ _ @ _).H: Univalence
A, B: AbGroup
E, F, G: AbSES B A
abses_baer_sum E (abses_baer_sum G F) =
abses_baer_sum E (abses_baer_sum F G)
  apply ap.H: Univalence
A, B: AbGroup
E, F, G: AbSES B A
abses_baer_sum G F = abses_baer_sum F G
  apply baer_sum_commutative.
Defined.

(** The Baer sum makes [AbSES B A] into an H-space. (In fact, a coherent H-space, but we leave that for now.) *)
Instance ishspace_abses `{Univalence} {B A : AbGroup}
  : IsHSpace (AbSES B A).H: Univalence
B, A: AbGroup
IsHSpace (AbSES B A)
Proof.H: Univalence
B, A: AbGroup
IsHSpace (AbSES B A)
  snapply Build_IsHSpace.H: Univalence
B, A: AbGroup
SgOp (AbSES B A)
H: Univalence
B, A: AbGroup
LeftIdentity ?hspace_op (point (AbSES B A))
H: Univalence
B, A: AbGroup
RightIdentity ?hspace_op (point (AbSES B A))
  -H: Univalence
B, A: AbGroup
SgOp (AbSES B A) exact abses_baer_sum.
  -H: Univalence
B, A: AbGroup
LeftIdentity abses_baer_sum (point (AbSES B A)) intro; apply baer_sum_unit_l.
  -H: Univalence
B, A: AbGroup
RightIdentity abses_baer_sum (point (AbSES B A)) intro; apply baer_sum_unit_r.
Defined.

Instance is0bifunctor_abses `{Univalence}
  : Is0Bifunctor (AbSES : AbGroup^op -> AbGroup -> pType)
  := Build_Is0Bifunctor'' _.

Instance is1bifunctor_abses `{Univalence}
  : Is1Bifunctor (AbSES : AbGroup^op -> AbGroup -> pType).H: Univalence
Is1Bifunctor (AbSES : AbGroup^op -> AbGroup -> pType)
Proof.H: Univalence
Is1Bifunctor (AbSES : AbGroup^op -> AbGroup -> pType)
  snapply Build_Is1Bifunctor''.H: Univalence
forall a : AbGroup^op, Is1Functor (AbSES a)
H: Univalence
forall b : AbGroup, Is1Functor (flip AbSES b)
H: Univalence
forall (a0 a1 : AbGroup^op) (f : a0 $-> a1)
(b0 b1 : AbGroup) (g : b0 $-> b1),
fmap01 AbSES a1 g $o fmap10 AbSES f b0 $==
fmap10 AbSES f b1 $o fmap01 AbSES a0 g
  1,2: exact _.H: Univalence
forall (a0 a1 : AbGroup^op) (f : a0 $-> a1)
(b0 b1 : AbGroup) (g : b0 $-> b1),
fmap01 AbSES a1 g $o fmap10 AbSES f b0 $==
fmap10 AbSES f b1 $o fmap01 AbSES a0 g
  intros ? ? f ? ? g.H: Univalence
a0, a1: AbGroup^op
f: a0 $-> a1
b0, b1: AbGroup
g: b0 $-> b1
fmap01 AbSES a1 g $o fmap10 AbSES f b0 $==
fmap10 AbSES f b1 $o fmap01 AbSES a0 g
  rapply hspace_phomotopy_from_homotopy.H: Univalence
a0, a1: AbGroup^op
f: a0 $-> a1
b0, b1: AbGroup
g: b0 $-> b1
IsHSpace (AbSES a1 b1)
H: Univalence
a0, a1: AbGroup^op
f: a0 $-> a1
b0, b1: AbGroup
g: b0 $-> b1
fmap01 AbSES a1 g $o fmap10 AbSES f b0 ==
fmap10 AbSES f b1 $o fmap01 AbSES a0 g
  1: exact ishspace_abses.H: Univalence
a0, a1: AbGroup^op
f: a0 $-> a1
b0, b1: AbGroup
g: b0 $-> b1
fmap01 AbSES a1 g $o fmap10 AbSES f b0 ==
fmap10 AbSES f b1 $o fmap01 AbSES a0 g
  intro E; cbn.H: Univalence
a0, a1: AbGroup^op
f: a0 $-> a1
b0, b1: AbGroup
g: b0 $-> b1
E: AbSES a0 b0
abses_pushout g (abses_pullback f E) =
abses_pullback f (abses_pushout g E)
  apply abses_pushout_pullback_reorder.
Defined.

(** ** Pushouts and pullbacks respect the Baer sum *)

Definition baer_sum_pushout `{Univalence}
  {A A' B : AbGroup} (f : A $-> A') (E F : AbSES B A)
  : abses_pushout f (abses_baer_sum E F)
    = abses_baer_sum (abses_pushout f E) (abses_pushout f F).H: Univalence
A, A', B: AbGroup
f: A $-> A'
E, F: AbSES B A
abses_pushout f (abses_baer_sum E F) =
abses_baer_sum (abses_pushout f E) (abses_pushout f F)
Proof.H: Univalence
A, A', B: AbGroup
f: A $-> A'
E, F: AbSES B A
abses_pushout f (abses_baer_sum E F) =
abses_baer_sum (abses_pushout f E) (abses_pushout f F)
  unfold abses_baer_sum.H: Univalence
A, A', B: AbGroup
f: A $-> A'
E, F: AbSES B A
abses_pushout f
  (abses_pullback ab_diagonal
     (abses_pushout ab_codiagonal
        (abses_direct_sum E F))) =
abses_pullback ab_diagonal
  (abses_pushout ab_codiagonal
     (abses_direct_sum (abses_pushout f E)
        (abses_pushout f F)))
  refine (abses_pushout_pullback_reorder _ _ _
            @ ap _ _).H: Univalence
A, A', B: AbGroup
f: A $-> A'
E, F: AbSES B A
abses_pushout f
  (abses_pushout ab_codiagonal (abses_direct_sum E F)) =
abses_pushout ab_codiagonal
  (abses_direct_sum (abses_pushout f E)
     (abses_pushout f F))
  refine ((abses_pushout_compose _ _ _)^ @ _).H: Univalence
A, A', B: AbGroup
f: A $-> A'
E, F: AbSES B A
abses_pushout (f $o ab_codiagonal)
  (abses_direct_sum E F) =
abses_pushout ab_codiagonal
  (abses_direct_sum (abses_pushout f E)
     (abses_pushout f F))
  refine (abses_pushout_homotopic _ _ _ _ @ _).H: Univalence
A, A', B: AbGroup
f: A $-> A'
E, F: AbSES B A
f $o ab_codiagonal == ?Goal
H: Univalence
A, A', B: AbGroup
f: A $-> A'
E, F: AbSES B A
abses_pushout ?Goal (abses_direct_sum E F) =
abses_pushout ab_codiagonal
  (abses_direct_sum (abses_pushout f E)
     (abses_pushout f F))
  1: apply ab_codiagonal_natural.H: Univalence
A, A', B: AbGroup
f: A $-> A'
E, F: AbSES B A
abses_pushout (ab_codiagonal $o functor_ab_biprod f f)
  (abses_direct_sum E F) =
abses_pushout ab_codiagonal
  (abses_direct_sum (abses_pushout f E)
     (abses_pushout f F))
  refine (abses_pushout_compose _ _ _ @ ap _ _).H: Univalence
A, A', B: AbGroup
f: A $-> A'
E, F: AbSES B A
abses_pushout (functor_ab_biprod f f)
  (abses_direct_sum E F) =
abses_direct_sum (abses_pushout f E)
  (abses_pushout f F)
  apply abses_directsum_distributive_pushouts.
Defined.

Definition baer_sum_pullback `{Univalence}
  {A B B' : AbGroup} (f : B' $-> B) (E F : AbSES B A)
  : abses_pullback f (abses_baer_sum E F)
    = abses_baer_sum (abses_pullback f E) (abses_pullback f F).H: Univalence
A, B, B': AbGroup
f: B' $-> B
E, F: AbSES B A
abses_pullback f (abses_baer_sum E F) =
abses_baer_sum (abses_pullback f E)
  (abses_pullback f F)
Proof.H: Univalence
A, B, B': AbGroup
f: B' $-> B
E, F: AbSES B A
abses_pullback f (abses_baer_sum E F) =
abses_baer_sum (abses_pullback f E)
  (abses_pullback f F)
  unfold abses_baer_sum.H: Univalence
A, B, B': AbGroup
f: B' $-> B
E, F: AbSES B A
abses_pullback f
  (abses_pullback ab_diagonal
     (abses_pushout ab_codiagonal
        (abses_direct_sum E F))) =
abses_pullback ab_diagonal
  (abses_pushout ab_codiagonal
     (abses_direct_sum (abses_pullback f E)
        (abses_pullback f F)))
  refine (abses_pullback_compose _ _ _ @ _).H: Univalence
A, B, B': AbGroup
f: B' $-> B
E, F: AbSES B A
abses_pullback (ab_diagonal $o f)
  (abses_pushout ab_codiagonal (abses_direct_sum E F)) =
abses_pullback ab_diagonal
  (abses_pushout ab_codiagonal
     (abses_direct_sum (abses_pullback f E)
        (abses_pullback f F)))
  refine ((abses_pushout_pullback_reorder _ _ _)^
            @ ap _ _
              @ abses_pushout_pullback_reorder _ _ _).H: Univalence
A, B, B': AbGroup
f: B' $-> B
E, F: AbSES B A
abses_pullback (ab_diagonal $o f)
  (abses_direct_sum E F) =
abses_pullback ab_diagonal
  (abses_direct_sum (abses_pullback f E)
     (abses_pullback f F))
  refine (abses_pullback_homotopic
            _ (functor_ab_biprod f f $o ab_diagonal) _ _ @ _).H: Univalence
A, B, B': AbGroup
f: B' $-> B
E, F: AbSES B A
ab_diagonal $o f ==
functor_ab_biprod f f $o ab_diagonal
H: Univalence
A, B, B': AbGroup
f: B' $-> B
E, F: AbSES B A
abses_pullback (functor_ab_biprod f f $o ab_diagonal)
  (abses_direct_sum E F) =
abses_pullback ab_diagonal
  (abses_direct_sum (abses_pullback f E)
     (abses_pullback f F))
  1: reflexivity.H: Univalence
A, B, B': AbGroup
f: B' $-> B
E, F: AbSES B A
abses_pullback (functor_ab_biprod f f $o ab_diagonal)
  (abses_direct_sum E F) =
abses_pullback ab_diagonal
  (abses_direct_sum (abses_pullback f E)
     (abses_pullback f F))
  refine ((abses_pullback_compose _ _ _)^ @ ap _ _).H: Univalence
A, B, B': AbGroup
f: B' $-> B
E, F: AbSES B A
abses_pullback (functor_ab_biprod f f)
  (abses_direct_sum E F) =
abses_direct_sum (abses_pullback f E)
  (abses_pullback f F)
  apply abses_directsum_distributive_pullbacks.
Defined.