Lemma PEq_isExact {x y z : ob A} (f : x --> y) (g : y --> z) (H : f · g = ZeroArrow (to_Zero A) _ _) : isExact A f g H <-> ∏ (b : PseudoElem y) (H : b · g = ZeroArrow (to_Zero A) _ _), PFiber f b. Proof. split. - intros isK b H'. unfold isExact in isK. set (K := make_Kernel _ _ _ _ isK). set (KI := KernelIn _ K (PseudoOb b) b H'). set (Pb := Abelian.Pullbacks A _ _ _ (factorization1_epi A f) KI). use make_PFiber. + exact (make_PseudoElem (PullbackPr1 Pb)). + use make_PEq. * exact Pb. * exact (make_Epi _ _ (AbelianPullbackEpi2 (factorization1_epi A f) KI Pb)). * use identity_Epi. * cbn. rewrite id_left. apply pathsinv0. set (tmp := PullbackSqrCommutes Pb). set (tmp' := factorization1 f). apply (maponpaths (λ gg : _, gg · (factorization1_monic A f))) in tmp. rewrite <- assoc in tmp. rewrite <- tmp' in tmp. clear tmp'. use (pathscomp0 tmp). clear tmp. rewrite <- assoc. apply cancel_precomposition. use (KernelCommutes (to_Zero A) K). - intros X. set (fac := factorization1 f). use make_isKernel. + intros w h H'. set (P := X (make_PseudoElem h) H'). set (PE := PFiber_Eq P). set (Pb := Abelian.Pullbacks A _ _ _ h (factorization1_monic A f)). set (isM := MonicPullbackisMonic' _ _ _ Pb). assert (i : is_z_isomorphism (PullbackPr1 Pb)). { use monic_epi_is_iso. - exact isM. - assert (ee : PEqEpi1 PE · h = PEqEpi2 PE · P · factorization1_epi A f · factorization1_monic A f). { cbn. set (ee := PEqEq PE). cbn in ee. rewrite ee. rewrite assoc. rewrite <- (assoc _ _ (KernelArrow (Abelian.Image f))). apply cancel_precomposition. exact fac. } set (tmp := PullbackArrow Pb _ (PEqEpi1 PE) ((PEqEpi2 PE) · (PFiber_Elem P) · (factorization1_epi A f)) ee). set (t := PullbackArrow_PullbackPr1 Pb _ (PEqEpi1 PE) ((PEqEpi2 PE) · (PFiber_Elem P) · (factorization1_epi A f)) ee). use (isEpi_precomp _ tmp). unfold tmp. use (isEpi_path _ _ _ (! t)). apply EpiisEpi. } set (q := PullbackSqrCommutes Pb). assert (e1 : h = (inv_from_iso (make_iso _ (is_iso_qinv _ _ i))) · PullbackPr2 Pb · factorization1_monic A f). { rewrite <- assoc. rewrite <- q. rewrite assoc. set (tmp := iso_after_iso_inv (make_iso _ (is_iso_qinv _ _ i))). cbn in tmp. cbn. rewrite tmp. rewrite id_left. apply idpath. } use unique_exists. * exact (inv_from_iso (make_iso (PullbackPr1 Pb) (is_iso_qinv _ _ i)) · PullbackPr2 Pb). * cbn. cbn in e1. rewrite <- e1. apply idpath. * intros y0. apply homset_property. * intros y0 XX. cbn in XX. use (KernelArrowisMonic (to_Zero A) (Abelian.Image f)). rewrite XX. apply e1. 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.Monics. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.Limits.Kernels. Require Import UniMath.CategoryTheory.Limits.Cokernels. Require Import UniMath.CategoryTheory.Limits.BinDirectSums.