Documentation

GQ2.RegularSummand

Lemma 6.11: ramified simple modules are split summands of regular modules #

The paper node Lemma 6.11 (§6.3, proof pp. 29–30): a ramified simple faithful module V over the tame image H_V is a projective 𝔽₂[H_V]-module — stated here in the equivalent consumer shape V is an equivariant split summand of a regular module 𝔽₂[H_V]^N. The regular module is carried as Fin N → C → ZMod 2 with the left-translation action spelled inline ((h • F) n x = F n (h⁻¹x)), so the statement needs no bespoke action instances.

#print axioms GQ2.lemma_6_11 = [propext, Classical.choice, Quot.sound]. This is the paper's own lemma — no single literature theorem states it (the paper assembles it from Clifford, Ann. of Math. 38 (1937) 533–550, and Higman, Duke Math. J. 21 (1954) 369–376, plus elementary facts).

Proof architecture (self-contained finite representation theory, no arithmetic) #

  1. P a Sylow 2-subgroup of C: cyclic (isCyclic_of_isPGroup_two_of_tame — it meets the odd inertia ⟨c τ⟩ trivially and embeds in the cyclic quotient).
  2. V|_P is free over 𝔽₂[P] (sylow_free_of_ramified): the constructive counting criterion free_of_card_fixedPoints_pow_le (geometric-series retraction, no structure theorem) reduces freeness to the bound #V^P ^ |P| ≤ #V; Jordan-block concavity (card_fixedPoints_pow_le_of_half) reduces the bound to the single involution ω = g₀^{2^{s−1}}; and involution_fixedPoints_sq_le proves #V^ω ^ 2 ≤ #V by an explicit 𝔽₂-rational trace element (see the InvolutionKernel section header) — a recorded deviation from the paper's 𝔽̄₂ weight-orbit argument.
  3. Freeness over P ⟹ split summand over C: the odd-index relative trace regular_summand_of_subgroup_summand (the sibling of LocalKummer.inflationVanishes_of_oddNormal's averaging — odd_nsmul_eq_self, no division).

File organisation. The proof is split into four dependency-ordered submodules: Trace (relative trace and tame kernels), Freeness (the cyclic 2-group criterion), Involution (the fixed-point kernel and Lemma 6.11), and Lifting (the equivariant lifting consequence). This umbrella preserves the original import path and public declaration names.

Paper-tag ledger (auto-generated by paperforge; do not edit) #