module Cat.Functor.Kan.Nerve where
Nerve and realisation🔗
Let be a functor from a -small category to a locally -small, -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 strict categories, which sends the -simplex 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 (-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 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 .
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 = Nat-path (λ _ → funext λ _ → D.idl _) Nerve .F-∘ _ _ = Nat-path (λ _ → funext λ _ → 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 ’s yoneda embedding along .
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 and natural transformation , we can produce a natural transformation using ’s 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 = 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 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 = Nat-path λ x → Nat-path λ y → funext λ 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 is -small and is -cocomplete, 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)
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 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 .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 , 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 ’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 . 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.
adj .unit .η P .is-natural x y f = funext λ _ → sym $ ↓colim.commutes P $ ↓hom (Nat-path λ _ → funext λ _ → P .F-∘ _ _ $ₚ _) adj .unit .is-natural x y f = Nat-path λ i → funext λ arg → sym $ ↓colim.factors _ {j = elem x i arg} _ _ ∙ ap (↓colim.ψ _) (↓Obj-path _ _ refl refl (Nat-path λ _ → funext λ _ → 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 (Nat-path λ _ → funext λ _ → sym (j .map .is-natural _ _ _ $ₚ _) ∙ ap (j .map .η _) (C.idl _)))) (λ j → D.idl _) adj .zag {d} = Nat-path λ c → funext λ f → ↓colim.factors (Nerve F .F₀ d) {j = elem _ c f} _ _ ∙ F.elimr refl