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.
AB5 is equivalent to exactness of filtered colimits
Statement
Let be a cocomplete abelian category. Then satisfies AB5 if and only if for every small filtered category , the filtered colimit functor is exact.
Facts & Assumptions
Given: A cocomplete abelian category .
AB5 is the directed-family lattice identity of The axioms AB5 and AB5*.
An exact functor preserves the finite limits and finite colimits of its source, and in particular preserves short exact sequences (Exact functor between abelian categories, Exact sequence and short exact sequence in an abelian category, Degenerate exactness criteria).
A filtered colimit is a colimit indexed by a small filtered category (Filtered categories and filtered colimits, Finite, small, and large limits and colimits; complete and cocomplete categories).
The meet of two subobjects is represented by their pullback, and the image of a morphism is the least subobject through which that morphism factors (The meet of two subobjects is their pullback, The image is the least subobject through which a morphism factors).
Weibel, Appendix A.4.6, states for a cocomplete abelian category that exactness of filtered colimits is equivalent to the directed-subobject identity
Proof
Assume AB5. Its defining identity [L1] is exactly the directed-subobject identity in [L5]. The forward implication of the cited equivalence therefore says that every filtered colimit functor is exact.
Conversely, assume every filtered colimit functor is exact. Let be a small directed poset indexing a family of monomorphisms , and let represent a fixed subobject of . For each , form the pullback square tikzcd P_i \arrow[r] \arrow[d] & C \arrow[d, "c"] \\ B_i \arrow[r, "b_i"'] & A. By [L4], the top-left leg represents . These pullback squares assemble into a diagram in . Because the filtered colimit functor is exact, [L2] and [L3] say that it preserves finite limits, so its colimit square tikzcd P \arrow[r] \arrow[d] & C \arrow[d, "c"] \\ B \arrow[r, "b"'] & A is again a pullback.
The image of is the join : each factors through , so every lies below , and any common upper bound of the family receives by the colimit universal property, so [L4] makes the least such upper bound. The same argument inside shows that the image of is .
Because the square of step 1.2 is a pullback, [L4] identifies the image of with the meet of the subobject represented by and the fixed subobject . Using step 2.1, this gives which is exactly AB5 by [L1].
Therefore AB5 is equivalent to exactness of filtered colimits.
Depends on
- Exact sequence and short exact sequence in an abelian category
- Degenerate exactness criteria
- The axioms AB5 and AB5*
- Filtered categories and filtered colimits
- Finite, small, and large limits and colimits; complete and cocomplete categories
- Exact functor between abelian categories
- The meet of two subobjects is their pullback
- The image is the least subobject through which a morphism factors
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
27 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
- Charles A. Weibel, An Introduction to Homological Algebra, Appendix A.4.6 (standard reference, not scraped)