proposition: 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: 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.
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.Monics UniMath.CategoryTheory.Epis UniMath.CategoryTheory.Limits.Kernels UniMath.CategoryTheory.Limits.Cokernels UniMath.CategoryTheory.Limits.BinDirectSums