Library UniMath.CategoryTheory.limits.graphs.coequalizers
Coequalizers defined in terms of colimits
Contents
- Definition of coequalizers
- Coincides with the direct definition
Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.Sets.
Require Import UniMath.MoreFoundations.Tactics.
Require Import UniMath.Combinatorics.StandardFiniteSets.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.limits.graphs.limits.
Require Import UniMath.CategoryTheory.limits.graphs.colimits.
Require Import UniMath.CategoryTheory.limits.coequalizers.
Local Open Scope cat.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.Sets.
Require Import UniMath.MoreFoundations.Tactics.
Require Import UniMath.Combinatorics.StandardFiniteSets.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.limits.graphs.limits.
Require Import UniMath.CategoryTheory.limits.graphs.colimits.
Require Import UniMath.CategoryTheory.limits.coequalizers.
Local Open Scope cat.
Section def_coequalizers.
Variable C : precategory.
Variable hs: has_homsets C.
Local Open Scope stn.
Definition One : two := ● 0.
Definition Two : two := ● 1.
Definition Coequalizer_graph : graph.
Show proof.
Definition Coequalizer_diagram {a b : C} (f g : C⟦a, b⟧) : diagram Coequalizer_graph C.
Show proof.
Definition Coequalizer_cocone {a b : C} (f g : C⟦a, b⟧) (d : C) (h : C⟦b, d⟧)
(H : f · h = g · h) : cocone (Coequalizer_diagram f g) d.
Show proof.
Definition isCoequalizer {a b : C} (f g : C⟦a, b⟧) (d : C) (h : C⟦b, d⟧)
(H : f · h = g · h) : UU := isColimCocone (Coequalizer_diagram f g) d
(Coequalizer_cocone f g d h H).
Definition mk_isCoequalizer {a b : C} (f g : C⟦a, b⟧) (d : C) (h : C⟦b, d⟧)
(H : f · h = g · h) :
(∏ e (h' : C⟦b, e⟧) (H' : f · h' = g · h'),
iscontr (total2 (fun hk : C⟦d, e⟧ => h · hk = h'))) ->
isCoequalizer f g d h H.
Show proof.
Definition Coequalizer {a b : C} (f g : C⟦a, b⟧) : UU := ColimCocone (Coequalizer_diagram f g).
Definition mk_Coequalizer {a b : C} (f g : C⟦a, b⟧) (d : C) (h : C⟦b, d⟧) (H : f · h = g · h)
(isCEq : isCoequalizer f g d h H) : Coequalizer f g.
Show proof.
Definition Coequalizers : UU := ∏ (a b : C) (f g : C⟦a, b⟧), Coequalizer f g.
Definition hasCoequalizers : UU := ∏ (a b : C) (f g : C⟦a, b⟧), ishinh (Coequalizer f g).
Definition CoequalizerObject {a b : C} {f g : C⟦a, b⟧} :
Coequalizer f g -> C := λ H, colim H.
Definition CoequalizerArrow {a b : C} {f g : C⟦a, b⟧} (E : Coequalizer f g) :
C⟦b, colim E⟧ := colimIn E Two.
Definition CoequalizerArrowEq {a b : C} {f g : C⟦a, b⟧} (E : Coequalizer f g) :
f · CoequalizerArrow E = g · CoequalizerArrow E.
Show proof.
Definition CoequalizerOut {a b : C} {f g : C⟦a, b⟧} (E : Coequalizer f g) e (h : C⟦b, e⟧)
(H : f · h = g · h) : C⟦colim E, e⟧.
Show proof.
Lemma CoequalizerArrowComm {a b : C} {f g : C⟦a, b⟧} (E : Coequalizer f g) (e : C) (h : C⟦b, e⟧)
(H : f · h = g · h) : CoequalizerArrow E · CoequalizerOut E e h H = h.
Show proof.
Lemma CoequalizerOutUnique {a b : C} {f g : C⟦a, b⟧} (E : Coequalizer f g) (e : C) (h : C⟦b, e⟧)
(H : f · h = g · h) (w : C⟦colim E, e⟧) (H' : CoequalizerArrow E · w = h) :
w = CoequalizerOut E e h H.
Show proof.
Definition isCoequalizer_Coequalizer {a b : C} {f g : C⟦a, b⟧} (E : Coequalizer f g) :
isCoequalizer f g (CoequalizerObject E) (CoequalizerArrow E)
(CoequalizerArrowEq E).
Show proof.
Variable C : precategory.
Variable hs: has_homsets C.
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).
use (@two_rec (two -> UU)).
- apply two_rec.
+ apply empty.
+ apply (unit ⨿ unit).
- apply (λ _, empty).
Definition Coequalizer_diagram {a b : C} (f g : C⟦a, 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.
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 : C⟦a, b⟧) (d : C) (h : C⟦b, d⟧)
(H : f · h = g · h) : cocone (Coequalizer_diagram f g) d.
Show proof.
use mk_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 _).
- 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 : C⟦a, b⟧) (d : C) (h : C⟦b, d⟧)
(H : f · h = g · h) : UU := isColimCocone (Coequalizer_diagram f g) d
(Coequalizer_cocone f g d h H).
Definition mk_isCoequalizer {a b : C} (f g : C⟦a, b⟧) (d : C) (h : C⟦b, d⟧)
(H : f · h = g · h) :
(∏ e (h' : C⟦b, e⟧) (H' : f · h' = g · h'),
iscontr (total2 (fun hk : C⟦d, 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 subtypeEquality;
[intros y; apply impred; intros t0; apply hs
|induction t as [t p]; apply path_to_ctr, (p Two)]).
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 subtypeEquality;
[intros y; apply impred; intros t0; apply hs
|induction t as [t p]; apply path_to_ctr, (p Two)]).
Definition Coequalizer {a b : C} (f g : C⟦a, b⟧) : UU := ColimCocone (Coequalizer_diagram f g).
Definition mk_Coequalizer {a b : C} (f g : C⟦a, b⟧) (d : C) (h : C⟦b, 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.
- use tpair.
+ exact d.
+ use Coequalizer_cocone.
* exact h.
* exact H.
- exact isCEq.
Definition Coequalizers : UU := ∏ (a b : C) (f g : C⟦a, b⟧), Coequalizer f g.
Definition hasCoequalizers : UU := ∏ (a b : C) (f g : C⟦a, b⟧), ishinh (Coequalizer f g).
Definition CoequalizerObject {a b : C} {f g : C⟦a, b⟧} :
Coequalizer f g -> C := λ H, colim H.
Definition CoequalizerArrow {a b : C} {f g : C⟦a, b⟧} (E : Coequalizer f g) :
C⟦b, colim E⟧ := colimIn E Two.
Definition CoequalizerArrowEq {a b : C} {f g : C⟦a, 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.
use (pathscomp0 _ (!(colimInCommutes E One Two (ii2 tt)))).
apply idpath.
Definition CoequalizerOut {a b : C} {f g : C⟦a, b⟧} (E : Coequalizer f g) e (h : C⟦b, e⟧)
(H : f · h = g · h) : C⟦colim E, e⟧.
Show proof.
now use colimArrow; use Coequalizer_cocone.
Lemma CoequalizerArrowComm {a b : C} {f g : C⟦a, b⟧} (E : Coequalizer f g) (e : C) (h : C⟦b, 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 : C⟦a, b⟧} (E : Coequalizer f g) (e : C) (h : C⟦b, e⟧)
(H : f · h = g · h) (w : C⟦colim 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'.
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 : C⟦a, b⟧} (E : Coequalizer f g) :
isCoequalizer f g (CoequalizerObject E) (CoequalizerArrow E)
(CoequalizerArrowEq E).
Show proof.
apply mk_isCoequalizer.
intros e h H.
use (unique_exists (CoequalizerOut E e h H)).
- exact (CoequalizerArrowComm E e h H).
- intros y. apply hs.
- intros y t. cbn in t.
use CoequalizerOutUnique.
exact t.
intros e h H.
use (unique_exists (CoequalizerOut E e h H)).
- exact (CoequalizerArrowComm E e h H).
- intros y. apply hs.
- intros y t. cbn in t.
use CoequalizerOutUnique.
exact t.
Definition identity_is_Coequalizer_input {a b : C} {f g : C⟦a, b⟧} (E : Coequalizer f g) :
total2 (fun hk : C⟦colim E, colim E⟧ => CoequalizerArrow E · hk = CoequalizerArrow E).
Show proof.
use tpair.
exact (identity _).
apply id_right.
exact (identity _).
apply id_right.
Lemma CoequalizerEndo_is_identity {a b : C} {f g : C⟦a, b⟧} (E : Coequalizer f g)
(k : C⟦colim 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.
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 : C⟦a, b⟧} (E1 E2 : Coequalizer f g) :
C⟦colim E1, colim E2⟧.
Show proof.
apply (CoequalizerOut E1 (colim E2) (CoequalizerArrow E2)).
exact (CoequalizerArrowEq E2).
exact (CoequalizerArrowEq E2).
Lemma are_inverses_from_Coequalizer_to_Coequalizer {a b : C} {f g : C⟦a, 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.
- 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 : C⟦a, b⟧} (E1 E2 : Coequalizer f g) :
is_iso (from_Coequalizer_to_Coequalizer E1 E2).
Show proof.
apply (is_iso_qinv _ (from_Coequalizer_to_Coequalizer E2 E1)).
apply are_inverses_from_Coequalizer_to_Coequalizer.
apply are_inverses_from_Coequalizer_to_Coequalizer.
Definition iso_from_Coequalizer_to_Coequalizer {a b : C} {f g : C⟦a, 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 : C⟦a , 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)).
apply inv_iso_unique'.
apply (pr1 (are_inverses_from_Coequalizer_to_Coequalizer E2 E1)).
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 : precategory.
Variable hs: has_homsets C.
Variable C : precategory.
Variable hs: has_homsets C.
Lemma equiv_isCoequalizer1 {a b : C} {f g : C⟦a, b⟧} (e : C) (h : C⟦b, 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.mk_Coequalizer f g h H X).
use (mk_isCoequalizer C hs).
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 hs.
- intros y T. cbn in T.
use (limits.coequalizers.CoequalizerOutsEq E).
use (pathscomp0 T).
exact (!(limits.coequalizers.CoequalizerCommutes E e' h' H')).
set (E := limits.coequalizers.mk_Coequalizer f g h H X).
use (mk_isCoequalizer C hs).
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 hs.
- 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 : C⟦a, b⟧) (e : C) (h : C⟦b, 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 := mk_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 hs.
- intros y T. cbn in T.
use (CoequalizerOutUnique C E).
exact T.
set (E := mk_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 hs.
- intros y T. cbn in T.
use (CoequalizerOutUnique C E).
exact T.
Definition equiv_Coequalizer1 {a b : C} (f g : C⟦a, b⟧) :
limits.coequalizers.Coequalizer f g -> Coequalizer C f g.
Show proof.
intros E.
exact (mk_Coequalizer
C f g _ _ _
(equiv_isCoequalizer1
(limits.coequalizers.CoequalizerObject E)
(limits.coequalizers.CoequalizerArrow E)
(limits.coequalizers.CoequalizerEqAr E)
(limits.coequalizers.isCoequalizer_Coequalizer E))).
exact (mk_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 : C⟦a, b⟧) :
limits.coequalizers.Coequalizer f g <- Coequalizer C f g.
Show proof.
intros E.
exact (@limits.coequalizers.mk_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 hs E))).
exact (@limits.coequalizers.mk_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 hs E))).
End coequalizers_coincide.