Displayed category

In category theory, it is common to construct one category $𝖣$ from a simpler one $𝖢$ by requiring objects and morphisms to carry additional data. This situation is perfectly encapsulated by a functor

𝐹 : 𝖣 \to 𝖢

which “forgets” the additional data we demanded, but there is an equivalent notion which is intentionally closer to the way $𝖣$ is constructed. A displayed category $𝖣$ over a category $𝖢$ , a situation denoted by

𝖣 ⇥ 𝖢

consists of¹ #m/def/cat/dis

for each object $𝑐 \in 𝖢 0$ , a collection $𝖣 𝑐$ of objects over $𝑐$ ;
for each morphism $𝑓 \in 𝖢 (𝑎, 𝑏)$ , $𝑥 \in 𝖣 𝑎$ and $𝑦 \in 𝖣 𝑏$ , a set of morphisms from $𝑥$ to $𝑦$ over $𝑓$ , denoted $𝖣 𝑓 (𝑥, 𝑦)$ or $𝑥 \to 𝑓 𝑦$ ;
for each object $𝑐 \in 𝖢 0$ and $𝑥 \in 𝖣 𝑐$ , a morphism $1 𝑥 \in 𝖣 i d 𝑐 (𝑥, 𝑥)$ ;
for all morphisms $𝑓 \in 𝖢 (𝑎, 𝑏)$ and $𝑔 \in 𝖢 (𝑏, 𝑐)$ and objects $𝑥 \in 𝖣 𝑎$ , $𝑦 \in 𝖣 𝑏$ , and $𝑧 \in 𝖣 𝑐$ , a composition function $(\circ) : 𝖣 𝑔 (𝑦, 𝑧) \times 𝖣 𝑓 (𝑥, 𝑦) \to 𝖣 𝑔 𝑓 (𝑥, 𝑧)$

where these data satisfy

$1 𝑦 \circ ¯ 𝑓 = ¯ 𝑓$ and $¯ 𝑓 \circ 1 𝑥 = ¯ 𝑓$ for any $¯ 𝑓 \in 𝖣 𝑓 (𝑥, 𝑦)$ ;
$¯ ℎ \circ (¯ 𝑔 \circ ¯ 𝑓) = (¯ ℎ \circ ¯ 𝑔) \circ ¯ 𝑓$ for appropriately typed $¯ 𝑓, ¯ 𝑔, ¯ ℎ$ .

In the quintessential examples, we think of an object $𝑥$ over $𝑎$ as a structure on $𝑎$ , and a morphism $¯ 𝑓 \in 𝖣 𝑓 (𝑥, 𝑦)$ as a witness that $¯ 𝑓$ is structure-preserving. Thus displayed categories are naturally used in a paradigm with propositions as types.

Further terminology

Consider a displayed category $𝖣 ⇥ 𝖢$ .

$𝖣$ is called thinly displayed iff every displayed hom-set $𝖣 𝑓 (𝑥', 𝑦')$ is subsingleton, i.e. there is at most one morphism lying over any morphism in $𝖢$ .

Displayed category

Further terminology

See also

Footnotes