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

A free PID complex decomposes into two-term cycle-boundary pieces

Statement

Assume AC. Let R be a commutative PID and C a nonnegative chain complex of free R-modules of arbitrary rank. Set ZnC=ker⁡dn, BnC=im⁡dn+1, and B−1C=0. Cycles and boundaries are free. There are sections sn:Bn−1C→Cn of the differential corestricted to its image, giving Cn≅ZnC⊕Bn−1C,c⟼(c−sn(dnc),dnc). In these coordinates the differential is (z,b)↦(b,0), with b included in Zn−1C. Consequently C is isomorphic to the direct sum of the two-term free complexes BpC↪ZpC in degrees p+1,p.

Let Z(C)n=ZnC and A(C)n=Bn−1C, both with zero differential. There is a canonical degreewise split short exact sequence of complexes 0⟶Z(C)→ιC→ρA(C)⟶0,ρn=dn:Cn→Bn−1C. The same assertions apply to any such complex D. No splitting of BpC↪ZpC is asserted.

Facts & Assumptions

Given: R,C and AC as in the statement; negative terms are zero.

[F1]

The cycle-boundary short exact sequences are 0→ZnC→Cn→Bn−1C→0 and 0→BnC→ZnC→HnC→0: The cycle-boundary short exact sequences for a free complex over a PID.

[F2]

Under AC, submodules of arbitrary free PID modules are free: Under Choice, a submodule of an arbitrary-rank free module over a PID is free.

[F3]

Under AC, free modules lift maps through surjections: Free modules are projective, with the exact choice boundary.

[F4]

Nonempty families of choices can be selected simultaneously under AC: The Axiom of Choice.

Proof

1.1F1F2given

Both ZnC and BnC are submodules of the free module Cn, the latter lying in the former since dndn+1=0. Apply the local submodule lemma to get their freeness for every n. Thus the second sequence in [F1] is a length-one free presentation of HnC.

2.1step 1.1F1F3F4

The surjection dn:Cn↠Bn−1C admits a lift of the identity of its free target, hence a section sn. For each n the set of such sections is nonempty; AC selects one for every degree. At n=0, take the unique map s0:0→C0.

3.1step 2.1F1

Define un(z,b)=z+sn(b) and vn(c)=(c−sn(dnc),dnc). The first component of vn(c) is a cycle because its differential is dnc−dnsn(dnc)=0. Both maps are linear. Substitution gives unvn(c)=c and vnun(z,b)=(z,b), since dnz=0 and dnsn(b)=b. Thus they are inverse isomorphisms.

4.1step 3.1F1

Compute dnun(z,b)=b. Since dn−1b=0, its image under vn−1 is (b,0). For each p let E(p) have BpC in degree p+1, ZpC in degree p, and differential the inclusion. In degree n, ⨁p≥0E(p) is ZnC⊕Bn−1C with precisely the differential just computed. The maps un therefore form the claimed chain isomorphism. Only two summands occur in each degree.

5.1step 2.1step 4.1F1∎

Inclusion ι is a chain map because dn kills ZnC. The map ρ is a chain map to the zero-differential complex A(C) because ρn−1dn=dn−1dn=0. Its kernel and image in degree n are ZnC and Bn−1C, respectively. This proves the canonical short exact sequence, and the selected sn prove degreewise splitting. Those sections need not be chain maps: dnsn(b)=b can be nonzero. All formulas hold for the zero complex and for degree zero; replacing C throughout by D proves the stated second application.

Depends on

Dependency tree · 2 levels

Sources