proposition: Lemma KernelZeroisMonic {x y z : A} (f : y --> z) (H : ZeroArrow (to_Zero A) x y · f = ZeroArrow (to_Zero A) x z ) (isK : isKernel (to_Zero A) (ZeroArrow (to_Zero A) _ _) f H) : isMonic f.
proof: Proof. intros w u v H'. set (Coeq := Coequalizer A u v). set (Coeqar := CoequalizerOut Coeq z f H'). set (Coeqar_epi := CoequalizerArrowEpi Coeq). set (Coeq_coker := EpiToCokernel Coeqar_epi). set (ker := @make_Kernel A (to_Zero A) _ _ _ (ZeroArrow (to_Zero A) x y) f H isK). assert (e0 : CokernelArrow Coeq_coker = CoequalizerArrow Coeq). { apply idpath. } assert (e1 : f = (CokernelArrow Coeq_coker) · Coeqar). { apply pathsinv0. rewrite e0. set (XX := CoequalizerCommutes Coeq z f H'). fold Coeqar in XX. apply XX. } assert (e2 : (KernelArrow (to_Kernels A _ _ Coeqar_epi)) · f = ZeroArrow (to_Zero A) _ _). { rewrite e1. rewrite assoc. rewrite CokernelCompZero. apply ZeroArrow_comp_left. } set (ar := KernelIn (to_Zero A) ker (to_Kernels A _ _ Coeqar_epi) (KernelArrow (to_Kernels A _ _ Coeqar_epi))). set (com1 := KernelCommutes (to_Zero A) ker (to_Kernels A _ _ Coeqar_epi) (KernelArrow (to_Kernels A _ _ Coeqar_epi)) e2). assert (e3 : KernelArrow ker = ZeroArrow (to_Zero A) _ _ ). { apply idpath. } assert (e4 : (KernelArrow (to_Kernels A _ _ Coeqar_epi)) = ZeroArrow (to_Zero A) _ _). { rewrite <- com1. apply ZeroArrow_comp_right. } assert (e5 : is_iso (CoequalizerArrow Coeq)). { set (coker2 := KernelZeroMonic_cokernel e4 Coeq_coker). apply (is_iso_qinv _ _ (CokernelofZeroArrow_is_iso (to_Zero A) coker2)). } set (isoar := make_iso (CoequalizerArrow Coeq) e5). set (coeq_eq := CoequalizerEqAr Coeq). apply (maponpaths (λ f : _, f · inv_from_iso isoar)) in coeq_eq. rewrite <- assoc in coeq_eq. rewrite <- assoc in coeq_eq. assert(areq : CoequalizerArrow Coeq = isoar). apply idpath. rewrite areq in coeq_eq. rewrite (iso_inv_after_iso isoar) in coeq_eq. rewrite <- id_right. rewrite <- coeq_eq. apply pathsinv0. apply id_right. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Algebra.Monoids UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Epis 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.Opp UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.CategoriesWithBinOps UniMath.CategoryTheory.PrecategoriesWithAbgrops UniMath.CategoryTheory.PreAdditive