Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-10
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.

The cycle-boundary tensor sequence has the Kunneth kernel and cokernel

Statement

Assume AC. Let R be a commutative PID and C,D nonnegative complexes of free R-modules of arbitrary rank. Tensor complexes use direct-sum totalization and d(c⊗y)=dCc⊗y+(−1)pc⊗dDy(c∈Cp). Put Z(C)p=ZpC and A(C)p=Bp−1C with zero differentials, where B−1C=0. Set X=Z(C)⊗RD, T=C⊗RD, Y=A(C)⊗RD. The canonical sequence 0→X→T→ρ⊗1Y→0 is exact.

Under the canonical identifications HnX≅⨁p+q=nZpC⊗RHqD,HnY≅⨁p+q=nBp−1C⊗RHqD, the connecting map ∂n:HnY→Hn−1X is the sum of inclusion-induced maps Bp−1C⊗HqD→Zp−1C⊗HqD, with positive sign. Consequently ker⁡∂n≅⨁r+q=n−1Tor⁡1R(HrC,HqD),coker⁡∂n+1≅⨁p+q=nHpC⊗RHqD. The corestricted map Hn(ρ⊗1) followed by this kernel identification is the established Tor quotient. The induced map from the displayed cokernel sends [z]⊗[w] to [z⊗w]. All indices in sums are nonnegative; empty sums are zero.

Facts & Assumptions

Given: The ring, complexes, AC, and tensor convention in the statement.

[F1]

The canonical cycle sequence is degreewise split, and cycles and boundaries give free presentations of homology: A free PID complex decomposes into two-term cycle-boundary pieces.

[F3]

Tensor products commute with arbitrary direct sums over a commutative ring: Tensor products commute with arbitrary direct sums.

[F4]

Short exact sequences of complexes give exact homology sequences: The long exact sequence in homology.

[F5]

With DC and supplied projective resolutions, balanced Tor is computed by resolving either variable: The balanced Tor bifunctor.

[F6]

Tensoring over a commutative ring is right exact: Tensoring is right exact.

[F7]

The earlier Tor quotient uses the canonical cycle-boundary presentations: The Kunneth Tor map.

[F8]

AC supplies simultaneous choices: The Axiom of Choice.

[F9]

A self-map of a set can be iterated from any given initial element: The recursion theorem.

[F10]

DC requests such a sequence along any entire relation from a prescribed point: The axiom of dependent choice: a relation in which every element is related to something admits an N-indexed chain.

[F11]

Under AC, free modules are projective: Free modules are projective, with the exact choice boundary.

Proof

1.1F8F9F10F1F11F5

AC implies the particular DC principle needed in [F5]. For an entire relation E on a nonempty set S, each successor set Ex={y:xEy} is nonempty. Choose f(x)∈Ex simultaneously. Recursion from any prescribed a∈S gives x0=a, xm+1=f(xm), hence xmExm+1 for every m. This is [F10]. For each HrC and HqD, [F1] supplies a length-one free resolution, and [F11] makes it projective. Thus [F5] applies to these actual supplied resolutions.

1.2F1F2F3

Choose the degreewise sections from [F1]. In bidegree (p,q), tensoring Cp≅ZpC⊕Bp−1C with Dq identifies the two maps with inclusion and projection of a direct sum. Their kernel and image therefore agree and projection is onto. Summing over the finite diagonal proves exactness of 0→X→T→Y→0. Inclusion and ρ⊗1 are chain maps: dC kills cycles and ρdC=0, while the terms (−1)pdD agree on both sides.

1.3F2F3F8

For a free module U=⨁i∈IRei placed in degree p, [F3] identifies U⊗Dq with ⨁iDq by ei⊗y↦y in coordinate i (the maps R⊗Dq→Dq, r⊗y↦ry, and y↦1⊗y are inverse). Its differential is coordinatewise (−1)pdD. A finite tuple is a cycle exactly when every coordinate is a cycle. Its image consists exactly of finite tuples of boundaries: for the reverse containment choose a preimage for each of the finitely many nonzero coordinates and multiply it by (−1)p. Quotienting therefore gives U⊗HqD≅Hp+q(U⊗D) by u⊗[y]↦[u⊗y]. Although a basis proves bijectivity, this formula is independent of that basis.

2.1F1step 1.3

Apply this calculation to the free modules U=ZpC and U=Bp−1C and sum in p. There is no differential between distinct p summands, so cycles, boundaries, and homology decompose over this finite diagonal. This gives both displayed homology identifications. The summand with p=0 in HnY is zero because B−1C=0.

2.2step 1.1F5F6

Fix r,q≥0. The resolution P1=BrC↪P0=ZrC↠HrC, with Pi=0 for i≥2, is projective by step 1.1. Tensoring it with HqD computes first homology as the kernel of jr⊗1:BrC⊗HqD→ZrC⊗HqD, because the degree-two boundary is zero. By [F5] this kernel is Tor⁡1R(HrC,HqD). Right exactness gives the cokernel as HrC⊗HqD, using the augmentation z↦[z]. No injectivity of jr⊗1 is assumed.

3.1F1F2F4step 1.2step 2.1

A class in a (p,q) summand of HnY is a finite sum of b⊗[y] with dDy=0. Lift its representing cycle to the corresponding sum sp(b)⊗y in Tn. Its differential is b⊗y+(−1)psp(b)⊗dDy=b⊗y, now in Xn−1. The lift-and-boundary construction of the connecting map in [F4] therefore gives ∂n(b⊗[y])=b⊗[y] with b included into Zp−1C. The formula holds for sums, not just decomposable classes.

4.1step 2.1step 3.1step 2.2

In step 3.1 put r=p−1 and discard the zero p=0 summand. A sum maps to zero exactly when each of its components does; its cokernel is the sum of the component cokernels, since each relation lies in its own summand. Step 2.2 thus gives the asserted kernel in degree n−1 and cokernel in degree n. At n=0 the kernel is zero; at n=1 it is precisely Tor⁡1(H0C,H0D). If HqD=0, both tensor modules are zero. If HrC=0, its presentation has BrC=ZrC and inclusion the identity, so tensoring gives an isomorphism with zero kernel and cokernel.

5.1F4F7step 1.2step 1.3step 2.2step 4.1∎

The homology LES makes the image of Hn(ρ⊗1) exactly ker⁡∂n. Corestrict it and use the identification of step 2.2. This is the same canonical sequence, map ρ, positive connecting map, and free presentation used to construct the quotient in [F7], so it is that quotient, rather than merely some surjection onto an isomorphic module. On the other side, the cokernel class of z⊗[w]∈ZpC⊗HqD is [z]⊗[w]; its image under Hn(X→T) is [z⊗w] by step 1.3. This identifies the asserted injection formula at the level of the actual maps.

Depends on

Dependency tree · 2 levels

Sources