module Cat.Functor.Kan.Nerve where

Nerve and realisation🔗

Let F:CDF : \mathcal{C} \to \mathcal{D} be a functor from a κ\kappa-small category C\mathcal{C} to a locally κ\kappa-small, κ\kappa-cocomplete category D\mathcal{D}. FF induces a pair of adjoint functors, as in the diagram below, where N|-| \dashv \mathbf{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 \hookrightarrow \mathfrak{Cat}_\mathrm{strict} from the simplex category to the category of 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^{\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-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 , 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 \mathbf{Hom}(F(-), X).

    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 = Nat-path  _  funext λ _  D.idl _)
    Nerve .F-∘ _ _ = Nat-path  _  funext λ _  sym (D.assoc _ _ _))

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

    coapprox :  C => Nerve F∘ F
    coapprox .η x .η y f            = F.₁ f
    coapprox .η x .is-natural _ _ _ = funext λ _  F.F-∘ _ _
    coapprox .is-natural _ _ _      = Nat-path λ _  funext λ _  F.F-∘ _ _

If we’re given a functor M:DPSh(C)M : \mathcal{D} \to \mathrm{PSh}(\mathcal{C}) and natural transformation CMFよ_\mathcal{C} \to MF, we can produce a natural transformation α:Nerve(F)M\alpha : \mathrm{Nerve}(F) \to M using MM’s own action on morphisms, since — in components — we have to transform an element of f:Hom(Fc,d)f : \mathbf{Hom}(Fc,d) into one of M(d)(c)M(d)(c). Using α\alpha, we obtain an element of M(Fc)(c)M(Fc)(c), which maps under M(f)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
The construction is concluded by straightforward, though tedious, computations using naturality. It’s not very enlightening.
    Nerve-is-lan .σ {M = M} α .η d .is-natural x y f =
      funext λ g 
        M.₁ (g D.∘ F.₁ f) .η y (α .η y .η y          ≡⟨ M.F-∘ g (F .F₁ f) ηₚ _ $ₚ _ 
        M.₁ g .η y (M .F₁ (F.₁ f) .η y (α .η y .η y ≡˘⟨ ap (M.F₁ g .η y) (α .is-natural _ _ _ ηₚ _ $ₚ _) ≡˘
        M.₁ g .η y (α .η x .η y  f C.∘ )            ≡⟨ ap! 
        M.₁ g .η y (α .η x .η y ( C.∘ f))              ≡⟨ ap (M.₁ g .η y) (α .η _ .is-natural _ _ _ $ₚ _) 
        M.₁ g .η y (M.₀ (F.₀ x) .F₁ f (α .η x .η x  ≡⟨ M.₁ g .is-natural _ _ _ $ₚ _ 
        M.₀ d .F₁ f (M.₁ g .η x (α .η x .η x        
      where module M = Functor M

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

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

    Nerve-is-lan .σ-uniq {M = M} {α = α} {σ′ = σ′} p =
      Nat-path λ x  Nat-path λ y  funext λ f 
        M.₁ f .η y (α .η y .η y          ≡⟨ ap (M.₁ f .η y) (p ηₚ _ ηₚ _ $ₚ _) 
        M.₁ f .η y (σ′ .η _ .η y  F.₁ ) ≡⟨ ap! F.F-id 
        M.₁ f .η y (σ′ .η _ .η y         ≡˘⟨ σ′ .is-natural _ _ _ ηₚ _ $ₚ _ ≡˘
        σ′ .η x .η y (f D.∘              ≡⟨ ap (σ′ .η x .η y) (D.idr _) 
        σ′ .η x .η y f                         
      where module M = Functor M

Since we have assumed C\mathcal{C} is κ\kappa-small and D\mathcal{D} is κ\kappa-cocomplete, any functor F:CDF : \mathcal{C} \to \mathcal{D} admits an extension Lan(F)\operatorname{Lan}_{よ}(F). 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)
  Realisation⊣Nerve : Realisation F cocompl  Nerve F
  Realisation⊣Nerve = adj where
    open _⊣_
    open ↓Obj
    open ↓Hom

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

(CP)CFD, (よ_\mathcal{C} \downarrow P) \to C \xrightarrow{F} D\text{,}

where we can identify CPよ_\mathcal{C} \downarrow P with the category of elements of the presheaf PP. Any object i:Ci : \mathcal{C} with section P(i)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 .F₀ 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 = funext λ _  happly (P .F-∘ _ _) _

The adjunction unit is easiest to describe: we must come up with a map F(i)Lan(F)(P)F(i) \to \operatorname{Lan}_{よ}(F)(P), in the context of an object i:Ci : \mathcal{C} and section a:P(i)a : P(i). 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’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:Do : \mathcal{D}. It will suffice to come up with a family of compatible maps F(j)oF(j) \to o, where jj is an object in the comma category

C(D(o)F). よ_\mathcal{C} \downarrow (よ_\mathcal{D}(o) \circ F)\text{.}

These, by definition, come with (natural) functions HomC(,j)HomD(F,o)\mathbf{Hom}_\mathcal{C}(-, j) \to \mathbf{Hom}_\mathcal{D}(F-, o), 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 .η _ comm
      where abstract
        :  {x y} (f : ↓Hom ( C) (const! (Nerve F .F₀ ob)) x y)
         y .map .η _ D.∘ F.₁ (f .α)  x .map .η _
      comm {x} {y} f =
        y .map .η _ D.∘ F.₁ (f .α) ≡˘⟨ y .map .is-natural _ _ _ $ₚ _ ≡˘
        y .map .η _ ( C.∘ f .α)     ≡⟨ ap (y .map .η _) 
        y .map .η _ (f .α C.∘     ≡⟨ f .sq ηₚ _ $ₚ _ 
        x .map .η (x .↓Obj.x)      

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.