CorollaryStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-09-27

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.

Gaussian cancellation preserves homotopy type and abelian-category homology

Statement

Let $X^{∙}$ be a cochain complex in an additive category $A$ with a pivot decomposition at degree $n$ , let ${\overset{ˉ}{X}}^{∙}$ be the candidate reduction at that pivot, and let $p : X^{∙} \to {\overset{ˉ}{X}}^{∙}, ı : {\overset{ˉ}{X}}^{∙} \to X^{∙}, h$ be the explicit cochain maps and contracting homotopy of Explicit strong deformation retract from Gaussian cancellation, so that $p ı = 1_{{\overset{ˉ}{X}}^{∙}}$ , $1_{X^{∙}} - ı p = d h + h d$ and $p h = 0 = h ı = h^{2}$ .

Homotopy type. Under the reindexing dictionary $C_{n} : = C^{- n}$ of Complexes, homotopies and contractibility in an additive category, the complexes $X^{∙}$ and ${\overset{ˉ}{X}}^{∙}$ become chain complexes $X_{∙}$ and ${\overset{ˉ}{X}}_{∙}$ and the maps $p, ı$ become chain maps whose homotopy classes are mutually inverse isomorphisms in the homotopy category $K (A)$ of The homotopy category of chain complexes. Thus $X^{∙}$ and ${\overset{ˉ}{X}}^{∙}$ are isomorphic in the homotopy category, over every additive category $A$ .
Homology. If $A$ is abelian, then for every integer $n$ the induced maps on the homology objects of the reindexed chain complexes are inverse isomorphisms, $H_{n} (ı) H_{n} (p) = 1_{H_{n} (X)}, H_{n} (p) H_{n} (ı) = 1_{H_{n} (\overset{ˉ}{X})},$ where the homology objects are those of Homology object of a chain complex and, in the cochain indexing, are the homology objects of $X^{∙}$ and ${\overset{ˉ}{X}}^{∙}$ in degree $- n$ .
What is not claimed. No identification of $X^{∙}$ with ${\overset{ˉ}{X}}^{∙}$ as complexes is asserted before the contractible summand is split off: by Gaussian elimination splits a contractible two-term complex the isomorphism only exists after passing to the biproduct ${\overset{ˉ}{X}}^{∙} \oplus K$ with the contractible two-term complex $K$ , and the objects of $X^{∙}$ and ${\overset{ˉ}{X}}^{∙}$ in degrees $n$ and $n + 1$ are in general different.

Facts & Assumptions

Given: A cochain complex $X^{∙}$ in an additive category $A$ with the pivot decomposition at degree $n$ , its candidate reduction ${\overset{ˉ}{X}}^{∙}$ , the explicit cochain maps $p, ı$ and contracting homotopy $h$ of Explicit strong deformation retract from Gaussian cancellation, the chain isomorphism $T$ of Gaussian elimination splits a contractible two-term complex, and — for clause 2 — the additional assumption that $A$ is abelian.

[L1]

$p$ and $ı$ are cochain maps satisfying $p ı = 1_{{\overset{ˉ}{X}}^{∙}}$ and $1_{X^{∙}} - ı p = d h + h d$ , with $h$ of degree $- 1$ and $p h = 0$ , $h ı = 0$ , $h^{2} = 0$ (Explicit strong deformation retract from Gaussian cancellation).

[L2]

Reindexing $C_{n} : = C^{- n}$ , $d_{n} : = d^{- n}$ turns a cochain complex over an additive category into a chain complex over the same category, a cochain map into a chain map and a degree- $(- 1)$ cochain homotopy $h$ into the chain homotopy $s_{n} : = h^{- n}$ of degree $+ 1$ with $f_{n} - g_{n} = d_{n + 1}^{D} s_{n} + s_{n - 1} d_{n}^{C}$ ; no sign is inserted (Complexes, homotopies and contractibility in an additive category).

[L3]

