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.

✓ 7 results · all verified · 4 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 3 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Derived Functors — Examples

1 · Prerequisites

2 · Summary

These examples keep the companion page concrete without turning it into an Ext or Tor page too early. They show the degree-zero and vanishing profiles of exact and Hom-based functors, make change-of-resolution and lift-independence visible, and separate acyclic resolutions from injective ones by a simple abelian-group computation.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-adaptedprecheck passaudited 2026-09-04‡ rests on unproved material (inherited)Open item page →

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

The left derived functors of an exact functor

Example

Let $P$ be supplied projective resolution data on a class $D$ and let $F : A \to B$ be exact. Then for every object $A \in D$ , $L_{0}^{P} F (A) ≅ F (A) and L_{n}^{P} F (A) = 0 for n > 0.$ So the full left-derived profile of an exact functor is concentrated in degree $0$ .

Facts & Assumptions

Given: An exact functor $F$ and an object $A \in D$ .

[L1]

The zero-th left derived functor of a right exact functor recovers the original functor (The zero-th left derived functor of a right exact functor recovers the functor).

[L2]

An exact functor has vanishing positive derived functors (An exact functor has vanishing positive derived functors).

Verification

technique · direct

1.1

Exact functors are in particular right exact, so [L1] gives $L_{0}^{P} F (A) ≅ F (A)$ .

L1given

2.1

Since $F$ is exact, [L2] gives $L_{n}^{P} F (A) = 0$ for every $n > 0$ . Therefore the example has exactly the displayed degree-zero profile.

L2step 1.1∎

ExampleConstruction: AI-generatedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04‡ rests on unproved material (inherited)Open item page →

The right derived functors of Hom from a fixed object

Example

Assume the Axiom of Dependent Choice. Fix an object $X$ in an abelian category $A$ , and consider the covariant functor $A (X, -) : A \to A b$ . For supplied injective resolution data $I$ on a class $D$ , $R_{I}^{0} A (X, -) ≅ A (X, -),$ and if $J \in D$ is injective then $R_{I}^{n} A (X, -) (J) = 0 (n > 0) .$ This is the basic right-derived pattern that later becomes Ext.

Facts & Assumptions

Given: The Axiom of Dependent Choice, an object $X$ , supplied injective resolution data $I$ , and an injective object $J \in D$ .

[L1]

Hom is left exact in each variable, so $A (X, -)$ is left exact (Hom is left exact in each variable).

[L2]

The zero-th right derived functor of a left exact functor recovers the functor (The zero-th right derived functor of a left exact functor recovers the functor).

[L3]

Positive right derived functors vanish on injective objects (Positive right derived functors vanish on injective objects).

Verification

technique · direct

1.1

By [L1], the functor $A (X, -)$ satisfies the hypothesis of [L2], so $R_{I}^{0} A (X, -) ≅ A (X, -)$ .

L1L2given

2.1

If $J$ is injective, then [L3] gives $R_{I}^{n} A (X, -) (J) = 0$ for every $n > 0$ . This is exactly the displayed example.

L3step 1.1∎

ExampleConstruction: AI-generatedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Two resolution data and their change isomorphism

Example

Assume the Axiom of Dependent Choice. Let $P, Q$ be two supplied projective resolution data and $I, J$ two supplied injective resolution data on the same class $D$ in an abelian category $A$ , and let $F : A \to B$ be an additive functor to an abelian category. For every object $A \in D$ and every degree $n$ , the page's change-of-data theorems produce isomorphisms $L_{n}^{P} F (A) \tilde{\to} L_{n}^{Q} F (A) and R_{I}^{n} F (A) \tilde{\to} R_{J}^{n} F (A),$ natural in $A$ .

Facts & Assumptions

Given: The Axiom of Dependent Choice, the supplied data $P, Q, I, J$ , the additive functor $F$ , an object $A \in D$ , and an integer $n$ .

[L1]

Two supplied projective resolution data define naturally isomorphic left derived functors (Two supplied projective resolution data define naturally isomorphic left derived functors).

[L2]

Two supplied injective resolution data define naturally isomorphic right derived functors (Two supplied injective resolution data define naturally isomorphic right derived functors).

Verification

technique · direct

1.1

Apply [L1] at the object $A$ . This gives the projective-side change isomorphism $L_{n}^{P} F (A) \tilde{\to} L_{n}^{Q} F (A)$ , natural in $A$ .

L1given

2.1

Apply [L2] at the same object $A$ . This gives the injective-side change isomorphism $R_{I}^{n} F (A) \tilde{\to} R_{J}^{n} F (A)$ , also natural in $A$ .

L2step 1.1∎

ExampleConstruction: AI-generatedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Independence of two comparison lifts on homology

Example

Assume the Axiom of Dependent Choice. Let $P$ be a supplied projective resolution datum on a class $D$ in an abelian category $A$ , let $F : A \to B$ be an additive functor to an abelian category, let $u : A \to B$ be a morphism with $A, B \in D$ , and let ${\tilde{u}}_{∙}, {\hat{u}}_{∙} : P_{∙} (A) \to P_{∙} (B)$ be two comparison lifts between chosen projective resolutions. Then for every $n$ they induce the same map $L_{n}^{P} F (A) \to L_{n}^{P} F (B) .$ This is what makes the left derived map well defined.

Facts & Assumptions

Given: The supplied datum $P$ , additive functor $F$ , morphism $u : A \to B$ with $A, B \in D$ , and two comparison lifts ${\tilde{u}}_{∙}, {\hat{u}}_{∙}$ .

[L1]

Two comparison maps lifting the same morphism are chain-homotopic (Projective comparison maps are unique up to chain homotopy).

[L2]

The induced homology map is independent of the chosen comparison lift (The induced homology map is independent of the chosen comparison lift).

