Lemma ComposeSplitMono {M:AdditiveCategory} {A B C : M} (i : A --> B) (j : B --> C) : isSplitMonomorphism i ⇒ isSplitMonomorphism j ⇒ isSplitMonomorphism (i · j). Proof. intros s t. apply (squash_to_hProp s); clear s; intros [P [p ip]];cbn in P. apply (squash_to_hProp ip); clear ip; intros [p' [i' ip]]. change (hProptoType (isBinDirectSum i i' p' p)) in ip. apply (squash_to_hProp t); clear t; intros [Q [q jq]];cbn in Q. apply (squash_to_hProp jq); clear jq; intros [q' [j' jq]]. change (hProptoType (isBinDirectSum j j' q' q)) in jq. apply (squash_to_hProp (to_hasBinDirectSums P Q)); intros PQ. apply hinhpr;unfold ExactCategoryDataToAdditiveCategory,pr1. exists PQ. exists (q' · p · ι₁ + q · ι₂). apply hinhpr. exists (q' · p'). exists (π₁ · i' · j + π₂ · j'). repeat split; rewrite ? rewrite_op. { rewrite assoc'. rewrite (assoc j). rewrite (to_IdIn1 jq). rewrite id_left. rewrite (to_IdIn1 ip). reflexivity. } { rewrite rightDistribute, 2 leftDistribute. rewrite (assoc' q'). rewrite (assoc' _ j). rewrite (assoc j). rewrite (to_IdIn1 jq). rewrite id_left. rewrite assoc'. rewrite (assoc i'). rewrite (to_IdIn2 ip). rewrite id_left. rewrite (assoc _ q'). rewrite (assoc' _ j'). rewrite (to_Unel2 jq); unfold to_unel. rewrite zeroRight, zeroLeft, runax. rewrite (assoc' _ j). rewrite (assoc j). rewrite (to_Unel1 jq). unfold to_unel. rewrite zeroLeft, zeroRight, lunax. rewrite assoc'. rewrite (assoc j'). rewrite (to_IdIn2 jq). rewrite id_left. apply (to_BinOpId PQ). } { rewrite rightDistribute. rewrite assoc'. rewrite (assoc' q'). rewrite (assoc j). rewrite (to_IdIn1 jq). rewrite id_left. rewrite assoc. rewrite (to_Unel1 ip); unfold to_unel. rewrite zeroLeft. rewrite lunax. rewrite assoc'. rewrite (assoc j). rewrite (to_Unel1 jq); unfold to_unel. rewrite zeroLeft, zeroRight. reflexivity. } { rewrite leftDistribute. rewrite assoc'. rewrite (assoc j). rewrite (to_IdIn1 jq). rewrite id_left. rewrite (assoc' _ i'). rewrite (to_Unel2 ip); unfold to_unel. rewrite zeroRight. rewrite lunax. rewrite assoc'. rewrite (assoc j'). rewrite (to_Unel2 jq);unfold to_unel. rewrite zeroLeft, zeroRight. reflexivity. } { rewrite rightDistribute, 2 leftDistribute. rewrite assoc. rewrite (assoc' _ i'). rewrite (assoc' _ ι₁). rewrite (assoc ι₁). rewrite (to_IdIn1 PQ). rewrite id_left. rewrite assoc. rewrite (assoc' q). rewrite (assoc _ _ (i' · j)). rewrite (to_Unel2 PQ); unfold to_unel. rewrite zeroLeft, zeroRight, runax. rewrite <- assocax. rewrite <- (leftDistribute _ _ j). rewrite 2 (assoc' q'). rewrite <- (rightDistribute q'). rewrite (to_BinOpId' ip). rewrite id_right. rewrite (assoc' _ ι₁). rewrite (assoc ι₁). rewrite (to_Unel1 PQ); unfold to_unel. rewrite zeroLeft, zeroRight, lunax. rewrite (assoc' q). rewrite (assoc ι₂). rewrite (to_IdIn2 PQ). rewrite id_left. exact (to_BinOpId' jq). } Qed.
Require Import UniMath.Algebra.Groups. Require Import UniMath.CategoryTheory.Core.Isos. Definition IsoArrowFrom {M : category}   {A B B':M} (g : A --> B) (g' : A --> B') := ∑ i : z_iso B B', g · i  = g'. Coercion IsoArrowFrom_pr1 {M : category} {A B B':M} (g : A --> B) (g' : A --> B') : IsoArrowFrom g g' -> z_iso B B' := pr1. IsoArrowTo g g' -> IsoArrowFrom (M:=M^op) g' g. Definition opposite_IsoArrowFrom {M:category} {A B B':M} {g : A --> B} {g' : A --> B'} : IsoArrowFrom g g' -> IsoArrowTo (M:=M^op) g' g. Lemma IsoArrowFrom_isaprop (M : category) {A B B':M} (g : A --> B) (g' : A --> B') : isEpi g -> isaprop (IsoArrowFrom g g'). isCokernel' f g -> isCokernel' f g' -> iscontr (IsoArrowFrom g g'). - exact (IsoArrowFrom_isaprop M g g' (CokernelIsEpi f g i)). + apply ArrowsFromZero. isKernelCokernelPair i p -> isKernelCokernelPair i p' -> iscontr (IsoArrowFrom p p'). Lemma ExactSequenceFromMono {M : ExactCategory} {A B C:M} (i : A --> B) (p : B --> C) : Lemma ExactSequenceFromEpi {M : ExactCategory} {A B C:M} (i : A --> B) (p : B --> C) : exact (ExactSequenceFromMono (M:=M^op) p i). exact (ExactSequenceFromMono _ _ (pr2 (kerCoker10 Z A)) (EC_IdentityIsMono A)). exact (ExactSequenceFromEpi _ _ (pr1 (kerCoker01 Z A)) (EC_IdentityIsEpi A)). Lemma FromZeroIsMono {M : ExactCategory} (Z:Zero M) (A:M) : isAdmissibleMonomorphism (0 : Z --> A). Definition MonoFromZero {M : ExactCategory} (Z:Zero M) (A:M) : Z ↣ A := (0 : Z --> A),,FromZeroIsMono Z A. Goal ∏ (M:ExactCategory) (A:M) (Z:Zero M), EpiToZero A Z = MonoFromZero (M:=M^op) (Zero_opp M Z) A. IsoArrowFrom f f' -> isAdmissibleMonomorphism f -> isAdmissibleMonomorphism f'. use ExactSequenceFromEpi. exists po. use ExactSequenceFromMono. { use ExactSequenceFromMono. exists pb. use ExactSequenceFromEpi. { use ExactSequenceFromEpi. apply hinhpr. exists D. exists (π₁ · p). apply ExactSequenceFromEpi. intros i i'. apply ExactSequenceFromMono. assert (Q := r' @ ! s'); clear r' s' u h. apply FromBinDirectSumsEq. Lemma AdmMonoFromComposite {M:ExactCategory} {A B C:M} (i:A-->B) (j:B-->C) : assert (es := ExactSequenceFromMono _ _ co); clear co. use (ExactToAdmMono (p:=k)). use (ExactSequenceFromEpi i k). Lemma AdmEpiFromComposite {M:ExactCategory} {A B C:M} (i:A-->B) (j:B-->C) : exact (AdmMonoFromComposite (M:=M^op) j i). assert (ijs := ExactSequenceFromMono (i·j) s L IJ). { use (ExactSequenceFromMono k u _ K). exists e4. intros T h e0. { exact (@AdmMonoFromComposite M). } { exact (@AdmEpiFromComposite M). } } }