Comma Category

definition example

For a Functor $L:\mathcal{D}\to \mathcal{C}$ and an object $c\in \mathcal{C}$, the comma category $L\downarrow c$ (DaoFP: $L/c$) has objects pairs $(d,f:Ld\to c)$ and morphisms $(d,f)\to (d^{\prime },f^{\prime })$ the arrows $h:d\to d^{\prime }$ with $f^{\prime }\circ Lh=f$:

It “describes the view of $c$ from the narrower perspective defined by the functor $L$” — think of $L$ as a model of $\mathcal{D}$ inside $\mathcal{C}$. Dually $c\downarrow R$ has objects $(d,f:c\to Rd)$. The general comma category $F\downarrow G$ of two functors into a common category has objects $(a,b,f:Fa\to Gb)$.

Sources: DaoFP §10.6 (“Comma category”, “Universal arrow”), §10.8 (Freyd’s theorem: the comma category $L/c$ as a cocone in $\mathcal{C}$ whose base is projected back to $\mathcal{D}$), Exercise 10.3.2; the Slice Category $\mathcal{C}/c$ is $\mathrm{Id}\downarrow c$; the Category of Elements of a presheaf is a comma category; CTfS Definition 4.6.4.1, Example 4.6.4.2, Exercise 4.6.4.3

• Special cases (CTfS §4.6.4): the Category of Elements ${\int }_{\mathcal{C}}I$ of $I:\mathcal{C}\to \mathbf{Set}$ is $(\{\star \}\downarrow I)$, because a function $\{\star \}\to I(c)$ is an element of $I(c)$ (CTfS Example 4.6.4.2); for two objects $c,c^{\prime }:1\to \mathcal{C}$ the comma category $(c\downarrow c^{\prime })$ is the discrete category on $\mathcal{C}(c,c^{\prime })$ (CTfS Exercise 4.6.4.3). CTfS: “category theory includes a highly developed and interoperable catalogue of materials and production techniques. One such is the comma category.”
• A Universal Arrow from $L$ to $c$ is a Terminal Object in $L\downarrow c$; $L$ has a right adjoint iff every $L\downarrow c$ has a terminal object, and then $Rc$ is its underlying object and ${\epsilon }_c$ its arrow (Adjunction via universal arrows).
• In the Adjoint Functor Theorem a solution set is a weakly terminal set in $L\downarrow c$; in Defunctionalization, for $L=(-\times a)$ the comma category $L\downarrow b$ has objects (environment $e$, function $e\times a\to b$) and morphisms “reduce the environment”.
• In the preorder case (Adjoint Functor Theorem for Preorders), $L\downarrow c$ is the set $\{d\mid Ld\le c\}$ and its “colimit” is the join defining the right adjoint.

LeanHaskell

#check CategoryTheory.Comma           -- Comma L R for L : A ⥤ T, R : B ⥤ T
#check CategoryTheory.CostructuredArrow   -- L ↓ c : objects (d, Ld ⟶ c)
#check CategoryTheory.StructuredArrow     -- c ↓ R : objects (d, c ⟶ Rd)

-- DaoFP §10.8: an object of the comma category (-×a) ↓ b is an environment with a function out of it
data Comma a b e = Comma e ((e, a) -> b)
-- a morphism (Comma e f) -> (Comma e' f') is h :: e -> e' with f' . first h = f  (reduces the environment)