proposition: Lemma CokernelOfDiagonal_is_iso {X : A} (BinProd : BinProduct A X X) : is_z_isomorphism ((BinProductArrow A BinProd (identity X) (ZeroArrow (to_Zero A) X X)) · (CokernelArrow (Cokernel (DiagonalMap BinProd)))).
proof: Proof. set (coker := Cokernel (DiagonalMap BinProd)). set (r := (BinProductArrow A BinProd (identity X) (ZeroArrow (to_Zero A) X X)) · (CokernelArrow coker)). set (M := make_Monic A _ (DiagonalMap_isMonic BinProd)). set (ker := MonicToKernel M). use monic_epi_is_iso. - use (@KernelZeroisMonic A (to_Zero A) _ _ _ (ZeroArrow_comp_left _ _ _ _ _ _)). use (make_isKernel). intros w h H'. use unique_exists. + exact (ZeroArrow (to_Zero A) w (to_Zero A)). + unfold r in H'. rewrite assoc in H'. set (y := KernelIn _ ker _ _ H'). cbn in y. set (com1 := KernelCommutes _ ker _ _ H'). cbn in com1. fold y in com1. unfold DiagonalMap in com1. assert (H : y = ZeroArrow (to_Zero A) w ker). { rewrite <- (id_right y). set (tmp := BinProductPr2Commutes A _ _ BinProd _ (identity X) (identity X)). rewrite <- tmp. rewrite assoc. rewrite com1. rewrite <- assoc. rewrite (BinProductPr2Commutes A _ _ BinProd _ (identity X) _). apply ZeroArrow_comp_right. } cbn. rewrite ZeroArrow_comp_left. cbn in H. apply pathsinv0 in H. use (pathscomp0 H). rewrite <- id_right. rewrite <- (BinProductPr1Commutes A _ _ BinProd _ (identity X) (ZeroArrow (to_Zero A) _ _)). rewrite assoc. rewrite <- com1. rewrite <- assoc. rewrite (BinProductPr1Commutes A _ _ BinProd _ (identity X) (identity X)). rewrite id_right. apply idpath. + intros y. apply hs. + intros y H. apply ArrowsToZero. - use (@CokernelZeroisEpi A _ _ (to_Zero A) _ (ZeroArrow_comp_right _ _ _ _ _ _)). use make_isCokernel. intros w h H'. use unique_exists. + exact (ZeroArrow (to_Zero A) (to_Zero A) w). + set(coker2 := CokernelOfKernelOfPr2 BinProd). set(coker2ar := CokernelArrow coker2). cbn in coker2ar. unfold r in H'. rewrite <- assoc in H'. set (y := CokernelOut _ coker2 _ _ H'). cbn in y. set (com1 := CokernelCommutes _ coker2 _ _ H'). cbn in com1. fold y in com1. assert (H : y = ZeroArrow (to_Zero A) X w). { rewrite <- (id_left y). set (tmp := BinProductPr2Commutes A _ _ BinProd _ (identity X) (identity X)). rewrite <- tmp. rewrite <- assoc. rewrite com1. rewrite assoc. rewrite CokernelCompZero. apply ZeroArrow_comp_left. } rewrite H in com1. rewrite ZeroArrow_comp_right in com1. rewrite <- (ZeroArrow_comp_right A (to_Zero A) _ _ _ (CokernelArrow coker)) in com1. apply CokernelArrowisEpi in com1. rewrite <- com1. apply ZeroArrow_comp_left. + intros y. apply hs. + intros y H. apply ArrowsFromZero. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Algebra.Monoids UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Limits.Zero UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Coequalizers UniMath.CategoryTheory.Limits.Kernels UniMath.CategoryTheory.Limits.Cokernels UniMath.CategoryTheory.Limits.Pushouts UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.BinDirectSums UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Epis UniMath.CategoryTheory.CategoriesWithBinOps UniMath.CategoryTheory.PrecategoriesWithAbgrops UniMath.CategoryTheory.PreAdditive UniMath.CategoryTheory.Additive UniMath.CategoryTheory.Abelian