TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 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 projective generator detects isomorphisms

Statement

Let $P$ be a projective generator of an abelian category. If

$A (P, f) : A (P, A) \to A (P, B)$

is an isomorphism for a morphism $f : A \to B$ , then $f$ is an isomorphism.

Facts & Assumptions

Given: A projective generator $P$ and a morphism $f : A \to B$ .

[L1]

Projectivity makes $A (P, -)$ exact on short exact sequences (Projective object characterisations).

[L2]

A generator is equivalently an object whose canonical coproduct maps are epic (The cancellation and epimorphism descriptions of a generator agree).

Proof

technique · direct

1.1L1construct

Apply [L1] to the short exact sequences $0 \to \ker (f) \to A \to im (f) \to 0$ and $0 \to im (f) \to B \to coker (f) \to 0$ . Since $A (P, f)$ is an isomorphism, the first sequence forces $A (P, \ker (f)) = 0$ and the second forces $A (P, coker (f)) = 0$ .

2.1L2step 1.1

Let $X$ be any object with $A (P, X) = 0$ . By [L2], the canonical map $∐_{u \in A (P, X)} P \to X$ is epic. But the indexing set is empty, so this is the zero map $0 \to X$ . An epic zero map forces $X = 0$ . Applying this to the objects in step 1.1 gives $\ker (f) = 0 = coker (f)$ .

3.1step 2.1∎

Therefore $f$ is both monic and epic, hence an isomorphism in an abelian category.

Depends on

Used by

Nothing in the library uses this result yet.

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

Pavel Etingof, Shlomo Gelaki, Dmitri Nikshych, and Victor Ostrik, Tensor Categories, Section 1.6 (standard reference, not scraped)