open import Cat.Instances.Shape.Terminal
open import Cat.Functor.Kan.Pointwise
open import Cat.Diagram.Colimit.Base
open import Cat.Instances.Functor
open import Cat.Functor.Kan.Base
open import Cat.Diagram.Initial
open import Cat.Functor.Adjoint
open import Cat.Functor.Compose
open import Cat.Instances.Comma
open import Cat.Functor.Base
open import Cat.Functor.Hom
open import Cat.Prelude

import Cat.Functor.Reasoning as Func
import Cat.Reasoning

module Cat.Functor.Kan.Nerve where

private
  variable o κ : Level
open Func
open _=>_
open is-lan

Nerve and realisation🔗

Let $F:\mathcal{C}\to \mathcal{D}$ be a functor from a $\kappa \text{-small}$ category $\mathcal{C}$ to a locally $\kappa \text{-small,}$ $\kappa \text{-}$cocomplete category $\mathcal{D}\text{.}$ $F$ induces a pair of adjoint functors, as in the diagram below, where $|-|⊣\mathbf{N}\text{.}$ In general, the left adjoint is called “realization”, and the right adjoint is called “nerve”.

An example to keep in mind is the inclusion $F:\Delta \hookrightarrow {\mathfrak{Cat}}_{\mathrm{strict}}$ from the simplex category to the category of strict categories, which sends the $n\text{-simplex}$ to the finite poset $[n]\text{.}$ In this case, the left adjoint is the ordinary realisation of a simplicial set $[{\Delta }^{\mathrm{op}},\mathbf{Sets}]$ as a strict category, and the right adjoint gives the simplicial nerve of a strict category.

Since these adjunctions come for very cheap ($\kappa \text{-cocompleteness}$ of the codomain category is all we need), they are built out of very thin abstract nonsense: The “realisation” left adjoint is given by the left Kan extension of $F$ along the Yoneda embedding $よ\text{,}$ which can be computed as a particular colimit, and the “nerve” right adjoint is given by the restricted Yoneda embedding functor $X\mapsto \mathbf{Hom}(F(-),X)\text{.}$

module _
  {o κ} {C : Precategory κ κ} {D : Precategory o κ}
  (F : Functor C D)
  where
    private
      module C = Cat.Reasoning C
      module D = Cat.Reasoning D
      module F = Func F

    Nerve : Functor D (PSh κ C)
    Nerve .F₀ c = Hom-into D c F∘ Functor.op F
    Nerve .F₁ f = よ₁ D f ◂ (Functor.op F)
    Nerve .F-id = ext λ _ _ → D.idl _
    Nerve .F-∘ _ _ = ext λ _ _ → sym (D.assoc _ _ _)

The action of $F$ on morphisms assembles into a natural transformation ${よ}_{\mathcal{C}}\Rightarrow \mathrm{Nerve}(F)F\text{,}$ which is universal in the following sense: the nerve functor associated to $F$ is the left Kan extension of $\mathcal{C}\text{’s}$ yoneda embedding along $F\text{.}$

    coapprox : よ C => Nerve F∘ F
    coapprox .η x .η y f            = F.₁ f
    coapprox .η x .is-natural _ _ _ = ext λ _   → F.F-∘ _ _
    coapprox .is-natural _ _ _      = ext λ _ _ → F.F-∘ _ _

