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.

Wreath double-power comparison and coefficient transposition

Statement

Assume AC. Let $p$ be prime, let $K$ be a finite oriented regular cell complex, and let

$x \in H_{c e l l}^{q} (K; F_{p}) .$

Index the $p^{2}$ factors of $K^{p^{2}}$ by $(i, j) \in Z / p \times Z / p$ , and let $α (i, j) = (i + 1, j)$ and $β (i, j) = (i, j + 1)$ . The iterated external power, formed first in the columns and then in the rows, and the one-step $p^{2}$ -fold external power for $R = ⟨ α, β ⟩ ≅ C_{p} \times C_{p}$ have the same pullback along the double diagonal to $W_{1} \times W_{2} \times K$ .

Using the standard cyclic basis on the two resolution factors, write this common class uniquely as

$\sum_{j, k \geq 0} [w_{j}] \times [w_{k}] \times D_{j, k} (x), D_{j, k} (x) \in H_{c e l l}^{p^{2} q - j - k} (K; F_{p}) .$

Then

$D_{j, k} (x) = (- 1)^{j k + p (p - 1) q / 2} D_{k, j} (x) .$

The coefficient is zero when $p^{2} q - j - k < 0$ . This lemma concerns the finite regular cellular construction. It asserts neither an Adem relation nor the later extension to arbitrary singular spaces.

Facts & Assumptions

Given: AC, a prime $p$ , a finite oriented regular cell complex $K$ , a degree- $q$ cellular class $x$ , and two copies $W_{1}, W_{2}$ of the standard cyclic resolution.

[F1]

The equivariant carrier comparison applies to any group acting freely on the chosen chain basis; relative extensions are valid for subcomplexes spanned by unions of free cell orbits (Equivariant p-fold external power and diagonal decomposition).

[F2]

The standard cyclic resolution has one cohomology basis class $[w_{j}]$ in every nonnegative degree (Free cyclic resolution, group cohomology, and cochain transfer).

[F3]

AC supplies a choice function for every set-indexed family of nonempty sets (The Axiom of Choice).

Proof

Proof technique: identify the direct and iterated tensor cocycles on a common row--column resolution, pull them back to two cyclic coordinates, and apply matrix transposition while retaining both Koszul signs.

1.1

Build the row--column free resolution. [given] Let $R = ⟨ α, β ⟩$ . On $W_{1} \otimes W_{2}^{\otimes p}$ , let $α$ act on $W_{1}$ and cyclically permute the $p$ copies of $W_{2}$ , with the tensor Koszul sign, and let $β$ act diagonally on those $p$ copies. These actions commute and implement the displayed permutations of the $p \times p$ array.

The tensor product is augmented and acyclic because each $W_{i}$ is an augmented free resolution and tensoring their augmented contractions over the field $F_{p}$ gives an augmented contraction. It is free as an $R$ -complex. Indeed, an element $α^{a} β^{b}$ fixing a tensor-basis cell must have $a = 0$ , since its action on the $W_{1}$ -cell is free; with $a = 0$ , freeness of every $W_{2}$ -cell forces $b = 0$ . Thus $W_{1} \otimes W_{2}^{\otimes p}$ is a free acyclic $R$ -resolution.

1.2

Define the one-step $R$ -power directly on the row--column resolution. [F1, F3, step 1.1] Choose a degree- $q$ cellular cocycle $c$ representing $x$ . Put $V = W_{1} \otimes W_{2}^{\otimes p}$ . On $V \otimes C^{\otimes p^{2}}$ define $P_{R} (c)$ on a pure tensor by

$ε_{1} (w) \prod_{r = 1}^{p} ε_{2} (v_{r}) \prod_{r = 1}^{p} \prod_{s = 1}^{p} c (z_{r, s}) .$

The tensor differential and $c d = 0$ make this a cocycle. It is $R$ -equivariant: a $p$ -cycle acting on degree- $q$ coefficient factors has sign $(- 1)^{q^{2} (p - 1)} = 1$ for odd $p$ , and every sign is $1$ over $F_{2}$ .

