proposition: 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: 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.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids UniMath.CategoryTheory.Limits.Zero UniMath.CategoryTheory.Limits.Pushouts UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Coequalizers UniMath.CategoryTheory.Limits.Opp UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Morphisms UniMath.CategoryTheory.CategoriesWithBinOps UniMath.CategoryTheory.PrecategoriesWithAbgrops UniMath.CategoryTheory.PreAdditive UniMath.CategoryTheory.Additive UniMath.CategoryTheory.Abelian UniMath.CategoryTheory.AbelianToAdditive UniMath.CategoryTheory.AbelianPushoutPullback UniMath.CategoryTheory.ShortExactSequences UniMath.CategoryTheory.PseudoElements UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Epis UniMath.CategoryTheory.Limits.Kernels UniMath.CategoryTheory.Limits.Cokernels UniMath.CategoryTheory.Limits.BinDirectSums