TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-29

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 $A$ be a cocomplete abelian category. Then $A$ satisfies AB5 if and only if for every small filtered category $J$ , the filtered colimit functor ${colim}_{J} : A^{J} \to A$ 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).

[L3]

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

[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 $(⋁_{i} B_{i}) \land C = ⋁_{i} (B_{i} \land C) .$

Proof

technique · direct

1.1L1L3L5assume-hyp

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.

1.2L2L3L4assume-hypconstruct

Conversely, assume every filtered colimit functor is exact. Let $I$ be a small directed poset indexing a family of monomorphisms $b_{i} : B_{i} ↣ A$ , and let $c : C ↣ A$ represent a fixed subobject of $A$ . For each $i \in I$ , 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 $B_{i} \land C$ . These pullback squares assemble into a diagram in $A^{I}$ . Because the filtered colimit functor ${colim}_{I}$ 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.

2.1L4step 1.2algebra

The image of $b : B \to A$ is the join $⋁_{i} B_{i}$ : each $b_{i}$ factors through $b$ , so every $B_{i}$ 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 $P \to C$ is $⋁_{i} (B_{i} \land C)$ .

3.1L1L4step 1.2step 2.1

Because the square of step 1.2 is a pullback, [L4] identifies the image of $P \to C$ with the meet of the subobject represented by $im (b)$ and the fixed subobject $C$ . Using step 2.1, this gives $(⋁_{i} B_{i}) \land C = ⋁_{i} (B_{i} \land C),$ which is exactly AB5 by [L1].

4.1step 1.1step 3.1∎

Therefore AB5 is equivalent to exactness of filtered colimits.

Depends on

Dependency tree · 2 levels

Sources

Charles A. Weibel, An Introduction to Homological Algebra, Appendix A.4.6