proposition: Lemma AbelianPushoutMonicisPullback1 {x y z : A} (f : Monic A x y) (g : x --> z) (Po : Pushout f g) : isPullback (PushoutSqrCommutes Po).
proof: Proof. set (DS := to_BinDirectSums (AbelianToAdditive A) y z). set (Po' := Pushout_from_Coequalizer_BinCoproduct A _ _ _ f g (BinDirectSum_BinCoproduct _ DS) (Abelian.Coequalizer A (f · (to_In1 DS)) (g · (to_In2 DS)))). set (i := z_iso_from_Pushout_to_Pushout Po Po'). use isPullback_up_to_z_iso. - exact Po'. - exact i. - use isPullback_mor_paths. + exact (PushoutIn1 Po'). + exact (PushoutIn2 Po'). + exact f. + exact g. + apply pathsinv0. exact (PushoutArrow_PushoutIn1 Po Po' (PushoutIn1 Po') (PushoutIn2 Po') (PushoutSqrCommutes Po')). + apply pathsinv0. exact (PushoutArrow_PushoutIn2 Po Po' (PushoutIn1 Po') (PushoutIn2 Po') (PushoutSqrCommutes Po')). + apply idpath. + apply idpath. + exact (PushoutSqrCommutes _ ). + set (K := MonicToKernel f). set (CK := Abelian.Cokernel f). fold CK in K. use make_isPullback. intros e h k Hk. use unique_exists. * use (KernelIn (to_Zero A) K). -- exact h. -- exact (AbelianPushoutMonicisPullback_eq f g Hk). * cbn. split. -- use (KernelCommutes (to_Zero A) K). -- assert (Hk' : h · PushoutIn1 Po' = k · PushoutIn2 Po') by apply Hk. set (comm := KernelCommutes (to_Zero A) K _ h (AbelianPushoutMonicisPullback_eq f g Hk)). cbn in comm. rewrite <- comm in Hk'. clear comm. apply (AbelianPushoutMonic2 f g Po'). rewrite <- Hk'. cbn. rewrite <- assoc. rewrite <- assoc. apply cancel_precomposition. rewrite assoc. rewrite assoc. apply pathsinv0. use CoequalizerEqAr. * intros y0. apply isapropdirprod; apply (homset_property A). * intros y0 X. cbn in X. use (KernelArrowisMonic (to_Zero A) K). rewrite KernelCommutes. exact (dirprod_pr1 X). Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets 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.opp_precat UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Epis UniMath.CategoryTheory.Morphisms UniMath.CategoryTheory.CategoriesWithBinOps UniMath.CategoryTheory.PrecategoriesWithAbgrops UniMath.CategoryTheory.PreAdditive UniMath.CategoryTheory.Additive UniMath.CategoryTheory.Abelian UniMath.CategoryTheory.AbelianToAdditive UniMath.CategoryTheory.Limits.Kernels UniMath.CategoryTheory.Limits.Cokernels UniMath.CategoryTheory.Limits.BinDirectSums