Library UniMath.CategoryTheory.Limits.Equalizers

Direct implementation of equalizers together with:
Written by Tomi Pannila Extended by Langston Barrett (Nov 2018)

Definition

Section def_equalizers.

  Context {C : category}.

Definition and construction of isEqualizer.
  Definition isEqualizer {x y z : C} (f g : y --> z) (e : x --> y)
             (H : e · f = e · g) : UU :=
     (w : C) (h : w --> y) (H : h · f = h · g),
      ∃! φ : w --> x, φ · e = h.

  Definition make_isEqualizer {x y z : C} (f g : y --> z) (e : x --> y)
             (H : e · f = e · g) :
    ( (w : C) (h : w --> y) (H' : h · f = h · g),
        ∃! ψ : w --> x, ψ · e = h) -> isEqualizer f g e H.
  Show proof.
    intros X. unfold isEqualizer. exact X.

  Lemma isaprop_isEqualizer {x y z : C} (f g : y --> z) (e : x --> y)
        (H : e · f = e · g) :
    isaprop (isEqualizer f g e H).
  Show proof.
    repeat (apply impred; intro).
    apply isapropiscontr.

  Lemma isEqualizer_path {hs : has_homsets C} {x y z : C} {f g : y --> z} {e : x --> y}
        {H H' : e · f = e · g} (iC : isEqualizer f g e H) :
    isEqualizer f g e H'.
  Show proof.
    use make_isEqualizer.
    intros w0 h H'0.
    use unique_exists.
    - exact (pr1 (pr1 (iC w0 h H'0))).
    - exact (pr2 (pr1 (iC w0 h H'0))).
    - intros y0. apply hs.
    - intros y0 X. exact (base_paths _ _ (pr2 (iC w0 h H'0) (tpair _ y0 X))).

Proves that the arrow to the equalizer object with the right commutativity property is unique.
  Lemma isEqualizerInUnique {x y z : C} (f g : y --> z) (e : x --> y)
        (H : e · f = e · g) (E : isEqualizer f g e H)
        (w : C) (h : w --> y) (H' : h · f = h · g)
        (φ : w --> x) (H'' : φ · e = h) :
    φ = (pr1 (pr1 (E w h H'))).
  Show proof.
    set (T := tpair (fun ψ : w --> x => ψ · e = h) φ H'').
    set (T' := pr2 (E w h H') T).
    apply (base_paths _ _ T').

Definition and construction of equalizers.
  Definition Equalizer {y z : C} (f g : y --> z) : UU :=
     e : ( w : C, w --> y),
          (∑ H : (pr2 e) · f = (pr2 e) · g, isEqualizer f g (pr2 e) H).

  Definition make_Equalizer {x y z : C} (f g : y --> z) (e : x --> y)
             (H : e · f = e · g) (isE : isEqualizer f g e H) :
    Equalizer f g.
  Show proof.
    use tpair.
    - use tpair.
      + apply x.
      + apply e.
    - simpl. exact (tpair _ H isE).

Equalizers in precategories.
  Definition Equalizers : UU := (y z : C) (f g : y --> z), Equalizer f g.
  Definition hasEqualizers : UU := (y z : C) (f g : y --> z),
      ishinh (Equalizer f g).

Returns the equalizer object.
  Definition EqualizerObject {y z : C} {f g : y --> z} (E : Equalizer f g) :
    C := pr1 (pr1 E).
  Coercion EqualizerObject : Equalizer >-> ob.

Returns the equalizer arrow.
  Definition EqualizerArrow {y z : C} {f g : y --> z} (E : Equalizer f g) :
    CE, y := pr2 (pr1 E).

The equality on morphisms that equalizers must satisfy.
  Definition EqualizerEqAr {y z : C} {f g : y --> z} (E : Equalizer f g) :
    EqualizerArrow E · f = EqualizerArrow E · g := pr1 (pr2 E).

Returns the property isEqualizer from Equalizer.
  Definition isEqualizer_Equalizer {y z : C} {f g : y --> z}
             (E : Equalizer f g) :
    isEqualizer f g (EqualizerArrow E) (EqualizerEqAr E) := pr2 (pr2 E).

Every morphism which satisfy the equalizer equality on morphism factors uniquely through the EqualizerArrow.
  Definition EqualizerIn {y z : C} {f g : y --> z} (E : Equalizer f g)
             (w : C) (h : w --> y) (H : h · f = h · g) :
    Cw, E := pr1 (pr1 (isEqualizer_Equalizer E w h H)).

  Lemma EqualizerCommutes {y z : C} {f g : y --> z} (E : Equalizer f g)
        (w : C) (h : w --> y) (H : h · f = h · g) :
    (EqualizerIn E w h H) · (EqualizerArrow E) = h.
  Show proof.
    exact (pr2 (pr1 ((isEqualizer_Equalizer E) w h H))).

  Lemma isEqualizerInsEq {x y z: C} {f g : y --> z} {e : x --> y}
        {H : e · f = e · g} (E : isEqualizer f g e H)
        {w : C} (φ1 φ2: w --> x) (H' : φ1 · e = φ2 · e) : φ1 = φ2.
  Show proof.
    assert (H'1 : φ1 · e · f = φ1 · e · g).
    rewrite <- assoc. rewrite H. rewrite assoc. apply idpath.
    set (E' := make_Equalizer _ _ _ _ E).
    set (E'ar := EqualizerIn E' w (φ1 · e) H'1).
    intermediate_path E'ar.
    apply isEqualizerInUnique. apply idpath.
    apply pathsinv0. apply isEqualizerInUnique. apply pathsinv0. apply H'.

  Lemma EqualizerInsEq {y z: C} {f g : y --> z} (E : Equalizer f g)
        {w : C} (φ1 φ2: Cw, E)
        (H' : φ1 · (EqualizerArrow E) = φ2 · (EqualizerArrow E)) : φ1 = φ2.
  Show proof.
    apply (isEqualizerInsEq (isEqualizer_Equalizer E) _ _ H').

  Lemma EqualizerInComp {y z : C} {f g : y --> z} (E : Equalizer f g) {x x' : C}
        (h1 : x --> x') (h2 : x' --> y)
        (H1 : h1 · h2 · f = h1 · h2 · g) (H2 : h2 · f = h2 · g) :
    EqualizerIn E x (h1 · h2) H1 = h1 · EqualizerIn E x' h2 H2.
  Show proof.
    use EqualizerInsEq. rewrite EqualizerCommutes.
    rewrite <- assoc. rewrite EqualizerCommutes.
    apply idpath.

Morphisms between equalizer objects with the right commutativity equalities.
  Definition identity_is_EqualizerIn {y z : C} {f g : y --> z}
             (E : Equalizer f g) :
     φ : CE, E, φ · (EqualizerArrow E) = (EqualizerArrow E).
  Show proof.
    exists (identity E).
    apply id_left.

  Lemma EqualizerEndo_is_identity {y z : C} {f g : y --> z} {E : Equalizer f g}
        (φ : CE, E) (H : φ · (EqualizerArrow E) = EqualizerArrow E) :
    identity E = φ.
  Show proof.
    set (H1 := tpair ((fun φ' : CE, E => φ' · _ = _)) φ H).
    assert (H2 : identity_is_EqualizerIn E = H1).
    - apply proofirrelevancecontr.
      apply (isEqualizer_Equalizer E).
      apply EqualizerEqAr.
    - apply (base_paths _ _ H2).

  Definition from_Equalizer_to_Equalizer {y z : C} {f g : y --> z}
             (E E': Equalizer f g) : CE, E'.
  Show proof.
    apply (EqualizerIn E' E (EqualizerArrow E)).
    apply EqualizerEqAr.

  Lemma are_inverses_from_Equalizer_to_Equalizer {y z : C} {f g : y --> z}
        {E E': Equalizer f g} :
    is_inverse_in_precat (from_Equalizer_to_Equalizer E E')
                         (from_Equalizer_to_Equalizer E' E).
  Show proof.
    split; apply pathsinv0; use EqualizerEndo_is_identity;
    rewrite <- assoc; unfold from_Equalizer_to_Equalizer;
      repeat rewrite EqualizerCommutes; apply idpath.

  Lemma isiso_from_Equalizer_to_Equalizer {y z : C} {f g : y --> z}
        (E E' : Equalizer f g) :
    is_iso (from_Equalizer_to_Equalizer E E').
  Show proof.

  Definition iso_from_Equalizer_to_Equalizer {y z : C} {f g : y --> z}
             (E E' : Equalizer f g) : iso E E' :=
    tpair _ _ (isiso_from_Equalizer_to_Equalizer E E').

  Lemma z_iso_from_Equalizer_to_Equalizer_inverses {y z : C} {f g : y --> z}
        (E E' : Equalizer f g) :
    is_inverse_in_precat (from_Equalizer_to_Equalizer E E') (from_Equalizer_to_Equalizer E' E).
  Show proof.
    use make_is_inverse_in_precat.
    - apply pathsinv0. use EqualizerEndo_is_identity.
      rewrite <- assoc. unfold from_Equalizer_to_Equalizer. rewrite EqualizerCommutes.
      rewrite EqualizerCommutes. apply idpath.
    - apply pathsinv0. use EqualizerEndo_is_identity.
      rewrite <- assoc. unfold from_Equalizer_to_Equalizer. rewrite EqualizerCommutes.
      rewrite EqualizerCommutes. apply idpath.

  Definition z_iso_from_Equalizer_to_Equalizer {y z : C} {f g : y --> z}
             (E E' : Equalizer f g) : z_iso E E'.
  Show proof.
    use make_z_iso.
    - exact (from_Equalizer_to_Equalizer E E').
    - exact (from_Equalizer_to_Equalizer E' E).
    - exact (z_iso_from_Equalizer_to_Equalizer_inverses E E').

Proof that the equalizer arrow is monic (EqualizerArrowisMonic)

We prove that EqualizerArrow is a monic.
  Lemma EqualizerArrowisMonic {y z : C} {f g : y --> z} (E : Equalizer f g ) :
    isMonic (EqualizerArrow E).
  Show proof.
    apply make_isMonic.
    intros z0 g0 h X.
    apply (EqualizerInsEq E).
    apply X.

  Lemma EqualizerArrowMonic {y z : C} {f g : y --> z} (E : Equalizer f g ) :
    Monic _ E y.
  Show proof.

  Definition identity_asEqualizer {y z : C} (f : y --> z) : (Equalizer f f).
  Show proof.
    use make_Equalizer.
    + exact y.
    + exact (identity y).
    + apply idpath.
    + use make_isEqualizer.
      intros x h p.
      use unique_exists.
      - exact h.
      - use id_right.
      - intro.
        use homset_property.
      - intros t t_tri.
        rewrite <-(id_right t).
        exact t_tri.

  Lemma z_iso_Equalizer_of_same_map {y z : C} {f g : y --> z} (E : Equalizer f g) (p:f = g) : is_z_isomorphism (EqualizerArrow E).
  Show proof.

End def_equalizers.

Make the C not implicit for Equalizers
Arguments Equalizers : clear implicits.

Alternative universal property


Section Equalizers'.

  Context {C : category} {c d : ob C} (f g : Cc, d).
  Context (E : ob C) (h : E --> c) (H : h · f = h · g).

A map into an equalizer can be turned into a map into c such that its composites with f and g are equal.
  Definition postcomp_with_equalizer_mor (a : ob C) (j : a --> E) :
     (k : a --> c), (k · f = k · g).
  Show proof.
    exists (j · h).
    refine (!assoc _ _ _ @ _).
    refine (_ @ assoc _ _ _).
    apply maponpaths.
    assumption.

  Definition isEqualizer' : UU :=
     (a : ob C), isweq (postcomp_with_equalizer_mor a).

  Definition isEqualizer'_weq (is : isEqualizer') :
     a, (a --> E) ( k : a --> c, (k · f = k · g)) :=
    λ a, make_weq (postcomp_with_equalizer_mor a) (is a).

  Lemma isaprop_isEqualizer' : isaprop isEqualizer'.
  Show proof.
    unfold isEqualizer'.
    apply impred; intro.
    apply isapropisweq.

Can isEqualizer'_to_isEqualizer be generalized to arbitrary precategories?
Compare to isBinProduct'_to_isBinProduct.
  Lemma isEqualizer'_to_isEqualizer :
    isEqualizer' -> isEqualizer f g h H.
  Show proof.
    intros isEq' E' h' H'.
    apply (@iscontrweqf (hfiber (isEqualizer'_weq isEq' _) (h',, H'))).
    - cbn; unfold hfiber.
      use weqfibtototal; intros j; cbn.
      unfold postcomp_with_equalizer_mor.
      apply subtypeInjectivity.
      intro; apply C.
    - apply weqproperty.

  Lemma isEqualizer_to_isEqualizer' :
    isEqualizer f g h H -> isEqualizer'.
  Show proof.
    intros isEq E'.
    unfold postcomp_with_equalizer_mor.
    unfold isweq, hfiber.
    intros hH'.
    apply (@iscontrweqf ( u : C E', E , u · h = pr1 hH')).
    - use weqfibtototal; intro; cbn.
      apply invweq.
      use subtypeInjectivity.
      intro; apply C.
    - exact (isEq E' (pr1 hH') (pr2 hH')).

  Lemma isEqualizer'_weq_isEqualizer :
    isEqualizer f g h H isEqualizer'.
  Show proof.
    apply weqimplimpl.
    - apply isEqualizer_to_isEqualizer'; assumption.
    - apply isEqualizer'_to_isEqualizer; assumption.
    - apply isaprop_isEqualizer.
    - apply isaprop_isEqualizer'.

End Equalizers'.

Definition isEqualizer_eq
           {C : category}
           {e x y : C}
           {f g f' g' : x --> y}
           {i i' : e --> x}
           (p : i · f = i · g)
           (q : i' · f' = i' · g')
           (s₁ : f = f')
           (s₂ : g = g')
           (s₃ : i = i')
           (He : isEqualizer f g i p)
  : isEqualizer f' g' i' q.
Show proof.
  intros w h r.
  use iscontraprop1.
  - abstract
      (induction s₁, s₂, s₃ ;
       apply (isapropifcontr (He w h r))).
  - simple refine (_ ,, _).
    + refine (EqualizerIn (make_Equalizer _ _ _ _ He) _ h _).
      abstract
        (induction s₁, s₂ ;
         exact r).
    + abstract
        (cbn ;
         induction s₁, s₂, s₃ ;
         apply (EqualizerCommutes (make_Equalizer _ _ _ _ He))).

Equalizers are closed under iso
Definition isEqualizer_z_iso
           {C : category}
           {e₁ e₂ x y : C}
           {f g : x --> y}
           {p₁ : e₁ --> x}
           {q₁ : p₁ · f = p₁ · g}
           {p₂ : e₂ --> x}
           {q₂ : p₂ · f = p₂ · g}
           (H : isEqualizer f g p₁ q₁)
           (h : z_iso e₂ e₁)
           (r : p₂ = h · p₁)
  : isEqualizer f g p₂ q₂.
Show proof.
  intros a k s.
  use iscontraprop1.
  - abstract
      (use invproofirrelevance ;
       intros φ φ ;
       use subtypePath ; [ intro ; apply homset_property | ] ;
       use (cancel_z_iso _ _ h) ;
       use (isEqualizerInsEq H) ;
       rewrite !assoc' ;
       rewrite <- !r ;
       exact (pr2 φ @ !(pr2 φ))).
  - refine (EqualizerIn (make_Equalizer _ _ _ _ H) _ k s · inv_from_z_iso h ,, _).
    abstract
      (rewrite r ;
       rewrite !assoc' ;
       rewrite !(maponpaths (λ z, _ · z) (assoc _ _ _)) ;
       refine (maponpaths (λ z, _ · (z · _)) (z_iso_after_z_iso_inv h) @ _) ;
       rewrite id_left ;
       apply (EqualizerCommutes (make_Equalizer _ _ _ _ H))).

In univalent categories, equalizers are unique up to equality
Proposition isaprop_Equalizer
            {C : category}
            (HC : is_univalent C)
            {x y : C}
            (f g : x --> y)
  : isaprop (Equalizer f g).
Show proof.
  use invproofirrelevance.
  intros φ φ.
  use subtypePath.
  {
    intro.
    use (isaprop_total2 (_ ,, _) (λ _, (_ ,, _))).
    - apply homset_property.
    - simpl.
      repeat (use impred ; intro).
      apply isapropiscontr.
  }
  use total2_paths_f.
  - use (isotoid _ HC).
    use z_iso_from_Equalizer_to_Equalizer.
  - rewrite transportf_isotoid ; cbn.
    apply EqualizerCommutes.

Lemma retract_is_equalizer
  {C : category}
  {a b : C}
  (f : retraction b a)
  : Equalizer (f · retraction_section f) (identity a).
Show proof.
  use make_Equalizer.
  - exact b.
  - exact (retraction_section f).
  - abstract (
      refine (_ @ !id_right _);
      refine (assoc _ _ _ @ _);
      refine (maponpaths (λ x, x · _) (retraction_is_retraction f) @ _);
      apply id_left
    ).
  - apply make_isEqualizer.
    intros d f' Hf'.
    use unique_exists.
    + exact (f' · f).
    + abstract exact (assoc' _ _ _ @ Hf' @ id_right _).
    + abstract (
        intro y;
        apply homset_property
      ).
    + abstract (
        intros g' Hg';
        refine (!id_right _ @ _);
        refine (!maponpaths _ (retraction_is_retraction f) @ _);
        refine (assoc _ _ _ @ _);
        apply (maponpaths (λ x, x · _));
        exact Hg'
      ).