Library UniMath.CategoryTheory.Limits.Graphs.Equalizers

Equalizers defined in terms of limits

Contents

  • Definition of equalizers
  • Coincides with the direct definition

Definition of equalizers in terms of limits

Section def_equalizers.

  Variable C : category.
  Let hs: has_homsets C := homset_property C.

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

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

  Definition Equalizer_diagram {a b : C} (f g : Ca, b) : diagram Equalizer_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 Equalizer_cone {a b : C} (f g : Ca, b) (d : C) (h : Cd, a) (H : h · f = h · g) :
    cone (Equalizer_diagram f g) d.
  Show proof.
    use make_cone.
    - use two_rec_dep.
      + exact h.
      + exact (h · f).
    - 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 isEqualizer {a b : C} (f g : Ca, b) (d : C) (h : Cd, a) (H : h · f = h · g) :
    UU := isLimCone (Equalizer_diagram f g) d (Equalizer_cone f g d h H).

  Definition make_isEqualizer {a b : C} (f g : Ca, b) (d : C) (h : Cd, a) (H : h · f = h · g) :
    ( e (h' : Ce, a) (H' : h' · f = h' · g),
     iscontr (total2 (fun hk : Ce, d => hk · h = h'))) -> isEqualizer f g d h H.
  Show proof.
    intros H' x cx.
    assert (H1 : coneOut cx One · f = coneOut cx One · g).
    {
      use (pathscomp0 (coneOutCommutes cx One Two (ii1 tt))).
      use (pathscomp0 _ (!(coneOutCommutes cx One Two (ii2 tt)))).
      apply idpath.
    }
    set (H2 := (H' x (coneOut cx One) H1)).
    use tpair.
    - use (tpair _ (pr1 (pr1 H2)) _).
      use two_rec_dep.
      + apply (pr2 (pr1 H2)).
      + use (pathscomp0 _ (coneOutCommutes cx One Two (ii1 tt))).
        change (coneOut (Equalizer_cone f g d h H) ( 1)%stn) with (h · f).
        rewrite assoc.
        apply cancel_postcomposition, (pr2 (pr1 H2)).
    - abstract (intro t; apply subtypePath;
                [ intros y; apply impred; intros t0; apply hs
                | induction t as [t p]; apply path_to_ctr, (p One)]).

  Definition Equalizer {a b : C} (f g : Ca, b) := LimCone (Equalizer_diagram f g).

  Definition make_Equalizer {a b : C} (f g : Ca, b) (d : C) (h : Cd, a)
             (H : h · f = h · g) (isEq : isEqualizer f g d h H) :
    Equalizer f g.
  Show proof.
    use tpair.
    - use tpair.
      + exact d.
      + use Equalizer_cone.
        * exact h.
        * exact H.
    - exact isEq.

  Definition Equalizers : UU := (a b : C) (f g : Ca, b), Equalizer f g.

  Definition hasEqualizers : UU := (a b : C) (f g : Ca, b), ishinh (Equalizer f g).

  Definition EqualizerObject {a b : C} {f g : Ca, b} : Equalizer f g -> C := λ H, lim H.

  Definition EqualizerArrow {a b : C} {f g : Ca, b} (E : Equalizer f g) :
    Clim E, a := limOut E One.

  Definition EqualizerArrowEq {a b : C} {f g : Ca, b} (E : Equalizer f g) :
    EqualizerArrow E · f = EqualizerArrow E · g.
  Show proof.
    use (pathscomp0 (limOutCommutes E One Two (ii1 tt))).
    use (pathscomp0 _ (!(limOutCommutes E One Two (ii2 tt)))).
    apply idpath.

  Definition EqualizerIn {a b : C} {f g : Ca, b} (E : Equalizer f g) (e : C) (h : Ce, a)
             (H : h · f = h · g) : Ce, lim E.
  Show proof.
    now use limArrow; use Equalizer_cone.

  Lemma EqualizerArrowComm {a b : C} {f g : Ca, b} (E : Equalizer f g) (e : C) (h : Ce, a)
        (H : h · f = h · g) : EqualizerIn E e h H · EqualizerArrow E = h.
  Show proof.
    exact (limArrowCommutes E e _ One).

  Lemma EqualizerInUnique {a b : C} {f g : Ca, b} (E : Equalizer f g) (e : C) (h : Ce, a)
        (H : h · f = h · g) (w : Ce, lim E) (H' : w · EqualizerArrow E = h) :
    w = EqualizerIn E e h H.
  Show proof.
    apply path_to_ctr.
    use two_rec_dep.
    - apply H'.
    - set (X := limOutCommutes E One Two (ii1 tt)).
      apply (maponpaths (λ h : _, w · h)) in X.
      use (pathscomp0 (!X)); rewrite assoc.
      change (dmor _ _) with f.
      change (coneOut _ _) with (h · f).
      apply cancel_postcomposition, H'.

  Lemma EqualizerInEq
    {a b : C}
    {f g : Ca, b}
    (E : Equalizer f g)
    (e : C)
    (h h' : Ce, EqualizerObject E)
    (H : h · EqualizerArrow E = h' · EqualizerArrow E)
    : h = h'.
  Show proof.
    refine (EqualizerInUnique E e (h' · EqualizerArrow E) _ h H @ !EqualizerInUnique E e (h' · EqualizerArrow E) _ h' (idpath _)).
    do 2 refine (assoc' _ _ _ @ !_).
    apply maponpaths.
    apply EqualizerArrowEq.

  Definition isEqualizer_Equalizer {a b : C} {f g : Ca, b} (E : Equalizer f g) :
    isEqualizer f g (EqualizerObject E) (EqualizerArrow E) (EqualizerArrowEq E).
  Show proof.
    apply make_isEqualizer.
    intros e h H.
    use (unique_exists (EqualizerIn E e h H)).
    - exact (EqualizerArrowComm E e h H).
    - intros y. apply hs.
    - intros y t. cbn in t.
      use EqualizerInUnique.
      exact t.

Equalizers to equalizers


  Definition identity_is_Equalizer_input {a b : C} {f g : Ca, b} (E : Equalizer f g) :
    total2 (fun hk : Clim E, lim E => hk · EqualizerArrow E = EqualizerArrow E).
  Show proof.
    use tpair.
    exact (identity _).
    apply id_left.

  Lemma EqualizerEndo_is_identity {a b : C} {f g : Ca, b} (E : Equalizer f g)
        (k : Clim E, lim E) (kH : k · EqualizerArrow E = EqualizerArrow E) :
    identity (lim E) = k.
  Show proof.
    apply lim_endo_is_identity.
    unfold limOut.
    use two_rec_dep; cbn.
    + apply kH.
    + set (X := (coneOutCommutes (limCone E) One Two (ii1 tt))).
      use (pathscomp0 (! (maponpaths (λ h' : _, k · h') X))).
      use (pathscomp0 _ X).
      rewrite assoc; change (dmor _ _) with f.
      apply cancel_postcomposition, kH.

  Definition from_Equalizer_to_Equalizer {a b : C} {f g : Ca, b} (E1 E2 : Equalizer f g) :
    Clim E1, lim E2.
  Show proof.
    apply (EqualizerIn E2 (lim E1) (EqualizerArrow E1)).
    exact (EqualizerArrowEq E1).

  Lemma are_inverses_from_Equalizer_to_Equalizer {a b : C} {f g : Ca, b} (E1 E2 : Equalizer f g) :
    is_inverse_in_precat (from_Equalizer_to_Equalizer E2 E1)
                         (from_Equalizer_to_Equalizer E1 E2).
  Show proof.
    split; apply pathsinv0.
    - apply EqualizerEndo_is_identity.
      rewrite <- assoc.
      unfold from_Equalizer_to_Equalizer.
      repeat rewrite EqualizerArrowComm.
      apply idpath.
    - apply EqualizerEndo_is_identity.
      rewrite <- assoc.
      unfold from_Equalizer_to_Equalizer.
      repeat rewrite EqualizerArrowComm.
      apply idpath.

  Lemma isiso_from_Equalizer_to_Equalizer {a b : C} {f g : Ca, b} (E1 E2 : Equalizer f g) :
    is_iso (from_Equalizer_to_Equalizer E1 E2).
  Show proof.

  Definition iso_from_Equalizer_to_Equalizer {a b : C} {f g : Ca, b} (E1 E2 : Equalizer f g) :
    iso (lim E1) (lim E2) := tpair _ _ (isiso_from_Equalizer_to_Equalizer E1 E2).

  Lemma inv_from_iso_iso_from_Pullback {a b : C} {f g : Ca , b} (E1 E2 : Equalizer f g):
    inv_from_iso (iso_from_Equalizer_to_Equalizer E1 E2) = from_Equalizer_to_Equalizer E2 E1.
  Show proof.
    apply pathsinv0.
    apply inv_iso_unique'.
    apply (pr1 (are_inverses_from_Equalizer_to_Equalizer E2 E1)).

Connections to other limits


  Lemma Equalizers_from_Lims :
    Lims C -> Equalizers.
  Show proof.
    intros H a b f g. apply H.

End def_equalizers.

Definitions coincide

In this section we show that the definition of equalizer as a limit coincides with the direct definition.
Section equalizers_coincide.

  Variable C : category.
  Let hs: has_homsets C := homset_property C.

isEqualizers


  Lemma equiv_isEqualizer1 {a b : C} {f g : Ca, b} (e : C) (h : Ce, a) (H : h · f = h · g) :
    Limits.Equalizers.isEqualizer f g h H -> isEqualizer C f g e h H.
  Show proof.
    intros X.
    set (E := Limits.Equalizers.make_Equalizer f g h H X).
    use (make_isEqualizer C).
    intros e' h' H'.
    use (unique_exists (Limits.Equalizers.EqualizerIn E e' h' H')).
    - exact (Limits.Equalizers.EqualizerCommutes E e' h' H').
    - intros y. apply hs.
    - intros y T. cbn in T.
      use (Limits.Equalizers.EqualizerInsEq E).
      use (pathscomp0 T).
      exact (!(Limits.Equalizers.EqualizerCommutes E e' h' H')).

  Lemma equiv_isEqualizer2 {a b : C} (f g : Ca, b) (e : C) (h : Ce, a) (H : h · f = h · g) :
    Limits.Equalizers.isEqualizer f g h H <- isEqualizer C f g e h H.
  Show proof.
    intros X.
    set (E := make_Equalizer C f g e h H X).
    intros e' h' H'.
    use (unique_exists (EqualizerIn C E e' h' H')).
    - exact (EqualizerArrowComm C E e' h' H').
    - intros y. apply hs.
    - intros y T. cbn in T.
      use (EqualizerInUnique C E).
      exact T.

Equalizers


  Definition equiv_Equalizer1 {a b : C} (f g : Ca, b) :
    Limits.Equalizers.Equalizer f g -> Equalizer C f g.
  Show proof.
    intros E.
    exact (make_Equalizer
             C f g _ _ _
             (equiv_isEqualizer1
                (Limits.Equalizers.EqualizerObject E)
                (Limits.Equalizers.EqualizerArrow E)
                (Limits.Equalizers.EqualizerEqAr E)
                (Limits.Equalizers.isEqualizer_Equalizer E))).

  Definition equiv_Equalizers1 : @Limits.Equalizers.Equalizers C -> Equalizers C.
  Show proof.
    intros E' a b f g.
    set (E := E' a b f g).
    exact (make_Equalizer
             C f g _ _ _
             (equiv_isEqualizer1
                (Limits.Equalizers.EqualizerObject E)
                (Limits.Equalizers.EqualizerArrow E)
                (Limits.Equalizers.EqualizerEqAr E)
                (Limits.Equalizers.isEqualizer_Equalizer E))).

  Definition equiv_Equalizer2 {a b : C} (f g : Ca, b) :
    Limits.Equalizers.Equalizer f g <- Equalizer C f g.
  Show proof.
    intros E.
    exact (@Limits.Equalizers.make_Equalizer
             C (EqualizerObject C E) a b f g
             (EqualizerArrow C E)
             (EqualizerArrowEq C E)
             (@equiv_isEqualizer2
                a b f g (EqualizerObject C E)
                (EqualizerArrow C E)
                (EqualizerArrowEq C E)
                (isEqualizer_Equalizer C E))).

  Definition equiv_Equalizers2 : @Limits.Equalizers.Equalizers C <- Equalizers C.
  Show proof.
    intros E' a b f g.
    set (E := E' a b f g).
    exact (@Limits.Equalizers.make_Equalizer
             C (EqualizerObject C E) a b f g
             (EqualizerArrow C E)
             (EqualizerArrowEq C E)
             (@equiv_isEqualizer2
                a b f g (EqualizerObject C E)
                (EqualizerArrow C E)
                (EqualizerArrowEq C E)
                (isEqualizer_Equalizer C E))).

End equalizers_coincide.