TheoremStatement: 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.

Every covariantly representable functor to Set preserves all existing small limits

Statement

Let $C$ be locally small and let $R : C \to S e t$ be covariantly representable. For every small diagram in $C$ whose limit exists, its image under $R$ is a limit in $S e t$ .

Facts & Assumptions

Given: A small $D : J \to C$ , a limit $(L, λ)$ , and a representation $R ≅ C (X, -)$ .

[F1]

Covariant and contravariant hom-assignments have their stated actions on morphisms and are functors (The covariant and contravariant hom-assignments and the hom-bifunctor of a locally small category, The assignments $C (a, -)$ and $C (-, a)$ are functors to $S e t$ ).

[F2]

A covariantly representable functor is naturally isomorphic to $C (X, -)$ (Presheaves, covariantly and contravariantly representable functors, and representations).

[F3]

A limit represents compatible cones by unique arrows (Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties).

[L1]

Every small set-valued diagram has a compatible-tuple limit (Set has all small limits, realized as compatible tuples in a set-indexed product).

[L2]

Yoneda's bijection and its inverse are natural in both variables (The Yoneda bijection $Nat (C (a, -), F) ≅ F (a)$ is natural in both $a$ and $F$ ).

Proof

technique · universal property

1.1

For the hom-functor, define $Φ : C (X, L) \to \prod_{j} C (X, D (j))$ by $Φ (f)_{j} = λ_{j} f$ . The cone equations put its image in the compatible subset that [L1] identifies as $\lim_{j} C (X, D (j))$ .

F1F3L1

1.2

Conversely, a compatible family $(f_{j} : X \to D (j))_{j}$ is a cone over $D$ . By [F3] there is a unique $f : X \to L$ with $λ_{j} f = f_{j}$ . This defines an inverse $Ψ$ to $Φ$ .

2.1

The equations in steps 1.1 and 1.2 give $Ψ Φ (f) = f$ by limit uniqueness and $Φ Ψ (f_{j}) = (f_{j})$ coordinatewise. Thus the image cone under $C (X, -)$ is a Set-limit.

F3step 1.1step 1.2

3.1

The natural isomorphism in [F2] transports this limiting cone to the image under $R$ ; its compatibility follows from naturality, equivalently from [L2]. Hence $R$ preserves the limit. Smallness is needed so the limit in [L1] is a set.

F2L1L2step 2.1∎

Depends on

Used by

Dependency tree · two levels

21 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, Theorem 3.5.5 (standard reference, not scraped)