module Cat.Bi.Diagram.Colimit.IndexedCategory {o h o' h'} {I : Precategory o h} (F : Pseudofunctor (Locally-discrete (I ^op)) (Cat (o ⊔ o') (h ⊔ h'))) where
Lax colimits of indexed categories🔗
An especially important case of lax colimits are those of indexed categories, i.e., contravariant pseudofunctors from a locally discrete bicategory into For an indexed category the lax colimit of coincides with the Grothendieck construction which we show in this module.
open Pseudofunctor open Modification open Cr.Inverses open Functor open Cr._≅_ open _=>ₗ_ open _=>_ private module I = Precategory I module F = Indexed-category F module F₀ {x} = Cr (F.₀ x) module G = Cr (∫ F.displayed) module Cat = Br (Cat (o ⊔ o') (h ⊔ h')) open Dr F.displayed
To construct the universal cocone, we use the canonical inclusion functors from the fibre categories of into The naturality 2-cells are straightforward to define, and we did so already off-screen.
univ-cocone : opᵖ F .lax =>ₒ ConstP F.∫ .lax univ-cocone .σ a = F.ιᶠ a univ-cocone .naturator .η f = nat-unidl-to (F.ιᶠ-base-change f)
Verifying that this data satisfies the required naturality and compatibility requirements is tedious but straightforward in principle, so we elide the details.
univ-cocone .naturator .is-natural f g reflᵢ = nat-unidl-to (F.ιᶠ-base-change f) ∘nt (_ ▸ F.₂ reflᵢ) ≡⟨ Cat.Hom.elimr (Fr.elim (postaction (Cat _ _) _) F.P₁.F-id) ⟩≡ nat-unidl-to (F.ιᶠ-base-change f) ≡⟨ Cat.Hom.introl Cat.◀.F-id ⟩≡ (idnt ◂ _) ∘nt nat-unidl-to (F.ιᶠ-base-change f) ∎ univ-cocone .ν-compositor f g = ext λ _ → sym $ let p : id' ∘' id' ≡ (id' F₀.∘ F.γ← _ .η _) ∘' id' F₀.∘ F.γ→ _ .η _ p = cast[] (idr' _ ∙[] F₀.insertr (F.γ≅' .invr) ∙[] symP F.cancel-id') in G.eliml (G.idl _) ∙ G.idl _ ∙∙ G.cdr (G.idl _ ∙ G.cdr (sym (G.idr _) ∙ Fr.weave (ιᶠ _ _) (F₀.cdr p))) ∙∙ sym (G.pushl3 (F.ιᶠ-base-change-comp f g ηₚ _)) univ-cocone .ν-unitor = ext λ _ → Fr.weave (ιᶠ _ _) (F₀.cdr (cast[] (F.cancel-id' ∙[] F₀.idl _ ∙[] symP (idr' _)))) ∙ G.introl (G.idl _)
To show that this cocone is universal, we must show that for any other lax cocone with apex we can construct a functor which factors the other cocone through the universal one.
module _ (X : Precategory (o ⊔ o') (h ⊔ h')) where
open Cr X hiding (invl ; invr) private module Ox = IndexedOplax {F = opᵖ F} {ConstP X} ν-unitor' : ∀ (α : ⌞ Pseudoₒ[ opᵖ F , ConstP X ] ⌟ ) {i} y → α .ν→ I.id .η y ∘ α .σ i .F₁ (F.υ→ .η _) ≡ id ν-unitor' α y = Ox.ν-unitor α y ∙ idr _
cocone→mediator₀ : opᵖ F .lax =>ₒ ConstP X .lax → Functor F.∫ X cocone→mediator₀ α = funct where
Assume that we are given a lax cocone This is an oplax transformation with functor components for each Since an object of bundles an with some we can use to map into giving us the object mapping we need.
module α = _=>ₗ_ α funct : Functor F.∫ X funct .F₀ (x , Fx) = α.σ x .F₀ Fx
For the morphism mapping, we are given in together with some with and and we must produce a morphism Taking gets us almost all of the way. To complete the definition, we need a morphism in but note that since is a transformation from to and sends all morphisms to the identity functor on this is exactly a component of naturator.
funct .F₁ {x , Fx} {y , Fy} (∫hom f Ff) = α.ν→ f .η Fy ∘ α.σ x .F₁ Ff
We can check that this gives a functorial assignment using the coherence identities of
funct .F-id {x , Fx} = ν-unitor' α Fx funct .F-∘ {x , Fx} {y , Fy} {z , Fz} (∫hom f Ff) (∫hom g Fg) = α.ν→ (f I.∘ g) .η Fz ∘ α.σ x .F₁ (Ff ∘' Fg) ≡⟨ cdr (sym $ Fr.collapse3 (α.σ x) refl) ⟩≡ α.ν→ (f I.∘ g) .η Fz ∘ α.σ x .F₁ (F.γ→ (g , f) .η Fz) ∘ _ ≡⟨ extendl (Ox.ν-compositor α f g Fz ∙ eliml (idl _)) ⟩≡ α.ν→ f .η Fz ∘ α.ν→ g .η _ ∘ α.σ x .F₁ (F.₁ g .F₁ Ff) ∘ α.σ x .F₁ Fg ≡⟨ cdr (extendl (α.ν→ g .is-natural _ _ _)) ∙ assoc _ _ _ ⟩≡ (α.ν→ f .η Fz ∘ α.σ y .F₁ Ff) ∘ α.ν→ g .η Fy ∘ α.σ x .F₁ Fg ∎
Furthermore, this assignment of cocones to functors itself extends to a functor from the category of oplax transformations from to to the functor category
cocone→mediator : Functor Pseudoₒ[ opᵖ F , ConstP X ] Cat[ F.∫ , X ] cocone→mediator .F₀ = cocone→mediator₀
The morphism mapping of this functor acts on modifications between cones, and produces a natural transformation of induced functors. This means that at each object we must give a component morphism in But unwrapping the definitions, we see that these are just the components of
cocone→mediator .F₁ γ .η (x , Fx) = γ .Γ x .η Fx
Naturality follows from the naturality of and functoriality turns out to be trivial.
cocone→mediator .F₁ {α} {β} γ .is-natural (x , Fx) (y , Fy) (∫hom f Ff) = γ .Γ y .η Fy ∘ α .ν→ f .η Fy ∘ α .σ x .F₁ Ff ≡˘⟨ extendl (γ .is-natural ηₚ Fy) ⟩≡˘ β .ν→ f .η Fy ∘ γ .Γ x .η (F.₁ f .F₀ Fy) ∘ α .σ x .F₁ Ff ≡⟨ pushr (γ .Γ x .is-natural _ _ _) ⟩≡ (β .ν→ f .η Fy ∘ β .σ x .F₁ Ff) ∘ γ .Γ x .η Fx ∎ cocone→mediator .F-id = ext λ _ → refl cocone→mediator .F-∘ γ δ = ext λ _ → refl
The final step is to show that the functor produced by cocone→mediator factors
essentially uniquely through the universal cocone. Formally, we must
prove that it forms an equivalence of categories together with
the functor which maps a functor
to the lax cocone defined by pullback through the universal cocone.
private hom→cocone' = hom→cocone₀ {h' = lzero} {o' ⊔ h'} F F.∫ univ-cocone X
This equivalence holds essentially by definition, but we must pass through some fairly tedious bureaucracy to establish it. These proofs mostly consist of eliminating identity morphisms, but the terms involved get very big, and we have to construct layered natural transformations and modifications.
cocone→mediator-unit : Id ≅ⁿ hom→cocone' F∘ cocone→mediator cocone→mediator-unit = to-natural-iso ni where abstract cocone-factors : ∀ (α : ⌞ Pseudoₒ[ opᵖ F , ConstP X ] ⌟ ) {a b} {f : I.Hom b a} i → α .ν→ f .η i ≡ (hom→cocone' F∘ cocone→mediator) .F₀ α .ν→ f .η i cocone-factors α i = sym $ idl _ ∙∙ eliml (idl _) ∙∙ idl _ ∙∙ idr _ ∙∙ elimr (α .σ _ .F-id) ni : make-natural-iso _ _ ni .make-natural-iso.eta α .Γ a .η _ = id ni .make-natural-iso.eta α .Γ a .is-natural _ _ _ = pushl (sym (ν-unitor' α _)) ∙∙ sym (cdr (α .σ a .F-∘ _ _)) ∙∙ sym (idr _) ni .make-natural-iso.eta α .is-natural = ext λ i → idr _ ∙∙ sym (cocone-factors α i) ∙∙ sym (idl _) ni .make-natural-iso.inv α .Γ a .η _ = id ni .make-natural-iso.inv α .Γ a .is-natural _ _ _ = idl _ ∙ cdr (α .σ a .F-∘ _ _) ∙∙ cancell (ν-unitor' α _) ∙∙ sym (idr _) ni .make-natural-iso.inv α .is-natural {b = b} = ext λ i → idr _ ∙∙ cocone-factors α i ∙∙ sym (idl _) ni .make-natural-iso.eta∘inv _ = ext λ _ _ → idl _ ni .make-natural-iso.inv∘eta _ = ext λ _ _ → idl _ ni .make-natural-iso.natural _ α f = ext λ _ _ → idr _ ∙ car (ν-unitor' α _) cocone→mediator-counit : cocone→mediator F∘ hom→cocone' ≅ⁿ Id cocone→mediator-counit = to-natural-iso ni where mediator-stable : ∀ (G : Functor F.∫ X) {a b} (f : G.Hom a b) → (cocone→mediator F∘ hom→cocone') .F₀ G .F₁ f ≡ G .F₁ f mediator-stable G (∫hom f Ff) = car (idl _ ∙ eliml (idl _) ∙∙ idl _ ∙∙ idr _) ∙ Fr.collapse G (∫Hom-path _ (I.idr _) $ cast[] $ F.cancel-id' ∙[] F₀.idl _) ni : make-natural-iso _ _ ni .make-natural-iso.eta G .η _ = id ni .make-natural-iso.eta G .is-natural _ _ f = idl _ ∙∙ mediator-stable G f ∙∙ sym (idr _) ni .make-natural-iso.inv G .η _ = id ni .make-natural-iso.inv G .is-natural _ _ f = idl _ ∙∙ sym (mediator-stable G f) ∙∙ sym (idr _) ni .make-natural-iso.eta∘inv _ = ext λ _ → idl _ ni .make-natural-iso.inv∘eta _ = ext λ _ → idl _ ni .make-natural-iso.natural G H α = ext λ _ → idr _ ∙ introl (H .F-id) ∙ sym (idl _) cocone→mediator⊣ : cocone→mediator ⊣ hom→cocone' cocone→mediator⊣ ._⊣_.unit = cocone→mediator-unit .to cocone→mediator⊣ ._⊣_.counit = cocone→mediator-counit .to cocone→mediator⊣ ._⊣_.zig = ext λ _ → idl _ cocone→mediator⊣ ._⊣_.zag {G} = ext λ _ _ → idr _ ∙ eliml (G .F-id)
Finally, we can state the promised result: the lax colimit of is given by
cocone→mediator-equiv : is-equivalence cocone→mediator cocone→mediator-equiv .is-equivalence.F⁻¹ = hom→cocone' cocone→mediator-equiv .is-equivalence.F⊣F⁻¹ = cocone→mediator⊣ cocone→mediator-equiv .is-equivalence.has-is-equivalence = record where unit-iso α = Cr.iso→invertible Laxₒ[ _ , _ ] (isoⁿ→iso cocone→mediator-unit α) counit-iso G = Cr.iso→invertible Cat[ _ , _ ] (isoⁿ→iso cocone→mediator-counit G) ∫-colim : is-lax-colimit {h' = lzero} {o' ⊔ h'} F F.∫ univ-cocone ∫-colim X = is-equivalenceᶜ→is-equivalence $ is-equivalence.inverse-equivalence (cocone→mediator-equiv X)