Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-29 rests on unproved material (inherited)
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.

Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

AB5 is equivalent to exactness of filtered colimits

Statement

Let A be a cocomplete abelian category. Then A satisfies AB5 if and only if for every small filtered category J, the filtered colimit functor colimJ:AJA is exact.

Facts & Assumptions

Given: A cocomplete abelian category A.

[L1]

AB5 is the directed-family lattice identity of The axioms AB5 and AB5*.

[L2]

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).

[L4]

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).

[L5]

Weibel, Appendix A.4.6, states for a cocomplete abelian category that exactness of filtered colimits is equivalent to the directed-subobject identity (iBi)C=i(BiC).

Proof

technique · direct
1.1

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.

L1L3L5assume-hyp
1.2

Conversely, assume every filtered colimit functor is exact. Let I be a small directed poset indexing a family of monomorphisms bi:BiA, and let c:CA represent a fixed subobject of A. For each iI, 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 BiC. These pullback squares assemble into a diagram in AI. Because the filtered colimit functor colimI 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.

L2L3L4assume-hypconstruct
2.1

The image of b:BA is the join iBi: each bi factors through b, so every Bi lies below im(b), and any common upper bound of the family receives b by the colimit universal property, so [L4] makes im(b) the least such upper bound. The same argument inside C shows that the image of PC is i(BiC).

L4step 1.2algebra
3.1

Because the square of step 1.2 is a pullback, [L4] identifies the image of PC with the meet of the subobject represented by im(b) and the fixed subobject C. Using step 2.1, this gives (iBi)C=i(BiC), which is exactly AB5 by [L1].

L1L4step 1.2step 2.1
4.1

Therefore AB5 is equivalent to exactness of filtered colimits.

step 1.1step 3.1

Depends on

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