Verification

technique · direct

1.1

By [L1], the two displayed lifts are chain-homotopic.

L1given

2.1

Apply [L2] to those two lifts. It follows that they induce the same map on every left derived object $L_{n}^{P} F (A) \to L_{n}^{P} F (B)$ .

L2step 1.1∎

ExampleConstruction: AI-generatedVerification: AI-adaptedprecheck passaudited 2026-09-04‡ rests on unproved material (inherited)Open item page →

An acyclic resolution that is not an injective resolution

Example

For the identity functor on abelian groups and a supplied projective resolution datum $P$ on a class containing the free abelian groups, the standard free resolution $0 \to Z \overset{\times 2}{\to} Z \to Z / 2 Z \to 0$ is an $F$ -acyclic resolution relative to $P$ , but it is not an injective resolution.

Facts & Assumptions

Given: The identity functor on abelian groups, a supplied projective resolution datum $P$ on a class containing the free abelian groups, and the displayed free resolution.

[L1]

Projective objects are acyclic for left derived functors (Positive left derived functors vanish on projective objects).

[L2]

An $F$ -acyclic resolution is an exact augmented resolution by $F$ -acyclic objects (An F-acyclic resolution).

[L3]

Projective and injective objects are defined by distinct lifting and extension properties (Projective object, Injective object).

Verification

technique · direct

1.1

The terms of the displayed resolution are free abelian groups, hence projective and in the domain of $P$ . By [L1], they are acyclic for the identity functor, so [L2] identifies the displayed exact sequence as an acyclic resolution relative to $P$ .

L1L2given

2.1

The term $Z$ is not injective, because the map $2 Z \to Z$ , $2 n \mapsto n$ , does not extend across $2 Z ↪ Z$ . By [L3], the resolution is therefore not an injective resolution.

L3step 1.1algebra∎

CounterexampleConstruction: AI-generatedVerification: AI-adaptedprecheck passaudited 2026-09-04‡ rests on unproved material (inherited)Open item page →

L_0 of a non-right-exact functor need not recover the functor

Statement refuted

For an additive functor, the zeroth left derived object always agrees with the original functor value.

Facts & Assumptions

Given: The functor $F (M) = {Hom}_{Z} (Z / 2 Z, M)$ , and supplied projective resolution data $P$ on a class containing $Z / 2 Z$ that assigns it the standard projective resolution below.

[L1]

The companion false statement is false (FALSE: every additive functor has L_0 naturally isomorphic to itself).

[L2]

Hom is left exact in each variable (Hom is left exact in each variable).

[L3]

Right exactness is sufficient for the natural recovery of $F$ from $L_{0}$ (The zero-th left derived functor of a right exact functor recovers the functor).

[L4]

Left derived objects are computed from the homology of an applied deleted projective resolution (Left derived objects relative to supplied projective resolution data).

Counterexample

technique · direct

1.1

The functor $F$ is additive and, by [L2], left exact. On the standard resolution $0 \to Z \overset{\times 2}{\to} Z \to Z / 2 \to 0$ assigned by $P$ , both groups ${Hom}_{Z} (Z / 2, Z)$ vanish. Therefore [L4] gives $L_{0}^{P} F (Z / 2) = H_{0} (0 \to 0) = 0.$

L2L4givenalgebra

2.1

On the other hand, $F (Z / 2) = {Hom}_{Z} (Z / 2, Z / 2) \neq 0$ . So $L_{0}^{P} F (Z / 2) \neq F (Z / 2)$ . This concrete computation realises the failure announced by [L1] and shows that the right-exactness hypothesis in the recovery theorem [L3] cannot simply be omitted.

L1L3step 1.1∎

ExampleConstruction: AI-generatedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04‡ rests on unproved material (inherited)Open item page →

A contravariant functor derived via the opposite category

Example

Take the contravariant functor $G = {Hom}_{Z} (-, Z) : A b \to A b .$ Fix supplied projective resolution data $P$ on a class $D$ of abelian groups. Regarded as a covariant functor on ${A b}^{o p}$ , $G$ has right derived objects, for $A \in D$ , $R_{P^{o p}}^{n} G (A) = H^{n} ⁣ (G (P (A)_{d e l})),$ using the opposite-category interpretation of the projective resolutions as injective resolutions in ${A b}^{o p}$ .

Facts & Assumptions

Given: The contravariant functor $G = {Hom}_{Z} (-, Z)$ , supplied projective data $P$ on $D$ , and an object $A \in D$ .

[L1]

Hom is left exact in each variable, so the displayed Hom functor is a standard contravariant example (Hom is left exact in each variable).

[L2]

Contravariant derived functors are derived on the opposite category (Contravariant derived functors are derived on the opposite category).

Verification

technique · direct

1.1

By [L1], $G$ is the sort of contravariant additive functor that later produces Ext-style right derived objects.

L1given

2.1

Apply [L2] to $G$ , $P$ , and $A$ . The projective resolution $P (A)$ in $A b$ is read in ${A b}^{o p}$ as an injective resolution, giving the displayed right derived object there. This makes the variance bookkeeping explicit.

L2step 1.1∎

Derived Functors — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

The left derived functors of an exact functor

Example

Facts & Assumptions

Verification

The right derived functors of Hom from a fixed object

Example

Facts & Assumptions

Verification

Two resolution data and their change isomorphism

Example

Facts & Assumptions

Verification

Independence of two comparison lifts on homology

Example

Facts & Assumptions

Verification

An acyclic resolution that is not an injective resolution

Example

Facts & Assumptions

Verification

L_0 of a non-right-exact functor need not recover the functor

Statement refuted

Facts & Assumptions

Counterexample

A contravariant functor derived via the opposite category

Example

Facts & Assumptions

Verification

Sources