For an additive category, $K (A)$ has the chain complexes as objects and the homotopy classes $[f]$ modulo null-homotopic chain maps as morphisms, with composition induced from representatives; $[f] = [g]$ exactly when $f - g$ is null-homotopic (The homotopy category of chain complexes, Homotopy classes of chain maps).

[L4]

In an abelian category, a chain complex has cycle subobjects $Z_{n} (C) = \ker (d_{n})$ with inclusions $k_{n}$ , boundary subobjects $B_{n} (C) = im (d_{n + 1})$ , the factorization $d_{n + 1} = k_{n} β_{n} e_{n}$ through the boundary-to-cycle map $β_{n} : B_{n} (C) \to Z_{n} (C)$ , and homology objects $H_{n} (C) = coker (β_{n})$ with quotient $q_{n} : Z_{n} (C) \to H_{n} (C)$ ; a chain map $u$ has a unique induced $H_{n} (u)$ characterized by $H_{n} (u) q_{n}^{C} = q_{n}^{D} Z_{n} (u)$ , where $Z_{n} (u)$ is the cycle map carried by $u$ ; and $H_{n}$ is additive, so $H_{n} (1) = 1$ and $H_{n} (u + v) = H_{n} (u) + H_{n} (v)$ (Chain complex in an abelian category, Cycle and boundary subobjects of a complex, The boundary subobject factors through the cycle subobject, Homology object of a chain complex, A chain map carries cycles to cycles and boundaries to boundaries, A chain map induces a well-defined map on homology, Homology is an additive functor).

[L5]

The cycle inclusion $k_{n}$ is a kernel and hence a monomorphism, and the homology quotient $q_{n}$ is a cokernel and hence an epimorphism (Kernels and cokernels in a category with zero morphisms as equalizers and coequalizers, Every equalizer is a monomorphism, and every coequalizer is an epimorphism).

[L6]

The isomorphism $T : X^{∙} \to {\overset{ˉ}{X}}^{∙} \oplus K$ has components $T^{n} = R^{- 1}$ and $T^{n + 1} = L$ in degrees $n, n + 1$ and identities elsewhere, so it is not an isomorphism of $X^{∙}$ with ${\overset{ˉ}{X}}^{∙}$ itself, and the objects in degrees $n, n + 1$ are $A \oplus U, B \oplus V$ on the source and $A, B$ on the reduction (Gaussian elimination splits a contractible two-term complex, Explicit strong deformation retract from Gaussian cancellation).

Proof

technique · direct

1.1

Clause 1. By [L1], $p ı = 1_{{\overset{ˉ}{X}}^{∙}}$ and $ı p = 1_{X^{∙}} - (d h + h d)$ . Under the reindexing [L2] these are chain maps $p_{∙}, ı_{∙}$ between $X_{∙}$ and ${\overset{ˉ}{X}}_{∙}$ with $p_{∙} ı_{∙} = 1$ and $ı_{∙} p_{∙} = 1_{X_{∙}} - w$ , where $w_{n} : = d_{n + 1} s_{n} + s_{n - 1} d_{n}$ and $s_{n} : = h^{- n}$ . The family $s$ exhibits $w ≃ 0$ , so $w$ is null-homotopic and $1_{X_{∙}} - ı_{∙} p_{∙} = w$ is null-homotopic; by [L3] therefore $[ı_{∙}] [p_{∙}] = [ı_{∙} p_{∙}] = [1_{X_{∙}}]$ and $[p_{∙}] [ı_{∙}] = [p_{∙} ı_{∙}] = [1_{{\overset{ˉ}{X}}_{∙}}]$ , so the two classes are mutually inverse isomorphisms in $K (A)$ .

L1L2L3algebra

1.2

