Displayed category

A displayed category $𝖣$ over a category $𝖢$ consists of¹ cat

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 𝖣 1 𝑐 (𝑥, 𝑥)$ ;
for all morphisms $𝑓 \in 𝖢 (𝑎, 𝑏)$ and $𝑔 \in 𝖢 (𝑏, 𝑐)$ and objects $𝑥 \in 𝖣 𝑎$ , $𝑦 \in 𝖣 𝑏$ , and $𝑧 \in 𝖣 𝑐$ , a composition function
$(\circ) : 𝖣 𝑔 (𝑦, 𝑧) \times 𝖣 𝑓 (𝑥, 𝑦) \to 𝖣 𝑔 \circ 𝑓 (𝑥, 𝑧)$

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. This motivates the total category $\int 𝖢 𝖣$ as the category of structures and structure morphisms, defined as follows:

an object $(𝑎, 𝑥) \in \int 𝖢 𝖣$ is a pair consisting of an object $𝑎 \in 𝖢$ and an object $𝑥 \in 𝖣 𝑎$ over $𝑎$ , so that
$(\int 𝖢 𝐷) 0 : = \sum 𝑎 \in 𝖢 0 𝖣 𝑎$
a morphism $(𝑓, ¯ 𝑓) : (𝑎, 𝑥) \to (𝑏, 𝑦)$ is a pair where $𝑓 \in 𝖢 (𝑎, 𝑏)$ and $¯ 𝑓 \in 𝖣 𝑓 (𝑥, 𝑦)$ , so that
$(\int 𝖢 𝖣) ((𝑎, 𝑥), (𝑏, 𝑦)) = \sum 𝑓 \in 𝖢 (𝑎, 𝑏) 𝖣 𝑓 (𝑥, 𝑦)$
composition and identities are induced from those of $𝖢$ and $𝖣$ in the straightforward way, and similarly for the axioms.

This is naturally equipped with a forgetful functor

𝜋 𝖣 1 : \int 𝖢 𝖣 \to 𝖢 .

develop | en | SemBr

2017. Displayed categories ↩

Displayed category

Graph View

Backlinks

Displayed category

Footnotes

Graph View

Backlinks