Library UniMath.CategoryTheory.AbelianPushoutPullback

Pushout of a Monic is Monic, Pullback of an Epi is Epi

Contents
  • Pushout of a Monic is Monic
  • Pushout of a Monic is Pullback
  • Pullback of an Epi is Epi
  • Pullback of an Epi is Pushout

Introduction

We show that in abelian categories pushout of a Monic is a Monic and pullback of an Epi is an Epi. Also, in this case the pushout diagram (resp. pullback diagram) is a pullback diagram (resp. pushout diagram).
More precisely, let f : x --> y and g : x --> z be morphisms in an abelian category. Consider the following pushout diagram x ----g----> z f | in2 | y ---in1---> w If f is a Monic, then in2 is a Monic, AbelianPushoutMonic2. If g is a Monic, then in1 is a Monic, AbelianPushoutMonic1. In both of the cases the above diagram is a pullback diagram, AbelianPushoutMonicisPullback1, AbelianPushoutMonicisPullback2.
Let f : x --> z and g : y --> z be morphisms in an abelian category. Consider the following pullback diagram w ---pr1---> x pr2 | f | y ----g----> z If f is an Epi, then pr2 is an Epi, AbelianPushoutEpi2, and if g is an Epi, then pr1 is an Epi, AbelianPushoutEpi1. In both of the cases the above diagram is a pushout diagram, AbelianPullbackEpiisPushout1, AbelianPullbackEpiisPushout2.
Section pushout_monic_pullback_epi.

  Context {A : AbelianPreCat}.
  Variable hs : has_homsets A.

  Local Opaque Abelian.Equalizer.
  Local Opaque Abelian.Coequalizer.
  Local Opaque to_BinDirectSums.
  Local Opaque to_binop to_inv.

