TheoremStatement: 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 elimination splits a contractible two-term complex

Statement

Let $X^{∙}$ be a cochain complex in an additive category with an invertible-block decomposition $d^{n} = (\begin{array}{cc} a & b \\ c & φ \end{array}) : A \oplus U \to B \oplus V$ and Schur complement $\overset{ˉ}{d} = a - b φ^{- 1} c$ , as in An invertible cochain differential block and its candidate reduction, and let ${\overset{ˉ}{X}}^{∙}$ be the candidate reduction. Let $K$ be the two-term cochain complex with $K^{n} = U$ , $K^{n + 1} = V$ , $K^{j} = 0$ for $j \notin {n, n + 1}$ and differential $d_{K}^{n} = φ$ ; write $\overset{ˉ}{X} \oplus K$ for the degreewise biproduct.

The cochain map $T : X^{∙} \to {\overset{ˉ}{X}}^{∙} \oplus K$ with components $T^{j} = 1 (j \notin {n, n + 1}), T^{n} = R^{- 1} = (\begin{array}{cc} 1 & 0 \\ φ^{- 1} c & 1 \end{array}), T^{n + 1} = L = (\begin{array}{cc} 1 & - b φ^{- 1} \\ 0 & 1 \end{array})$ is an isomorphism of cochain complexes, with inverse the cochain map $T^{- 1}$ whose components are $1$ in degrees $j \notin {n, n + 1}$ , $R$ in degree $n$ and $L^{- 1}$ in degree $n + 1$ .
$K$ is contractible, with contracting homotopy $k^{n + 1} = φ^{- 1} : V \to U$ and $k^{j} = 0$ for $j \neq n + 1$ .
$X^{∙}$ and ${\overset{ˉ}{X}}^{∙}$ are homotopy equivalent: the projection $\tilde{p} : \overset{ˉ}{X} \oplus K \to \overset{ˉ}{X}$ and the inclusion $\tilde{ı} : \overset{ˉ}{X} \to \overset{ˉ}{X} \oplus K$ satisfy $\tilde{p} \tilde{ı} = 1$ and $1 - \tilde{ı} \tilde{p} = d \tilde{h} + \tilde{h} d$ for the homotopy $\tilde{h}$ vanishing except in degree $n + 1$ , where ${\tilde{h}}^{n + 1} = (\begin{array}{cc} 0 & 0 \\ 0 & φ^{- 1} \end{array})$ , so that $p : = \tilde{p} T$ and $ı : = T^{- 1} \tilde{ı}$ are homotopy inverse cochain maps.
The construction is a chain isomorphism followed by deletion of a contractible summand: it does not identify $X^{∙}$ with ${\overset{ˉ}{X}}^{∙}$ before that summand is split off, and in general $X^{∙}$ and ${\overset{ˉ}{X}}^{∙}$ do not even have the same objects.

Facts & Assumptions

Given: A cochain complex $X^{∙}$ in an additive category with a pivot decomposition at degree $n$ , its candidate reduction ${\overset{ˉ}{X}}^{∙}$ , the two-term complex $K$ , and the maps $T, T^{- 1}, L, R, L^{- 1}, R^{- 1}, \tilde{p}, \tilde{ı}, \tilde{h}$ displayed above.

[L1]

The candidate reduction is a cochain complex; $L d^{n} R = (\begin{array}{cc} \overset{ˉ}{d} & 0 \\ 0 & φ \end{array})$ ; $R^{- 1} (p; q) = (p; 0)$ , $(r s) L^{- 1} = (r 0)$ and $r b φ^{- 1} = - s$ (Triangular basis changes diagonalize an invertible differential block).

[L2]

The decomposition of $X$ at degrees $n, n + 1$ , the candidate reduction ${\overset{ˉ}{X}}^{∙}$ with objects $A, B$ in those degrees and the two-term complex $K$ with differential $φ$ are as in the block definition; in particular ${\overset{ˉ}{d}}^{n - 1} = p$ , ${\overset{ˉ}{d}}^{n} = \overset{ˉ}{d}$ , ${\overset{ˉ}{d}}^{n + 1} = r$ and the differential of $\overset{ˉ}{X} \oplus K$ in degree $n$ is $(\begin{array}{cc} \overset{ˉ}{d} & 0 \\ 0 & φ \end{array})$ (An invertible cochain differential block and its candidate reduction).

