PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04

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.

Contravariant derived functors are derived on the opposite category

Statement

Let $G : A \to B$ be a contravariant additive functor between abelian categories, regarded as a covariant functor $G : A^{o p} \to B$ . If $P$ is a supplied projective resolution datum on a class $D$ in $A$ , then reversing arrows turns it into a supplied injective resolution datum $P^{o p}$ on the same class in $A^{o p}$ , and for every $A \in D$ , $R_{P^{o p}}^{n} G (A) = H^{n} ⁣ (G (P (A)_{d e l})) .$ Thus contravariant derived functors are computed on the opposite category.

Facts & Assumptions

Given: A contravariant additive functor $G$ , a supplied projective datum $P$ on $D$ , and an object $A \in D$ .

[L1]

A contravariant functor on $A$ is a covariant functor on $A^{o p}$ (Covariant functor, identity functor, composite functor, and contravariant functor, Opposite category $C^{o p}$ ).

[L2]

If $A$ is abelian then $A^{o p}$ is abelian (The opposite of an abelian category is abelian).

[L3]

Projective objects are defined by lifting against epimorphisms, while injective objects are defined dually by extension across monomorphisms (Projective object, Injective object).

[L4]

Right derived objects are defined from supplied injective resolution data (Right derived objects relative to supplied injective resolution data).

Proof

technique · direct

1.1

By [L1] and [L2], $G$ may be treated as a covariant additive functor on the abelian category $A^{o p}$ .

L1L2given

1.2

A projective resolution in $A$ becomes, after reversing arrows, a coaugmented exact complex in $A^{o p}$ . Because [L3] exchanges the lifting and extension conditions under passage to the opposite category, each projective term becomes injective there. Hence the supplied datum $P$ becomes an injective resolution datum $P^{o p}$ on $D$ in $A^{o p}$ .

L2L3construct

2.1

Applying [L4] to the covariant functor $G : A^{o p} \to B$ and the injective datum $P^{o p}$ gives $R_{P^{o p}}^{n} G (A) = H^{n} (G (P (A)_{d e l})) .$ This is exactly the correct opposite-category formulation of deriving the original contravariant functor.

L1L4step 1.2∎

Depends on

Used by

Dependency tree · two levels

14 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

Joseph J. Rotman, An Introduction to Homological Algebra, 2nd ed. (standard reference, not scraped)