Library UniMath.CategoryTheory.Limits.Graphs.Coequalizers

Coequalizers defined in terms of colimits

Contents

  • Definition of coequalizers
  • Coincides with the direct definition

Definition of coequalizers in terms of colimits

Section def_coequalizers.

  Variable C : category.

  Local Open Scope stn.
  Definition One : two := 0.
  Definition Two : two := 1.

  Definition Coequalizer_graph : graph.
  Show proof.
    exists two.
    use (@two_rec (two -> UU)).
    - apply two_rec.
      + apply empty.
      + apply (unit ⨿ unit).
    - apply (λ _, empty).

  Lemma is_connected_coequalizer_graph :
      is_connected Coequalizer_graph.
  Show proof.
    use (is_connected_pointed Coequalizer_graph ( 0)%stn).
    intro v.
    induction v as [v v2].
    induction v as [|v Hv].
    - exists 0.
      apply subtypePath; [intro; apply propproperty|].
      reflexivity.
    - induction v as [|v Hv2]; [|induction (nopathsfalsetotrue v2)].
      exists 1.
      exists ( 1)%stn.
      split.
      * do 2 apply inl.
        exact tt.
      * apply subtypePath; [intro; apply propproperty|].
        reflexivity.

  Definition Coequalizer_diagram {a b : C} (f g : Ca, b) : diagram Coequalizer_graph C.
  Show proof.
    exists (two_rec a b).
    use two_rec_dep.
    - use two_rec_dep; simpl.
      + apply fromempty.
      + intro x. induction x.
        exact f. exact g.
    - intro. apply fromempty.

  Definition Coequalizer_cocone {a b : C} (f g : Ca, b) (d : C) (h : Cb, d)
             (H : f · h = g · h) : cocone (Coequalizer_diagram f g) d.
  Show proof.
    use make_cocone.
    - use two_rec_dep.
      + exact (f · h).
      + exact h.
    - use two_rec_dep; use two_rec_dep.
      + exact (empty_rect _).
      + intro e. induction e.
        * apply idpath.
        * apply (! H).
      + exact (empty_rect _).
      + exact (empty_rect _).

  Definition isCoequalizer {a b : C} (f g : Ca, b) (d : C) (h : Cb, d)
             (H : f · h = g · h) : UU := isColimCocone (Coequalizer_diagram f g) d
                                                         (Coequalizer_cocone f g d h H).

  Definition make_isCoequalizer {a b : C} (f g : Ca, b) (d : C) (h : Cb, d)
             (H : f · h = g · h) :
    ( e (h' : Cb, e) (H' : f · h' = g · h'),
     iscontr (total2 (fun hk : Cd, e => h · hk = h'))) ->
    isCoequalizer f g d h H.
  Show proof.
    intros H' x cx.
    assert (H1 : f · coconeIn cx Two = g · coconeIn cx Two).
    {
      use (pathscomp0 (coconeInCommutes cx One Two (ii1 tt))).
      use (pathscomp0 _ (!(coconeInCommutes cx One Two (ii2 tt)))).
      apply idpath.
    }
    set (H2 := (H' x (coconeIn cx Two) H1)).
    use tpair.
    - use (tpair _ (pr1 (pr1 H2)) _).
      use two_rec_dep.
      + use (pathscomp0 _ (coconeInCommutes cx One Two (ii1 tt))).
        change (coconeIn (Coequalizer_cocone f g d h H) _) with (f · h).
        change (dmor _ _) with f.
        rewrite <- assoc.
        apply cancel_precomposition, (pr2 (pr1 H2)).
      + apply (pr2 (pr1 H2)).
    - abstract (intro t; apply subtypePath;
               [intros y; apply impred; intros t0; apply C
               |induction t as [t p]; apply path_to_ctr, (p Two)]).

  Definition Coequalizer {a b : C} (f g : Ca, b) : UU := ColimCocone (Coequalizer_diagram f g).

  Definition make_Coequalizer {a b : C} (f g : Ca, b) (d : C) (h : Cb, d) (H : f · h = g · h)
             (isCEq : isCoequalizer f g d h H) : Coequalizer f g.
  Show proof.
    use tpair.
    - use tpair.
      + exact d.
      + use Coequalizer_cocone.
        * exact h.
        * exact H.
    - exact isCEq.

  Definition Coequalizers : UU := (a b : C) (f g : Ca, b), Coequalizer f g.

  Definition hasCoequalizers : UU := (a b : C) (f g : Ca, b), ishinh (Coequalizer f g).

  Definition CoequalizerObject {a b : C} {f g : Ca, b} :
    Coequalizer f g -> C := λ H, colim H.

  Definition CoequalizerArrow {a b : C} {f g : Ca, b} (E : Coequalizer f g) :
    Cb, colim E := colimIn E Two.

  Definition CoequalizerArrowEq {a b : C} {f g : Ca, b} (E : Coequalizer f g) :
    f · CoequalizerArrow E = g · CoequalizerArrow E.
  Show proof.
    use (pathscomp0 (colimInCommutes E One Two (ii1 tt))).
    use (pathscomp0 _ (!(colimInCommutes E One Two (ii2 tt)))).
    apply idpath.

  Definition CoequalizerOut {a b : C} {f g : Ca, b} (E : Coequalizer f g) e (h : Cb, e)
             (H : f · h = g · h) : Ccolim E, e.
  Show proof.
    now use colimArrow; use Coequalizer_cocone.

  Lemma CoequalizerArrowComm {a b : C} {f g : Ca, b} (E : Coequalizer f g) (e : C) (h : Cb, e)
        (H : f · h = g · h) : CoequalizerArrow E · CoequalizerOut E e h H = h.
  Show proof.
    exact (colimArrowCommutes E e _ Two).

  Lemma CoequalizerOutUnique {a b : C} {f g : Ca, b} (E : Coequalizer f g) (e : C) (h : Cb, e)
        (H : f · h = g · h) (w : Ccolim E, e) (H' : CoequalizerArrow E · w = h) :
    w = CoequalizerOut E e h H.
  Show proof.
    apply path_to_ctr.
    use two_rec_dep.
    - set (X := colimInCommutes E One Two (ii1 tt)).
      apply (maponpaths (λ h : _, h · w)) in X.
      use (pathscomp0 (!X)); rewrite <- assoc.
      change (dmor _ _) with f.
      change (coconeIn _ _) with (f · h).
      apply cancel_precomposition, H'.
    - apply H'.

  Definition isCoequalizer_Coequalizer {a b : C} {f g : Ca, b} (E : Coequalizer f g) :
    isCoequalizer f g (CoequalizerObject E) (CoequalizerArrow E)
                  (CoequalizerArrowEq E).
  Show proof.
    apply make_isCoequalizer.
    intros e h H.
    use (unique_exists (CoequalizerOut E e h H)).
    - exact (CoequalizerArrowComm E e h H).
    - intros y. apply C.
    - intros y t. cbn in t.
      use CoequalizerOutUnique.
      exact t.

  Definition CoequalizerOfArrows
             {a a' b b' : C} {f g : a --> b}
             {f' g' : a' --> b'}
             (cfg : Coequalizer f g)
             (cfg' : Coequalizer f' g')
             (u : a --> a')
             (v : b --> b')
             (eqf : f · v = u · f')
             (eqg : g · v = u · g')
    :
      CoequalizerObject cfg --> CoequalizerObject cfg'.
  Show proof.
    unshelve eapply CoequalizerOut.
    - refine (v · _).
      apply CoequalizerArrow.
    - abstract (rewrite ! assoc, eqf , eqg, ! assoc' ;
                 apply cancel_precomposition, CoequalizerArrowEq).
  Lemma CoequalizerOfArrowsEq
        {a a' b b' : C} {f g : a --> b}
        {f' g' : a' --> b'}
        (cfg : Coequalizer f g)
        (cfg' : Coequalizer f' g')
        (u : a --> a')
        (v : b --> b')
        (eqf : f · v = u · f')
        (eqg : g · v = u · g')
    :
      CoequalizerArrow cfg · CoequalizerOfArrows cfg cfg' u v eqf eqg =
      v · CoequalizerArrow cfg'.
  Show proof.
    apply CoequalizerArrowComm.

Coequalizers to coequalizers


  Definition identity_is_Coequalizer_input {a b : C} {f g : Ca, b} (E : Coequalizer f g) :
    total2 (fun hk : Ccolim E, colim E => CoequalizerArrow E · hk = CoequalizerArrow E).
  Show proof.
    use tpair.
    exact (identity _).
    apply id_right.

  Lemma CoequalizerEndo_is_identity {a b : C} {f g : Ca, b} (E : Coequalizer f g)
        (k : Ccolim E, colim E) (kH :CoequalizerArrow E · k = CoequalizerArrow E) :
    identity (colim E) = k.
  Show proof.
    apply colim_endo_is_identity.
    unfold colimIn.
    use two_rec_dep; cbn.
    + set (X := (coconeInCommutes (colimCocone E) One Two (ii1 tt))).
      use (pathscomp0 (! (maponpaths (λ h' : _, h' · k) X))).
      use (pathscomp0 _ X).
      rewrite <- assoc. apply cancel_precomposition.
      apply kH.
    + apply kH.

  Definition from_Coequalizer_to_Coequalizer {a b : C} {f g : Ca, b} (E1 E2 : Coequalizer f g) :
    Ccolim E1, colim E2.
  Show proof.
    apply (CoequalizerOut E1 (colim E2) (CoequalizerArrow E2)).
    exact (CoequalizerArrowEq E2).

  Lemma are_inverses_from_Coequalizer_to_Coequalizer {a b : C} {f g : Ca, b}
        (E1 E2 : Coequalizer f g) :
    is_inverse_in_precat (from_Coequalizer_to_Coequalizer E2 E1)
                         (from_Coequalizer_to_Coequalizer E1 E2).
  Show proof.
    split; apply pathsinv0.
    - apply CoequalizerEndo_is_identity.
      rewrite assoc.
      unfold from_Coequalizer_to_Coequalizer.
      repeat rewrite CoequalizerArrowComm.
      apply idpath.
    - apply CoequalizerEndo_is_identity.
      rewrite assoc.
      unfold from_Coequalizer_to_Coequalizer.
      repeat rewrite CoequalizerArrowComm.
      apply idpath.

  Lemma isiso_from_Coequalizer_to_Coequalizer {a b : C} {f g : Ca, b} (E1 E2 : Coequalizer f g) :
    is_iso (from_Coequalizer_to_Coequalizer E1 E2).
  Show proof.

  Definition iso_from_Coequalizer_to_Coequalizer {a b : C} {f g : Ca, b}
             (E1 E2 : Coequalizer f g) : iso (colim E1) (colim E2) :=
    tpair _ _ (isiso_from_Coequalizer_to_Coequalizer E1 E2).

  Lemma inv_from_iso_iso_from_Pullback {a b : C} {f g : Ca , b} (E1 E2 : Coequalizer f g):
    inv_from_iso (iso_from_Coequalizer_to_Coequalizer E1 E2) =
    from_Coequalizer_to_Coequalizer E2 E1.
  Show proof.
    apply pathsinv0.
    apply inv_iso_unique'.
    apply (pr1 (are_inverses_from_Coequalizer_to_Coequalizer E2 E1)).

Connections to other colimits


  Lemma Coequalizers_from_Colims : Colims C -> Coequalizers.
  Show proof.
    intros H a b f g. apply H.

End def_coequalizers.

Definitions coincide

In this section we show that the definition of coequalizer as a colimit coincides with the direct definition.
Section coequalizers_coincide.

  Variable C : category.

isCoequalizers


  Lemma equiv_isCoequalizer1 {a b : C} {f g : Ca, b} (e : C) (h : Cb, e) (H : f · h = g · h) :
    Limits.Coequalizers.isCoequalizer f g h H -> isCoequalizer C f g e h H.
  Show proof.
    intros X.
    set (E := Limits.Coequalizers.make_Coequalizer f g h H X).
    use (make_isCoequalizer C).
    intros e' h' H'.
    use (unique_exists (Limits.Coequalizers.CoequalizerOut E e' h' H')).
    - exact (Limits.Coequalizers.CoequalizerCommutes E e' h' H').
    - intros y. apply C.
    - intros y T. cbn in T.
      use (Limits.Coequalizers.CoequalizerOutsEq E).
      use (pathscomp0 T).
      exact (!(Limits.Coequalizers.CoequalizerCommutes E e' h' H')).

  Lemma equiv_isCoequalizer2 {a b : C} (f g : Ca, b) (e : C) (h : Cb, e) (H : f · h = g · h) :
    Limits.Coequalizers.isCoequalizer f g h H <- isCoequalizer C f g e h H.
  Show proof.
    intros X.
    set (E := make_Coequalizer C f g e h H X).
    intros e' h' H'.
    use (unique_exists (CoequalizerOut C E e' h' H')).
    - exact (CoequalizerArrowComm C E e' h' H').
    - intros y. apply C.
    - intros y T. cbn in T.
      use (CoequalizerOutUnique C E).
      exact T.

Coequalizers


  Definition equiv_Coequalizer1 {a b : C} (f g : Ca, b) :
    Limits.Coequalizers.Coequalizer f g -> Coequalizer C f g.
  Show proof.
    intros E.
    exact (make_Coequalizer
             C f g _ _ _
             (equiv_isCoequalizer1
                (Limits.Coequalizers.CoequalizerObject E)
                (Limits.Coequalizers.CoequalizerArrow E)
                (Limits.Coequalizers.CoequalizerEqAr E)
                (Limits.Coequalizers.isCoequalizer_Coequalizer E))).

  Definition equiv_Coequalizer2 {a b : C} (f g : Ca, b) :
    Limits.Coequalizers.Coequalizer f g <- Coequalizer C f g.
  Show proof.
    intros E.
    exact (@Limits.Coequalizers.make_Coequalizer
             C a b (CoequalizerObject C E) f g
             (CoequalizerArrow C E)
             (CoequalizerArrowEq C E)
             (@equiv_isCoequalizer2
                a b f g (CoequalizerObject C E)
                (CoequalizerArrow C E)
                (CoequalizerArrowEq C E)
                (isCoequalizer_Coequalizer C E))).

End coequalizers_coincide.

Post-composing a coequalizer diagram with a functor yields a coequalizer diagram.
Lemma mapdiagram_coequalizer_eq_diag {C : category}{D : category}
      (F : functor C D){a b : C}(f g : a --> b) :
  eq_diag (C := D)
          (mapdiagram F (Coequalizer_diagram _ f g))
          (Coequalizer_diagram _ (# F f) (# F g)).
Show proof.
  use tpair.
  - use StandardFiniteSets.two_rec_dep; cbn; apply idpath.
  - use StandardFiniteSets.two_rec_dep; use StandardFiniteSets.two_rec_dep;
       try exact (empty_rect _ ).
     intro e.
     induction e; apply idpath.