[L3]

Cochain maps, homotopies, homotopy equivalence, contractibility and degreewise biproducts are defined by componentwise equations, and the identity of a zero object is the zero morphism (Complexes, homotopies and contractibility in an additive category).

Proof

technique · direct

1.1

Away from degrees $n - 1, n, n + 1$ the components of $T$ are identities and ${\overset{ˉ}{X}}^{∙} \oplus K$ agrees with $X^{∙}$ in the two adjacent degrees of each such case, so $T$ commutes with the differentials there; at degree $n - 1$ one has $T^{n} d^{n - 1} = R^{- 1} (p; q) = (p; 0) = {\overset{ˉ}{d}}^{n - 1} T^{n - 1}$ by [L1] and [L2].

L1L2algebra

1.2

At degree $n$ , $T^{n + 1} d^{n} = L d^{n} = (\begin{array}{cc} \overset{ˉ}{d} & 0 \\ 0 & φ \end{array}) R^{- 1} = d_{\overset{ˉ}{X} \oplus K}^{n} T^{n}$ , using $L d^{n} R = diag (\overset{ˉ}{d}, φ)$ and $R^{- 1} R = 1$ from [L1].

L1L2algebra

1.3

$K$ is a cochain complex: its only composite of consecutive differentials is $d_{K}^{n + 1} d_{K}^{n} = 0 \cdot φ = 0$ , the differentials into and out of the zero objects $K^{j}$ being zero morphisms.

L2L3algebra

1.4

$K$ is contractible with the displayed $k$ : in degree $n$ one has $d_{K}^{n - 1} k^{n} + k^{n + 1} d_{K}^{n} = 0 + φ^{- 1} φ = 1_{U}$ , in degree $n + 1$ one has $d_{K}^{n} k^{n + 1} + k^{n + 2} d_{K}^{n + 1} = φ φ^{- 1} + 0 = 1_{V}$ , and in every other degree both terms are zero morphisms on a zero object.

L3algebra

2.1

At degree $n + 1$ , $T^{n + 2} d^{n + 1} = (\begin{array}{cc} r & s \end{array})$ and $d_{\overset{ˉ}{X} \oplus K}^{n + 1} T^{n + 1} = (\begin{array}{cc} r & 0 \end{array}) L = (\begin{array}{cc} r & - r b φ^{- 1} \end{array}) = (\begin{array}{cc} r & s \end{array})$ , using $r b φ^{- 1} = - s$ from [L1]. Hence $T$ is a cochain map.

L1L2step 1.2algebra

2.2

