PropositionStatement: 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.

Explicit strong deformation retract from Gaussian cancellation

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$ , let ${\overset{ˉ}{X}}^{∙}$ be the candidate reduction, and let $X^{∙} ≃ {\overset{ˉ}{X}}^{∙}$ be the homotopy equivalence of Gaussian elimination splits a contractible two-term complex. Define graded maps $p : X^{∙} \to {\overset{ˉ}{X}}^{∙}$ , $ı : {\overset{ˉ}{X}}^{∙} \to X^{∙}$ and $h : X^{∙} \to X^{∙}$ by the components $p^{n} = (\begin{array}{cc} 1 & 0 \end{array}), p^{n + 1} = (\begin{array}{cc} 1 & - b φ^{- 1} \end{array}), ı^{n} = (\begin{array}{c} 1 \\ - φ^{- 1} c \end{array}), ı^{n + 1} = (\begin{array}{c} 1 \\ 0 \end{array}),$ with all other components of $p$ and $ı$ identities, and by $h^{n + 1} = (\begin{array}{cc} 0 & 0 \\ 0 & φ^{- 1} \end{array}), h^{j} = 0 (j \neq n + 1) .$ Then $p$ and $ı$ are cochain maps, and with the conventions of Complexes, homotopies and contractibility in an additive category for the components of composites, $p ı = 1_{{\overset{ˉ}{X}}^{∙}}, 1_{X^{∙}} - ı p = d h + h d, p h = 0, h ı = 0, h^{2} = 0.$ Here $(p h)^{j} = p^{j - 1} h^{j}$ , $(h ı)^{j} = h^{j} ı^{j}$ and $(h^{2})^{j} = h^{j - 1} h^{j}$ , so each side condition is a statement about the indicated composite in the degree written. In particular $p$ and $ı$ are the homotopy inverses of the homotopy equivalence of the previous theorem, exhibited by the explicit homotopy $h$ .

Facts & Assumptions

Given: A cochain complex $X^{∙}$ in an additive category with the pivot decomposition at degree $n$ , its reduction ${\overset{ˉ}{X}}^{∙}$ , and the graded maps $p, ı, h$ displayed above.

[L1]

The chain isomorphism $T$ of Gaussian elimination splits a contractible two-term complex has components $T^{n} = R^{- 1} = (\begin{array}{cc} 1 & 0 \\ φ^{- 1} c & 1 \end{array})$ and $T^{n + 1} = L = (\begin{array}{cc} 1 & - b φ^{- 1} \\ 0 & 1 \end{array})$ , identities elsewhere, and the transported homotopy equivalence has the form $p = \tilde{p} T$ , $ı = T^{- 1} \tilde{ı}$ , $h = T^{- 1} \tilde{h} T$ with ${\tilde{h}}^{n + 1} = (\begin{array}{cc} 0 & 0 \\ 0 & φ^{- 1} \end{array})$ and $\tilde{p}, \tilde{ı}$ the projection onto and inclusion of the reduction summand.

[L2]

The blocks satisfy $L d^{n} R = diag (\overset{ˉ}{d}, φ)$ , $R^{- 1} (p; q) = (p; 0)$ , $(r s) L^{- 1} = (r 0)$ , $q = - φ^{- 1} c p$ , $r b φ^{- 1} = - s$ , $\overset{ˉ}{d} p = 0$ and $r \overset{ˉ}{d} = 0$ (Triangular basis changes diagonalize an invertible differential block, Gaussian elimination splits a contractible two-term complex).

[L3]

Composites of the graded maps above are formed degreewise — $(p h)^{j} = p^{j - 1} h^{j}$ , $(h ı)^{j} = h^{j} ı^{j}$ and $(h^{2})^{j} = h^{j - 1} h^{j}$ — and the components of $p$ and $ı$ in degrees $j \notin {n, n + 1}$ are identities, so $ı^{j} p^{j} = 1_{X^{j}}$ there, sums and negatives being those of the additive ambient category (Complexes, homotopies and contractibility in an additive category).

Proof

technique · direct

1.1

The components of $p$ are those of $\tilde{p} T$ : in degree $n$ , $p^{n} = (\begin{array}{cc} 1 & 0 \end{array}) R^{- 1} = (\begin{array}{cc} 1 & 0 \end{array})$ ; in degree $n + 1$ , $p^{n + 1} = (\begin{array}{cc} 1 & 0 \end{array}) L = (\begin{array}{cc} 1 & - b φ^{- 1} \end{array})$ ; and in the remaining degrees both factors are identities. Since $p$ is a composite of cochain maps, it is a cochain map.

L1algebra

1.2

The components of $ı$ are those of $T^{- 1} \tilde{ı}$ : in degree $n$ , $ı^{n} = R (\begin{array}{c} 1 \\ 0 \end{array}) = (\begin{array}{c} 1 \\ - φ^{- 1} c \end{array})$ ; in degree $n + 1$ , $ı^{n + 1} = L^{- 1} (\begin{array}{c} 1 \\ 0 \end{array}) = (\begin{array}{c} 1 \\ 0 \end{array})$ ; and in the remaining degrees both factors are identities. So $ı$ is a cochain map.

L1algebra

1.3

