Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-12
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 kronecker pairing is independent of cocycle and cycle representatives

Statement

The Kronecker rule [φ],[c]=φ(c) is independent of both cocycle and cycle representatives and is additive in both variables. For a continuous f:XY, αHn(Y;G) and zHn(X;Z), it satisfies fα,z=α,fz. For a coefficient homomorphism u:GG, it satisfies uα,z=uα,z. The same representative-independence argument gives the R-bilinear pairing for R-linear cochains on chains over a commutative ring R.

Facts & Assumptions

[F1]

Kronecker evaluation pairing specifies evaluation on cocycle/cycle representatives.

[F2]

Singular cochain complex with coefficients gives δψ=ψ, and Singular cohomology with coefficients identifies changes of cocycle representative as coboundaries. The singular chain complex and singular homology identifies changes of cycle representative as boundaries.

[F3]

Singular cohomology is contravariantly functorial gives f[φ]=[φf#] and coefficient postcomposition; Singular chains and singular homology are covariantly functorial gives f[c]=[f#c].

Proof

Given: A cocycle φ and cycle c of degree n0, with the spaces, maps and coefficients needed in each assertion.

1.1

Replacing φ by φ+δψ changes its value on c by (δψ)(c)=ψ(c)=ψ(0)=0. Replacing c by c+b changes its value under φ by φ(b)=(δφ)(b)=0. The replacement cocycle is still closed and the replacement cycle still a cycle by their defining quotient subgroups. Applying the two equalities successively therefore allows both representatives to change at once. This proves descent through both quotients.

F1F2
2.1

On representatives (φ+ψ)(c)=φ(c)+ψ(c) and φ(c+c)=φ(c)+φ(c). Zero and negatives obey the same evaluation rules. In the ring version, φ(rc)=rφ(c) and (rφ)(c)=rφ(c) by R-linearity; the two vanishing calculations of step 1.1 use the same positive differential and remain valid for R-linear maps.

F1F2step 1.1
2.2

For representatives of α,z, the left spatial pairing is (φf#)(c)=φ(f#c), exactly the right pairing by [F3]. Its representatives are valid cycles and cocycles because the induced maps preserve them. Likewise (uφ)(c)=u(φ(c)) proves coefficient naturality. Step 1.1 makes these representative identities identities on quotient classes.

F1F3step 1.1
3.1

Step 1.1 proves representative independence, step 2.1 descends to biadditivity and the stated R-bilinearity, and step 2.2 proves naturality. In degree zero there are no negative cochains to change the cocycle, but changing a zero-cycle by a one-boundary is still covered by the second calculation. Negative-degree groups and empty-space or zero-coefficient groups pair to zero. On a point, the degree-zero chain m[x] evaluates to mφ(x), including m=0 and m=1; no generators in higher unnormalized chain degrees are discarded. The proof compares arbitrary representatives without choosing a representative function, so it uses no AC.

F1F2step 1.1step 2.1step 2.2

Depends on

Used by

Cited to discharge well-definedness by Kronecker evaluation pairing.

Dependency tree · two levels

15 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