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 (A:=AbelianToPreAdditive A hs) DS)
(g · to_In2 (A:=AbelianToPreAdditive A hs) DS)).
set (M1 := @isMonic_to_binop_BinDirectSum1' (AbelianToAdditive A hs) x y z f g DS).
set (K := MonicToKernel' A hs (make_Monic _ _ M1) CK).
intros z0 g0 H. cbn in H. rewrite assoc in H.
set (φ := KernelIn _ K z0 (g0 · to_In2 (A:=AbelianToPreAdditive A hs) DS) H).
set (KComm := KernelCommutes (to_Zero A) K z0 (g0 · to_In2 (A:=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 (A:=AbelianToPreAdditive A hs) DS)
(@to_inv (AbelianToAdditive A hs) _ _
(g · to_In2 (A:=AbelianToPreAdditive A hs) DS)))
· to_Pr1 DS).
{
rewrite to_postmor_linear'. 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' := make_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 make_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' := make_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 (E1 := @isEpi_to_binop_BinDirectSum1' (AbelianToAdditive A hs) x y z f g DS).
set (CK := EpiToCokernel' A hs (make_Epi _ _ E1) K).
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.
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' := make_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 make_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' := make_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.