Pushout of a Monic is Monic


  Lemma AbelianPushoutMonic2 {x y z : A} (f : Monic A x y) (g : x --> z) (Po : Pushout f g) :
    Monics.isMonic (PushoutIn2 Po).
  Proof.
    set (DS := to_BinDirectSums (AbelianToAdditive A hs) y z).
    set (Po' := Pushout_from_Coequalizer_BinCoproduct
                  A hs _ _ _ f g (BinDirectSum_BinCoproduct _ DS)
                  (Abelian.Coequalizer
                     A hs
                     (f · (to_In1 _ DS))
                     (g · (to_In2 _ DS)))).
    set (iso := iso_from_Pushout_to_Pushout Po Po').
    apply (isMonic_postcomp
             A _ (PushoutArrow Po Po' (PushoutIn1 Po') (PushoutIn2 Po')
                               (PushoutSqrCommutes Po'))).
    rewrite (PushoutArrow_PushoutIn2
               Po _ (PushoutIn1 Po') (PushoutIn2 Po')
               (PushoutSqrCommutes Po')).
    set (CE := Coequalizer A hs (f · to_In1 (AbelianToPreAdditive A hs) DS)
                           (g · to_In2 (AbelianToPreAdditive A hs) DS)).
    set (CK := AdditiveCoequalizerToCokernel (AbelianToAdditive A hs) _ _ CE).
    set (M1 := @isMonic_to_binop_BinDirectSum1' (AbelianToAdditive A hs) x y z f g DS).
    set (K := MonicToKernel' A hs (mk_Monic _ _ M1) CK).
    use (@to_isMonic (AbelianToAdditive A hs)).
    intros z0 g0 H. cbn in H. rewrite assoc in H.
    set (φ := KernelIn _ K z0 (g0 · to_In2 (AbelianToPreAdditive A hs) DS) H).
    set (KComm := KernelCommutes (to_Zero A) K z0 (g0 · to_In2 (AbelianToPreAdditive A hs) DS) H).
    fold φ in KComm.
    assert (e1 : φ = ZeroArrow (to_Zero A) _ _).
    {
      use (MonicisMonic _ f).
      rewrite ZeroArrow_comp_left. cbn in KComm.
      assert (e2 : (MonicArrow _ f) =
                   (@to_binop (AbelianToAdditive A hs) _ _
                              (f · to_In1 (AbelianToPreAdditive A hs) DS)
                              (@to_inv (AbelianToAdditive A hs) _ _
                                       (g · to_In2 (AbelianToPreAdditive A hs) DS)))
                     · to_Pr1 _ DS).
      {
        rewrite to_postmor_linear'. rewrite <- assoc.
        rewrite PreAdditive_invlcomp. rewrite <- assoc.
        set (tmp := to_IdIn1 _ DS). cbn in tmp. cbn. rewrite tmp. clear tmp.
        set (tmp := to_Unel2' DS). cbn in tmp. rewrite tmp. clear tmp.
        rewrite ZeroArrow_comp_right. rewrite id_right. apply pathsinv0.
        set (tmp := @to_runax'' (AbelianToAdditive A hs) (to_Zero A) _ _ f). exact tmp.
      }
      rewrite e2. clear e2. rewrite assoc. cbn in KComm. cbn. rewrite KComm.
      rewrite <- assoc. set (tmp := to_Unel2' DS). cbn in tmp. rewrite tmp. clear tmp.
      apply ZeroArrow_comp_right.
    }
    use (to_In2_isMonic _ DS). cbn in KComm. use (pathscomp0 (! KComm)).
    rewrite e1. rewrite ZeroArrow_comp_left. rewrite ZeroArrow_comp_left. apply idpath.
  Qed.

  Lemma AbelianPushoutMonic1 {x y z : A} (f : x --> y) (g : Monic A x z) (Po : Pushout f g) :
    Monics.isMonic (PushoutIn1 Po).
  Proof.
    set (Po' := mk_Pushout _ _ _ _ _ _ (is_symmetric_isPushout hs _ (isPushout_Pushout Po))).
    use (AbelianPushoutMonic2 g f Po').
  Qed.

Pushout of Monic is Pullback


  Local Lemma AbelianPushoutMonicisPullback_eq {x y z : A} (f : Monic A x y) (g : x --> z)
        {e : A} {h : A e, y } {k : A e, z }
        (Hk : let DS := to_BinDirectSums (AbelianToAdditive A hs) y z in
              let Po' := Pushout_from_Coequalizer_BinCoproduct
                           A hs _ _ _ f g (BinDirectSum_BinCoproduct _ DS)
                           (Abelian.Coequalizer A hs (f · (to_In1 _ DS)) (g · (to_In2 _ DS))) in
              h · PushoutIn1 Po' = k · PushoutIn2 Po') :
    let DS := to_BinDirectSums (AbelianToAdditive A hs) y z in
    let Po' := Pushout_from_Coequalizer_BinCoproduct
                 A hs _ _ _ f g (BinDirectSum_BinCoproduct _ DS)
                 (Abelian.Coequalizer A hs (f · (to_In1 _ DS)) (g · (to_In2 _ DS))) in
    h · CokernelArrow (Abelian.Cokernel f) = ZeroArrow (to_Zero A) e (Abelian.Cokernel f).
  Proof.
    intros DS Po'. cbn zeta in Hk. fold DS in Hk. fold Po' in Hk.
    set (CK := Abelian.Cokernel f).
    assert (e1 : f · CokernelArrow CK = g · ZeroArrow (to_Zero A) z CK).
    {
      rewrite CokernelCompZero. rewrite ZeroArrow_comp_right. apply idpath.
    }
    rewrite <- (PushoutArrow_PushoutIn1 Po' CK (CokernelArrow CK) (ZeroArrow (to_Zero A) _ _) e1).
    rewrite assoc. rewrite Hk. clear Hk. rewrite <- assoc.
    rewrite (PushoutArrow_PushoutIn2 Po' CK (CokernelArrow CK) (ZeroArrow (to_Zero A) _ _) e1).
    apply ZeroArrow_comp_right.
  Qed.

  Lemma AbelianPushoutMonicisPullback1 {x y z : A} (f : Monic A x y) (g : x --> z)
        (Po : Pushout f g) : isPullback (PushoutIn1 Po) (PushoutIn2 Po) f g (PushoutSqrCommutes Po).
  Proof.
    set (DS := to_BinDirectSums (AbelianToAdditive A hs) y z).
    set (Po' := Pushout_from_Coequalizer_BinCoproduct
                  A hs _ _ _ f g (BinDirectSum_BinCoproduct _ DS)
                  (Abelian.Coequalizer
                     A hs
                     (f · (to_In1 _ DS))
                     (g · (to_In2 _ DS)))).
    set (i := iso_from_Pushout_to_Pushout Po Po').
    use isPullback_up_to_iso.
    - exact hs.
    - exact Po'.
    - exact i.
    - use isPullback_mor_paths.
      + exact hs.
      + 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 mk_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 hs.
          -- apply hs.
        × intros y0 X. cbn in X.
          use (KernelArrowisMonic (to_Zero A) K). rewrite KernelCommutes. exact (dirprod_pr1 X).
  Qed.

  Lemma AbelianPushoutMonicisPullback2 {x y z : A} (f : x --> y) (g : Monic A x z)
        (Po : Pushout f g) : isPullback (PushoutIn1 Po) (PushoutIn2 Po) f g (PushoutSqrCommutes Po).
  Proof.
    set (Po' := mk_Pushout _ _ _ _ _ _ (is_symmetric_isPushout hs _ (isPushout_Pushout Po))).
    use is_symmetric_isPullback.
    - exact hs.
    - exact (! (PushoutSqrCommutes _ )).
    - exact (AbelianPushoutMonicisPullback1 g f Po').
  Qed.

Pullback of an Epi is Epi


  Lemma AbelianPullbackEpi2 {x y z : A} (f : Epi A x z) (g : y --> z) (Pb : Pullback f g) :
    Epis.isEpi (PullbackPr2 Pb).
  Proof.
    set (DS := to_BinDirectSums (AbelianToAdditive A hs) x y).
    set (Pb' := Pullback_from_Equalizer_BinProduct
                  A hs _ _ _ f g (BinDirectSum_BinProduct _ DS)
                  (Abelian.Equalizer
                     A hs
                     ((to_Pr1 _ DS) · f)
                     ((to_Pr2 _ DS) · g))).
    set (iso := iso_from_Pullback_to_Pullback Pb Pb').
    apply (isEpi_precomp
             A (PullbackArrow Pb Pb' (PullbackPr1 Pb') (PullbackPr2 Pb')
                              (PullbackSqrCommutes Pb'))).
    rewrite (PullbackArrow_PullbackPr2
               Pb _ (PullbackPr1 Pb') (PullbackPr2 Pb')
               (PullbackSqrCommutes Pb')).
    set (E := Equalizer A hs ((to_Pr1 _ DS) · f) ((to_Pr2 _ DS) · g)).
    set (K := AdditiveEqualizerToKernel (AbelianToAdditive A hs) _ _ E).
    set (E1 := @isEpi_to_binop_BinDirectSum1' (AbelianToAdditive A hs) x y z f g DS).
    set (CK := EpiToCokernel' A hs (mk_Epi _ _ E1) K).
    use (@to_isEpi (AbelianToAdditive A hs)).
    intros z0 g0 H. cbn in H. cbn. rewrite <- assoc in H.
    set (φ := CokernelOut _ CK z0 (to_Pr2 _ DS · g0) H).
    set (CKComm := CokernelCommutes (to_Zero A) CK z0 (to_Pr2 _ DS · g0) H).
    fold φ in CKComm.
    assert (e1 : φ = ZeroArrow (to_Zero A) _ _).
    {
      use (EpiisEpi _ f).
      rewrite ZeroArrow_comp_right. cbn in CKComm.
      assert (e2 : (EpiArrow _ f) =
                   (to_In1 _ DS)
                     · (@to_binop (AbelianToAdditive A hs) _ _
                                   (to_Pr1 _ DS · f)
                                   (@to_inv (AbelianToAdditive A hs) _ _ (to_Pr2 _ DS · g)))).
      {
        rewrite to_premor_linear'. rewrite assoc.
        rewrite PreAdditive_invrcomp. rewrite assoc.
        set (tmp := to_IdIn1 _ DS). cbn in tmp. cbn. rewrite tmp. clear tmp.
        set (tmp := to_Unel1' DS). cbn in tmp. rewrite tmp. clear tmp.
        rewrite ZeroArrow_comp_left. rewrite id_left. apply pathsinv0.
        set (tmp := @to_runax'' (AbelianToAdditive A hs) (to_Zero A) _ _ f). exact tmp.
      }
      rewrite e2. clear e2. rewrite <- assoc. cbn in CKComm. cbn. rewrite CKComm.
      rewrite assoc. set (tmp := to_Unel1' DS). cbn in tmp. rewrite tmp. clear tmp.
      apply ZeroArrow_comp_left.
    }
    use (to_Pr2_isEpi _ DS). cbn in CKComm. use (pathscomp0 (! CKComm)).
    rewrite e1. rewrite ZeroArrow_comp_right. rewrite ZeroArrow_comp_right. apply idpath.
  Qed.

  Lemma AbelianPullbackEpi1 {x y z : A} (f : x --> z) (g : Epi A y z) (Pb : Pullback f g) :
    Epis.isEpi (PullbackPr1 Pb).
  Proof.
    set (Pb' := mk_Pullback _ _ _ _ _ _ (is_symmetric_isPullback hs _ (isPullback_Pullback Pb))).
    use (AbelianPullbackEpi2 g f Pb').
  Qed.

Pullback of Epi is Pushout


  Local Lemma AbelianPullbackEpiisPushout1_eq {x y z : A} (f : Epi A x z) (g : y --> z)
        {e : A} {h : A x, e } {k : A y, e }
        (Hk : let DS := to_BinDirectSums (AbelianToAdditive A hs) x y in
              let Pb' := Pullback_from_Equalizer_BinProduct
                           A hs _ _ _ f g (BinDirectSum_BinProduct _ DS)
                           (Abelian.Equalizer A hs ((to_Pr1 _ DS) · f) ((to_Pr2 _ DS) · g)) in
              PullbackPr1 Pb' · h = PullbackPr2 Pb' · k) :
    let DS := to_BinDirectSums (AbelianToAdditive A hs) x y in
    let Pb' := Pullback_from_Equalizer_BinProduct
                           A hs _ _ _ f g (BinDirectSum_BinProduct _ DS)
                           (Abelian.Equalizer A hs ((to_Pr1 _ DS) · f) ((to_Pr2 _ DS) · g)) in
    let K := Abelian.Kernel f in
    KernelArrow K · h = ZeroArrow (to_Zero A) K e.
  Proof.
    intros DS Pb' K. cbn zeta in Hk. fold DS in Hk. fold Pb' in Hk.
    assert (e1 : KernelArrow K · f = ZeroArrow (to_Zero A) _ _ · g).
    {
      rewrite KernelCompZero. rewrite ZeroArrow_comp_left. apply idpath.
    }
    rewrite <- (PullbackArrow_PullbackPr1 Pb' K (KernelArrow K) (ZeroArrow (to_Zero A) _ _) e1).
    rewrite <- assoc. rewrite Hk. clear Hk. rewrite assoc.
    rewrite (PullbackArrow_PullbackPr2 Pb' K (KernelArrow K) (ZeroArrow (to_Zero A) _ _) e1).
    apply ZeroArrow_comp_left.
  Qed.

  Lemma AbelianPullbackEpiisPushout1 {x y z : A} (f : Epi A x z) (g : y --> z) (Pb : Pullback f g) :
    isPushout (PullbackPr1 Pb) (PullbackPr2 Pb) f g (PullbackSqrCommutes Pb).
  Proof.
    set (DS := to_BinDirectSums (AbelianToAdditive A hs) x y).
    set (Pb' := Pullback_from_Equalizer_BinProduct
                  A hs _ _ _ f g (BinDirectSum_BinProduct _ DS)
                  (Abelian.Equalizer A hs ((to_Pr1 _ DS) · f) ((to_Pr2 _ DS) · g))).
    set (i := iso_from_Pullback_to_Pullback Pb' Pb).
    use isPushout_up_to_iso.
    - exact hs.
    - exact Pb'.
    - exact i.
    - use isPushout_mor_paths.
      + exact hs.
      + exact (PullbackPr1 Pb').
      + exact (PullbackPr2 Pb').
      + exact f.
      + exact g.
      + apply pathsinv0.
        exact (PullbackArrow_PullbackPr1
                 Pb Pb' (PullbackPr1 Pb') (PullbackPr2 Pb') (PullbackSqrCommutes Pb')).
      + apply pathsinv0.
        exact (PullbackArrow_PullbackPr2
                 Pb Pb' (PullbackPr1 Pb') (PullbackPr2 Pb') (PullbackSqrCommutes Pb')).
      + apply idpath.
      + apply idpath.
      + exact (PullbackSqrCommutes _ ).
      + set (CK := EpiToCokernel f).
        set (K := Abelian.Kernel f). fold K in CK.
        use mk_isPushout.
        intros e h k Hk.
        use unique_exists.
        × use (CokernelOut (to_Zero A) CK).
          -- exact h.
          -- exact (AbelianPullbackEpiisPushout1_eq f g Hk).
        × cbn. split.
          -- use (CokernelCommutes (to_Zero A) CK).
          -- assert (Hk' : PullbackPr1 Pb' · h = PullbackPr2 Pb' · k) by apply Hk.
             set (comm := CokernelCommutes
                            (to_Zero A) CK _ h (AbelianPullbackEpiisPushout1_eq f g Hk)).
             cbn in comm. rewrite <- comm in Hk'. clear comm.
             apply (AbelianPullbackEpi2 f g Pb'). rewrite <- Hk'.
             cbn. rewrite assoc. rewrite assoc. apply cancel_postcomposition.
             rewrite <- assoc. rewrite <- assoc. apply pathsinv0.
             use EqualizerEqAr.
        × intros y0. apply isapropdirprod.
          -- apply hs.
          -- apply hs.
        × intros y0 X. cbn in X.
          use (CokernelArrowisEpi (to_Zero A) CK). rewrite CokernelCommutes. exact (dirprod_pr1 X).
  Qed.

  Lemma AbelianPullbackEpiisPushout2 {x y z : A} (f : x --> z) (g : Epi A y z) (Pb : Pullback f g) :
    isPushout (PullbackPr1 Pb) (PullbackPr2 Pb) f g (PullbackSqrCommutes Pb).
  Proof.
    set (Pb' := mk_Pullback _ _ _ _ _ _ (is_symmetric_isPullback hs _ (isPullback_Pullback Pb))).
    use is_symmetric_isPushout.
    - exact hs.
    - exact (! (PullbackSqrCommutes _ )).
    - exact (AbelianPullbackEpiisPushout1 g f Pb').
  Qed.

End pushout_monic_pullback_epi.