Lemma FiveLemma_isMonic {A : AbelianPreCat} {FR1 FR2 : FiveRow} (FRM : FiveRowMorphism FR1 FR2) (H1 : is_z_isomorphism (FMor1 FRM)) (H2 : is_z_isomorphism (FMor2 FRM)) (H4 : is_z_isomorphism (FMor4 FRM)) (H5 : is_z_isomorphism (FMor5 FRM)) : isMonic (FMor3 (A:=A) FRM). Proof. use (dirprod_pr2 (PEq_isMonic (FMor3 FRM))). intros d' a X. apply pathsinv0. cbn in X. set (X' := PEq_Zero_Eq' _ _ X). cbn in X'. assert (e1 : a · FDiff3 FR1 = ZeroArrow (to_Zero A) _ _). { set (comm := FComm3 FRM). use (is_iso_isMonic A _ H4). rewrite <- assoc. rewrite comm. clear comm. rewrite assoc. rewrite X'. rewrite ZeroArrow_comp_left. rewrite ZeroArrow_comp_left. apply idpath. } set (b := dirprod_pr1 (PEq_isExact _ _ (FEq2 FR1)) (FEx2 FR1) a e1). set (PE1 := PseudoIm b (FMor2 FRM)). assert (e2 : PE1 · FDiff2 FR2 = ZeroArrow (to_Zero A) _ _). { cbn. set (comm := FComm2 FRM). rewrite <- assoc. rewrite <- comm. clear comm. rewrite assoc. set (tmp := PEqEq (PFiber_Eq b)). cbn in tmp. use (EpiisEpi _ (PEqEpi2 (PFiber_Eq b))). rewrite assoc. cbn in tmp. cbn. rewrite <- tmp. clear tmp. rewrite <- assoc. rewrite X'. rewrite ZeroArrow_comp_right. rewrite ZeroArrow_comp_right. apply idpath. } set (b' := dirprod_pr1 (PEq_isExact _ _ (FEq1 FR2)) (FEx1 FR2) PE1 e2). set (a' := dirprod_pr1 (PEq_isEpi (FMor1 FRM)) (is_iso_isEpi A _ H1) b'). assert (e3 : PEq (PseudoIm a' (FDiff1 FR1)) b). { assert (e31 : PEq (PseudoIm (PseudoIm a' (FDiff1 FR1)) (FMor2 FRM)) (PseudoIm b (FMor2 FRM))). { use (PEq_trans (PEq_Im_Comm a' (FComm1 FRM))). use (PEq_trans (PEq_Im _ _ (FDiff1 FR2) (PFiber_Eq a'))). use (PEq_trans (PFiber_Eq b')). use PEq_refl. } exact (dirprod_pr1 (PEq_isMonic' (FMor2 FRM)) (is_iso_isMonic A _ H2) (PseudoIm a' (FDiff1 FR1)) b e31). } assert (e4 : PEq (PseudoIm (PseudoIm a' (FDiff1 FR1)) (FDiff2 FR1)) a). { use (PEq_trans _ (PFiber_Eq b)). use (PEq_trans _ (PEq_Im _ _ (FDiff2 FR1) e3)). use PEq_refl. } use PEq_Zero_Eq'. - exact (PseudoOb a'). - use (PEq_trans (PEq_symm e4)). use (PEq_trans (PEq_Comp a' (FDiff1 FR1) (FDiff2 FR1))). use (PEq_trans (PEq_Im_Paths a' (FEq1 FR1))). use PEq_Eq_Zero. cbn. apply ZeroArrow_comp_right. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.Algebra.Monoids. Require Import UniMath.CategoryTheory.Limits.Zero. Require Import UniMath.CategoryTheory.Limits.Pushouts. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Opp. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.Morphisms. Require Import UniMath.CategoryTheory.CategoriesWithBinOps. Require Import UniMath.CategoryTheory.PrecategoriesWithAbgrops. Require Import UniMath.CategoryTheory.PreAdditive. Require Import UniMath.CategoryTheory.Additive. Require Import UniMath.CategoryTheory.Abelian. Require Import UniMath.CategoryTheory.AbelianToAdditive. Require Import UniMath.CategoryTheory.AbelianPushoutPullback. Require Import UniMath.CategoryTheory.ShortExactSequences. Require Import UniMath.CategoryTheory.PseudoElements. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.Limits.Kernels. Require Import UniMath.CategoryTheory.Limits.Cokernels. Require Import UniMath.CategoryTheory.Limits.BinDirectSums.