Lemma PullbackSplitEpi {M:AdditiveCategory} {A A'' C : M} (q : A --> A'') (g : C --> A'') : isSplitEpimorphism q -> ∃ PB : Pullback q g, isSplitEpimorphism (PullbackPr2 PB). Proof. intros s. apply (squash_to_hProp s); clear s; intros [A' [i e]]. apply (squash_to_hProp e); clear e; intros [p [j e]]. apply (squash_to_hProp (to_hasBinDirectSums A' C)); intros A'C. apply hinhpr. use tpair. - use tpair. + exists A'C. exists (π₁ · i + π₂ · g · j). exact π₂. + simpl. rewrite rewrite_op. use tpair. * rewrite leftDistribute. rewrite (assoc' _ j q). rewrite (to_IdIn2 e). rewrite id_right. rewrite (assoc' _ i q). rewrite (to_Unel1 e); unfold to_unel. rewrite zeroRight, lunax. reflexivity. * intros T r s eqn. apply iscontraprop1. { apply invproofirrelevance. intros h k. apply subtypePath. { intros l. apply isapropdirprod;apply to_has_homsets. } induction h as [h [H H']], k as [k [K K']]. simpl. rewrite <- (id_right h), <- (id_right k). rewrite <- (to_BinOpId' A'C). rewrite 2 rightDistribute. rewrite 4 assoc. rewrite H', K'. apply (maponpaths (λ z, z + s · ι₂)). rewrite rightDistribute in H, K. rewrite 3 assoc in H, K. rewrite H' in H. rewrite K' in K. apply (maponpaths (λ z, z · ι₁)). apply (to_In1_isMonic _ (make_BinDirectSum _ _ _ _ _ _ _ _ e)). change (h · π₁ · i = k · π₁ · i). apply (grrcan (T-->A) (s · g · j)). exact (H @ !K). } exists (r · p · ι₁ + s · ι₂). split. { rewrite leftDistribute, 2 rightDistribute. rewrite assoc'. rewrite (assoc _ _ i). rewrite (to_IdIn1 A'C). rewrite id_left. rewrite (assoc' (r · p)). rewrite 2 (assoc ι₁). rewrite (to_Unel1 A'C); unfold to_unel. rewrite 2 zeroLeft, zeroRight, runax. rewrite (assoc' s). rewrite (assoc ι₂). rewrite (to_Unel2 A'C); unfold to_unel. rewrite zeroLeft, zeroRight, lunax. rewrite 2 assoc. rewrite (assoc' s). rewrite (to_IdIn2 A'C). rewrite id_right. rewrite (!eqn). rewrite 2 assoc'. rewrite <- (rightDistribute r). rewrite (to_BinOpId' e). apply id_right. } { rewrite leftDistribute. rewrite (assoc' (r · p)). rewrite (to_Unel1 A'C); unfold to_unel. rewrite zeroRight, lunax. rewrite assoc'. rewrite (to_IdIn2 A'C). apply id_right. } - cbn. exact (hinhpr(A',,ι₁,, hinhpr (π₁,,ι₂,,BinDirectSum_isBinDirectSum _ A'C))). Qed.
Require Import UniMath.Algebra.Groups. Require Import UniMath.CategoryTheory.Core.Isos. Definition IsoArrowFrom {M : category}   {A B B':M} (g : A --> B) (g' : A --> B') := ∑ i : z_iso B B', g · i  = g'. Coercion IsoArrowFrom_pr1 {M : category} {A B B':M} (g : A --> B) (g' : A --> B') : IsoArrowFrom g g' -> z_iso B B' := pr1. IsoArrowTo g g' -> IsoArrowFrom (M:=M^op) g' g. Definition opposite_IsoArrowFrom {M:category} {A B B':M} {g : A --> B} {g' : A --> B'} : IsoArrowFrom g g' -> IsoArrowTo (M:=M^op) g' g. Lemma IsoArrowFrom_isaprop (M : category) {A B B':M} (g : A --> B) (g' : A --> B') : isEpi g -> isaprop (IsoArrowFrom g g'). isCokernel' f g -> isCokernel' f g' -> iscontr (IsoArrowFrom g g'). - exact (IsoArrowFrom_isaprop M g g' (CokernelIsEpi f g i)). + apply ArrowsFromZero. isKernelCokernelPair i p -> isKernelCokernelPair i p' -> iscontr (IsoArrowFrom p p'). Lemma ExactSequenceFromMono {M : ExactCategory} {A B C:M} (i : A --> B) (p : B --> C) : Lemma ExactSequenceFromEpi {M : ExactCategory} {A B C:M} (i : A --> B) (p : B --> C) : exact (ExactSequenceFromMono (M:=M^op) p i). exact (ExactSequenceFromMono _ _ (pr2 (kerCoker10 Z A)) (EC_IdentityIsMono A)). exact (ExactSequenceFromEpi _ _ (pr1 (kerCoker01 Z A)) (EC_IdentityIsEpi A)). Lemma FromZeroIsMono {M : ExactCategory} (Z:Zero M) (A:M) : isAdmissibleMonomorphism (0 : Z --> A). Definition MonoFromZero {M : ExactCategory} (Z:Zero M) (A:M) : Z ↣ A := (0 : Z --> A),,FromZeroIsMono Z A. Goal ∏ (M:ExactCategory) (A:M) (Z:Zero M), EpiToZero A Z = MonoFromZero (M:=M^op) (Zero_opp M Z) A. IsoArrowFrom f f' -> isAdmissibleMonomorphism f -> isAdmissibleMonomorphism f'. use ExactSequenceFromEpi. exists po. use ExactSequenceFromMono. { use ExactSequenceFromMono. exists pb. use ExactSequenceFromEpi. { use ExactSequenceFromEpi. apply hinhpr. exists D. exists (π₁ · p). apply ExactSequenceFromEpi. intros i i'. apply ExactSequenceFromMono. assert (Q := r' @ ! s'); clear r' s' u h. apply FromBinDirectSumsEq. Lemma AdmMonoFromComposite {M:ExactCategory} {A B C:M} (i:A-->B) (j:B-->C) : assert (es := ExactSequenceFromMono _ _ co); clear co. use (ExactToAdmMono (p:=k)). use (ExactSequenceFromEpi i k). Lemma AdmEpiFromComposite {M:ExactCategory} {A B C:M} (i:A-->B) (j:B-->C) : exact (AdmMonoFromComposite (M:=M^op) j i). assert (ijs := ExactSequenceFromMono (i·j) s L IJ). { use (ExactSequenceFromMono k u _ K). exists e4. intros T h e0. { exact (@AdmMonoFromComposite M). } { exact (@AdmEpiFromComposite M). } } }