Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6-sol)audited 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.

K-flat sheaf complexes preserve quasi-isomorphisms

Statement

Let X be a topological space, let K∙ be a K-flat bounded-above complex of abelian sheaves on X (K-flat complexes of abelian sheaves in the bounded-above setting), and let s:A∙→B∙ be a quasi-isomorphism of bounded-above complexes of abelian sheaves (Quasi-isomorphism).

  1. The induced morphism of tensor-product total complexes Tot⁡(s⊗id⁡K):Tot⁡(A∙⊗ZK∙)⟶Tot⁡(B∙⊗ZK∙) of Tensor product of abelian sheaves and its total complex is a quasi-isomorphism.
  2. The same holds with the K-flat factor on the left: if K∙ is K-flat and s is a quasi-isomorphism, then Tot⁡(id⁡K⊗s) is a quasi-isomorphism, through the canonical isomorphism Tot⁡(K∙⊗ZA∙)≅Tot⁡(A∙⊗ZK∙) which on Kj⊗ZAi is y⊗x↦(−1)ijx⊗y.

Facts & Assumptions

[F1]

A bounded-above complex K∙ is K-flat when for every acyclic bounded-above complex F∙ the tensor-product total complex Tot⁡(F∙⊗ZK∙) is acyclic (K-flat complexes of abelian sheaves in the bounded-above setting).

[F2]

For a cochain map f the cone Cone⁡(f) is acyclic if and only if f is a quasi-isomorphism (The cone criterion from the general long exact sequence, Quasi-isomorphism).

[F3]

The cone convention is Cone⁡(f)n=Yn⊕Xn+1 with d(y,x)=(dYy+fx,−dXx) (Derived category of an abelian category).

[F4]

The tensor-product total complex has degree-n term ⨁i+j=nFi⊗ZGj and differential dFi⊗id⁡+(−1)iid⁡⊗dGj on the summand Fi⊗ZGj (Tensor product of abelian sheaves and its total complex).

[F5]

A complex is bounded above when Fn=0 for all sufficiently large n, so a complex whose terms are built from finitely many bounded-above complexes is again bounded above (Bounded, bounded below, and bounded above complexes).

[F6]

A complex is acyclic when it is exact at every degree (Exactness of a complex at a degree and acyclic complexes).

[F7]

A cochain map f:C∙→D∙ satisfies dDnfn=fn+1dCn in every degree (Cochain map).

[F8]

The tensor total complex of bounded-above complexes is defined with finite diagonals, and the Koszul signs of clause 3 of the stalk computation match the module-level convention (Stalks, coproducts and right exactness of the abelian sheaf tensor product).

Proof

Given: Bounded-above complexes A∙,B∙,K∙ of abelian sheaves on X with K∙ K-flat and s:A∙→B∙ a quasi-isomorphism, and bounded-above complexes F∙,G∙ for the swap computation.

1.1

For each i the map si⊗id⁡Kj is defined on the summands Ai⊗ZKj of Tot⁡(A∙⊗ZK∙) and is compatible with the coproduct injections, so it induces a degree-zero morphism Tot⁡(s⊗id⁡); it is a cochain map because s is a cochain map [F7] and the Koszul differential [F4] has the same shape on both sides, the sign factor (−1)i being unchanged by si.

F4F7
1.2

Assume the cone convention of [F3]. Define φ:Tot⁡(Cone⁡(s)⊗ZK∙)⟶Cone⁡(Tot⁡(s⊗id⁡K)) to be the identity on the summands Bp⊗ZKj and the identity, after the identification of the A-part of Cone⁡(s)p with Ap+1, on the summands Ap+1⊗ZKj. Then φ is an isomorphism of graded groups, both sides having degree-n term ⨁p+j=n(Bp⊗ZKj)⊕⨁p+j=n(Ap+1⊗ZKj), and a direct check on generators shows that it commutes with the differentials: for b∈Bp the element b⊗y of Cone⁡(s)p⊗Kj has dCone⁡(s)(b,0)=(dBb,0), so both sides give dBb⊗y+(−1)pb⊗dKy; for a∈Ap+1 the element (0,a)⊗y has dCone⁡(s)(0,a)=(s(a),−dAa), so the left side is s(a)⊗y−dAa⊗y+(−1)pa⊗dKy, while the right side, by [F3] with f=Tot⁡(s⊗id⁡) and by the Koszul differential of Tot⁡(A∙⊗ZK∙) [F4], is (s(a)⊗y, −dAa⊗y+(−1)pa⊗dKy), the same element. Hence φ is an isomorphism of complexes.

F3F4
2.1

Since s is a quasi-isomorphism, Cone⁡(s) is acyclic [F2, F6]; it is a bounded-above complex of abelian sheaves because its terms Bn⊕An+1 vanish for all sufficiently large n by [F5], and K∙ is bounded above, so the tensor-product total complex Tot⁡(Cone⁡(s)⊗ZK∙) is acyclic by the K-flatness of K∙ [F1]. By the isomorphism of step 1.2 the cone Cone⁡(Tot⁡(s⊗id⁡K)) of step 1.1 is acyclic, and therefore Tot⁡(s⊗id⁡K) is a quasi-isomorphism by the cone criterion [F2]. This is clause 1.

F1F2F5step 1.1step 1.2
3.1

For bounded-above F∙,G∙ define T:Tot⁡(F∙⊗ZG∙)→Tot⁡(G∙⊗ZF∙) on the summand Fi⊗ZGj by T(x⊗y):=(−1)ijy⊗x. This is an isomorphism of graded groups, and it commutes with the differentials: by [F4] the differential applied first gives T(dFx⊗y+(−1)ix⊗dGy)=(−1)(i+1)jy⊗dFx+(−1)i+i(j+1)dGy⊗x, while applying the differential of Tot⁡(G∙⊗ZF∙) first gives (−1)ij(dGy⊗x+(−1)jy⊗dFx); the two expressions agree because (−1)(i+1)j=(−1)ij(−1)j and (−1)i+i(j+1)=(−1)ij; the Koszul signs used are those of the sheaf-level total complex, consistent with the module-level convention on stalks [F8]. Applying step 1.1 and step 2.1 to the swap of s gives clause 2.

F4step 1.1step 2.1
4.1

Clause 1 is step 2.1 and clause 2 is step 3.1. Both isomorphisms are canonical: the cone is the canonical cone of [F3], the identification of step 1.2 is the identity on the canonical summands, and the swap sign (−1)ij is forced by the Koszul convention [F4] through the computation of step 3.1; no selection is made beyond the hypotheses, and the K-flatness input [F1] is a universal statement about all acyclic bounded-above complexes. ∎

F1F3F4step 1.1step 1.2step 2.1step 3.1

Depends on

Used by

Dependency tree · two levels

46 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