CounterexampleConstruction: Literature-sourcedVerification: 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.

Filtered colimits in Set need not commute with countably infinite products

Statement refuted

Filtered colimits in $S e t$ commute with arbitrary set-indexed products.

Facts & Assumptions

Given: Positive integers $i, j$ and sets $M_{i, j} = {1, \dots, i}$ , with inclusions as $i$ increases.

[F1]

A category is filtered when it is nonempty, every two objects have a common target, and every parallel pair is equalized at a later stage (Filtered categories and filtered colimits).

[L1]

Filtered colimits commute with finite, not asserted infinite, limits in $S e t$ (Filtered colimits commute with finite limits in Set).

[F2]

Products in a category represent families of coordinate maps (Products and coproducts as limits and colimits of discrete diagrams, including their existence-and-uniqueness equations).

Counterexample

technique · bounded sequences

1.1F1F2

The positive-integer chain is nonempty, two indices have their maximum as a common target, and it has no distinct parallel arrows, so it is filtered by [F1]. For fixed $i$ , the countable product $\prod_{j \geq 1} M_{i, j}$ is the set of positive-integer sequences all of whose entries are at most $i$ .

1.2F2

For each $j$ , the filtered colimit ${colim}_{i} M_{i, j}$ is $N_{> 0}$ . The product of these coordinatewise colimits is the set of all positive-integer sequences, including $(1, 2, 3, \dots)$ , which is unbounded.

2.1step 1.1

Its filtered colimit over $i$ is therefore the set of bounded positive-integer sequences: a sequence appears at some stage exactly when one integer bounds all its coordinates.

3.1L1step 2.1step 1.2∎

Hence the canonical map from step 2.1 to the set in step 1.2 is not surjective. The arbitrary-product assertion is false, while [L1] is not contradicted because the product is infinite.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

12 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

The Stacks Project, Categories, Section 4.19 (standard reference, not scraped)