If we’re given a functor $M:\mathcal{D}\to \mathrm{PSh}(\mathcal{C})$ and natural transformation ${よ}_{\mathcal{C}}\to MF\text{,}$ we can produce a natural transformation $\alpha :\mathrm{Nerve}(F)\to M$ using $M\text{’s}$ own action on morphisms, since — in components — we have to transform an element of $f:\mathbf{Hom}(Fc,d)$ into one of $M(d)(c)\text{.}$ Using $\alpha \text{,}$ we obtain an element of $M(Fc)(c)\text{,}$ which maps under $M(f)$ to what we want.

    Nerve-is-lan : is-lan F (よ C) Nerve coapprox
    Nerve-is-lan .σ {M = M} α .η d .η c f =
      M .F₁ f .η c (α .η c .η c C.id)

    Nerve-is-lan .σ {M = M} α .η d .is-natural x y f = funext λ g →
      M.₁ (g D.∘ F.₁ f) .η y (α .η y .η y C.id)          ≡⟨ M.F-∘ g (F .F₁ f) ηₚ _ $ₚ _ ⟩≡
      M.₁ g .η y (M .F₁ (F.₁ f) .η y (α .η y .η y C.id)) ≡˘⟨ ap (M.F₁ g .η y) (α .is-natural _ _ _ ηₚ _ $ₚ _) ⟩≡˘
      M.₁ g .η y (α .η x .η y ⌜ f C.∘ C.id ⌝)            ≡⟨ ap! C.id-comm ⟩≡
      M.₁ g .η y (α .η x .η y (C.id C.∘ f))              ≡⟨ ap (M.₁ g .η y) (α .η _ .is-natural _ _ _ $ₚ _) ⟩≡
      M.₁ g .η y (M.₀ (F.₀ x) .F₁ f (α .η x .η x C.id))  ≡⟨ M.₁ g .is-natural _ _ _ $ₚ _ ⟩≡
      M.₀ d .F₁ f (M.₁ g .η x (α .η x .η x C.id))        ∎
      where module M = Functor M

    Nerve-is-lan .σ {M = M} α .is-natural x y f = ext λ z g →
      M .F-∘ f g ηₚ _ $ₚ _

    Nerve-is-lan .σ-comm {M = M} {α = α} = ext λ x y f →
      M.₁ (F.₁ f) .η y (α .η y .η y C.id) ≡˘⟨ α .is-natural _ _ _ ηₚ _ $ₚ _ ⟩≡˘
      α .η x .η y (f C.∘ C.id)            ≡⟨ ap (α .η x .η y) (C.idr _) ⟩≡
      α .η x .η y f                       ∎
      where module M = Functor M

    Nerve-is-lan .σ-uniq {M = M} {α = α} {σ' = σ'} p = ext λ x y f →
      M.₁ f .η y (α .η y .η y C.id)          ≡⟨ ap (M.₁ f .η y) (p ηₚ _ ηₚ _ $ₚ _) ⟩≡
      M.₁ f .η y (σ' .η _ .η y ⌜ F.₁ C.id ⌝) ≡⟨ ap! F.F-id ⟩≡
      M.₁ f .η y (σ' .η _ .η y D.id)         ≡˘⟨ σ' .is-natural _ _ _ ηₚ _ $ₚ _ ⟩≡˘
      σ' .η x .η y (f D.∘ D.id)              ≡⟨ ap (σ' .η x .η y) (D.idr _) ⟩≡
      σ' .η x .η y f                         ∎
      where module M = Functor M

module _
  {o κ κ'} {C : Precategory κ κ} {D : Precategory o κ'}
  (F : Functor C D)
  (cocompl : is-cocomplete κ κ D)
  where

Since we have assumed $\mathcal{C}$ is $\kappa \text{-small}$ and $\mathcal{D}$ is $\kappa \text{-cocomplete,}$ any functor $F:\mathcal{C}\to \mathcal{D}$ admits an extension ${\mathrm{Lan}}_{よ}(F)\text{.}$ This instance of generalised abstract nonsense is the left adjoint we were after, the “realisation” functor.

  Realisation : Functor (PSh κ C) D
  Realisation = Lan.Ext (cocomplete→lan (よ C) F cocompl)

  approx : F => Realisation F∘ よ C
  approx = Lan.eta (cocomplete→lan (よ C) F cocompl)

  Realisation-is-lan : is-lan (よ C) F Realisation approx
  Realisation-is-lan = Lan.has-lan (cocomplete→lan (よ C) F cocompl)

module _
  {o κ} {C : Precategory κ κ} {D : Precategory o κ}
  (F : Functor C D)
  (cocompl : is-cocomplete κ κ D)
  where

  private
    module C = Cat.Reasoning C
    module D = Cat.Reasoning D
    module F = Func F

    module ↓colim c' =
      comma-colimits→lan.↓colim (よ C) F (λ c'' → cocompl (F F∘ Dom (よ C) (!Const c''))) c'

  Realisation⊣Nerve : Realisation F cocompl ⊣ Nerve F
  Realisation⊣Nerve = adj where
    open _⊣_
    open ↓Obj
    open ↓Hom

Recall that ${\mathrm{Lan}}_{よ}(F)(P)$ is defined pointwise as the colimit under the diagram

where we can identify ${よ}_{\mathcal{C}}\downarrow P$ with the category of elements of the presheaf $P\text{.}$ Any object $i:\mathcal{C}$ with section $P(i)$ defines an object of this category, which in the proof below we denote elem.

    elem : (P : Functor (C ^op) (Sets κ)) (i : C.Ob)
         → (arg : P ʻ i) → ↓Obj (よ C) (!Const P)
    elem P i arg .x = i
    elem P i arg .y = tt
    elem P i arg .map .η j h = P .F₁ h arg
    elem P i arg .map .is-natural _ _ f = ext λ _ → P .F-∘ _ _ $ₚ _

The adjunction unit is easiest to describe: we must come up with a map $F(i)\to {\mathrm{Lan}}_{よ}(F)(P)\text{,}$ in the context of an object $i:\mathcal{C}$ and section $a:P(i)\text{.}$ This is an object in the diagram that we took a colimit over, so the coprojection $\psi$ has a component expressing precisely what we need. Naturality is omitted from this page for brevity, but it follows from $\psi \text{’s}$ universal property.

    adj : Realisation F cocompl ⊣ Nerve F
    adj .unit .η P .η i a = ↓colim.ψ P (elem P i a)

In the other direction, we’re mapping out of a colimit, into an arbitrary object $o:\mathcal{D}\text{.}$ It will suffice to come up with a family of compatible maps $F(j)\to o\text{,}$ where $j$ is an object in the comma category

These, by definition, come with (natural) functions ${\mathbf{Hom}}_{\mathcal{C}}(-,j)\to {\mathbf{Hom}}_{\mathcal{D}}(F-,o)\text{,}$ which we can evaluate at the identity morphism to get the map we want. That this assembles into a map from the colimit follows from that same naturality:

    adj .counit .η ob = ↓colim.universal _ (λ j → j .map .η _ C.id) comm
      where abstract
      comm
        : ∀ {x y} (f : ↓Hom (よ C) (!Const (Nerve F .F₀ ob)) x y)
        → y .map .η _ C.id D.∘ F.₁ (f .α) ≡ x .map .η _ C.id
      comm {x} {y} f =
        y .map .η _ C.id D.∘ F.₁ (f .α) ≡˘⟨ y .map .is-natural _ _ _ $ₚ _ ⟩≡˘
        y .map .η _ (C.id C.∘ f .α)     ≡⟨ ap (y .map .η _) C.id-comm-sym ⟩≡
        y .map .η _ (f .α C.∘ C.id)     ≡⟨ f .sq ηₚ _ $ₚ _ ⟩≡
        x .map .η (x .↓Obj.x) C.id      ∎

Naturality of this putative counit follows from the uniqueness of maps from a colimit, and the triangle identities follow because, essentially, “matching” on a colimit after applying one of the coprojections does the obvious thing.

    adj .unit .η P .is-natural x y f =
      funext λ _ → sym $ ↓colim.commutes P $ ↓hom (ext λ _ _ → P .F-∘ _ _ $ₚ _)
    adj .unit .is-natural x y f = ext λ i arg → sym $
        ↓colim.factors _ {j = elem x i arg} _ _
      ∙ ap (↓colim.ψ _) (↓Obj-path _ _ refl refl
          (ext λ _ _ → f .is-natural _ _ _ $ₚ _))

    adj .counit .is-natural x y f = ↓colim.unique₂ _ _
      (λ {x'} {y'} f →
        D.pullr (sym (y' .map .is-natural _ _ _ $ₚ _)
                  ∙ ap (y' .map .η _) C.id-comm-sym)
        ∙ ap (_ D.∘_) (f .sq ηₚ _ $ₚ C.id))
      (λ j →
        D.pullr (↓colim.factors _ _ _)
        ∙ ↓colim.factors _ _ _)
      (λ j → D.pullr (↓colim.factors _ _ _))

    adj .zig {A} = ↓colim.unique₂ A _ (λ f → ↓colim.commutes _ f)
      (λ j →
          D.pullr (↓colim.factors _ _ _)
        ∙ ↓colim.factors _ _ _
        ∙ ap (↓colim.ψ _)
            (↓Obj-path _ _ refl refl
              (ext λ _ _ →
                  sym (j .map .is-natural _ _ _ $ₚ _)
                ∙ ap (j .map .η _) (C.idl _))))
      (λ j → D.idl _)
    adj .zag {d} = ext λ c f →
      ↓colim.factors (Nerve F .F₀ d) {j = elem _ c f} _ _
      ∙ F.elimr refl