Lemma AdmMonoFromComposite {M:ExactCategory} {A B C:M} (i:A-->B) (j:B-->C) : hasCokernel i -> isAdmissibleMonomorphism (i·j) -> isAdmissibleMonomorphism i. 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.
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). } } }