Graph Algorithm Library

1 Introduction

1.1 Over category

Proposition 1.1.1 Sliced adjoint functors

If \(a : F \vdash G\) is an adjunction between \(F : C \to D\) and \(G : D \to C\) and \(X : C\), then there is an adjunction between \(F / X : C / X \to D / F(X)\) and \(G / X : D / F(X) \to C / X\).

Proof

See https://ncatlab.org/nlab/show/sliced+adjoint+functors+–+section.

Proposition 1.1.2 Limit-preserving functors lift to over categories

Let \(J\) be a shape (i.e. a category). Let \(\widetilde J\) denote the category which is the same as \(J\), but has an extra object \(*\) which is terminal. If \(F : C \to D\) is a functor preserving limits of shape \(\widetilde J\), then the obvious functor \(C / X \to D / F(X)\) preserves limits of shape \(J\).

Proof

Extend a functor \(K\colon J \to C / X\) to a functor \(\widetilde K\colon \widetilde J \to C\), by letting \(\widetilde K (*) = X\).

Proposition 1.1.3 Essential image of a sliced functor

If \(F : C \to D\) is a full functor between cartesian-monoidal categories, then \(F / X : C / X \hom D / F(X)\) has the same essential image as \(F\).

Proof

Transfer all diagrams.