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 : precategory.
  Variable hs: has_homsets C.

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

  Definition Equalizer_graph : graph.
  Proof.
     two.
    use (@two_rec (two UU)).
    - apply two_rec.
      + apply empty.
      + apply (unit ⨿ unit).
    - apply (λ _, empty).
  Defined.

  Definition Equalizer_diagram {a b : C} (f g : Ca, b) : diagram Equalizer_graph C.
  Proof.
     (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.
  Defined.

  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.
  Proof.
    use mk_cone.
    - use two_rec_dep.
      + exact h.
      + exact (h · f).
    - use two_rec_dep; use two_rec_dep.
      + exact (empty_rect _).
      + intro e. unfold idfun. induction e.
        × apply idpath.
        × apply (! H).
      + exact (empty_rect _).
      + exact (empty_rect _).
  Defined.

  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 mk_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, dhk · h = h'))) isEqualizer f g d h H.
  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 subtypeEquality;
                [ intros y; apply impred; intros t0; apply hs
                | induction t as [t p]; apply path_to_ctr, (p One)]).
  Defined.

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

  Definition mk_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.
  Proof.
    use tpair.
    - use tpair.
      + exact d.
      + use Equalizer_cone.
        × exact h.
        × exact H.
    - exact isEq.
  Defined.

  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.
  Proof.
    use (pathscomp0 (limOutCommutes E One Two (ii1 tt))).
    use (pathscomp0 _ (!(limOutCommutes E One Two (ii2 tt)))).
    apply idpath.
  Qed.

  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.
  Proof.
    now use limArrow; use Equalizer_cone.
  Defined.

  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.
  Proof.
    exact (limArrowCommutes E e _ One).
  Qed.

  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.
  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'.
  Qed.

  Definition isEqualizer_Equalizer {a b : C} {f g : Ca, b} (E : Equalizer f g) :
    isEqualizer f g (EqualizerObject E) (EqualizerArrow E) (EqualizerArrowEq E).
  Proof.
    apply mk_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.
  Qed.

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 Ehk · EqualizerArrow E = EqualizerArrow E).
  Proof.
    use tpair.
    exact (identity _).
    apply id_left.
  Defined.

  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.
  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.
  Qed.

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

  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).
  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.
  Qed.

  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).
  Proof.
    apply (is_iso_qinv _ (from_Equalizer_to_Equalizer E2 E1)).
    apply are_inverses_from_Equalizer_to_Equalizer.
  Qed.

  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.
  Proof.
    apply pathsinv0.
    apply inv_iso_unique'.
    apply (pr1 (are_inverses_from_Equalizer_to_Equalizer E2 E1)).
  Qed.

Connections to other limits


  Lemma Equalizers_from_Lims :
    Lims C Equalizers.
  Proof.
    intros H a b f g. apply H.
  Defined.

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 : precategory.
  Variable hs: has_homsets 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.
  Proof.
    intros X.
    set (E := limits.equalizers.mk_Equalizer f g h H X).
    use (mk_isEqualizer C hs).
    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')).
  Qed.

  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.
  Proof.
    intros X.
    set (E := mk_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.
  Qed.

Equalizers


  Definition equiv_Equalizer1 {a b : C} (f g : Ca, b) :
    limits.equalizers.Equalizer f g Equalizer C f g.
  Proof.
    intros E.
    exact (mk_Equalizer
             C f g _ _ _
             (equiv_isEqualizer1
                (limits.equalizers.EqualizerObject E)
                (limits.equalizers.EqualizerArrow E)
                (limits.equalizers.EqualizerEqAr E)
                (limits.equalizers.isEqualizer_Equalizer E))).
  Defined.

  Definition equiv_Equalizers1 : @limits.equalizers.Equalizers C Equalizers C.
  Proof.
    intros E' a b f g.
    set (E := E' a b f g).
    exact (mk_Equalizer
             C f g _ _ _
             (equiv_isEqualizer1
                (limits.equalizers.EqualizerObject E)
                (limits.equalizers.EqualizerArrow E)
                (limits.equalizers.EqualizerEqAr E)
                (limits.equalizers.isEqualizer_Equalizer E))).
  Defined.

  Definition equiv_Equalizer2 {a b : C} (f g : Ca, b) :
    limits.equalizers.Equalizer f g <- Equalizer C f g.
  Proof.
    intros E.
    exact (@limits.equalizers.mk_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 hs E))).
  Defined.

  Definition equiv_Equalizers2 : @limits.equalizers.Equalizers C <- Equalizers C.
  Proof.
    intros E' a b f g.
    set (E := E' a b f g).
    exact (@limits.equalizers.mk_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 hs E))).
  Defined.

End equalizers_coincide.