TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-28

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.

A pullback is the kernel of the difference of the two legs, and dually for pushouts

Statement

Let $f : A \to C$ and $g : B \to C$ be morphisms in an abelian category. Then a pullback of the cospan $A \overset{f}{\to} C \overset{g}{\leftarrow} B$ is a kernel of the difference map

$f \circ p_{A} - g \circ p_{B} : A \oplus B \to C,$

where $p_{A}$ and $p_{B}$ are the biproduct projections. Dually, a pushout of $B \overset{s}{\leftarrow} A \overset{t}{\to} C$ is a cokernel of $i_{B} \circ s - i_{C} \circ t : A \to B \oplus C$ .

Facts & Assumptions

Given: An abelian category and a cospan $A \overset{f}{\to} C \overset{g}{\leftarrow} B$ .

[L1]

Abelian categories have finite limits and finite colimits (An abelian category has all finite limits and all finite colimits).

[L2]

On a biproduct the injections and projections satisfy the standard identity-sum relations (On a biproduct, the injections and projections satisfy the identity-sum relation).

[L3]

In a preadditive category, equalizers are kernels of differences (In a preadditive category, the equalizer of a parallel pair is the kernel of their difference).

[L4]

An abelian category is additive and therefore preadditive (Abelian category).

Proof

technique · direct

1.1L1L3L4

By [L1] there is a product of $A$ and $B$ , and by [L4] that product is the biproduct $A \oplus B$ . In the preadditive structure of [L4], a morphism $x : X \to A \oplus B$ satisfies $(f p_{A} - g p_{B}) x = 0$ exactly when $f p_{A} x = g p_{B} x$ . So by [L3], a kernel of $f p_{A} - g p_{B}$ is an equalizer of the parallel pair $f p_{A}, g p_{B}$ .

2.1L2step 1.1

Giving $x : X \to A \oplus B$ is the same as giving its two composites to $A$ and $B$ , and the equality in step 1.1 is exactly the pullback compatibility condition. Therefore the equalizer in step 1.1 is a pullback of $f$ and $g$ .

3.1L1L3L4step 2.1∎

Reversing all arrows gives the pushout statement: in an abelian category a pushout is the cokernel of the corresponding difference map.

Depends on

Used by

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, Section 12.5, Lemma 12.5.11 (standard reference, not scraped)