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

import Cat.Functor.Reasoning as Functor-kit
import Cat.Reasoning

module Cat.Functor.Kan.Nerve where

Nerve and realisation🔗

Let F:CDF : \ca{C} \to \ca{D} be a functor from a κ\kappa-small category C\ca{C} to a locally κ\kappa-small, κ\kappa-cocomplete category D\ca{D}. FF induces a pair of adjoint functors, as in the diagram below, where N|-| \dashv \bf{N}. 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:ΔCatstrictF : \Delta \mono \strcat from the simplex category to strict categories, which sends the nn-simplex to the finite poset [n][n]. In this case, the left adjoint is the ordinary realisation of a simplicial set [Δop,Sets][\Delta\op,\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-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 FF along the Yoneda embedding \yo, which can be computed as a particular colimit, and the “nerve” right adjoint is given by the restricted Yoneda embedding functor XHom(F(),X)X \mapsto \hom(F(-), X).

  Nerve : {D : Precategory κ κ}  Functor D C  Functor C (PSh κ D)
  Nerve F .F₀ x .F₀ y    = el (C.Hom (F .F₀ y) x) (C.Hom-set _ _)
  Nerve F .F₀ x .F₁ f g  = g C.∘ F .F₁ f
  Nerve F .F₀ x .F-id    = funext λ x  C.elimr (F .F-id)
  Nerve F .F₀ x .F-∘ f g = funext λ x  C.pushr (F .F-∘ _ _)

  Nerve F .F₁ f .η _ g            = f C.∘ g
  Nerve F .F₁ _ .is-natural _ _ _ = funext λ _  C.assoc _ _ _

  Nerve F .F-id    = Nat-path λ _  funext λ _  C.idl _
  Nerve F .F-∘ f g = Nat-path λ _  funext λ _  sym (C.assoc _ _ _)

The realisation left adjoint is constructed by general abstract nonsense.

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

  Realisation⊣Nerve
    : {D : Precategory κ κ} (F : Functor D C)
     Realisation F  Nerve F

The construction of the nerve-realisation adjunction is done below in components, but understanding it is not necessary: Either ponder the ΔCatstrict\Delta \mono \strcat example from above, or take it as a foundational assumption. However, if you’re feeling particularly brave, feel free to look at the code. Godspeed.

  Realisation⊣Nerve {D = D} F = adj where
    module D = Cat.Reasoning D
    open _⊣_
    open ↓Obj
    open ↓Hom
    module F = Functor-kit F

    hom′ : (P : Functor (D ^op) (Sets κ)) (i : D.Ob)
          (arg :  P .F₀ i )
          ↓Obj ( D) _
    hom′ P i arg .x = i
    hom′ P i arg .y = tt
    hom′ P i arg .map .η j h = P .F₁ h arg
    hom′ P i arg .map .is-natural _ _ f = funext λ _  happly (P .F-∘ _ _) _

    cocone′ :  ob  Cocone (F F∘ Dom ( D) (const! (Nerve F .F₀ ob)))
    cocone′ ob .coapex = ob
    cocone′ ob .ψ obj = obj .map .η _ D.id
    cocone′ ob .commutes {x} {y} f =
      happly (sym (y .map .is-natural _ _ _)) _
       ap (y .map .η (x .↓Obj.x)) (sym D.id-comm)
       happly (ap  e  e .η (x .↓Obj.x)) (f .sq)) _

Before proceeding, take a moment to appreciate the beauty of the adjunction unit and counit, and you’ll see that it makes sense that nerve and realisation are adjoints: The unit is given by the coprojections defining the left Kan extension as a colimit, and the counit is given by the unique “colimiting” map from that colimit.

    adj : Realisation F  Nerve F
    adj .unit .η P .η i arg = cocompl _ .bot .ψ (hom′ P i arg)
    adj .counit .η ob       = cocompl _ .has⊥ (cocone′ ob) .centre .hom

    adj .unit .η P .is-natural x y f = funext λ arg 
      sym (cocompl _ .bot .commutes {x = obj′ arg}
          ( record { sq = Nat-path  _  refl) })
           ap (cocompl _ .bot .ψ)
            (↓Obj-path _ _ refl refl
              (Nat-path λ _  funext λ _  happly (P .F-∘ _ _) _)))
      where
        obj′ :  arg  ↓Obj ( _) _
        obj′ arg .↓Obj.x = y
        obj′ arg .↓Obj.y = tt
        obj′ arg .map .η j h = P .F₁ (f D.∘ h) arg
        obj′ arg .map .is-natural X Y F = funext λ A 
            happly (P .F-∘ _ _) _
           happly (P .F-∘ _ _) _
           λ i  P .F₁ F (P .F-∘ A f (~ i) arg)

    adj .unit .is-natural x y f = Nat-path λ i  funext λ arg  sym $
      cocompl (F F∘ Dom ( D) (const! x)) .has⊥ (lan-approximate cocompl _ _ f)
        .centre .commutes (hom′ x i arg)
       ap (cocompl _ .bot .ψ)
           (↓Obj-path _ _ refl refl
              (Nat-path λ _  funext λ _  happly (f .is-natural _ _ _) _))

    adj .counit .is-natural x y f = ap hom $
      is-contr→is-prop
        (cocompl (F F∘ Dom ( D) (const! (Nerve F .F₀ x))) .has⊥ cocone₂)
        (cocone-hom _ λ o 
            C.pullr (cocompl _ .has⊥ (lan-approximate cocompl _ _ _)
                      .centre .commutes _)
           cocompl _ .has⊥ (cocone′ y) .centre .commutes _)
        (cocone-hom _ λ o 
          C.pullr (cocompl _ .has⊥ (cocone′ x) .centre .commutes _))
      where
        cocone₂ : Cocone _
        cocone₂ .coapex = y
        cocone₂ .ψ ob = f C.∘ ob .map .η _ D.id
        cocone₂ .commutes {x₂} {y₂} f =
          C.pullr ( sym (happly (y₂ .map .is-natural _ _ _) _)
                   ap (y₂ .map .η _) (sym D.id-comm))
           ap (_ C.∘_) (happly (ap  e  e .η (x₂ .↓Obj.x)) (f .sq)) D.id)

    adj .zig {A} = ap hom $
      is-contr→is-prop (cocompl (F F∘ Dom ( D) (const! A)) .has⊥ (cocompl _ .bot))
        (cocone-hom _ λ o 
            C.pullr (cocompl _ .has⊥ (lan-approximate cocompl _ _ _)
                               .centre .commutes _)
           cocompl _ .has⊥ (cocone′ _) .centre .commutes _
           ap (cocompl (F F∘ Dom ( D) (const! A)) .bot .ψ)
                  (↓Obj-path _ _ _ refl (Nat-path λ x  funext λ _ 
                      sym (happly (o .map .is-natural _ _ _) _)
                     ap (o .map .η x) (D.idl _))))
        (cocone-hom _ λ o  C.idl _)

    adj .zag {B} = Nat-path λ x  funext λ a 
        cocompl (F F∘ Dom ( D) (const! (Nerve F .F₀ B))) .has⊥ (cocone′ B)
          .centre .commutes (hom′ _ x a)
       F.elimr refl