Clause 2, first composite. Assume $A$ abelian. By [L2] the reindexed complexes are chain complexes in $A$ , and $p_{∙} ı_{∙} = 1_{{\overset{ˉ}{X}}_{∙}}$ strictly by [L1]. Functoriality and additivity of $H_{n}$ in [L4] give $H_{n} (p) H_{n} (ı) = H_{n} (p_{∙} ı_{∙}) = H_{n} (1_{{\overset{ˉ}{X}}_{∙}}) = 1_{H_{n} (\overset{ˉ}{X})}$ .

L1L2L4algebra

1.3

Cycle-level computation. Let $k_{n} : Z_{n} (X) \to X_{n}$ be the cycle inclusion, so $d_{n} k_{n} = 0$ , and let $d_{n + 1} = k_{n} β_{n} e_{n}$ be the factorization of [L4]. Then $w_{n} k_{n} = d_{n + 1} s_{n} k_{n} + s_{n - 1} d_{n} k_{n} = k_{n} β_{n} (e_{n} s_{n} k_{n})$ , because the second summand vanishes and the first is $d_{n + 1} (s_{n} k_{n})$ . As a difference of the chain maps $1_{X_{∙}}$ and $ı_{∙} p_{∙}$ , the map $w$ is a chain map, so [L4] gives a cycle map $Z_{n} (w)$ with $k_{n} Z_{n} (w) = w_{n} k_{n} = k_{n} β_{n} (e_{n} s_{n} k_{n})$ ; by [L5] the inclusion $k_{n}$ is monic, so $Z_{n} (w) = β_{n} (e_{n} s_{n} k_{n})$ .

L4L5algebra

2.1

The homotopy term induces zero. Applying the homology quotient $q_{n} : Z_{n} (X) \to H_{n} (X)$ to step 1.3 gives $q_{n} Z_{n} (w) = q_{n} β_{n} (e_{n} s_{n} k_{n}) = 0$ , since $q_{n}$ is the cokernel of $β_{n}$ by [L4]. The characterizing property $H_{n} (w) q_{n} = q_{n} Z_{n} (w)$ of [L4] therefore gives $H_{n} (w) q_{n} = 0$ , and $q_{n}$ is epic by [L5], so $H_{n} (w) = 0$ for every $n$ .

L4L5step 1.3algebra

3.1

Clause 2, second composite. By [L1] and [L2], $ı_{∙} p_{∙} = 1_{X_{∙}} - w$ with $w$ as in step 1.1, so functoriality and additivity of $H_{n}$ in [L4] give $H_{n} (ı) H_{n} (p) = H_{n} (1_{X_{∙}}) + H_{n} (- w) = 1_{H_{n} (X)} - H_{n} (w)$ , which equals $1_{H_{n} (X)}$ by step 2.1. Together with step 1.2 the two induced maps are inverse isomorphisms.

L1L2L4step 2.1algebra

4.1

Conclusion. Step 1.1 proves clause 1: the classes are inverse in $K (A)$ over an arbitrary additive category. Steps 1.2 and 2.1, 3.1 prove clause 2: over an abelian category $H_{n} (p)$ and $H_{n} (ı)$ are mutually inverse isomorphisms on every homology object. Clause 3 is the qualification carried by [L6]: the displayed identities are those of the deformation retract of $X^{∙}$ onto ${\overset{ˉ}{X}}^{∙}$ and of the chain isomorphism onto ${\overset{ˉ}{X}}^{∙} \oplus K$ , so no equality or canonical identification of the complexes $X^{∙}$ and ${\overset{ˉ}{X}}^{∙}$ is being asserted. ∎

step 1.1step 1.2step 2.1step 3.1L6

Depends on

Used by

A unit pivot forces the minus Schur sign Example
Additive functors preserve chosen Gaussian cancellations Proposition

Dependency tree · two levels

32 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

David Clark, Scott Morrison and Kevin Walker, Fixing the Functoriality of Khovanov Homology, Appendix A.1, printed pp. 1562-1563 (standard reference, not scraped)
Charles A. Weibel, An Introduction to Homological Algebra, ch. 1, printed pp. 2-5 and 17-18 (standard reference, not scraped)