proposition: Lemma AdmMonoFromComposite {M:ExactCategory} {A B C:M} (i:A-->B) (j:B-->C) : hasCokernel i -> isAdmissibleMonomorphism (i·j) -> isAdmissibleMonomorphism i.
proof: Proof. intros hc im. apply (squash_to_hProp (to_hasBinDirectSums C B)); intros CB. apply (squash_to_hProp (to_hasBinDirectSums B C)); intros BC. set (q := ToBinDirectSum CB (i · j) i). assert (s := AdmMonoEnlargement _ (i·j) i im : isAdmissibleMonomorphism q); clear im. assert (e : q · elem12 _ (grinv j) = ToBinDirectSum CB 0 i). { apply ToBinDirectSumsEq. - rewrite BinDirectSumPr1Commutes. unfold elem12. rewrite rightDistribute, leftDistribute. rewrite id_right. rewrite (assoc' π₂). rewrite (assoc q). rewrite (assoc (q · π₂)). rewrite (assoc' _ _ π₁). rewrite (to_IdIn1 CB). rewrite id_right. rewrite rightMinus. unfold q. rewrite BinDirectSumPr1Commutes, BinDirectSumPr2Commutes. apply (grrinvax (Hom_add _ _ _)). - rewrite BinDirectSumPr2Commutes. unfold elem12. rewrite rightDistribute, leftDistribute. rewrite id_right. rewrite assoc. rewrite (assoc' _ _ π₂). rewrite (to_Unel1 CB); unfold to_unel. rewrite zeroRight. rewrite runax. unfold q. rewrite BinDirectSumPr2Commutes. reflexivity. } assert (e' : q · elem12 _ (grinv j) · SwitchMap _ _ _ _ = ToBinDirectSum BC i 0). { rewrite e. apply SwitchMapEqnTo. } assert (l : isAdmissibleMonomorphism (ToBinDirectSum BC i 0)). { induction e'. apply EC_ComposeMono. - apply EC_ComposeMono. + exact s. + apply IsIsoIsMono. apply elem12_isiso. - apply IsIsoIsMono. apply (SwitchIso C B). } clear e' e s q. apply (squash_to_hProp hc); clear hc; intros [D [k ic]]. apply (squash_to_hProp (to_hasBinDirectSums D C)); intros DC. assert (PB := is_symmetric_isPullback _ (MapPlusIdentityToPullback k C BC DC)). assert (co := CokernelPlusIdentity i k C BC DC ic). assert (es := ExactSequenceFromMono _ _ co); clear co. assert (t : i · to_In1 BC = ToBinDirectSum BC i 0). { rewrite <- ToBinDirectSumFormulaUnique. unfold ToBinDirectSumFormula. rewrite rewrite_op. rewrite zeroLeft, runax. reflexivity. } assert (l' : isAdmissibleMonomorphism (i · to_In1 BC)). { induction (!t). exact l. } clear l t. assert (ee := es l'); clear es l'. use (ExactToAdmMono (p:=k)). use (ExactSequenceFromEpi i k). - use KernelPlusIdentity. 4: exact (EC_ExactToKernel ee). - use (IsPullbackEpiIsEpi (_,,PB)). exact (ExactToAdmEpi ee). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Epis UniMath.CategoryTheory.Limits.Zero UniMath.CategoryTheory.Limits.Kernels UniMath.CategoryTheory.Limits.Cokernels UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.Pushouts UniMath.CategoryTheory.Limits.BinDirectSums UniMath.CategoryTheory.Limits.Opp UniMath.CategoryTheory.CategoriesWithBinOps UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.PrecategoriesWithAbgrops UniMath.CategoryTheory.PreAdditive UniMath.CategoryTheory.Morphisms UniMath.CategoryTheory.Additive UniMath.CategoryTheory.Subcategory.Full UniMath.MoreFoundations.Propositions