The cyclic 2-group freeness criterion for Lemma 6.11 #
The constructive counting criterion that recognizes a finite 𝔽₂[P]-module as a finite power of the regular module.
See GQ2.RegularSummand for the paper-facing overview and references.
The counting criterion for 𝔽₂[P]-freeness over a cyclic 2-group #
free_of_card_fixedPoints_pow_le: a finite 2-torsion module V over a cyclic 2-group P
satisfying the counting bound #V^P ^ |P| ≤ #V is equivariantly isomorphic to a regular
module Fin r → P → ZMod 2. This is the 𝔽₂-rational endgame of the paper's Lemma 6.11
(pp. 29–30): the paper produces a regular 𝔽̄₂[P]-basis from free weight orbits and descends
projectivity along the faithfully flat 𝔽₂ ⊆ 𝔽̄₂; the counting criterion is the rational
shadow of that descent (the reverse bound #V ≤ #V^P ^ |P| always holds — Jordan filtration
of the nilpotent ν := γ + 1, γ the generator action — so the hypothesis pins every block
to full size |P|).
Proof shape: ν^{2^s} = 0 and the group sum is ∑_{p ∈ P} p = ν^{2^s−1} (freshman's dream
in characteristic 2 — no Lucas/Kummer needed). If some v₀ has ν^{2^s−1} v₀ ≠ 0, pick a
functional λ with λ(ν^{2^s−1} v₀) = 1; then the composite T := φ ∘ j of the orbit map
j F := ∑_x F x • x•v₀ with the coefficient map φ w := (x ↦ λ(x⁻¹•w)) is the convolution
by an augmentation-1 element, i.e. T = 1 + (nilpotent)·B — invertible by an explicit
geometric series — so ρ := T⁻¹ ∘ φ retracts j and one free rank-1 block splits off
equivariantly; recurse on the complement (the bound is inherited). Otherwise
ν^{2^s−1} = 0, the kernel filtration gives #V ≤ #V^P ^ (2^s−1), and the counting
hypothesis collapses V = 0.
One Jordan-increment identity: dim ker f^{k+1} = dim ker f^k + dim(im f^k ⊓ ker f).
The map f^k : ker f^{k+1} → im f^k ⊓ ker f is onto with kernel ker f^k; rank-nullity.
Concavity of the Jordan-increment sequence: k ↦ dim ker f^k is concave, i.e.
dim ker f^{k+2} + dim ker f^k ≤ 2·dim ker f^{k+1}. The increment dim(im f^k ⊓ ker f) is
non-increasing (im f^{k+1} ≤ im f^k, intersect with ker f, finrank_mono). This is the
linear-algebra heart of the elementary-abelian reduction (see the section docstring).
Numeric core of the elementary-abelian reduction #
For a concave monotone sequence b with b 0 = 0 (the Jordan-kernel dimensions
b k = dim ker ν^k), the "midpoint is free" hypothesis 2·b m = b(2m) forces every
increment to equal the first, hence b(2m) = 2m·b 1. Concavity alone gives the reverse
b(2m) ≤ 2·b m (increments non-increasing), so a future rep-theory leaf only needs the
inequality 2·b m ≤ b(2m) (the involution acts freely enough), not the full equality.
The counting criterion for 𝔽₂[P]-freeness over a cyclic 2-group: a finite
2-torsion P-module with #V^P ^ |P| ≤ #V is equivariantly isomorphic to a regular module
Fin r → P → ZMod 2 (with the left-translation action spelled inline). The reverse
inequality is automatic, so the hypothesis says exactly that the fixed space is as small as
freeness demands.
Elementary-abelian reduction of the counting bound to the involution ω = g₀^{2^{s-1}}.
Given the involution's own counting bound #V^ω ^ 2 ≤ #V (ω acts "freely enough"), the full
𝔽₂[P]-counting bound #V^P ^ |P| ≤ #V follows. This is the standard reduction of freeness
over a cyclic p-group to freeness over its order-p subgroup, the p = 2 case of
Chouinard's theorem, made elementary here: b k := dim ker ν^k is concave
(finrank_ker_pow_concave) with b 0 = 0 and b(2^s) = dim V; the leaf gives
2·b(2^{s-1}) ≤ dim V = b(2^s) and concavity gives the reverse (seq_double_le), so
2·b(2^{s-1}) = b(2^s) and seq_first_increment_le forces 2^s·b 1 = b(2^s), whence
#V^P ^ |P| = 2^{b 1·2^s} ≤ 2^{dim V} = #V.