The components of $h$ are those of $\tilde{h}$ transported by the identities in degrees other than $n + 1$ : $(T^{- 1} \tilde{h} T)^{n + 1} = R {\tilde{h}}^{n + 1} L = (\begin{array}{cc} 0 & 0 \\ 0 & φ^{- 1} \end{array})$ , because $L$ preserves the $V$ -coordinate, ${\tilde{h}}^{n + 1}$ records only it with $φ^{- 1}$ , and $R$ leaves the element $(0; φ^{- 1} v)$ unchanged; in degree $j \neq n + 1$ one has ${\tilde{h}}^{j} = 0$ and hence $h^{j} = 0$ .

L1algebra

2.1

$p ı = 1_{{\overset{ˉ}{X}}^{∙}}$ : in degree $n$ one has $p^{n} ı^{n} = (\begin{array}{cc} 1 & 0 \end{array}) (\begin{array}{c} 1 \\ - φ^{- 1} c \end{array}) = 1_{A}$ ; in degree $n + 1$ one has $p^{n + 1} ı^{n + 1} = (\begin{array}{cc} 1 & - b φ^{- 1} \end{array}) (\begin{array}{c} 1 \\ 0 \end{array}) = 1_{B}$ ; in every other degree $p^{j} ı^{j} = 1 \cdot 1 = 1$ .

step 1.1step 1.2algebra

2.2

$(1 - ı p)^{n} = (\begin{array}{cc} 1 & 0 \\ 0 & 1 \end{array}) - (\begin{array}{c} 1 \\ - φ^{- 1} c \end{array}) (\begin{array}{cc} 1 & 0 \end{array}) = (\begin{array}{cc} 0 & 0 \\ φ^{- 1} c & 1 \end{array})$ and $(d h + h d)^{n} = d^{n - 1} h^{n} + h^{n + 1} d^{n} = (\begin{array}{cc} 0 & 0 \\ 0 & φ^{- 1} \end{array}) (\begin{array}{cc} a & b \\ c & φ \end{array}) = (\begin{array}{cc} 0 & 0 \\ φ^{- 1} c & 1 \end{array})$ , using $h^{n} = 0$ and the block form of $d^{n}$ .

step 1.3L2algebra

2.3

$(1 - ı p)^{n + 1} = (\begin{array}{cc} 1 & 0 \\ 0 & 1 \end{array}) - (\begin{array}{c} 1 \\ 0 \end{array}) (\begin{array}{cc} 1 & - b φ^{- 1} \end{array}) = (\begin{array}{cc} 0 & b φ^{- 1} \\ 0 & 1 \end{array})$ and $(d h + h d)^{n + 1} = d^{n} h^{n + 1} + h^{n + 2} d^{n + 1} = (\begin{array}{cc} a & b \\ c & φ \end{array}) (\begin{array}{cc} 0 & 0 \\ 0 & φ^{- 1} \end{array}) = (\begin{array}{cc} 0 & b φ^{- 1} \\ 0 & 1 \end{array})$ , using $h^{n + 2} = 0$ .

step 1.3L2algebra

2.4

$(p h)^{j} = p^{j - 1} h^{j} = 0$ for all $j$ : for $j = n + 1$ this is $p^{n} h^{n + 1} = (\begin{array}{cc} 1 & 0 \end{array}) (\begin{array}{cc} 0 & 0 \\ 0 & φ^{- 1} \end{array}) = (\begin{array}{cc} 0 & 0 \end{array})$ , and for $j \neq n + 1$ the factor $h^{j}$ is zero.

step 1.1step 1.3L3algebra

2.5

$(h ı)^{j} = h^{j} ı^{j} = 0$ for all $j$ : for $j = n + 1$ this is $h^{n + 1} ı^{n + 1} = (\begin{array}{cc} 0 & 0 \\ 0 & φ^{- 1} \end{array}) (\begin{array}{c} 1 \\ 0 \end{array}) = (\begin{array}{c} 0 \\ 0 \end{array})$ , and for $j \neq n + 1$ the factor $h^{j}$ is zero.

step 1.2step 1.3L3algebra

2.6

$(h^{2})^{j} = h^{j - 1} h^{j} = 0$ for all $j$ : if $j \neq n + 1$ then $h^{j} = 0$ , and if $j = n + 1$ then $h^{j - 1} = h^{n} = 0$ .

step 1.3L3algebra

3.1

In every degree $j \notin {n, n + 1}$ one has $h^{j} = 0$ and $ı^{j} p^{j} = 1 \cdot 1 = 1$ , hence $(1 - ı p)^{j} = 0 = (d h + h d)^{j}$ . Together with steps 2.2 and 2.3 this gives $1 - ı p = d h + h d$ .

step 1.3step 2.2step 2.3L3algebra

4.1

Steps 2.1, 2.2, 2.3 and 3.1 show $p ı = 1$ and $1 - ı p = d h + h d$ for the explicit cochain maps $p, ı$ and homotopy $h$ , and steps 2.4 to 2.6 verify the three side conditions $p h = 0$ , $h ı = 0$ and $h^{2} = 0$ in the degree conventions stated. Hence the displayed data is an explicit strong deformation retract of $X^{∙}$ onto ${\overset{ˉ}{X}}^{∙}$ : a chosen retraction, a chosen section and a chosen contracting homotopy with the side conditions above. ∎

step 2.1step 2.2step 2.3step 3.1step 2.4step 2.5step 2.6

Depends on

Used by

Dependency tree · two levels

9 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)
Dror Bar-Natan, Fast Khovanov Homology Computations, section 4 Lemma 4.2 and section 5, printed p. 5 (standard reference, not scraped)