proposition: Lemma KernelPlusIdentity {M:ExactCategory} {A B C:M} (f:A-->B) (g:B-->C) (D:M) (BD : BinDirectSum B D) (CD : BinDirectSum C D) : isKernel' (f · ι₁) (directSumMap BD CD g (identity D)) -> isKernel' f g.
proof: Proof. intros K. apply makeMonicKernel. - exact (isMonic_postcomp _ _ _ (KernelIsMonic _ _ K)). - use (to_In1_isMonic _ CD). rewrite zeroLeft. rewrite assoc'. assert (Q := pr1 K); simpl in Q. rewrite assoc' in Q. rewrite directSumMapEqIn1 in Q. exact Q. - intros T h eqn. assert (E : h · ι₁ · directSumMap BD CD g (identity D) = 0). { rewrite assoc'. rewrite directSumMapEqIn1. rewrite assoc. refine (maponpaths (λ r, r·ι₁) eqn @ _). apply zeroLeft. } assert (Q := iscontrpr1 (pr2 K T (h·ι₁) E)); simpl in Q. induction Q as [p e]. exists p. rewrite assoc in e. apply (to_In1_isMonic _ _ _ _ _ e). 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