CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13

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.

Hom(X,−) is continuous, while Hom(−,X) sends every existing small colimit to a limit of sets

Statement

For every object $X$ of a locally small category $C$ , $C (X, -) : C \to S e t$ preserves all small limits that exist. Moreover, for every small diagram $D$ with a colimit, there is a natural bijection

$C (colim D, X) ≅ \lim_{j \in J^{o p}} C (D (j), X) .$

Facts & Assumptions

Given: An object $X$ and the indicated existing limits or colimits.

[L1]

Every covariantly representable functor preserves small limits (Every covariantly representable functor to Set preserves all existing small limits).

[F1]

$C (X, -)$ and $C (-, X)$ are the covariant and contravariant hom-functors (The covariant and contravariant hom-assignments and the hom-bifunctor of a locally small category).

[L2]

A colimit in $C$ is a limit in $C^{o p}$ (A limiting cone for a diagram is exactly a colimiting cocone for the formally dual diagram in the opposite category).

[F2]

Continuous means preserving all small limits (Preservation, reflection, and creation of limits and colimits; continuous and cocontinuous functors).

Proof

technique · direct corollary

1.1

The functor $C (X, -)$ is represented by $X$ , so [L1] says that it preserves every small existing limit. By [F2], it is continuous whenever the term is applied to the available small limits of its domain.

L1F1F2

1.2

Regard a colimit cocone $D (j) \to Q$ as a limiting cone in $C^{o p}$ by [L2]. Applying [L1] there to the representable $C^{o p} (X, -) = C (-, X)$ gives the displayed limit of hom-sets.

L1F1L2

2.1

Explicitly, the bijection sends $f : Q \to X$ to the compatible family of composites $D (j) \to Q \to X$ ; the colimit existence and uniqueness clauses give its inverse and prove uniqueness.

step 1.2∎

Depends on

Used by

The hom-functor turns a coend into an end and carries an end to an end Corollary

Dependency tree · two levels

17 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, Category Theory in Context, Theorems 3.5.5 and 3.5.6 (standard reference, not scraped)