Timings for Colimit.v
Require Import Basics Types.
Require Import Diagrams.Diagram.
Require Import Diagrams.Graph.
Require Import Diagrams.Cocone.
Require Import Diagrams.ConstantDiagram.
Require Import Diagrams.CommutativeSquares.
Require Import Colimits.Coeq.
Local Open Scope path_scope.
Generalizable All Variables.
(** This file contains the definition of colimits, and functoriality results on colimits. *)
(** * Colimits *)
(** ** Abstract definition *)
(** A colimit is the extremity of a cocone. *)
Class IsColimit `(D: Diagram G) (Q: Type) := {
iscolimit_cocone :: Cocone D Q;
iscolimit_unicocone : UniversalCocone iscolimit_cocone;
}.
Coercion iscolimit_cocone : IsColimit >-> Cocone.
Arguments Build_IsColimit {G D Q} C H : rename.
Arguments iscolimit_cocone {G D Q} C : rename.
Arguments iscolimit_unicocone {G D Q} H : rename.
(** [cocone_postcompose_inv] is defined for convenience: it is only the inverse of [cocone_postcompose]. It allows to recover the map [h] from a cocone [C']. *)
Definition cocone_postcompose_inv `{D: Diagram G} {Q X}
(H : IsColimit D Q) (C' : Cocone D X) : Q -> X
:= @equiv_inv _ _ _ (iscolimit_unicocone H X) C'.
(** ** Existence of colimits *)
(** Every diagram has a colimit. It could be described as the following HIT
<<
HIT Colimit {G : Graph} (D : Diagram G) : Type :=
| colim : forall i, D i -> Colimit D
| colimp : forall i j (f : G i j) (x : D i) : colim j (D _f f x) = colim i x
.
>>
but we instead describe it as the coequalizer of the source and target maps of the diagram. The source type in the coequalizer ought to be:
<<
{x : sig D & {y : sig D & {f : G x.1 y.1 & D _f f x.2 = y.2}}}
>>
However we notice that the path type forms a contractible component, so we can use the more efficient:
<<
{x : sig D & {j : G & G x.1 j}}
>>
*)
Definition Colimit {G : Graph} (D : Diagram G) : Type :=
@Coeq
{x : sig D & {j : G & G x.1 j}}
(sig D)
(fun t => t.1)
(fun t => (t.2.1; D _f t.2.2 t.1.2))
.
Definition colim {G : Graph} {D : Diagram G} (i : G) (x : D i) : Colimit D :=
coeq (i ; x).
Definition colimp {G : Graph} {D : Diagram G} (i j : G) (f : G i j) (x : D i)
: colim j (D _f f x) = colim i x
:= (cglue ((i; x); j; f))^.
(** To obtain a path [colim j (D _f f x) = colim j (D _f f y)] from a path [x = y], one can either use [ap (D _f f)] followed by [ap (colim j)], or conjugate [ap (colim i)] by [colimp i j f]. These paths are equivalent. *)
Definition ap_colim_homotopic {G : Graph} {D : Diagram G} {i j : G} (f : G i j) {x y : D i} (p : x = y)
: ap (colim j) (ap (D _f f) p)
= colimp i j f x @ ap (colim i) p @ (colimp i j f y)^.
exact (ap_homotopic (colimp _ _ _) p).
Definition Colimit_ind {G : Graph} {D : Diagram G} (P : Colimit D -> Type)
(q : forall i x, P (colim i x))
(pp_q : forall (i j : G) (g: G i j) (x : D i),
(@colimp G D i j g x) # (q j (D _f g x)) = q i x)
: forall w, P w.
Definition Colimit_ind_beta_colimp {G : Graph} {D : Diagram G}
(P : Colimit D -> Type) (q : forall i x, P (colim i x))
(pp_q : forall (i j: G) (g: G i j) (x: D i),
@colimp G D i j g x # q _ (D _f g x) = q _ x)
(i j : G) (g : G i j) (x : D i)
: apD (Colimit_ind P q pp_q) (colimp i j g x) = pp_q i j g x.
refine (Coeq_ind_beta_cglue _ _ _ _ @ _).
apply moveL_transport_p_V.
Definition Colimit_rec {G : Graph} {D : Diagram G} (P : Type) (C : Cocone D P)
: Colimit D -> P.
srapply (Colimit_ind _ C).
refine (transport_const _ _ @ _).
Definition Colimit_rec_beta_colimp {G : Graph} {D : Diagram G}
(P : Type) (C : Cocone D P) (i j : G) (g: G i j) (x: D i)
: ap (Colimit_rec P C) (colimp i j g x) = legs_comm C i j g x.
rapply (cancelL (transport_const (colimp i j g x) _)).
srapply ((apD_const (Colimit_ind (fun _ => P) C _) (colimp i j g x))^ @ _).
exact (Colimit_ind_beta_colimp (fun _ => P) C _ i j g x).
Arguments colim : simpl never.
Arguments colimp : simpl never.
(** The natural cocone to the colimit. *)
Definition cocone_colimit {G : Graph} (D : Diagram G) : Cocone D (Colimit D)
:= Build_Cocone colim colimp.
(** Given a cocone [C] and [f : Colimit D -> P] inducing a "homotopic" cocone, [Colimit_rec P C] is homotopic to [f]. *)
Definition Colimit_rec_homotopy {G : Graph} {D : Diagram G} (P : Type) (C : Cocone D P)
(f : Colimit D -> P)
(h_obj : forall i, legs C i == f o colim i)
(h_comm : forall i j (g : G i j) x,
legs_comm C i j g x @ h_obj i x = h_obj j ((D _f g) x) @ ap f (colimp i j g x))
: Colimit_rec P C == f.
cbn beta; intros i j g x.
lhs napply (Colimit_rec_beta_colimp _ _ _ _ _ _ @@ 1).
(** "Homotopic" cocones induces homotopic maps. *)
Definition Colimit_rec_homotopy' {G : Graph} {D : Diagram G} (P : Type) (C1 C2 : Cocone D P)
(h_obj : forall i, legs C1 i == legs C2 i)
(h_comm : forall i j (g : G i j) x,
legs_comm C1 i j g x @ h_obj i x = h_obj j (D _f g x) @ legs_comm C2 i j g x)
: Colimit_rec P C1 == Colimit_rec P C2.
snapply Colimit_rec_homotopy.
rhs napply (1 @@ Colimit_rec_beta_colimp _ _ _ _ _ _).
(** [Colimit_rec] is an equivalence. *)
Instance isequiv_colimit_rec `{Funext} {G : Graph}
{D : Diagram G} (P : Type)
: IsEquiv (Colimit_rec (D:=D) P).
srapply isequiv_adjointify.
exact (cocone_postcompose (cocone_colimit D)).
snapply Colimit_rec_homotopy.
apply Colimit_rec_beta_colimp.
Definition equiv_colimit_rec `{Funext} {G : Graph} {D : Diagram G} (P : Type)
: Cocone D P <~> (Colimit D -> P) := Build_Equiv _ _ _ (isequiv_colimit_rec P).
(** It follows that the HIT Colimit is an abstract colimit. *)
Instance unicocone_colimit `{Funext} {G : Graph} (D : Diagram G)
: UniversalCocone (cocone_colimit D).
srapply Build_UniversalCocone; intro Y.
(* The goal is to show that [cocone_postcompose (cocone_colimit D)] is an equivalence, but that's the inverse to the equivalence we just defined. *)
exact (isequiv_inverse (equiv_colimit_rec Y)).
Instance iscolimit_colimit `{Funext} {G : Graph} (D : Diagram G)
: IsColimit D (Colimit D)
:= Build_IsColimit _ (unicocone_colimit D).
(** ** Functoriality of concrete colimits *)
(** We will capitalize [Colimit] in the identifiers to indicate that these definitions relate to the concrete colimit defined above. Below, we will also get functoriality for abstract colimits, without the capital C. However, to apply those results to the concrete colimit uses [iscolimit_colimit], which requires [Funext], so it is also useful to give direct proofs of some facts. *)
(** We first work in a more general situation. Any diagram map [m : D1 => D2] induces a map between the canonical colimit of [D1] and any cocone over [D2]. We use "half" to indicate this situation. *)
Definition functor_Colimit_half {G : Graph} {D1 D2 : Diagram G} (m : DiagramMap D1 D2) {Q} (HQ : Cocone D2 Q)
: Colimit D1 -> Q.
exact (cocone_precompose m HQ).
Definition functor_Colimit_half_beta_colimp {G : Graph} {D1 D2 : Diagram G} (m : DiagramMap D1 D2) {Q} (HQ : Cocone D2 Q) (i j : G) (g : G i j) (x : D1 i)
: ap (functor_Colimit_half m HQ) (colimp i j g x) = legs_comm (cocone_precompose m HQ) i j g x
:= Colimit_rec_beta_colimp _ _ _ _ _ _.
(** Homotopic diagram maps induce homotopic maps. *)
Definition functor_Colimit_half_homotopy {G : Graph} {D1 D2 : Diagram G}
{m1 m2 : DiagramMap D1 D2} (h : DiagramMap_homotopy m1 m2)
{Q} (HQ : Cocone D2 Q)
: functor_Colimit_half m1 HQ == functor_Colimit_half m2 HQ.
destruct h as [h_obj h_comm].
snapply Colimit_rec_homotopy'.
Open Scope long_path_scope.
(* TODO: Most of the work here comes from a mismatch between the direction of the path in [DiagramMap_comm] and [legs_comm] in the [Cocone] record, causing a reversal in [cocone_precompose]. There is no reversal in [cocone_postcompose], so I think [Cocone] should change. If that is done, then this result wouldn't be needed at all, and one could directly use [Colimit_rec_homotopy']. *)
exact (concat_Ap (legs_comm HQ i j g) (h_obj i x))^.
Close Scope long_path_scope.
(** Now we specialize to the case where the second cone is a colimiting cone. *)
Definition functor_Colimit {G : Graph} {D1 D2 : Diagram G} (m : DiagramMap D1 D2)
: Colimit D1 -> Colimit D2
:= functor_Colimit_half m (cocone_colimit D2).
(** A homotopy between diagram maps [m1, m2 : D1 => D2] gives a homotopy between the induced maps. *)
Definition functor_Colimit_homotopy {G : Graph} {D1 D2 : Diagram G}
{m1 m2 : DiagramMap D1 D2} (h : DiagramMap_homotopy m1 m2)
: functor_Colimit m1 == functor_Colimit m2
:= functor_Colimit_half_homotopy h _.
(** Composition of diagram maps commutes with [functor_Colimit_half], provided the first map uses [functor_Colimit]. *)
Definition functor_Colimit_half_compose {G : Graph} {A B C : Diagram G} (f : DiagramMap A B) (g : DiagramMap B C) {Q} (HQ : Cocone C Q)
: functor_Colimit_half (diagram_comp g f) HQ == functor_Colimit_half g HQ o functor_Colimit f.
snapply Colimit_rec_homotopy.
Open Scope long_path_scope.
lhs napply (ap_V _ _ @@ 1).
lhs napply (inverse2 (ap_pp (HQ j) _ _) @@ 1).
lhs napply (inv_pp _ _ @@ 1).
lhs napply (ap_compose (functor_Colimit f)).
lhs napply (ap _ (Colimit_rec_beta_colimp _ _ _ _ _ _)).
(* [legs_comm] unfolds to a composite of paths, but the next line works best without unfolding it. *)
1: napply functor_Colimit_half_beta_colimp.
lhs_V napply (ap_compose (colim j)); simpl.
lhs napply (ap_V (HQ j o g j) _).
Close Scope long_path_scope.
(** ** Functoriality of abstract colimits *)
Section FunctorialityColimit.
Context `{Funext} {G : Graph}.
(** Colimits are preserved by composition with a (diagram) equivalence. *)
Definition iscolimit_precompose_equiv {D1 D2 : Diagram G}
(m : D1 ~d~ D2) {Q : Type}
: IsColimit D2 Q -> IsColimit D1 Q.
srapply (Build_IsColimit (cocone_precompose m HQ) _).
apply cocone_precompose_equiv_universality, HQ.
Definition iscolimit_postcompose_equiv {D: Diagram G} `(f: Q <~> Q')
: IsColimit D Q -> IsColimit D Q'.
srapply (Build_IsColimit (cocone_postcompose HQ f) _).
apply cocone_postcompose_equiv_universality, HQ.
(** A diagram map [m : D1 => D2] induces a map between any two colimits of [D1] and [D2]. *)
Definition functor_colimit {D1 D2 : Diagram G} (m : DiagramMap D1 D2)
{Q1 Q2} (HQ1 : IsColimit D1 Q1) (HQ2 : IsColimit D2 Q2)
: Q1 -> Q2 := cocone_postcompose_inv HQ1 (cocone_precompose m HQ2).
(** And this map commutes with diagram map. *)
Definition functor_colimit_commute {D1 D2 : Diagram G}
(m : DiagramMap D1 D2) {Q1 Q2}
(HQ1 : IsColimit D1 Q1) (HQ2: IsColimit D2 Q2)
: cocone_precompose m HQ2
= cocone_postcompose HQ1 (functor_colimit m HQ1 HQ2)
:= (eisretr (cocone_postcompose HQ1) _)^.
(** Additional coherence with postcompose and precompose. *)
Definition cocone_precompose_postcompose_comp {D1 D2 : Diagram G}
(m : DiagramMap D1 D2) {Q1 Q2 : Type} (HQ1 : IsColimit D1 Q1)
(HQ2 : IsColimit D2 Q2) {T : Type} (t : Q2 -> T)
: cocone_postcompose HQ1 (t o functor_colimit m HQ1 HQ2)
= cocone_precompose m (cocone_postcompose HQ2 t).
lhs napply cocone_postcompose_comp.
lhs_V exact (ap (fun x => cocone_postcompose x t)
(functor_colimit_commute m HQ1 HQ2)).
napply cocone_precompose_postcompose.
(** In order to show that colimits are functorial, we show that this is true after precomposing with the cocone. *)
Definition postcompose_functor_colimit_compose {D1 D2 D3 : Diagram G}
(m : DiagramMap D1 D2) (n : DiagramMap D2 D3)
{Q1 Q2 Q3} (HQ1 : IsColimit D1 Q1) (HQ2 : IsColimit D2 Q2)
(HQ3 : IsColimit D3 Q3)
: cocone_postcompose HQ1 (functor_colimit n HQ2 HQ3 o functor_colimit m HQ1 HQ2)
= cocone_postcompose HQ1 (functor_colimit (diagram_comp n m) HQ1 HQ3).
lhs napply cocone_precompose_postcompose_comp.
lhs_V napply (ap _ (functor_colimit_commute n HQ2 HQ3)).
lhs napply cocone_precompose_comp.
napply functor_colimit_commute.
Definition functor_colimit_compose {D1 D2 D3 : Diagram G}
(m : DiagramMap D1 D2) (n : DiagramMap D2 D3)
{Q1 Q2 Q3} (HQ1 : IsColimit D1 Q1) (HQ2 : IsColimit D2 Q2)
(HQ3 : IsColimit D3 Q3)
: functor_colimit n HQ2 HQ3 o functor_colimit m HQ1 HQ2
= functor_colimit (diagram_comp n m) HQ1 HQ3
:= @equiv_inj _ _
(cocone_postcompose HQ1) (iscolimit_unicocone HQ1 Q3) _ _
(postcompose_functor_colimit_compose m n HQ1 HQ2 HQ3).
(** ** Colimits of equivalent diagrams *)
(** Now we have that two equivalent diagrams have equivalent colimits. *)
Context {D1 D2 : Diagram G} (m : D1 ~d~ D2) {Q1 Q2}
(HQ1 : IsColimit D1 Q1) (HQ2 : IsColimit D2 Q2).
Definition functor_colimit_eissect
: functor_colimit m HQ1 HQ2
o functor_colimit (diagram_equiv_inv m) HQ2 HQ1 == idmap.
srapply (equiv_inj (cocone_postcompose HQ2) _).
2:symmetry; apply cocone_postcompose_identity.
1: apply cocone_postcompose_comp.
rewrite eisretr, cocone_precompose_postcompose, eisretr.
rewrite cocone_precompose_comp, diagram_inv_is_section.
apply cocone_precompose_identity.
Definition functor_colimit_eisretr
: functor_colimit (diagram_equiv_inv m) HQ2 HQ1
o functor_colimit m HQ1 HQ2 == idmap.
srapply (equiv_inj (cocone_postcompose HQ1) _).
2:symmetry; apply cocone_postcompose_identity.
1: apply cocone_postcompose_comp.
rewrite eisretr, cocone_precompose_postcompose, eisretr.
rewrite cocone_precompose_comp, diagram_inv_is_retraction.
apply cocone_precompose_identity.
#[export] Instance isequiv_functor_colimit
: IsEquiv (functor_colimit m HQ1 HQ2)
:= isequiv_adjointify _ _
functor_colimit_eissect functor_colimit_eisretr.
Definition equiv_functor_colimit : Q1 <~> Q2
:= Build_Equiv _ _ _ isequiv_functor_colimit.
End FunctorialityColimit.
(** ** Unicity of colimits *)
(** A particular case of the functoriality result is that all colimits of a diagram are equivalent (and hence equal in presence of univalence). *)
Theorem colimit_unicity `{Funext} {G : Graph} {D : Diagram G} {Q1 Q2 : Type}
(HQ1 : IsColimit D Q1) (HQ2 : IsColimit D Q2)
: Q1 <~> Q2.
srapply equiv_functor_colimit.
srapply (Build_diagram_equiv (diagram_idmap D)).
(** ** Colimits are left adjoint to constant diagram *)
Theorem colimit_adjoint `{Funext} {G : Graph} {D : Diagram G} {C : Type}
: (Colimit D -> C) <~> DiagramMap D (diagram_const C).
refine (equiv_colimit_rec C oE _).
apply equiv_diagram_const_cocone.