Finite-degree bicomplex comparison
Abstract
Triangular column homology comparison controls native total homology through a finite degree.
Let C be any abelian category with independent object universe u and morphism universe v. Let K and L be bicomplexes indexed by two natural numbers, with both differentials lowering their respective index. The column p is the actual complex K.X p, and columnMap(phi,p) is phi.f p. Its degree-q homology map is the native homologyMap.
Theorem 1.1 (Isomorphisms below the boundary and epimorphism on it).
Proof. Machine-checked in Lean as D5/S3/Topology/TauCeti/Algebra/Homology/FiniteDegreeComparison.finite_degree_comparison_total_map (✓ std3). ∎
Source. Repository-derived.
Acknowledgement. The Tau Ceti contributors; Claude (extension-homology support) (2026). First-quadrant row-to-total quasi-isomorphism comparison. URL: https://github.com/TauCetiProject/TauCeti/blob/580580ea8726c50dcf98e199fa0a7caef5a74302/TauCeti/Algebra/Homology/TotalComplex.lean.
Commentary.
Assume the actual column homology map is an isomorphism when p+q is at most k and an epimorphism when p+q=k+1. Then the actual total map is an isomorphism on homology in every degree n at most k and an epimorphism in degree k+1. The boundary epimorphisms are part of the hypotheses and the conclusion. No condition is imposed above that boundary, and no entire row or column is required to be a quasi-isomorphism.
The total object in degree n is the native finite coproduct over p+q=n, and totalMap(phi,down(Nat)) is HomologicalComplex2.total.map on these same coproducts. The differential on the (p,q) summand is d1+(-1)^p d2. Finite antidiagonals supply the needed coproducts in every abelian category. There is no bound on the set of columns or on the support, and no supplied convergence theorem, comparison hypothesis, field or module restriction.
First prove a row version by simultaneous induction on Q: row-homology isomorphisms at p+q<Q and epimorphisms at p+q=Q imply total-homology isomorphisms below Q and an epimorphism at Q. Row zero includes into the total. The quotient is the extension by zero of Tot(rowsSucc(K)) along n mapped to n+1. The short exact sequence splits in each degree, naturally in the bicomplex map. At Q=0 its quotient has zero homology in degree zero, so row-zero surjectivity gives the required epimorphism.
For Q+1, apply the induction hypothesis to rowsSucc, whose row q is the original row q+1. Its triangular bounds are exactly those for Q after reindexing. Extension by zero gives the quotient isomorphisms in degrees below Q+1 and epimorphisms through Q+1, including the preceding degree needed by the middle-map isomorphism lemma. On row zero, the bounded hypotheses supply the isomorphism at the requested degree, the monomorphism in the following degree, and the boundary epimorphism. The local homology-sequence diagram lemmas then give both total assertions. Deleting a row preserves p, so the quotient keeps the sign (-1)^p; this extension is not a signed suspension.
Flip the bicomplex so that its rows are the original columns, with their actual maps phi.f p. The native totalFlipIso identifies the flipped total with the original total by multiplication by (-1)^(p*q) on each summand. Its naturality identifies the total of the flipped morphism with the actual total morphism. Apply the row induction at Q=k+1 and transport homology across this signed isomorphism to obtain precisely the stated column result.
This is a standard general finite-degree comparison theorem. The row-zero decomposition and local transfer statements come from the cited Tau Ceti sources; the bounded induction composes them here. This theorem alone makes no claim about an augmentation, a nerve, an open cover, or a singular-chain construction.
Application to the homological nerve theorem
Let X be any topological space, I any index type, U an open cover indexed by I, G any abelian group and k a natural number. For a finite subset s of I write U_s for the intersection of its cover members. A supported face is a nonempty finite s for which U_s is nonempty. Assume that reduced singular homology Htilde_j(U_s;G) vanishes whenever s is supported, its cardinality is at most k+1, and j+card(s) is at most k+1. Then ordinary singular H_n(X;G) and ordinary simplicial H_n(N(U);G) are isomorphic for every n at most k. Nonzero H_(k+1)(N(U);G) implies nonzero H_(k+1)(X;G). This is the known homological nerve conclusion of Gillespie, Theorem 1, with arbitrary coefficient groups; the Library note identifies the original source and the additional Cech suppliers. It is an application of the comparison theorem and those suppliers.
Choose an order on I internally. The ordinary incidence nerve chain group in degree p is the coproduct of G over supported finite faces of cardinality p+1. For positive p its boundary deletes each vertex i with sign (-1) to the number of vertices of s strictly below i. In particular, an ordered edge has boundary its second vertex minus its first. The outgoing differential in degree zero is zero; this is ordinary H0, with no augmentation term in the nerve chain complex. Empty cover members contribute no vertices, and infinite covers use finite faces without imposing a bound on their cardinalities across degrees.
The singular Cech bicomplex has in position (p,q) the coproduct of singular q-chains of U_s over all finite s of cardinality p+1. Map it to a support-sensitive bicomplex B whose (p,0) object is the coproduct of G over those s and their nonemptiness witnesses, with zero positive vertical degrees. Thus an empty intersection has zero target. The actual map on each summand is the singular augmentation to that support object. It commutes with the singular differential and the signed face deletions, so the native total differential remains dH+(-1)^p dV.
For every intersection, the induced degree-zero support augmentation is epimorphic. If the intersection is inhabited, its map becomes the ordinary H0 augmentation after identifying the support object with G, and a point supplies a section. If it is empty, both chains and support target are zero. Its H0 map is an isomorphism under reduced-H0 vanishing. In every positive degree the target homology is zero, giving an unconditional epimorphism and an isomorphism when the corresponding reduced homology vanishes. This argument never asserts that ordinary H0 of the empty space surjects onto an arbitrary G.
Exact coproducts of abelian groups identify the actual column homology map with the coproduct of those summand maps. At p+q at most k, the identity card(s)=p+1 turns the needed vanishing into precisely q+card(s) at most k+1. Empty intersections already have zero source and target. All column maps are epimorphic without a vanishing assumption, including the boundary (k+1,0), whose faces have cardinality k+2. The finite-degree comparison therefore gives an isomorphism on actual total homology through k and an epimorphism at k+1. The exact-coproduct property here is supplied by AddCommGrpCat’s AB4 structure; it is an ingredient of this application, not an extra hypothesis of the general finite-antidiagonal comparison theorem.
The actual Cech total augmentation is a quasi-isomorphism onto singular chains for any open cover. Its descent uses the ordered free-cover contraction and the small-singular-chain equivalence. The zero row of B is chain-isomorphic to the incidence nerve by the same supported-face generators and signed deletions. Since B has zero positive vertical degrees, its native zero-row inclusion is a chain isomorphism onto its total complex. Compose the inverse homology map of the actual Cech augmentation, the actual total comparison, and the inverse nerve-to-total identification. This particular singular-to-nerve map has the stated isomorphism range and is epimorphic in degree k+1. A zero source cannot surject onto a nonzero target, giving the nonvanishing implication without asserting an isomorphism in that boundary degree.
Independent input universes require explicit coefficient and endpoint transport. If X, I and G have universe levels x, i and g, use the canonical lift of G in AddCommGrpCat at a=max(x,g) for original-space singular homology, and at b=max(i,g) for original-index nerve homology. Compare the canonical lifts of those endpoint objects at W=max(x,i,g). Coproduct reindexing identifies original singular simplices and supported finite faces with the common-universe models; nested coefficient lifts flatten to the same original G. The identifications preserve simplex operators, intersection inclusions, face cardinality, deletion and rank signs. Ordinary homology transport uses the actual degree short complexes. Reduced H0 transport additionally uses the vertex-induced augmentation square and its kernel comparison; positive reduced degrees use ordinary transport. Faithful endpoint lifting reflects zero objects, so the boundary nonvanishing statement concerns the original endpoint homology groups. No homology carrier is required to fit in g alone.
The conclusion includes empty X, empty indices, empty cover members, infinite covers, zero G and k=0. It requires neither finiteness, local finiteness, paracompactness, field coefficients nor full acyclicity of all intersections. It asserts an isomorphism through k and only an epimorphism at k+1, with no bound above that degree. The order is an internal choice, not a user premise. The additional descent and transport suppliers are distinct from the single frozen comparison declaration described above; this application exposition does not introduce a separate Lean declaration or a literature-novel theorem.