Lemma CoIm_to_Im_is_iso {x y : A} (f : x --> y) : is_z_isomorphism (CoIm_to_Im f). Proof. use monic_epi_is_iso. - use (isMonic_postcomp A _ (KernelArrow (Image f))). intros z g1 g2 H. set (q := Coequalizer A g1 g2). set (ar := CoIm_to_Im f · KernelArrow (Image f)). set (ar1 := CoequalizerOut q _ ar). set (com1 := CoequalizerCommutes q _ _ H). assert (isE : isEpi ((CokernelArrow (CoImage f)) · (CoequalizerArrow q))). { apply isEpi_comp. apply CokernelArrowisEpi. apply CoequalizerArrowisEpi. } set (E := make_Epi A ((CokernelArrow (CoImage f)) · (CoequalizerArrow q)) isE). set (coker := EpiToCokernel E). assert (e0 : (KernelArrow (to_Kernels A _ _ E)) · ((CokernelArrow (CoImage f)) · (CoequalizerArrow q)) = ZeroArrow (to_Zero A) _ (EpiToCokernel E)). { set (tmp := CokernelCompZero (to_Zero A) (EpiToCokernel E)). rewrite <- tmp. apply cancel_precomposition. unfold E. apply idpath. } assert (e : (KernelArrow (to_Kernels A _ _ E)) · f = ZeroArrow (to_Zero A) _ _). { set (tmp := CoIm_to_Im_eq f). apply (maponpaths (λ f : _, (KernelArrow (to_Kernels A _ _ E)) · f)) in tmp. use (pathscomp0 tmp). rewrite <- assoc. rewrite <- com1. rewrite assoc. rewrite assoc. set (tmpar1 := CoIm_to_Im f · KernelArrow (Image f)). set (tmpar2 := CoequalizerOut q y tmpar1 H). rewrite <- (ZeroArrow_comp_left A (to_Zero A) _ _ _ tmpar2). apply cancel_postcomposition. rewrite <- assoc. rewrite e0. apply idpath. } set (l := KernelIn (to_Zero A) (Kernel f) _ _ e). assert (e1 : (KernelArrow (to_Kernels A _ _ E)) · (CokernelArrow (CoImage f)) = ZeroArrow (to_Zero A) _ _). { set (tmp := KernelCommutes (to_Zero A) (Kernel f) _ _ e). rewrite <- tmp. fold l. rewrite <- (ZeroArrow_comp_right A (to_Zero A) _ _ _ l). rewrite <- assoc. apply cancel_precomposition. unfold CoImage. apply CokernelCompZero. } set (ar2 := CokernelOut (to_Zero A) coker _ _ e1). set (com2 := CokernelCommutes (to_Zero A) coker _ _ e1). assert (e2 : CokernelArrow (CoImage f) · (CoequalizerArrow q) · (CokernelOut (to_Zero A) coker _ _ e1) = CokernelArrow (CoImage f)). { apply com2. } assert (e3 : (CoequalizerArrow q) · (CokernelOut (to_Zero A) coker (CoImage f) _ e1) = identity _). { set (isE1 := CokernelArrowisEpi (to_Zero A) (CoImage f)). unfold isEpi in isE1. apply isE1. rewrite assoc. rewrite id_right. apply e2. } assert (e4 : isMonic (CoequalizerArrow q)). { apply (isMonic_postcomp A _ (CokernelOut (to_Zero A) coker (CoImage f) _ e1)). set (tmp := @identity_isMonic A (CoImage f)). rewrite <- e3 in tmp. apply tmp. } set (coeqeq := CoequalizerEqAr q). apply e4 in coeqeq. apply coeqeq. - use (isEpi_precomp A (CokernelArrow (CoImage f)) _). intros z g1 g2 H. set (q := Equalizer A g1 g2). set (ar := CokernelArrow (CoImage f) · CoIm_to_Im f). set (ar1 := EqualizerIn q _ ar). set (com1 := EqualizerCommutes q _ _ H). assert (isE : isMonic ((EqualizerArrow q) · (KernelArrow (Image f)))). { apply isMonic_comp. apply EqualizerArrowisMonic. apply KernelArrowisMonic. } set (M := make_Monic A ((EqualizerArrow q) · (KernelArrow (Image f))) isE). set (ker := MonicToKernel M). assert (e0 : (EqualizerArrow q) · (KernelArrow (Image f)) · (CokernelArrow (to_Cokernels A _ _ M)) = ZeroArrow (to_Zero A) (MonicToKernel M) _). { use (pathscomp0 _ (KernelCompZero (to_Zero A) (MonicToKernel M))). apply cancel_precomposition. apply idpath. } assert (e : f · (CokernelArrow (to_Cokernels A _ _ M)) = ZeroArrow (to_Zero A) _ _). { set (tmp := CoIm_to_Im_eq f). apply (maponpaths (λ f : _, f · (CokernelArrow (to_Cokernels A _ _ M)))) in tmp. use (pathscomp0 tmp). rewrite <- com1. set (tmpar1 := CokernelArrow (CoImage f) · CoIm_to_Im f). set (tmpar2 := EqualizerIn q x tmpar1 H). rewrite <- (ZeroArrow_comp_right A (to_Zero A) _ _ _ tmpar2). rewrite <- assoc. rewrite <- assoc. apply cancel_precomposition. rewrite assoc. rewrite e0. apply idpath. } set (l := CokernelOut (to_Zero A) (Cokernel f) _ _ e). assert (e1 : (KernelArrow (Image f)) · (CokernelArrow (to_Cokernels A _ _ M)) = ZeroArrow (to_Zero A) _ _). { set (tmp := CokernelCommutes (to_Zero A) (Cokernel f) _ _ e). rewrite <- tmp. fold l. rewrite <- (ZeroArrow_comp_left A (to_Zero A) _ _ _ l). rewrite assoc. apply cancel_postcomposition. unfold Image. apply KernelCompZero. } set (ar2 := KernelIn (to_Zero A) ker _ _ e1). set (com2 := KernelCommutes (to_Zero A) ker _ _ e1). assert (e2 : (KernelIn (to_Zero A) ker _ _ e1) · (EqualizerArrow q) · KernelArrow (Image f) = KernelArrow (Image f)). { rewrite <- com2. rewrite <- assoc. apply cancel_precomposition. unfold ker. apply idpath. } assert (e3 : (KernelIn (to_Zero A) ker (Image f) _ e1) · (EqualizerArrow q) = identity _). { set (isM1 := KernelArrowisMonic (to_Zero A) (Image f)). unfold isMonic in isM1. apply isM1. rewrite id_left. apply e2. } assert (e4 : isEpi (EqualizerArrow q)). { apply (isEpi_precomp A (KernelIn (to_Zero A) ker (Image f) _ e1)). set (tmp := @identity_isEpi A (Image f)). rewrite <- e3 in tmp. apply tmp. } set (eqeq := EqualizerEqAr q). apply e4 in eqeq. apply eqeq. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Algebra.Monoids. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.Limits.Zero. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Kernels. Require Import UniMath.CategoryTheory.Limits.Cokernels. Require Import UniMath.CategoryTheory.Limits.Pushouts. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Opp. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.CategoriesWithBinOps. Require Import UniMath.CategoryTheory.PrecategoriesWithAbgrops. Require Import UniMath.CategoryTheory.PreAdditive. isKernel (to_Zero A) (ZeroArrowFrom x) M (ArrowsFromZero A (to_Zero A) y (ZeroArrowFrom x · M) (ZeroArrow (to_Zero A) _ _)). make_Kernel (to_Zero A) (ZeroArrowFrom _) M _ (MonicKernelZero_isKernel M). - intros y0 Y. apply ArrowsFromZero.