TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-26

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The twisted arrow category is the category of elements of the hom-bifunctor

Statement

Let $C$ be a locally small category (Small, locally small, and large categories) and let $C (-, -) : C^{o p} \times C \to S e t$ be its hom-bifunctor (The covariant and contravariant hom-assignments and the hom-bifunctor of a locally small category, The hom-assignment $C (-, -) : C^{o p} \times C \to S e t$ is a bifunctor). Write $\int C (-, -)$ for its category of elements (The category of elements of a covariant functor or a presheaf) and $π_{\int} : \int C (-, -) \to C^{o p} \times C$ for the projection sending $((a, b), x)$ to $(a, b)$ .

The assignment

$Φ : Tw (C) ⟶ \int C (-, -), (f : c \to c^{'}) ⟼ ((c, c^{'}), f), (a, b) ⟼ (a, b)$

is an isomorphism of categories (The twisted arrow category and its projection to $C^{o p} \times C$ ): it is a bijection on objects and on morphisms, it preserves identities and composites, and it satisfies $π_{\int} \circ Φ = π$ .

Facts & Assumptions

Given: A locally small category $C$ .

[F4]

A category $C$ is locally small when every $C (A, B)$ is a set (Small, locally small, and large categories).

[L1]

For every locally small category $C$ , the hom-assignment $C (-, -) : C^{o p} \times C \to S e t$ is a functor (The hom-assignment $C (-, -) : C^{o p} \times C \to S e t$ is a bifunctor).

[F2]

The hom-assignment sends $(a, b)$ to $C (a, b)$ , and a morphism $(a, b) \to (a^{'}, b^{'})$ of the product category, consisting of $h : a^{'} \to a$ and $u : b \to b^{'}$ , acts by $C (h, u) : C (a, b) ⟶ C (a^{'}, b^{'}), f ⟼ u \circ f \circ h$ (The covariant and contravariant hom-assignments and the hom-bifunctor of a locally small category).

[F1]

The category of elements $\int F$ of a functor $F : C \to S e t$ has objects the pairs $(c, x)$ with $x \in F (c)$ , and a morphism $(c, x) \to (d, y)$ given by a morphism $f : c \to d$ in $C$ satisfying $F (f) (x) = y$ ; identities and composition are those of $C$ (The category of elements of a covariant functor or a presheaf).

[F3]

The objects of $Tw (C)$ are the morphisms of $C$ , and for $f : c \to c^{'}$ and $g : d \to d^{'}$ a morphism $f \to g$ is a pair $(a, b)$ with $b f a = g$ , where $a : d \to c$ and $b : c^{'} \to d^{'}$ (The twisted arrow category and its projection to $C^{o p} \times C$ ).

[F5]

The product category has morphisms $(f, g) : (C, D) \to (C^{'}, D^{'})$ , componentwise identities, and componentwise composition $(f^{'}, g^{'}) \circ (f, g) = (f^{'} \circ f, g^{'} \circ g)$ (Product category and its projection functors).

Proof

technique · direct

1.1L1F2F4

Because $C$ is locally small, every hom-collection $C (a, b)$ is a set and the hom-assignment is a functor into $S e t$ on $C^{o p} \times C$ , so its category of elements is formed by the published construction.

2.1F1F3F5step 1.1

An object of $\int C (-, -)$ is a pair $((c, c^{'}), x)$ with $x \in C (c, c^{'})$ ; since a morphism of $C$ is determined by, and determines, its domain, its codomain and its member of the corresponding hom-collection, the assignment $(f : c \to c^{'}) \mapsto ((c, c^{'}), f)$ is a bijection from the objects of $Tw (C)$ to the objects of $\int C (-, -)$ .

3.1F1F2F3step 2.1

A morphism $((c, c^{'}), f) \to ((d, d^{'}), g)$ of $\int C (-, -)$ is a morphism $(a, b) : (c, c^{'}) \to (d, d^{'})$ of $C^{o p} \times C$ , that is a pair with $a : d \to c$ and $b : c^{'} \to d^{'}$ in $C$ , satisfying $C (a, b) (f) = g$ ; by the displayed action of [F2] that equation reads $b f a = g$ , which is the defining condition of a morphism $f \to g$ of $Tw (C)$ . So $Φ$ is a bijection on each morphism collection, and it changes neither the pair $(a, b)$ nor the variance.

4.1F3step 2.1step 3.1∎

Identities and composites agree because both categories take them from $C^{o p} \times C$ : the identity of $f$ is $(1_{c}, 1_{c^{'}})$ on both sides and the composite of $(a, b)$ with $(a^{'}, b^{'})$ is $(a \circ a^{'}, b^{'} \circ b)$ on both sides. Hence $Φ$ is a functor, bijective on objects and morphisms, so an isomorphism of categories; and $π_{\int} Φ (f) = (c, c^{'}) = π (f)$ on objects with $π_{\int} Φ (a, b) = (a, b) = π (a, b)$ on morphisms, so $π_{\int} \circ Φ = π$ .

Remarks

The identification is what keeps this page from re-minting a published construction: every statement below that computes an end as a limit over $Tw (C)$ may equally be read as a statement about $\int C (-, -)$ , and the smallness of $Tw (C)$ for small $C$ is the smallness of that category of elements.

Local smallness is used exactly once, in step 1.1, and it is used to know that $C (a, b)$ is a set so that the hom-assignment is $S e t$ -valued. Without it there is no hom-bifunctor to take elements of, while $Tw (C)$ is still defined; so the twisted arrow category is the more primitive of the two constructions.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

13 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

E. Riehl, Categorical Homotopy Theory, §7.1 (standard reference, not scraped)
F. Loregian, (Co)end Calculus (arXiv:1501.02503v7), Definition 1.2.2 (standard reference, not scraped)