TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16

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.

Freyd's representability theorem for continuous Set-valued functors satisfying a solution set condition

Statement

Let $C$ be complete and locally small, and let $F : C \to S e t$ be continuous. Suppose there is a supplied set of pairs $(S_{i}, y_{i})$ with $y_{i} \in F (S_{i})$ such that, for every $C \in C$ and every $x \in F (C)$ , some $i$ and some $f : S_{i} \to C$ satisfy $F (f) (y_{i}) = x .$ Then $F$ is covariantly representable.

Facts & Assumptions

Given: The category, functor, and supplied set of element-pairs in the Statement.

[L1]

The category of elements $\int F$ has objects $(C, x)$ and morphisms $f : (C, x) \to (D, y)$ satisfying $F (f) (x) = y$ (The category of elements of a covariant functor or a presheaf).

[L2]

For a covariant Set-valued functor, a universal element is exactly an initial object of $\int F$ (Universal elements are initial in a covariant category of elements and terminal in a presheaf category of elements).

[L3]

A covariant $S e t$ -valued functor is representable when it is naturally isomorphic to $C (R, -)$ for some object $R$ (Presheaves, covariantly and contravariantly representable functors, and representations).

[L5]

For locally small $C$ , a pair $(R, u)$ with $u \in F (R)$ is universal for $F : C \to S e t$ if and only if, for every object $c$ and every $x \in F (c)$ , there is a unique morphism $f : R \to c$ with $F (f) (u) = x$ (A representation is equivalently a universal element with a unique factorisation property).

[L4]

The objectwise GAFT constructs an initial comma object from completeness, local smallness, continuity, and a supplied solution set (General adjoint functor theorem, objectwise initial-object form).

Proof

technique · constructive

1.1L1construct

By [L1], each pair $(S_{i}, y_{i})$ is an object of $\int F$ , and the displayed factorisation condition says exactly that every $(C, x)$ receives a morphism from some $(S_{i}, y_{i})$ . Thus these pairs form a supplied jointly weakly initial set in $\int F$ .

2.1step 1.1L4choose

The category $\int F$ is the comma category $(1 ↓ F)$ for a singleton $1$ . Since $F$ is continuous, [L4] applies to the supplied set from step 1.1 and gives an initial object $(R, u)$ , without selecting over a proper class.

3.1step 2.1L2L3L5discharge-construct∎

By [L2], $(R, u)$ is a universal element of $F$ . By [L5] the map $Φ_{c} : C (R, c) \to F (c)$ , $f \mapsto F (f) (u)$ , is then a bijection for every object $c$ ; it is natural in $c$ because for $g : c \to c^{'}$ functoriality gives $F (g) (Φ_{c} (f)) = F (g) (F (f) (u)) = F (g \circ f) (u) = Φ_{c^{'}} (g \circ f)$ . Hence $C (R, -) ≅ F$ as functors, which is representability in the sense of [L3].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

23 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 4.7.15 (standard reference, not scraped)