Alphabeta Math
PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 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.

Change-of-injective-resolution isomorphisms satisfy identity and cocycle laws

Statement

Assume the Axiom of Dependent Choice.

Let I,J,K be supplied injective resolution data on the same domain, and let F:A→B be an additive functor between abelian categories. For each ordered pair (S,T) among these data, let θS,T be the change-of-data natural isomorphism whose component at an object A is induced by any comparison extension S∙(A)→T∙(A) of 1A. Then:

  1. θI,I=1RInF for every n.
  2. θJ,K∘θI,J=θI,K for every n.

Facts & Assumptions

Given: An object A in the common domain and an integer n.

[L1]

The chosen injective resolutions of the same object are homotopy equivalent under that object (Injective resolutions of the same object are homotopy equivalent under that object).

[L2]

Two injective comparison maps extending the same morphism are cochain-homotopic (Injective comparison maps are unique up to cochain homotopy).

[L3]

Reindexing turns cochain homotopies into chain homotopies, and homology then respects both homotopy and composition (Cochain complex in an abelian category, Chain-homotopic maps induce the same map on homology, Homology respects identities and composition).

[L4]

Comparison extensions exist for morphisms between objects in the domain of each supplied injective datum (A morphism has a comparison extension between the supplied injective resolutions).

Proof

technique · direct
1.1L1L2L3L4givenconstruct

For any ordered pair (S,T), [L1] gives comparison extensions cA:S∙(A)→T∙(A) and dA:T∙(A)→S∙(A) of 1A. Their composites extend 1A, so [L2] and [L3] show that the induced cohomology maps are inverse. Any other choice of cA extends the same identity and hence induces the same map. For a morphism u:A→B, choose within-data comparison extensions using [L4]. The two composites from S∙(A) to T∙(B) both extend u, so [L2] and [L3] give the naturality square. Thus the displayed construction specifies a well-defined natural isomorphism θS,T.

2.1L2L3step 1.1

For the pair (I,I), the identity cochain map on I∙(A) is a comparison extension of 1A. Any comparison extension used in step 1.1 to define θI,I(A) extends the same identity morphism, so [L2] makes it cochain-homotopic to the identity. By [L3], the induced map on cohomology is therefore the identity on RInF(A).

2.2L2L3step 1.1algebra

For the triple (I,J,K), the cochain map defining θJ,K(A)∘θI,J(A) is the composite of two comparison extensions of 1A, while the map defining θI,K(A) is another comparison extension of 1A. By [L2] these are cochain-homotopic, so [L3] gives θJ,K(A)∘θI,J(A)=θI,K(A).

3.1step 1.1step 2.1step 2.2∎

Since A was arbitrary, steps 2.1 and 2.2 prove the identity and cocycle laws for the natural isomorphisms constructed in step 1.1.

Depends on

Used by

Dependency tree · two levels

22 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