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

Free cyclic resolution, group cohomology, and cochain transfer

Statement

Let p be prime, Cp=T, R=Fp[Cp], and N=1+T++Tp1. The augmented complex of free left R-modules

Re2NRe1T1Re0εFp0,

with d(e2r+1)=(T1)e2r and d(e2r)=Ne2r1 for r1, is exact. If Fp has the trivial R-action, then the cohomology of HomR(W,Fp), with the cup product induced by the standard equivariant diagonal, is

H(Cp;Fp)={F2[t],p=2,t=1,Fp[u]Λ(v),p odd,u=2, v=1.

With the positive connecting convention, one may take v=[w1] and u=[w2]=βv when p is odd; for p=2, t=[w1] and βt=t2.

On quotient cellular chains, the standard equivariant diagonal has the exact form

D(e2r)=a=0re2ae2r2a+p(p1)2a=0r1e2a+1e2r2a1,

D(e2r+1)=a=02r+1eae2r+1a.

In particular, at p=2 every split of the total resolution degree occurs with coefficient one.

More generally, let HG with G finite, let C be a chain complex of left Fp[G]-modules, and let A be a left Fp[G]-module. There is a cochain map

TrHG:HomH(C,A)HomG(C,A)

such that TrHGResHG=[G:H] on G-equivariant cochains. Consequently this composite is zero over Fp whenever p divides [G:H]; the transfer of an arbitrary H-equivariant class need not itself be zero.

Facts & Assumptions

Given: A prime p, the displayed cyclic resolution, and, for the transfer clause, HG, C, and A as in the statement.

[F1]

Cohomology is the quotient of cocycles by coboundaries (Singular cohomology with coefficients).

[F2]

For the mod-p Bockstein, least nonnegative residue lifts are canonical and require no AC (Bockstein connecting operation).

[F3]

The cochain external product evaluates a tensor functional on tensor chains, with no extra sign in that evaluation (Additive singular cohomology cross product). The cyclic chain diagonal used to define the internal product is the explicit Steenrod--Epstein construction quoted in Step 4.1, not a claim of the cross-product definition.

Proof

Proof technique: compute kernels in the truncated polynomial group ring, then evaluate the explicit cyclic diagonal and define transfer directly on the finite quotient set.

1.1

Identify the group ring and the two differentials. [given] Put s=T1. In characteristic p, (1+s)p=1+sp, so the basis 1,T,,Tp1 gives

RFp[s]/(sp).

Expanding (T1)p1 and using (p1j)(1)j(modp) gives N=sp1. Hence sN=Ns=sp=0, which proves d2=0.

1.2

Define transfer without choosing coset representatives. [given] For a left coset gHG/H and fHomH(Cn,A), define

ΦgH(f)(c)=gf(g1c).

This depends only on the coset: replacing g by gh gives

ghf(h1g1c)=ghh1f(g1c)=gf(g1c)

by H-equivariance. Hence TrHGf=gHG/HΦgH(f) is a specified finite sum over the quotient set, not a sum requiring a chosen transversal. For kG, substitution g=kr permutes G/H and gives (Trf)(kc)=k(Trf)(c), so the result is G-equivariant.

2.1

Prove exactness in every degree. [step 1.1] Every element of R has a unique form a0+a1s++ap1sp1. Multiplication by s has kernel Fpsp1=NR and image sR; multiplication by N=sp1 has kernel sR and image Fpsp1. Finally kerε=sR, the image of the first map T1=s. These equalities prove exactness at Fp, at Re0, and alternately at every positive degree. They also cover p=2, where the two displayed multipliers coincide.

2.2

Verify the cochain and restriction identities. [step 1.2] Because the G-action commutes with the differential of C,

δΦgH(f)(c)=gf(g1dc)=ΦgH(δf)(c).

The finite sum therefore commutes with δ. If f is already G-equivariant, every summand satisfies gf(g1c)=f(c), whence

TrHGResHG(f)=[G:H]f.

When p[G:H], that scalar is zero in Fp. This proves only the stated composite identity, not vanishing of transfer on an arbitrary class.

3.1

Compute the equivariant cochain groups. [F1, step 2.1] Let wjHomR(Rej,Fp) have wj(ej)=1. Each cochain group is the one-dimensional span of wj. Since the trivial action sends s to 0 and N to p=0, precomposition with every differential is zero. Thus every wj is a cocycle, there are no nonzero coboundaries, and [F1] gives one basis class [wj] in each degree.

4.1

Evaluate the cyclic diagonal. [F3, step 3.1] Steenrod--Epstein's cyclic-diagonal lemma in Chapter V, section 5, on printed page 67 constructs the equivariant cellular diagonal. After passing to the quotient and writing the single cell in degree j again as ej, its formulas on printed page 68 are

D(e2r)=a=0re2ae2r2a+p(p1)2a=0r1e2a+1e2r2a1,

D(e2r+1)=a=02r+1eae2r+1a.

The source verifies before quotienting that this is a chain map and a diagonal approximation; reduction modulo p therefore defines the cup product. Evaluating by the tensor functional of [F3] gives

w12=p(p1)2w2,w2r=w2r,w2rw1=w2r+1.

For p=2 the first coefficient is 1, so induction gives wj=w1j for every j. For odd p the coefficient is divisible by p, so w12=0, while the other two equations show that the displayed u=[w2] and v=[w1] produce the unique basis class in every degree. There can be no further relation, because a nonzero polynomial monomial ur or urv is exactly the nonzero basis vector in its degree. This proves the two asserted graded-algebra descriptions.

5.1

Fix the Bockstein sign. [F2, step 4.1] For the quotient cellular model over Z/p2, the relevant boundary is e2=pe1. Lift w1 by the canonical residues of [F2]. Its coboundary takes e2 to p; division by the coefficient inclusion apa therefore gives w2. Thus the positive convention here is β[w1]=[w2]. This says βt=t2 at p=2 and permits u=βv at odd p. This sign differs from sources that build a minus sign into their cochain connector.

6.1

If H=G transfer is the identity, while zero coefficients make it zero. [step 2.1, step 2.2, step 5.1] The prime endpoint p=2 was treated separately, and every odd prime uses the same divisible odd-odd coefficient. If H=G, the quotient has one element and transfer is the identity; if H={1}, the same formula is the full finite group sum. Zero chain groups, zero cochains, and zero modules make all maps zero. There are no negative resolution degrees; e0 and the augmentation were checked in step 2.1. The source's geometric model retains all cells, while the algebraic computation depends only on the displayed free modules and so has no separate degenerate-simplex exception. The only coefficient lift in step 5.1 is the canonical residue lift singled out in [F2], and step 1.2 sums representative-independent functions over a finite set. Thus the proof makes no arbitrary choice and uses no AC. ∎

Depends on

Used by

Dependency tree · two levels

8 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