Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-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.

A chain map is a quasi-isomorphism exactly when its cone is acyclic

Statement

Let f:C∙→D∙ be a chain map in an abelian category. Then f is a quasi-isomorphism if and only if Cone⁡(f) is acyclic.

Facts & Assumptions

Given: A chain map f:C∙→D∙ in an abelian category and an integer n.

[L1]

A quasi-isomorphism induces isomorphisms on all homology objects (Quasi-isomorphism, A chain map induces a well-defined map on homology).

[L2]

The cone has degree-n object Dn⊕Cn−1 and differential (y,x)↦(dDy+fn−1x,−dCx); this is biproduct matrix notation for morphisms (The mapping cone of a chain map).

[L3]

The homology map qE,n:Zn(E)→Hn(E) is the cokernel of the boundary inclusion. Acyclicity means Hn(E)=0 for every n (Homology object of a chain complex, Exactness of a complex at a degree and acyclic complexes).

[L4]

Every boundary inclusion is the kernel of its homology cokernel, and epimorphisms remain epic under pullback. Hence if qE,nt=0 for a morphism t:T→Zn(E), an epic pullback cover e:T′→T admits v:T′→En+1 with dn+1v=zE,nte (Every monomorphism is the kernel of its cokernel, and dually every epimorphism is the cokernel of its kernel, The pullback of an epimorphism is an epimorphism).

[L5]

In an abelian category, zero kernel detects monicity, zero cokernel detects epicity, and a monic epic is an isomorphism (In an abelian category, monic means zero kernel and epic means zero cokernel, An abelian category is balanced).

Proof

technique · direct
1.1L3L4

By [L3], Hn(E)=0 exactly when the boundary map En+1→Zn(E) is epic. By [L4], this is equivalent to the following arrow condition: every t:T→Zn(E) becomes a boundary after precomposition with some epimorphism e:T′→T. We use this condition for E=Cone⁡(f), and use the analogous condition qE,nt=0 for boundaries in C and D.

1.2L1L2L4assume-hypconstructalgebra

Conversely, assume f is a quasi-isomorphism. Let t:T→Zn(Cone⁡(f)) be any morphism, and write the components of its composite with the cycle inclusion as y:T→Dn and x:T→Cn−1. The cone-cycle equation gives dCx=0 and dDy+fn−1x=0. Thus x=zC,n−1x0 for a unique x0:T→Zn−1(C), and Hn−1(f)qC,n−1x0=qD,n−1fn−1x=0. Since Hn−1(f) is monic, qC,n−1x0=0. By [L4], after an epic cover e0:T0→T there is w:T0→Cn with dCw=xe0.

2.1L1L2L3L4L5step 1.1assume-hypconstructalgebra

Assume the cone is acyclic. To test the kernel of Hn−1(f), take a morphism t:T→Zn−1(C) with Hn−1(f)qC,n−1t=0. By [L4], after an epic cover e0:T0→T there is y:T0→Dn with dDy=fn−1zC,n−1te0. The column (−y,zC,n−1te0):T0→Cone⁡(f)n is a cycle by [L2]. By step 1.1, after another epic cover e1:T1→T0 it is the cone boundary of a column (v,w):T1→Dn+1⊕Cn. The second component of that boundary says zC,n−1te0e1=−dCw, so qC,n−1te0e1=0. Cancel the epimorphisms to obtain qC,n−1t=0. To apply this to the kernel k:K→Hn−1(C) of Hn−1(f), pull back the epic qC,n−1 along k, obtaining an epic e:T→K and t:T→Zn−1(C) with qC,n−1t=ke. The preceding argument gives ke=0, hence k=0. Thus Hn−1(f) is monic by [L5].

2.2L1L3L4step 1.2constructalgebra

The morphism ye0+fnw:T0→Dn is a cycle, so it factors through Zn(D) as r:T0→Zn(D). Since Hn(f) is an isomorphism, there is h:T0→Hn(C) with Hn(f)h=qD,nr. Pull back the epic qC,n:Zn(C)→Hn(C) along h, obtaining an epic e1:T1→T0 and s:T1→Zn(C) with qC,ns=he1. Therefore qD,n(re1−Zn(f)s)=0. By [L4], after an epic cover e2:T2→T1 there is v:T2→Dn+1 with dDv=(ye0+fnw)e1e2−fnzC,nse2.

3.1L1L2L3L5step 1.1step 2.1assume-hypconstructalgebra

To test epicity of Hn(f), take any t:T→Zn(D). The column (zD,nt,0):T→Cone⁡(f)n is a cycle. By step 1.1, after an epic cover e:T′→T it is the boundary of (v,w):T′→Dn+1⊕Cn. The second component says dCw=0, so w=zC,ns for a unique s:T′→Zn(C). The first component gives qD,nte=Hn(f)qC,ns. Hence coker⁡(Hn(f))qD,nte=0 for every t. Taking t=1Zn(D) and cancelling the epimorphisms e and qD,n yields coker⁡(Hn(f))=0. Thus Hn(f) is epic by [L5]. Since n is arbitrary, this step and step 2.1 make every Hn(f) an isomorphism; [L1] makes f a quasi-isomorphism.

4.1L2L3step 1.1step 3.1step 1.2step 2.2constructalgebra∎

Put u=−we1e2+zC,nse2:T2→Cn. The cone differential of (v,u) is (ye0e1e2,xe0e1e2) by [L2] and steps 1.2 and 2.2. Thus te0e1e2 is a cone boundary. Since the composite cover is epic, step 1.1 gives Hn(Cone⁡(f))=0. This holds for every n, so the cone is acyclic by [L3]. The two implications prove the equivalence.

Depends on

Used by

Dependency tree · two levels

29 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