Library UniMath.CategoryTheory.EpiFacts

Definition of an effective epimorphism.
Proof that natural transformations that are pointwise effective epis are effective epis.
Proof that if the target category has pushouts, a natural transformation that is an epimorphism is pointwise epimorphic
Faithul functors reflect epimorphisms
Definition of a split epimorphism
Split epis are absolute (ie are preserved by any functor)

Ambroise LAFONT January 2017

Definition of an effective epimorphism. An effective epimorphism p: A -> B is a morphism which has a kernel pair and which is the coequalizer of its kernel pair.

Section EffectiveEpi.
  Context {C:precategory} {A B:C}.
  Variable (f: C ⟦A ,B ⟧).

  Definition kernel_pair := Pullback f f.

  Definition isEffective :=
    ∑ g:kernel_pair ,
         (isCoequalizer (PullbackPr1 g)
                        (PullbackPr2 g) f (PullbackSqrCommutes g)).
End EffectiveEpi.

Definition EpisAreEffective (C:precategory) :=
  ∏ (A B:C) (f:C ⟦A ,B ⟧), isEpi f → isEffective f.

Let f be a natural transformation. If f is pointwise effective, then f is effective

Section IsEffectivePw.

  Context {C : precategory} {D : category} .

  Local Notation CD := (functor_category C D).

  Lemma eq_pb_pw {X Y Z:functor C D}
        (a: X ⟹ Z) (b: Y ⟹ Z)
        (c:C)
    : eq_diag
        (pullback_diagram D (a c) (b c))
        (diagram_pointwise (homset_property D)
                           (pullback_diagram CD a b) c).
  Proof.
    intros.
    use tpair.
    use StandardFiniteSets.three_rec_dep; apply idpath.
    use StandardFiniteSets.three_rec_dep; use StandardFiniteSets.three_rec_dep;
      exact (empty_rect _ ) || (exact (λ _, idpath _)).
  Defined.

  Lemma eq_coeq_pw {X Y: functor C D} (a b:X ⟹ Y) (c:C) :
    eq_diag
      (Coequalizer_diagram D (a c) (b c))
      (diagram_pointwise (homset_property D)
                         (Coequalizer_diagram CD a b) c).
  Proof.
    intros.
    use tpair.
    use StandardFiniteSets.two_rec_dep; reflexivity.
    use StandardFiniteSets.two_rec_dep; use StandardFiniteSets.two_rec_dep;
       try exact (empty_rect _ ).
    intros g'.
    destruct g'.
    apply idpath.
    apply idpath.
  Defined.

  Context {X Y :functor C D } {a:X ⟹ Y}.

  Lemma isEffectivePw : (∏ (x:C ), isEffective (a x)) → isEffective (C:=CD) a.
  Proof.
    intros h.
    red.
    transparent assert (f:(kernel_pair (C:=CD) a)).
    { apply equiv_Pullback_2;[apply homset_property|].
      apply LimFunctorCone.
      intro c.
      specialize (h c).
      set (f := pr1 h).
      apply equiv_Pullback_1 in f;[|apply homset_property].
      use (eq_diag_liftlimcone _ _ f).
      apply eq_pb_pw.
    }
    ∃ f.
    apply equiv_isCoequalizer2;[apply homset_property|].
    apply pointwise_Colim_is_isColimFunctor.
    intro x.
    set (g:= f).
    assert (hf := (pr2 (h x))); simpl in hf.
    apply equiv_isCoequalizer1 in hf;[|apply homset_property].
    set (eqd := eq_coeq_pw (PullbackPr1 g) (PullbackPr2 g) x).
    set (z:= (eq_diag_iscolimcocone _ eqd hf)).
    set (CC := (make_ColimCocone _ _ _ z)).
    apply (is_iso_isColim (homset_property D) _ CC).
    rewrite <- (colimArrowUnique CC _ _ (identity _)).
    apply identity_is_iso.
    use StandardFiniteSets.two_rec_dep;
    cbn beta;
    rewrite id_right;
    apply idpath.
  Qed.

End IsEffectivePw.

if the target category has pushouts, a natural transformation that is an epimorphism is pointwise epimorphic

Section PointwiseEpi.

  Context {C : precategory} {D : category}.

  Local Notation CD := (functor_category C D).

  Lemma eq_po_pw {X Y Z :functor C D} {a: X ⟹ Y } {b: X ⟹ Z} x :
    eq_diag
      (pushout_diagram D (a x) (b x))
      (diagram_pointwise (homset_property D)
                         (pushout_diagram CD a b) x).
  Proof.
    use tpair.
    use StandardFiniteSets.three_rec_dep; apply idpath.
    use StandardFiniteSets.three_rec_dep; use StandardFiniteSets.three_rec_dep;
      exact (empty_rect _ )||exact (λ _, idpath _).
  Defined.

  Lemma Pushouts_pw_epi (colimD : graphs.pushouts.Pushouts D) (A B : functor C D)
       (a: A ⟹ B) (epia:isEpi (C:=CD) a) : ∏ (x:C ), isEpi (a x).
  Proof.
    intro x; simpl.
    apply (epi_to_pushout (C:=CD)) in epia.
    apply pushout_to_epi.
    simpl.
    apply equiv_isPushout1 in epia; [| apply homset_property].
    apply equiv_isPushout2; [ apply homset_property|].
    red in epia.
    red.
    eapply (isColimFunctor_is_pointwise_Colim
              (homset_property _)) in epia; cycle 1.
    {
      intro c.
      eapply eq_diag_liftcolimcocone.
      - apply eq_po_pw.
      - apply colimD.
    }
    apply (eq_diag_iscolimcocone _ (sym_eq_diag _ _ (eq_po_pw x)))in epia; cycle 1.
    set (CC := (make_ColimCocone _ _ _ epia)).
    eapply (is_iso_isColim (homset_property D) _ CC).
    rewrite <- (colimArrowUnique CC _ _ (identity _)).
    apply identity_is_iso.
    use StandardFiniteSets.three_rec_dep;
    cbn beta;
    rewrite id_right;
    apply idpath.
  Qed.

End PointwiseEpi.

faithul functors reflect epimorphisms

Lemma faithful_reflects_epis {C D:precategory} (U:functor C D) (hU:faithful U)
      {a b:C} (f:C ⟦a ,b ⟧) : isEpi (#U f) → isEpi f.
Proof.
  intros hf c u v huv.
  eapply invmaponpathsincl.
  apply hU.
  cbn.
  apply hf.
  rewrite <- functor_comp, <- functor_comp.
  now rewrite huv.
Qed.