module Cat.Functor.Kan.Nerve where

Nerve and realisation🔗

Let be a functor from a category to a locally cocomplete category induces a pair of adjoint functors, as in the diagram below, where In general, the left adjoint is called “realization”, and the right adjoint is called “nerve”.

An example to keep in mind is the inclusion from the simplex category to the category of strict categories, which sends the to the finite poset In this case, the left adjoint is the ordinary realisation of a simplicial set as a strict category, and the right adjoint gives the simplicial nerve of a strict category.

Since these adjunctions come for very cheap ( 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 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

    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 on morphisms assembles into a natural transformation which is universal in the following sense: the nerve functor associated to is the left Kan extension of yoneda embedding along

    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 and natural transformation we can produce a natural transformation using own action on morphisms, since — in components — we have to transform an element of into one of Using we obtain an element of which maps under 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)
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 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

Since we have assumed is and is any functor admits an extension 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 is defined pointwise as the colimit under the diagram

where we can identify with the category of elements of the presheaf Any object with section 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 in the context of an object and section This is an object in the diagram that we took a colimit over, so the coprojection has a component expressing precisely what we need. Naturality is omitted from this page for brevity, but it follows from 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 It will suffice to come up with a family of compatible maps where is an object in the comma category

These, by definition, come with (natural) functions 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.