LemmaStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-09-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.

Extension from subobjects of a generator detects injectivity

Statement

Assume the Axiom of Choice.

Let $A$ be a locally small Grothendieck category with a generator $U$ , and let $I$ be an object. If every morphism $N \to I$ from every subobject $N \subseteq U$ extends to a morphism $U \to I$ , then $I$ is injective.

Facts & Assumptions

Given: The Axiom of Choice, a locally small Grothendieck category with a generator $U$ , and an object $I$ satisfying the extension property for every subobject $N \subseteq U$ .

[A1]

AC permits choosing a set of representatives of the subobject classes of $B$ , and it is the hypothesis of Zorn's lemma (The Axiom of Choice).

[L1]

In an abelian category, if a subobject $A^{'} ⊊ B$ is proper, then some morphism from the generator into $B$ factors through $B$ but not through $A^{'}$ (A generator detects comparison of subobjects).

[L2]

A Grothendieck category is an abelian category with AB5 and a generator (Grothendieck category).

[L3]

In a locally small abelian category with a generator, every object has only a set of subobjects up to equivalence (An AB3 locally small abelian category with a generator is well-powered).

[L4]

Injective objects are exactly those extending morphisms across monomorphisms (Injective object).

[L5]

Zorn's lemma supplies maximal elements once every chain has an upper bound (Zorn's lemma).

[L6]

In a cocomplete abelian category, AB5 implies exactness of filtered colimits (AB5 is equivalent to exactness of filtered colimits).

Proof

technique · direct

1.1A1L3givenalgebra

To extend a map $u : A \to I$ across a monomorphism $A ↣ B$ , use [A1] to fix representatives of the set of subobject classes $A^{'} \subseteq B$ containing $A$ , taking $A$ itself as the representative of its class. Consider pairs $(A^{'}, u^{'})$ with $u^{'} : A^{'} \to I$ extending $u$ . By [L3] and local smallness, these pairs form a set. Order them by extension: $(A^{'}, u^{'}) \leq (A^{''}, u^{''})$ exactly when $A^{'} \subseteq A^{''}$ as subobjects of $B$ and $u^{''} ∣_{A^{'}} = u^{'}$ . This is a partial order and the initial pair $(A, u)$ belongs to it.

2.1L2L6step 1.1algebra

The empty chain has upper bound $(A, u)$ . For a nonempty chain $T$ of partial extensions, let $A_{\infty}$ be the colimit of its subobjects inside $B$ . The chain is filtered, and [L2, L6] make the induced map $A_{\infty} \to B$ monic, so it represents their union. The maps in the chain are compatible by the extension order from step 1.1, so the colimit universal property induces $u_{\infty} : A_{\infty} \to I$ extending $u$ . Transport this map along the isomorphism to the selected representative of the union from step 1.1; its pair is an upper bound of $T$ . Thus every chain has an upper bound.

3.1A1L5step 2.1choose

By [A1] and [L5], choose a maximal partial extension $(A_{\max}, u_{\max})$ .

4.1L1step 3.1givenchoosealgebra

Suppose $A_{\max} \neq B$ . By [L1], there exists a morphism $ψ : U \to B$ that does not factor through $A_{\max}$ . Let $B_{0} = im (ψ)$ , let $N = A_{\max} \cap B_{0}$ inside $B$ , and let $M = ψ^{- 1} (N) \subseteq U$ . The composite $M \to N \to A_{\max} \overset{u_{\max}}{\to} I$ extends by hypothesis to a morphism $χ : U \to I$ .

5.1step 4.1algebra

Because $\ker (ψ) \subseteq M$ , the map $χ$ vanishes on $\ker (ψ)$ and therefore factors through $B_{0} = im (ψ)$ ; write the factor map as $u_{0} : B_{0} \to I$ . The maps $u_{\max} : A_{\max} \to I$ and $u_{0} : B_{0} \to I$ agree on $N = A_{\max} \cap B_{0}$ , so they glue to a map $A_{\max} + B_{0} \to I$ extending $u_{\max}$ . Since $ψ$ does not factor through $A_{\max}$ , the subobject $A_{\max} + B_{0}$ is strictly larger than $A_{\max}$ , contradicting maximality. Therefore $A_{\max} = B$ .

6.1L4step 5.1∎

Every map across a monomorphism extends, so $I$ is injective by [L4].

Depends on

Used by

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

The Stacks Project, Section 19.11: Injectives in Grothendieck categories (standard reference, not scraped)
Romyar Sharifi, Homological Algebra (standard reference, not scraped)