This class depends only on $x$ . If $c^{'} - c = δ b$ , the usual interval cochain $D : I \otimes C \to F_{p} [- q]$ has endpoints $c, c^{'}$ . Apply the relative carrier theorem in [F1] with $Γ = R$ and the whole target $I^{\otimes p^{2}} \otimes V$ as carrier for each free orbit generator of $I \otimes V$ . This carrier is $R$ -invariant and augmented acyclic: the cellular interval complex and $V$ have augmented contractions, and their finite tensor product over $F_{p}$ is augmented contractible. The two endpoint copies of $V$ span an $R$ -subcomplex made of free cell orbits, since $R$ acts freely on the $V$ basis; both prescribed endpoint maps are augmentation-preserving. The theorem therefore extends the two endpoint maps to an $R$ -map $I \otimes V ⟶ I^{p^{2}} \otimes V,$ where $R$ permutes the interval factors as it permutes the matrix positions. After the canonical signed regrouping, evaluation by $D^{\otimes p^{2}}$ is a cochain homotopy from $P_{R} (c)$ to $P_{R} (c^{'})$ . The relative subcomplex is exactly the one just checked. Its orbitwise fillings are the only use of AC here.

2.1

Compare with the iterated cocycle and pull back. [F1, step 1.1, step 1.2] Form the iterated representative by first applying $ε_{2} \otimes c^{\otimes p}$ in each row and then applying the same tensor-power formula with $ε_{1}$ to the $p$ resulting factors. The canonical signed regrouping

$(W_{2} \otimes C^{\otimes p})^{\otimes p} ⟶ W_{2}^{\otimes p} \otimes C^{\otimes p^{2}}$

moves each resolution and coefficient factor through exactly the same homogeneous factors as the tensor-evaluation convention. The two Koszul signs therefore cancel, and on every pure tensor the iterated functional is exactly $P_{R} (c)$ .

For the resolution diagonal $d_{2} : W_{2} \to W_{2}^{\otimes p}$ , use the whole $W_{2}^{\otimes p}$ as carrier. It is $C_{p}$ -invariant and augmented acyclic by the tensor contraction, while $W_{2}$ has free $C_{p}$ -orbit cells, so [F1] gives an augmentation-preserving equivariant comparison, unique up to carried homotopy. For the cellular double diagonal, assign to a product basis generator $v \otimes e$ the cellular chains of the product of the closed characteristic cell $\overline{e}$ in all $p^{2}$ coordinates, tensored with the relevant resolution carrier. Regularity makes $\overline{e}$ a closed disk; its finite product has augmented-acyclic cellular chains. These nested carriers are $R$ -invariant under permutation of the product coordinates. The source $V \otimes C$ has free $R$ -orbit basis by Step 1.1, so [F1] supplies the equivariant carried approximation to $d^{'} : K \to K^{p^{2}}$ and uniqueness up to carried homotopy. The two cocycles therefore have the same pullback to $W_{1} \otimes W_{2} \otimes C_{*} (K; F_{p})$ , which proves the first claim. Carrier homotopy uniqueness makes the resulting class independent of the chosen resolution and cellular diagonal approximations.

3.1

Define the double coefficients uniquely. [F2, step 2.1] After the double pullback, $α$ acts only on $W_{1}$ , $β$ only on $W_{2}$ , and both act trivially on $K$ . In equivariant Hom, the two resolution differentials act by their augmentations and hence by zero over $F_{p}$ . Since each resolution degree is free of rank one, the total cochain complex decomposes coordinatewise and [F2] gives

$H_{R}^{n} (W_{1} \times W_{2} \times K; F_{p}) = ⨁_{j + k \leq n} [w_{j}] \times [w_{k}] \times H_{c e l l}^{n - j - k} (K; F_{p}) .$

For $n = p^{2} q$ , the unique coordinates in this direct sum are the classes $D_{j, k} (x)$ in the statement. A coordinate with $j + k > p^{2} q$ lies in a negative cellular cochain degree and is therefore zero.

4.1

Compute the effect of transposing the array. [F2, step 1.1, step 3.1] Let $λ (i, j) = (j, i)$ . It conjugates $α$ to $β$ and $β$ to $α$ . On the two-factor cyclic resolution the compatible chain map is the graded symmetry

$L (v_{1} \otimes v_{2}) = (- 1)^{∣ v_{1} ∣ ∣ v_{2} ∣} v_{2} \otimes v_{1} .$

Consequently $L$ sends the $(j, k)$ -basis coordinate to $(- 1)^{j k}$ times the $(k, j)$ -coordinate.

The permutation $λ$ fixes the $p$ diagonal positions and exchanges the other $p^{2} - p$ positions in $p (p - 1) / 2$ pairs. Its sign is therefore $(- 1)^{p (p - 1) / 2}$ . Permuting $p^{2}$ degree- $q$ coefficient factors acts on their one-dimensional tensor line by the $q$ th power of that sign, namely $(- 1)^{p (p - 1) q / 2}$ .

The direct tensor cocycle of step 2.1 is invariant under the simultaneous position transpose and this coefficient action, while the double diagonal is fixed by transpose. Hence transpose sends its $(j, k)$ -summand to

$(- 1)^{j k + p (p - 1) q / 2} [w_{k}] \times [w_{j}] \times D_{j, k} (x) .$

Uniqueness of the coordinates in step 3.1, followed by exchanging $j$ and $k$ , gives the asserted formula.

5.1

Empty and zero complexes give zero coefficients, and a point gives $D_{0, 0} (a) = a$ . [F3, step 1.2, step 2.1, step 3.1, step 4.1] For the empty complex or the zero cellular complex all classes and coefficients are zero. For a point in degree zero, only $D_{0, 0} (a) = a^{p^{2}} = a$ can be nonzero. The zero class is represented by the zero cocycle and has every coefficient zero. Step 3.1 includes $j = 0$ , $k = 0$ , and $j + k = p^{2} q$ , and proves vanishing beyond that endpoint.

At $p = 2$ , both displayed signs are invisible in $F_{2}$ ; at odd primes the cyclic equivariance sign in step 2.1 is $1$ , while the transpose sign remains exactly the exponent in step 4.1. Cellular chains have no singular degeneracy operators, so a degenerate-simplex check is item-specifically inapplicable and remains part of the deferred singular extension. The sole use of AC from [F3] is the carrier comparison already isolated in step 1.2; all index sets and tensor regroupings and transpositions here are explicit and finite. No implication in the argument uses Cartan or an Adem relation. ∎

Depends on

Used by

Dependency tree · two levels

9 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

N. E. Steenrod and D. B. A. Epstein, Cohomology Operations (standard reference, not scraped)