Direct definition of binary direct sum using preadditive categories.

Contents

• Definition of binary direct sums (also known as biproducts)
• Criteria for binary direct sums
• Quotient has binary direct sums
BinDirectSum is at the same time product and coproduct of the underlying objects together with the following equalities
i1 · p1 = identity and i2 · p2 = identity i1 · p2 = unit and i2 · p1 = unit p1 · i1 + p2 · i2 = identity

Lemma rewrite_op {A:PreAdditive} (x y:A) :
@to_binop (categoryWithAbgrops_precategoryWithBinOps (PreAdditive_categoryWithAbgrops A)) x y
=
@op (pr1monoid (grtomonoid (abgrtogr (@to_abgr (PreAdditive_categoryWithAbgrops A) x y)))).
Proof.
reflexivity.
Defined.

Section def_bindirectsums.

Context (hs := @to_has_homsets A : has_homsets A).

Open Scope abgrcat.

Definition of binary direct sum.
Definition isBinDirectSum (a b co : A) (i1 : a --> co) (i2 : b --> co)
(p1 : co --> a) (p2 : co --> b) : hProp :=
i1 · p1 = 1 i2 · p2 = 1
i1 · p2 = 0 i2 · p1 = 0
p1 · i1 + p2 · i2 = 1.

Definition to_isBinCoproduct {a b co : A} {i1 : a --> co} {i2 : b --> co}
{p1 : co --> a} {p2 : co --> b} :
isBinDirectSum a b co i1 i2 p1 p2 isBinCoproduct A a b co i1 i2.
Proof.
intros [e11 [e22 [e12 [e21 e]]]].
intros T f g.
use unique_exists.
- exact ((p1 · f) + (p2 · g)).
- cbn beta. split.
+
assert (q := to_premor_linear' i1 (p1 · f) (p2 · g)).
rewrite 2 rewrite_op in q. rewrite q. clear q.
rewrite 2 assoc. rewrite e11. rewrite id_left.
rewrite e12. rewrite to_postmor_unel'. rewrite runax.
reflexivity.
+ assert (q := to_premor_linear' i2 (p1 · f) (p2 · g)).
rewrite 2 rewrite_op in q. rewrite q. clear q.
rewrite 2 assoc. rewrite e22. rewrite id_left.
rewrite e21. rewrite to_postmor_unel'. rewrite lunax.
reflexivity.
- intros h. cbn beta. apply isapropdirprod;apply hs.
- intros h. cbn beta. intros [p q]. rewrite <- p, <- q.
rewrite 2 assoc.
assert (Q := to_postmor_linear' (p1 · i1) (p2 · i2) h).
rewrite 2 rewrite_op in Q. rewrite <- Q.
rewrite e. rewrite id_left. reflexivity.
Defined.

Definition to_isBinProduct {a b co : A} {i1 : a --> co} {i2 : b --> co}
{p1 : co --> a} {p2 : co --> b} :
isBinDirectSum a b co i1 i2 p1 p2 isBinProduct A a b co p1 p2.
Proof.
intros [e11 [e22 [e12 [e21 e]]]].
intros T f g.
use unique_exists.
- exact ((f · i1) + (g · i2)).
- cbn beta. split.
+ assert (q := to_postmor_linear' (f · i1) (g · i2) p1).
rewrite 2 rewrite_op in q. rewrite q. clear q.
rewrite <- 2 assoc. rewrite e11. rewrite id_right.
rewrite e21. rewrite to_premor_unel'. rewrite runax.
reflexivity.
+ assert (q := to_postmor_linear' (f · i1) (g · i2) p2).
rewrite 2 rewrite_op in q. rewrite q. clear q.
rewrite <- 2 assoc. rewrite e22. rewrite id_right.
rewrite e12. rewrite to_premor_unel'. rewrite lunax.
reflexivity.
- intros h. cbn beta. apply isapropdirprod;apply hs.
- intros h. cbn beta. intros [p q]. rewrite <- p, <- q.
rewrite <- 2 assoc.
assert (Q := to_premor_linear' h (p1 · i1) (p2 · i2)).
rewrite 2 rewrite_op in Q. rewrite <- Q.
rewrite e. rewrite id_right. reflexivity.
Defined.

Definition to_IdIn1 {a b co : A} {i1 : a --> co} {i2 : b --> co} {p1 : co --> a} {p2 : co --> b}
(B : isBinDirectSum a b co i1 i2 p1 p2) :
i1 · p1 = identity a := pr1 B.

Definition to_IdIn2 {a b co : A} {i1 : a --> co} {i2 : b --> co} {p1 : co --> a} {p2 : co --> b}
(B : isBinDirectSum a b co i1 i2 p1 p2) :
i2 · p2 = identity b := pr12 B.

Definition to_Unel1 {a b co : A} {i1 : a --> co} {i2 : b --> co} {p1 : co --> a} {p2 : co --> b}
(B : isBinDirectSum a b co i1 i2 p1 p2) :
i1 · p2 = (to_unel a b) := pr122 B.

Definition to_Unel2 {a b co : A} {i1 : a --> co} {i2 : b --> co} {p1 : co --> a} {p2 : co --> b}
(B : isBinDirectSum a b co i1 i2 p1 p2) :
i2 · p1 = (to_unel b a) := pr122 (pr2 B).

Definition to_BinOpId {a b co : A} {i1 : a --> co} {i2 : b --> co} {p1 : co --> a} {p2 : co --> b}
(B : isBinDirectSum a b co i1 i2 p1 p2) :
(to_binop co co) (p1 · i1) (p2 · i2) = identity co := pr222 (pr2 B).

The following definition constructs isBinDirectSum from data.
Definition make_isBinDirectSum (a b co : A)
(i1 : a --> co) (i2 : b --> co) (p1 : co --> a) (p2 : co --> b)
(H1 : i1 · p1 = identity a) (H2 : i2 · p2 = identity b)
(H3 : i1 · p2 = (to_unel a b)) (H4 : i2 · p1 = (to_unel b a))
(H5 : (to_binop co co) (p1 · i1) (p2 · i2) = identity co)
: isBinDirectSum a b co i1 i2 p1 p2 := H1,,H2,,H3,,H4,,H5.

Definition of BinDirectSums.
Definition BinDirectSum (a b : A) : UU :=
coab : ( co : A, a --> co × b --> co × co --> a × co --> b),
isBinDirectSum a b (pr1 coab) (pr1 (pr2 coab)) (pr1 (pr2 (pr2 coab)))
(pr1 (pr2 (pr2 (pr2 coab)))) (pr2 (pr2 (pr2 (pr2 coab)))).

Construction of BinDirectSum.
Definition make_BinDirectSum (a b co : A) (i1 : a --> co) (i2 : b --> co)
(p1 : co --> a) (p2 : co --> b) (H : isBinDirectSum a b co i1 i2 p1 p2) :
BinDirectSum a b := tpair _ (tpair _ co (i1,,(i2,,(p1,,p2)))) H.

BinDirectSum in categories.
Definition BinDirectSums : UU := (a b : A), BinDirectSum a b.

Definition make_BinDirectSums (H : (a b : A), BinDirectSum a b) : BinDirectSums := H.

Definition hasBinDirectSums : hProp.
Proof.
( (a b : A), BinDirectSum a b ).
apply impred; intro p.
apply impred; intro q.
apply isapropishinh.
Defined.

The direct sum object.
Definition BinDirectSumOb {a b : A} (B : BinDirectSum a b) : A := pr1 (pr1 B).
Coercion BinDirectSumOb : BinDirectSum >-> ob.

Accessor functions
Definition to_In1 {a b : A} (B : BinDirectSum a b) : Aa, B := dirprod_pr1 (pr2 (pr1 B)).

Definition to_In2 {a b : A} (B : BinDirectSum a b) : Ab, B :=
dirprod_pr1 (dirprod_pr2 (pr2 (pr1 B))).

Definition to_Pr1 {a b : A} (B : BinDirectSum a b) : AB, a :=
dirprod_pr1 (dirprod_pr2 (dirprod_pr2 (pr2 (pr1 B)))).

Definition to_Pr2 {a b : A} (B : BinDirectSum a b) : AB, b :=
dirprod_pr2 (dirprod_pr2 (dirprod_pr2 (pr2 (pr1 B)))).

Another coercion
Construction of BinCoproduct and BinProduct from BinDirectSum.
Definition BinDirectSum_BinCoproduct {a b : A} (B : BinDirectSum a b) :
BinCoproduct A a b.
Proof.
use (make_BinCoproduct A a b B (to_In1 B) (to_In2 B)).
exact (to_isBinCoproduct B).
Defined.

Definition BinDirectSum_BinProduct {a b : A} (B : BinDirectSum a b) : BinProduct A a b.
Proof.
use (make_BinProduct A a b B (to_Pr1 B) (to_Pr2 B)).
exact (to_isBinProduct B).
Defined.

An arrow to BinDirectSum and arrow from BinDirectSum.
Definition ToBinDirectSum {a b : A} (B : BinDirectSum a b) {c : A} (f : c --> a)
(g : c --> b) : Ac, B := BinProductArrow A (BinDirectSum_BinProduct B) f g.

Definition FromBinDirectSum {a b : A} (B : BinDirectSum a b) {c : A} (f : a --> c)
(g : b --> c) : AB, c := BinCoproductArrow A (BinDirectSum_BinCoproduct B) f g.

Commutativity of BinDirectSum.
Definition BinDirectSumIn1Commutes {a b : A} (B : BinDirectSum a b) :
(c : A) (f : a --> c) (g : b --> c), (to_In1 B) · (FromBinDirectSum B f g) = f.
Proof.
intros c f g.
apply (BinCoproductIn1Commutes A a b (BinDirectSum_BinCoproduct B) c f g).
Qed.

Definition BinDirectSumIn2Commutes {a b : A} (B : BinDirectSum a b) :
(c : A) (f : a --> c) (g : b --> c), (to_In2 B) · (FromBinDirectSum B f g) = g.
Proof.
intros c f g.
apply (BinCoproductIn2Commutes A a b (BinDirectSum_BinCoproduct B) c f g).
Qed.

Definition BinDirectSumPr1Commutes {a b : A} (B : BinDirectSum a b) :
(c : A) (f : c --> a) (g : c --> b), (ToBinDirectSum B f g) · (to_Pr1 B) = f.
Proof.
intros c f g.
apply (BinProductPr1Commutes A a b (BinDirectSum_BinProduct B) c f g).
Qed.

Definition BinDirectSumPr2Commutes {a b : A} (B : BinDirectSum a b) :
(c : A) (f : c --> a) (g : c --> b), (ToBinDirectSum B f g) · (to_Pr2 B) = g.
Proof.
intros c f g.
apply (BinProductPr2Commutes A a b (BinDirectSum_BinProduct B) c f g).
Qed.

Uniqueness of arrow to and from BinDirectSum using the BinProduct and BinCoproduct structures.
Definition ToBinDirectSumUnique {a b : A} (B : BinDirectSum a b) {c : A} (f : c --> a)
(g : c --> b) (k : c --> B) :
k · to_Pr1 B = f k · to_Pr2 B = g k = ToBinDirectSum B f g :=
BinProductArrowUnique _ _ _ (BinDirectSum_BinProduct B) c f g k.

Definition FromBinDirectSumUnique {a b : A} (B : BinDirectSum a b) {c : A} (f : a --> c)
(g : b --> c) (k : B --> c) :
to_In1 B · k = f to_In2 B · k = g k = FromBinDirectSum B f g :=
BinCoproductArrowUnique _ _ _ (BinDirectSum_BinCoproduct B) c f g k.

Uniqueness of arrows to and from BinDirectSum
Lemma ToBinDirectSumsEq {c d : A} (DS : BinDirectSum c d) {x : A} (k1 k2 : x --> DS) :
k1 · to_Pr1 DS = k2 · to_Pr1 DS
k1 · to_Pr2 DS = k2 · to_Pr2 DS k1 = k2.
Proof.
intros H1 H2.
rewrite (ToBinDirectSumUnique DS (k1 · to_Pr1 DS) (k1 · to_Pr2 DS) k1).
apply pathsinv0.
apply ToBinDirectSumUnique.
- apply pathsinv0. apply H1.
- apply pathsinv0. apply H2.
- apply idpath.
- apply idpath.
Qed.

Lemma FromBinDirectSumsEq {c d : A} (DS : BinDirectSum c d) {x : A} (k1 k2 : DS --> x) :
to_In1 DS · k1 = to_In1 DS · k2 to_In2 DS · k1 = to_In2 DS · k2 k1 = k2.
Proof.
intros H1 H2.
rewrite (FromBinDirectSumUnique DS (to_In1 DS · k1) (to_In2 DS · k1) k1).
apply pathsinv0.
apply FromBinDirectSumUnique.
- apply pathsinv0. apply H1.
- apply pathsinv0. apply H2.
- apply idpath.
- apply idpath.
Qed.

The following definitions give a formula for the unique morphisms to and from the BinDirectSum. These formulas are important when one uses bindirectsums. The formulas are
to bindirectsum unique arrow = f · in1 + g · in2 from bindirectsum unique arrow = pr1 · f + pr2 · g
Definition ToBinDirectSumFormula {a b : A} (B : BinDirectSum a b) {c : A} (f : c --> a)
(g : c --> b) : Ac, B := (to_binop c B) (f · to_In1 B) (g · to_In2 B).

Definition FromBinDirectSumFormula {a b : A} (B : BinDirectSum a b) {c : A} (f : a --> c)
(g : b --> c) : AB, c := (to_binop B c) (to_Pr1 B · f) (to_Pr2 B · g).

Let us prove that these formulas indeed are the unique morphisms we claimed them to be.
Lemma ToBinDirectSumFormulaUnique {a b : A} (B : BinDirectSum a b) {c : A} (f : c --> a)
(g : c --> b) : ToBinDirectSumFormula B f g = ToBinDirectSum B f g.
Proof.
apply ToBinDirectSumUnique.
- unfold ToBinDirectSumFormula.
unfold to_binop.
use (pathscomp0 (to_postmor_linear c (to_Pr1 B) (f · to_In1 B) (g · to_In2 B))).
unfold to_postmor. repeat rewrite <- assoc.
rewrite (to_IdIn1 B).
rewrite id_right.
rewrite (to_Unel2 B).
set (XX := to_premor_unel A a g).
unfold to_premor in XX.
unfold to_unel.
rewrite XX.
apply (to_runax c a).
- unfold ToBinDirectSumFormula.
unfold to_binop. cbn.
use (pathscomp0 (to_postmor_linear c (to_Pr2 B) (f · to_In1 B) (g · to_In2 B))).
unfold to_postmor. repeat rewrite <- assoc.
rewrite (to_IdIn2 B). rewrite (to_Unel1 B). rewrite id_right.
set (XX := to_premor_unel A b f).
unfold PrecategoriesWithAbgrops.to_premor in XX.
unfold PrecategoriesWithAbgrops.to_unel.
rewrite XX. clear XX.
apply (to_lunax c b).
Qed.

Lemma FromBinDirectSumFormulaUnique {a b : A} (B : BinDirectSum a b) {c : A} (f : a --> c)
(g : b --> c) : FromBinDirectSumFormula B f g = FromBinDirectSum B f g.
Proof.
unfold FromBinDirectSumFormula.
apply FromBinDirectSumUnique.
- use (pathscomp0 (to_premor_linear c (to_In1 B) (to_Pr1 B · f) (to_Pr2 B · g))).
unfold to_premor. repeat rewrite assoc.
rewrite (to_IdIn1 B). rewrite (to_Unel1 B). rewrite id_left.
set (XX := to_postmor_unel A a g).
unfold to_postmor in XX.
unfold to_unel.
rewrite XX.
apply (to_runax a c).
- use (pathscomp0 (to_premor_linear c (to_In2 B) (to_Pr1 B · f) (to_Pr2 B · g))).
unfold to_premor. repeat rewrite assoc.
rewrite (to_IdIn2 B). rewrite (to_Unel2 B). rewrite id_left.
set (XX := to_postmor_unel A b f).
unfold to_postmor in XX.
unfold to_unel.
rewrite XX.
apply (to_lunax b c).
Qed.

The following definitions give 2 ways to construct a morphisms a ⊕ c --> b ⊕ d from two morphisms f : a --> b and g : c --> d , by using the binary direct sums as a product and as a coproduct.
Definition BinDirectSumIndAr {a b c d : A} (f : a --> b) (g : c --> d)
(B1 : BinDirectSum a c) (B2 : BinDirectSum b d) :
AB1, B2 := ToBinDirectSum B2 ((to_Pr1 B1) · f) ((to_Pr2 B1) · g).

Definition BinDirectSumIndAr' {a b c d : A} (f : a --> b) (g : c --> d)
(B1 : BinDirectSum a c) (B2 : BinDirectSum b d) :
AB1, B2 := FromBinDirectSum B1 (f · (to_In1 B2)) (g · (to_In2 B2)).

Both of the above morphisms are given by the following formula.
Definition BinDirectSumIndArFormula {a b c d: A} (f : a --> b) (g : c --> d)
(B1 : BinDirectSum a c) (B2 : BinDirectSum b d) :
AB1, B2 := (to_binop B1 B2) (to_Pr1 B1 · f · to_In1 B2) (to_Pr2 B1 · g · to_In2 B2).

Lemma BinDirectSumIndArEq1 {a b c d : A} (f : a --> b) (g : c --> d)
(B1 : BinDirectSum a c) (B2 : BinDirectSum b d) :
BinDirectSumIndAr f g B1 B2 = BinDirectSumIndArFormula f g B1 B2.
Proof.
unfold BinDirectSumIndAr.
rewrite <- ToBinDirectSumFormulaUnique.
unfold ToBinDirectSumFormula.
unfold BinDirectSumIndArFormula.
apply idpath.
Qed.

Lemma BinDirectSumIndArEq2 {a b c d : A} (f : a --> b) (g : c --> d)
(B1 : BinDirectSum a c) (B2 : BinDirectSum b d) :
BinDirectSumIndAr' f g B1 B2 = BinDirectSumIndArFormula f g B1 B2.
Proof.
unfold BinDirectSumIndAr'.
rewrite <- FromBinDirectSumFormulaUnique.
unfold FromBinDirectSumFormula.
unfold BinDirectSumIndArFormula.
rewrite assoc. rewrite assoc.
apply idpath.
Qed.

Thus we have equality.
Definition BinDirectSumIndArEq {a b c d : A} (f : a --> b) (g : c --> d)
(B1 : BinDirectSum a c) (B2 : BinDirectSum b d) :
BinDirectSumIndAr f g B1 B2 = BinDirectSumIndAr' f g B1 B2.
Proof.
rewriteBinDirectSumIndArEq1.
rewriteBinDirectSumIndArEq2.
apply idpath.
Qed.

Composition of IndAr

Lemma BinDirectSumIndArComp {a b c d e f : A} (f1 : a --> b) (f2 : b --> c)
(g1 : d --> e) (g2 : e --> f) (B1 : BinDirectSum a d) (B2 : BinDirectSum b e)
(B3 : BinDirectSum c f) :
BinDirectSumIndAr f1 g1 B1 B2 · BinDirectSumIndAr f2 g2 B2 B3 =
BinDirectSumIndAr (f1 · f2) (g1 · g2) B1 B3.
Proof.
rewrite BinDirectSumIndArEq1. rewrite (BinDirectSumIndArEq1 f2). rewrite (BinDirectSumIndArEq1 (f1 · f2)).
unfold BinDirectSumIndArFormula.
rewrite to_postmor_linear'.
rewrite to_premor_linear'.
rewrite assoc. rewrite assoc. rewrite assoc. rewrite assoc. rewrite assoc. rewrite assoc.
rewrite <- (assoc _ (to_In1 B2)). rewrite <- (assoc _ (to_In1 B2)).
rewrite (to_IdIn1 B2). rewrite id_right.
rewrite (to_Unel1 B2). rewrite to_premor_unel'.
rewrite to_postmor_unel'. rewrite to_postmor_unel'. rewrite to_runax'.
rewrite to_premor_linear'.
rewrite assoc. rewrite assoc. rewrite assoc. rewrite assoc.
rewrite <- (assoc _ (to_In2 B2)). rewrite <- (assoc _ (to_In2 B2)).
rewrite (to_IdIn2 B2). rewrite id_right.
rewrite (to_Unel2 B2). rewrite to_premor_unel'.
rewrite to_postmor_unel'. rewrite to_postmor_unel'.
rewrite to_lunax'.
apply idpath.
Qed.

End def_bindirectsums.
Arguments BinDirectSumIndAr {_ _ _ _ _}.
Arguments BinDirectSumOb {_ _ _}.
Arguments BinDirectSum {_}.
Arguments to_Pr1 {_ _ _} _.
Arguments to_Pr2 {_ _ _} _.
Arguments to_In1 {_ _ _} _.
Arguments to_In2 {_ _ _} _.
Arguments to_BinOpId {_ _ _ _ _ _ _ _}.
Arguments to_IdIn1 {_ _ _ _ _ _ _ _}.
Arguments to_IdIn2 {_ _ _ _ _ _ _ _}.
Arguments to_Unel1 {_ _ _ _ _ _ _ _}.
Arguments to_Unel2 {_ _ _ _ _ _ _ _}.
Arguments ToBinDirectSum {_ _ _} _ {_}.
Arguments isBinDirectSum {_ _ _ _}.

In1 and In2 are monics, and Pr1 and Pr2 are epis.
Section bindirectsums_monics_and_epis.

Lemma to_In1_isMonic {a b : A} (B : BinDirectSum a b) : isMonic (to_In1 B).
Proof.
intros z f g H.
apply (maponpaths (λ h : _, h · (to_Pr1 B))) in H.
repeat rewrite <- assoc in H. rewrite (to_IdIn1 B) in H.
repeat rewrite id_right in H. apply H.
Qed.

Lemma to_In2_isMonic {a b : A} (B : BinDirectSum a b) : isMonic (to_In2 B).
Proof.
intros z f g H.
apply (maponpaths (λ h : _, h · (to_Pr2 B))) in H.
repeat rewrite <- assoc in H. rewrite (to_IdIn2 B) in H.
repeat rewrite id_right in H. apply H.
Qed.

Lemma to_Pr1_isEpi {a b : A} (B : BinDirectSum a b) : isEpi (to_Pr1 B).
Proof.
intros z f g H.
apply (maponpaths (λ h : _, (to_In1 B) · h)) in H.
repeat rewrite assoc in H. rewrite (to_IdIn1 B) in H.
repeat rewrite id_left in H. apply H.
Qed.

Lemma to_Pr2_isEpi {a b : A} (B : BinDirectSum a b) : isEpi (to_Pr2 B).
Proof.
intros z f g H.
apply (maponpaths (λ h : _, (to_In2 B) · h)) in H.
repeat rewrite assoc in H. rewrite (to_IdIn2 B) in H.
repeat rewrite id_left in H. apply H.
Qed.

End bindirectsums_monics_and_epis.

If a PreAdditive category has BinProducts, then it has all direct sums.
Section bindirectsums_criteria.

Hypothesis hs : has_homsets A.
Variable Z : Zero A.

Definition BinDirectSums_from_binproduct_bincoproducts_eq1 {X Y : A} (P : BinProduct A X Y) :
BinProductArrow A P (identity X) (ZeroArrow Z X Y) · BinProductPr1 A P = identity _ .
Proof.
apply BinProductPr1Commutes.
Qed.

Definition BinDirectSums_from_binproduct_bincoproducts_eq2 {X Y : A} (P : BinProduct A X Y) :
BinProductArrow A P (identity X) (ZeroArrow Z X Y) · BinProductPr2 A P = to_unel X Y.
Proof.
apply BinProductPr2Commutes.
Qed.

Definition BinDirectSums_from_binproduct_bincoproducts_eq3 {X Y : A} (P : BinProduct A X Y) :
BinProductArrow A P (ZeroArrow Z Y X) (identity _ ) · BinProductPr1 A P = to_unel Y X.
Proof.
apply BinProductPr1Commutes.
Qed.

Definition BinDirectSums_from_binproduct_bincoproducts_eq4 {X Y : A} (P : BinProduct A X Y) :
BinProductArrow A P (ZeroArrow Z Y X) (identity _ ) · BinProductPr2 A P = identity _ .
Proof.
apply BinProductPr2Commutes.
Qed.

Definition BinDirectSums_from_binproduct_bincoproducts_eq5 {X Y : A} (P : BinProduct A X Y) :
to_binop
(BinProductObject A P) (BinProductObject A P)
(BinProductPr1 A P · BinProductArrow A P(identity X) (ZeroArrow Z X Y))
(BinProductPr2 A P · BinProductArrow A P (ZeroArrow Z Y X) (identity Y)) = identity _ .
Proof.
apply BinProductArrowsEq.
- rewrite to_postmor_linear'.
rewrite <- assoc. rewrite <- assoc.
rewrite BinProductPr1Commutes. rewrite BinProductPr1Commutes.
rewrite id_right. rewrite ZeroArrow_comp_right.
rewrite id_left.
apply to_runax.
- rewrite to_postmor_linear'.
rewrite <- assoc. rewrite <- assoc.
rewrite BinProductPr2Commutes. rewrite BinProductPr2Commutes.
rewrite id_right. rewrite ZeroArrow_comp_right.
rewrite id_left.
apply to_lunax.
Qed.

Definition BinDirectSums_from_binproduct_bincoproducts_isCoproduct {X Y : A}
(P : BinProduct A X Y) :
isBinCoproduct A X Y (BinProductObject A P)
(BinProductArrow A P (identity X) (ZeroArrow Z X Y))
(BinProductArrow A P (ZeroArrow Z Y X) (identity Y)).
Proof.
use (make_isBinCoproduct _ hs).
intros c f g.
use unique_exists.
- exact (to_binop (BinProductObject A P) c (BinProductPr1 A P · f) (BinProductPr2 A P · g)).
- split.
+ rewrite to_premor_linear'.
rewrite assoc. rewrite assoc.
rewrite BinProductPr1Commutes.
rewrite BinProductPr2Commutes.
rewrite ZeroArrow_comp_left.
rewrite id_left.
apply to_runax.
+ rewrite to_premor_linear'.
rewrite assoc. rewrite assoc.
rewrite BinProductPr1Commutes.
rewrite BinProductPr2Commutes.
rewrite ZeroArrow_comp_left.
rewrite id_left.
apply to_lunax.
- intros y. apply isapropdirprod. apply hs. apply hs.
- intros y H. induction H as [t p]. rewrite <- t. rewrite <- p.
rewrite assoc. rewrite assoc.
rewrite <- to_postmor_linear'.
rewrite (BinDirectSums_from_binproduct_bincoproducts_eq5 P).
rewrite id_left. apply idpath.
Qed.

Definition BinDirectSums_from_binproduct_bincoproducts_isProduct {X Y : A}
(P : BinProduct A X Y) :
isBinProduct A X Y (BinProductObject A P) (BinProductPr1 A P) (BinProductPr2 A P).
Proof.
use (make_isBinProduct _ hs).
intros c f g.
use unique_exists.
- exact (BinProductArrow A P f g).
- split.
+ apply BinProductPr1Commutes.
+ apply BinProductPr2Commutes.
- intros y. apply isapropdirprod.
+ apply hs.
+ apply hs.
- intros y H. induction H as [t p]. rewrite <- t. rewrite <- p.
rewrite <- precompWithBinProductArrow.
apply BinProductArrowsEq.
+ rewrite <- assoc. rewrite BinProductPr1Commutes. apply idpath.
+ rewrite <- assoc. rewrite BinProductPr2Commutes. apply idpath.
Qed.

Definition BinDirectSum_from_BinProduct {X Y : A} (P : BinProduct A X Y) :
BinDirectSum X Y :=
make_BinDirectSum
A X Y
(BinProductObject A P)
(BinProductArrow A P (identity X) (ZeroArrow Z X Y))
(BinProductArrow A P (ZeroArrow Z Y X) (identity Y))
(BinProductPr1 A P)
(BinProductPr2 A P)
(make_isBinDirectSum
_ _ _ _ _ _ _ _
(BinDirectSums_from_binproduct_bincoproducts_eq1 P)
(BinDirectSums_from_binproduct_bincoproducts_eq4 P)
(BinDirectSums_from_binproduct_bincoproducts_eq2 P)
(BinDirectSums_from_binproduct_bincoproducts_eq3 P)
(BinDirectSums_from_binproduct_bincoproducts_eq5 P)).

Definition BinDirectSums_from_BinProducts (BinProds : BinProducts A) : BinDirectSums A.
Proof.
intros X Y.
exact (BinDirectSum_from_BinProduct (BinProds X Y)).
Defined.

End bindirectsums_criteria.

BinDirectSums in quotient of PreAdditive category

In this section we show that, if a PreAdditive A has BinDirectSums, then the quotient of the preadditive category has BinDirectSums. This is used to show that quotient of an CategoryWithAdditiveStructure is CategoryWithAdditiveStructure.
Section bindirectsums_in_quot.

Hypothesis Z : Zero A.
Hypothesis BD : BinDirectSums A.
Hypothesis PAC : PreAdditiveComps A PAS.

Lemma Quotcategory_isBinCoproduct (x y : A) :
isBinCoproduct (Quotcategory_PreAdditive A PAS PAC) x y (BD x y)
(to_quot_mor A PAS (to_In1 (BD x y)))
(to_quot_mor A PAS (to_In2 (BD x y))).
Proof.
use make_isBinCoproduct.
- apply has_homsets_Quotcategory.
- intros c f g.
set (f'' := @issurjsetquotpr (@to_abgr A x c) (binopeqrel_subgr_eqrel (PAS x c)) f).
use (squash_to_prop f''). apply isapropiscontr. intros f'. clear f''.
set (g'' := @issurjsetquotpr (@to_abgr A y c) (binopeqrel_subgr_eqrel (PAS y c)) g).
use (squash_to_prop g''). apply isapropiscontr. intros g'. clear g''.
induction f' as [f1 f2]. induction g' as [g1 g2]. cbn in f1, g1.
use unique_exists.
+ exact (to_quot_mor A PAS (FromBinDirectSum A (BD x y) f1 g1)).
+ cbn beta. split.
× use (pathscomp0 (Quotcategory_comp_linear A PAS PAC _ _)).
rewrite BinDirectSumIn1Commutes. exact f2.
× use (pathscomp0 (Quotcategory_comp_linear A PAS PAC _ _)).
rewrite BinDirectSumIn2Commutes. exact g2.
+ intros y0. apply isapropdirprod; apply has_homsets_Quotcategory.
+ intros y0 T. cbn beta in T. induction T as [T1 T2].
× set (y'' := @issurjsetquotpr (@to_abgr A (BD x y) c)
(binopeqrel_subgr_eqrel (PAS (BD x y) c)) y0).
use (squash_to_prop y''). apply has_homsets_Quotcategory. intros y'. clear y''.
induction y' as [y1 y2]. rewrite <- y2. rewrite <- y2 in T1. rewrite <- y2 in T2.
cbn in y1.
rewrite <- (@id_left (Quotcategory_PreAdditive A PAS PAC) _ _
(setquotpr (binopeqrel_subgr_eqrel (PAS (BD x y) c)) y1)).
rewrite <- (@id_left A _ _ (FromBinDirectSum A (BD x y) f1 g1)).
rewrite <- (to_BinOpId (BD x y)). rewrite to_postmor_linear'.
repeat rewrite <- assoc.
rewrite BinDirectSumIn1Commutes.
rewrite BinDirectSumIn2Commutes.
rewrite <- f2 in T1. rewrite <- g2 in T2. unfold to_quot_mor.
set (tmp := @setquotpr_linear A PAS PAC (BD x y) c). unfold to_quot_mor in tmp.
rewrite tmp. clear tmp.
set (tmp := @Quotcategory_comp_linear A PAS PAC (BD x y) x c).
unfold to_quot_mor in tmp. rewrite <- tmp. clear tmp.
rewrite <- T1.
set (tmp := @Quotcategory_comp_linear A PAS PAC (BD x y) y c).
unfold to_quot_mor in tmp. rewrite <- tmp. clear tmp.
rewrite <- T2. unfold to_quot_mor. rewrite comp_eq. rewrite comp_eq.
rewrite assoc. rewrite assoc.
rewrite <- to_postmor_linear'.
repeat rewrite <- comp_eq.
set (tmp := @Quotcategory_comp_linear A PAS PAC (BD x y) x (BD x y)).
unfold to_quot_mor in tmp. rewrite tmp. clear tmp.
set (tmp := @Quotcategory_comp_linear A PAS PAC (BD x y) y (BD x y)).
unfold to_quot_mor in tmp. rewrite tmp. clear tmp.
set (tmp := @setquotpr_linear A PAS PAC (BD x y) (BD x y)). unfold to_quot_mor in tmp.
rewrite <- tmp. clear tmp.
rewrite comp_eq.
rewrite (to_BinOpId (BD x y)).
rewrite comp_eq. apply cancel_postcomposition.
apply idpath.
Qed.

Lemma Quotcategory_isBinProduct (x y : A) :
isBinProduct (Quotcategory_PreAdditive A PAS PAC) x y (BD x y)
(to_quot_mor A PAS (to_Pr1 (BD x y)))
(to_quot_mor A PAS (to_Pr2 (BD x y))).
Proof.
use make_isBinProduct.
- apply has_homsets_Quotcategory.
- intros c f g.
set (f'' := @issurjsetquotpr (@to_abgr A c x) (binopeqrel_subgr_eqrel (PAS c x)) f).
use (squash_to_prop f''). apply isapropiscontr. intros f'. clear f''.
set (g'' := @issurjsetquotpr (@to_abgr A c y) (binopeqrel_subgr_eqrel (PAS c y)) g).
use (squash_to_prop g''). apply isapropiscontr. intros g'. clear g''.
induction f' as [f1 f2]. induction g' as [g1 g2]. cbn in f1, g1.
use unique_exists.
+ exact (to_quot_mor A PAS (ToBinDirectSum (BD x y) f1 g1)).
+ cbn beta. split.
× use (pathscomp0 (Quotcategory_comp_linear A PAS PAC _ _)).
rewrite BinDirectSumPr1Commutes. exact f2.
× use (pathscomp0 (Quotcategory_comp_linear A PAS PAC _ _)).
rewrite BinDirectSumPr2Commutes. exact g2.
+ intros y0. apply isapropdirprod; apply has_homsets_Quotcategory.
+ intros y0 T. cbn beta in T. induction T as [T1 T2].
× set (y'' := @issurjsetquotpr (@to_abgr A c (BD x y))
(binopeqrel_subgr_eqrel (PAS c (BD x y))) y0).
use (squash_to_prop y''). apply has_homsets_Quotcategory. intros y'. clear y''.
induction y' as [y1 y2]. rewrite <- y2. rewrite <- y2 in T1. rewrite <- y2 in T2.
cbn in y1.
rewrite <- (@id_right (Quotcategory_PreAdditive A PAS PAC) _ _
(setquotpr (binopeqrel_subgr_eqrel (PAS c (BD x y))) y1)).
rewrite <- (@id_right A _ _ (ToBinDirectSum (BD x y) f1 g1)).
rewrite <- (to_BinOpId (BD x y)). rewrite to_premor_linear'.
repeat rewrite assoc.
rewrite BinDirectSumPr1Commutes.
rewrite BinDirectSumPr2Commutes.
rewrite <- f2 in T1. rewrite <- g2 in T2. unfold to_quot_mor.
set (tmp := @setquotpr_linear A PAS PAC c (BD x y)). unfold to_quot_mor in tmp.
rewrite tmp. clear tmp.
set (tmp := @Quotcategory_comp_linear A PAS PAC c x (BD x y)).
unfold to_quot_mor in tmp. rewrite <- tmp. clear tmp.
rewrite <- T1.
set (tmp := @Quotcategory_comp_linear A PAS PAC c y (BD x y)).
unfold to_quot_mor in tmp. rewrite <- tmp. clear tmp.
rewrite <- T2. unfold to_quot_mor. rewrite comp_eq. rewrite comp_eq.
rewrite <- assoc. rewrite <- assoc.
rewrite <- to_premor_linear'.
repeat rewrite <- comp_eq.
set (tmp := @Quotcategory_comp_linear A PAS PAC (BD x y) x (BD x y)).
unfold to_quot_mor in tmp. rewrite tmp. clear tmp.
set (tmp := @Quotcategory_comp_linear A PAS PAC (BD x y) y (BD x y)).
unfold to_quot_mor in tmp. rewrite tmp. clear tmp.
set (tmp := @setquotpr_linear A PAS PAC (BD x y) (BD x y)). unfold to_quot_mor in tmp.
rewrite <- tmp. clear tmp.
rewrite comp_eq.
rewrite (to_BinOpId (BD x y)).
rewrite comp_eq. apply cancel_precomposition.
apply idpath.
Qed.

Opaque Quotcategory_PreAdditive.   Lemma Quotcategory_isBinDirectSum (x y : A) :
isBinDirectSum
(A := Quotcategory_PreAdditive A PAS PAC)
(to_quot_mor A PAS (to_In1 (BD x y))) (to_quot_mor A PAS (to_In2 (BD x y)))
(to_quot_mor A PAS (to_Pr1 (BD x y))) (to_quot_mor A PAS (to_Pr2 (BD x y))).
Proof.
use make_isBinDirectSum.
- unfold to_quot_mor.
rewrite <- comp_eq.
set (tmp := @Quotcategory_comp_linear A PAS PAC x (BD x y) x).
unfold to_quot_mor in tmp. rewrite tmp. clear tmp.
rewrite (to_IdIn1 (BD x y)).
apply idpath.
- unfold to_quot_mor.
rewrite <- comp_eq.
set (tmp := @Quotcategory_comp_linear A PAS PAC y (BD x y) y).
unfold to_quot_mor in tmp. rewrite tmp. clear tmp.
rewrite (to_IdIn2 (BD x y)).
apply idpath.
- unfold to_quot_mor.
rewrite <- comp_eq.
set (tmp := @Quotcategory_comp_linear A PAS PAC x (BD x y) y).
unfold to_quot_mor in tmp. rewrite tmp. clear tmp.
rewrite (to_Unel1 (BD x y)).
apply idpath.
- unfold to_quot_mor.
rewrite <- comp_eq.
set (tmp := @Quotcategory_comp_linear A PAS PAC y (BD x y) x).
unfold to_quot_mor in tmp. rewrite tmp. clear tmp.
rewrite (to_Unel2 (BD x y)).
apply idpath.
- unfold to_quot_mor.
repeat rewrite <- comp_eq.
set (tmp := @Quotcategory_comp_linear A PAS PAC (BD x y) x (BD x y)).
unfold to_quot_mor in tmp. rewrite tmp. clear tmp.
set (tmp := @Quotcategory_comp_linear A PAS PAC (BD x y) y (BD x y)).
unfold to_quot_mor in tmp. rewrite tmp. clear tmp.
set (tmp := @setquotpr_linear A PAS PAC (BD x y) (BD x y)). unfold to_quot_mor in tmp.
rewrite <- tmp. clear tmp.
rewrite (to_BinOpId (BD x y)).
apply idpath.
Qed.
Definition Quotcategory_BinDirectSums : BinDirectSums (Quotcategory_PreAdditive A PAS PAC).
Proof.
intros x y.
use make_BinDirectSum.
- exact (BD x y).
- exact (to_quot_mor A PAS (to_In1 (BD x y))).
- exact (to_quot_mor A PAS (to_In2 (BD x y))).
- exact (to_quot_mor A PAS (to_Pr1 (BD x y))).
- exact (to_quot_mor A PAS (to_Pr2 (BD x y))).
- exact (Quotcategory_isBinDirectSum x y).
Defined.

End bindirectsums_in_quot.

Notation "'π₁'" := (to_Pr1 _) : abgrcat.
Notation "'π₂'" := (to_Pr2 _) : abgrcat.
Notation "'ι₁'" := (to_In1 _) : abgrcat.
Notation "'ι₂'" := (to_In2 _) : abgrcat.
Local Open Scope abgrcat.

Definition reverseBinDirectSum {M:PreAdditive} {A B:M} : BinDirectSum A B BinDirectSum B A.
Proof.
intros AB.
refine (make_BinDirectSum M B A (BinDirectSumOb AB) ι₂ ι₁ π π _).
unfold isBinDirectSum.
(to_IdIn2 (pr2 AB)).
(to_IdIn1 (pr2 AB)).
(to_Unel2 (pr2 AB)).
(to_Unel1 (pr2 AB)).
cbn. rewrite rewrite_op.
exact (commax (to_abgr _ _) _ _ @ to_BinOpId (pr2 AB)).
Defined.

Definition oppositeBinDirectSum {M:PreAdditive} {x y:M} :
BinDirectSum x y BinDirectSum (A:=oppositePreAdditive M) x y.
Proof.
intros Q.
use make_BinDirectSum.
+ exact (BinDirectSumOb Q).
+ exact (to_Pr1 Q).
+ exact (to_Pr2 Q).
+ exact (to_In1 Q).
+ exact (to_In2 Q).
+ exact (make_isBinDirectSum (oppositePreAdditive M) _ _ _ _ _ _ _
(to_IdIn1 Q) (to_IdIn2 Q) (to_Unel2 Q) (to_Unel1 Q)
(to_BinOpId Q)).
Defined.

Definition isTrivialDirectSum {M : PreAdditive} (Z:Zero M) (A:M) : @isBinDirectSum M A Z A 1 0 1 0.
Proof.
repeat split; cbn.
- apply id_right.
- apply ArrowsToZero.
- apply ArrowsToZero.
- apply ArrowsFromZero.
- rewrite id_right. rewrite to_premor_unel'. rewrite rewrite_op. rewrite runax. reflexivity.
Qed.
Definition TrivialDirectSum {M : PreAdditive} (Z:Zero M) (A:M) : BinDirectSum A Z.
Proof.
exact (make_BinDirectSum _ _ _ _ _ _ _ _ (isTrivialDirectSum _ _)).
Defined.
Definition isTrivialDirectSum' {M : PreAdditive} (Z:Zero M) (A:M) : @isBinDirectSum M Z A A 0 1 0 1.
Proof.
repeat split; cbn.
- apply ArrowsToZero.
- apply id_right.
- apply ArrowsFromZero.
- apply ArrowsToZero.
- rewrite id_right. rewrite to_premor_unel'. rewrite rewrite_op. rewrite lunax. reflexivity.
Qed.
Definition TrivialDirectSum' {M : PreAdditive} (Z:Zero M) (A:M) : BinDirectSum Z A.
Proof.
exact (make_BinDirectSum _ _ _ _ _ _ _ _ (isTrivialDirectSum' _ _)).
Defined.
Definition replaceSum {M:PreAdditive} {A B C:M} (S:BinDirectSum A B) :
z_iso C S BinDirectSum A B .
Proof.
intros r.
(C,, ι₁ · z_iso_inv r,, ι₂ · z_iso_inv r,, r · π,, r · π).
repeat split; cbn.
+ rewrite assoc'. rewrite (assoc _ r). rewrite z_iso_after_z_iso_inv, id_left. exact (to_IdIn1 S).
+ rewrite assoc'. rewrite (assoc _ r). rewrite z_iso_after_z_iso_inv, id_left. exact (to_IdIn2 S).
+ rewrite assoc'. rewrite (assoc _ r). rewrite z_iso_after_z_iso_inv, id_left. exact (to_Unel1 S).
+ rewrite assoc'. rewrite (assoc _ r). rewrite z_iso_after_z_iso_inv, id_left. exact (to_Unel2 S).
+ rewrite rewrite_op. rewrite 2 (assoc' r). rewrite 4 (assoc _ _ (z_iso_inv_mor r)).
rewrite <- leftDistribute. rewrite <- rightDistribute. rewrite wrap_inverse'.
× reflexivity.
× exact (to_BinOpId S).
Defined.
Lemma DirectSumIn1Pr2 {M:PreAdditive} {a b:M} (S:BinDirectSum a b) : to_In1 S · to_Pr2 S = 0.
Proof.
exact (to_Unel1 S).
Defined.
Lemma DirectSumIn2Pr1 {M:PreAdditive} {a b:M} (S:BinDirectSum a b) : to_In2 S · to_Pr1 S = 0.
Proof.
exact (to_Unel2 S).
Defined.