Alphabeta MathHow 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
Definition
A category is filtered when every finite diagram in admits a cocone. Equivalently:
- is nonempty;
- for every there are an object and arrows ;
- for every parallel pair , there is with .
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
Used by
- Filtered colimits in Set need not commute with countably infinite products Counterexample
- Compactly supported singular cohomology Definition
- Finitary functors and finitary monads Definition
- Refinement-colimit Čech cohomology Definition
- The stalk of a presheaf at a point Definition
- Extension-by-zero generators detect sheaf-cohomology vanishing Lemma
- Filtered colimits and sheaf cohomology on Noetherian spaces Lemma
- Filtered colimits of abelian groups are exact Lemma
- Filtered colimits of sheaves and sections over compact opens Lemma
- The constant sheaf is the sheaf of locally constant functions Lemma
- Two representatives in a filtered colimit of sets are equal exactly when they become equal at one common later stage Lemma
- AB5 is equivalent to exactness of filtered colimits Theorem
- Filtered colimits commute with finite limits in Set Theorem
Dependency tree · two levels
8 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, Definition 3.8.7 (standard reference, not scraped)