ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-11

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.

Quivers and quiver homomorphisms form a functor category of set-valued diagrams

Example

Directed multigraphs, also called quivers, are set-valued functors on a fixed two-object indexing category.

Facts & Assumptions

Given: The category $\mathcal J$ freely generated by two arrows $s,t:E\to V$ .

[L1]

A functor category has functors as objects and natural transformations as morphisms (Functor category $[\mathcal C,\mathcal D]$ ).

[L2]

The target category is $\mathbf{Set}$ (Sets and functions form the large locally small category $\mathbf{Set}$ ).

Verification

technique · direct

1.1

Let $\mathcal J$ have objects $E,V$ , identities, and two distinct arrows $s,t:E\to V$ . A functor $Q:\mathcal J\to\mathbf{Set}$ consists of a set $Q(E)$ of edges, a set $Q(V)$ of vertices, and source and target maps $Q(s),Q(t):Q(E)\to Q(V)$ . This is exactly a quiver.

L1L2

2.1

A natural transformation $\alpha:Q\Rightarrow Q'$ consists of functions $\alpha_E:Q(E)\to Q'(E)$ and $\alpha_V:Q(V)\to Q'(V)$ with $\alpha_VQ(s)=Q'(s)\alpha_E$ and $\alpha_VQ(t)=Q'(t)\alpha_E$ . These are precisely the incidence-preservation equations for a quiver homomorphism.

step 1.1L1

3.1

Since identities and composition are componentwise in the functor category, this identification respects identity quiver maps and their composites. Hence quivers and quiver homomorphisms form $[\mathcal J,\mathbf{Set}]$ .

step 2.1L1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 23 results over 11 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Emily Riehl, Category Theory in Context, Example 1.5.3 (standard reference, not scraped)