The family $T^{'}$ with components $1$ in degrees $j \notin {n, n + 1}$ , $R$ in degree $n$ and $L^{- 1}$ in degree $n + 1$ is a two-sided inverse of $T$ componentwise: $T^{' n} T^{n} = R R^{- 1} = 1$ , $T^{n} T^{' n} = R^{- 1} R = 1$ , $T^{' n + 1} T^{n + 1} = L^{- 1} L = 1$ , $T^{n + 1} T^{' n + 1} = L L^{- 1} = 1$ , and the remaining components are identities.

L1step 1.2algebra

2.3

In the biproduct ${\overset{ˉ}{X}}^{∙} \oplus K$ the projection $\tilde{p}$ onto $\overset{ˉ}{X}$ and the inclusion $\tilde{ı}$ of $\overset{ˉ}{X}$ satisfy $\tilde{p} \tilde{ı} = 1_{\overset{ˉ}{X}}$ . For the homotopy $\tilde{h}$ that vanishes in all degrees except $n + 1$ , where ${\tilde{h}}^{n + 1} = (\begin{array}{cc} 0 & 0 \\ 0 & φ^{- 1} \end{array})$ in the coordinates $B \oplus V \to A \oplus U$ , one computes degreewise: in degree $n$ both $1 - \tilde{ı} \tilde{p} = (\begin{array}{cc} 0 & 0 \\ 0 & 1_{U} \end{array})$ and $d \tilde{h} + \tilde{h} d = {\tilde{h}}^{n + 1} (\begin{array}{cc} \overset{ˉ}{d} & 0 \\ 0 & φ \end{array}) = (\begin{array}{cc} 0 & 0 \\ 0 & 1_{U} \end{array})$ ; in degree $n + 1$ both $1 - \tilde{ı} \tilde{p} = (\begin{array}{cc} 0 & 0 \\ 0 & 1_{V} \end{array})$ and $d \tilde{h} + \tilde{h} d = (\begin{array}{cc} \overset{ˉ}{d} & 0 \\ 0 & φ \end{array}) {\tilde{h}}^{n + 1} = (\begin{array}{cc} 0 & 0 \\ 0 & 1_{V} \end{array})$ ; in all other degrees $\tilde{h} = 0$ and $\tilde{ı} \tilde{p} = 1$ .

L2L3step 1.3algebra

3.1

The family $T^{'}$ is a cochain map: for every $j$ , using the equation $T^{j + 1} d^{j} = d_{\overset{ˉ}{X} \oplus K}^{j} T^{j}$ for the cochain map $T$ and the componentwise inverse identities of step 2.2, one has $T^{' j + 1} d_{\overset{ˉ}{X} \oplus K}^{j} = T^{' j + 1} d_{\overset{ˉ}{X} \oplus K}^{j} T^{j} T^{' j} = T^{' j + 1} T^{j + 1} d^{j} T^{' j} = d^{j} T^{' j}$ . Hence $T^{'} = T^{- 1}$ is the displayed inverse cochain map.

step 2.2step 1.1step 1.2step 2.1algebra

4.1

Define $p : = \tilde{p} T : X^{∙} \to {\overset{ˉ}{X}}^{∙}$ , $ı : = T^{- 1} \tilde{ı} : {\overset{ˉ}{X}}^{∙} \to X^{∙}$ and $h : = T^{- 1} \tilde{h} T$ . Then $p ı = \tilde{p} T T^{- 1} \tilde{ı} = \tilde{p} \tilde{ı} = 1$ and $1 - ı p = T^{- 1} (1 - \tilde{ı} \tilde{p}) T = T^{- 1} (d \tilde{h} + \tilde{h} d) T = d (T^{- 1} \tilde{h} T) + (T^{- 1} \tilde{h} T) d = d h + h d$ , using $T d = d T$ and $T^{- 1} d = d T^{- 1}$ for the chain isomorphisms $T, T^{- 1}$ of steps 1.1 to 2.2. Hence $p$ and $ı$ are cochain maps that are homotopy inverse, so $X^{∙}$ and ${\overset{ˉ}{X}}^{∙}$ are homotopy equivalent.

step 2.3step 3.1algebra

5.1

Steps 1.1, 1.2 and 2.1 show that $T$ is a cochain map and steps 2.2 and 3.1 show that $T^{'}$ is a two-sided inverse cochain map, so $T$ is an isomorphism of complexes with inverse $T^{- 1} = T^{'}$ ; steps 1.3 and 1.4 show that $K$ is a complex contractible via $φ^{- 1}$ ; and step 4.1 transports the direct-sum deformation retract along $T$ to the homotopy equivalence of $X^{∙}$ with ${\overset{ˉ}{X}}^{∙}$ . Because the construction replaces the objects $A \oplus U$ , $B \oplus V$ by $A$ , $B$ and modifies the neighbouring differentials, it never asserts an equality of complexes between $X^{∙}$ and ${\overset{ˉ}{X}}^{∙}$ : the deletion of $K$ is a homotopy equivalence only after the chain isomorphism $T$ . ∎

step 1.1step 1.2step 2.1step 2.2step 3.1step 1.4step 4.1

Depends on

Used by

Gaussian cancellation preserves homotopy type and abelian-category homology Corollary
The isolated differential 2 on the integers cannot be cancelled Counterexample
Additive functors preserve chosen Gaussian cancellations Proposition
Explicit strong deformation retract from Gaussian cancellation Proposition
Transferred maps are functorial up to homotopy, with strict naturality limits Proposition

Dependency tree · two levels

8 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

Dror Bar-Natan, Fast Khovanov Homology Computations, section 4 Lemma 4.2 and section 5, printed p. 5 (standard reference, not scraped)
David Clark, Scott Morrison and Kevin Walker, Fixing the Functoriality of Khovanov Homology, Appendix A.1, printed pp. 1562-1563 (standard reference, not scraped)