DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 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.

Filtered categories and filtered colimits

A category $J$ is filtered when every finite diagram in $J$ admits a cocone. Equivalently:

$J$ is nonempty;
for every $j, k$ there are an object $ℓ$ and arrows $j \to ℓ \leftarrow k$ ;
for every parallel pair $f, g : j ⇉ k$ , there is $h : k \to ℓ$ with $h f = h g$ .

The equivalence uses finite diagrams as in Finite, small, and large limits and colimits; complete and cocomplete categories; the nonempty and zigzag language agrees with the connectedness convention in Isomorphism, groupoid, and connected category. A filtered colimit is a colimit (Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties) of a diagram indexed by a small filtered category. Smallness is included so the colimit is among the ordinary small colimits.

Depends on