Assembling prop_5_15 (deformation duality) from the simple-module case + dévissage #
prop_5_15 : IsSelfDual t A for every finite elementary 𝔽₂[C]-module. Route: the simple modules
are self-dual (trivial module via trivialSelfDual; nontrivial simples via lemma_5_13 + the
degree-one pairing), then lemma_5_11 (dévissage, GQ2/Devissage.lean) two-out-of-three along a
composition series.
This file lives outside FoxHeisenberg.lean because it needs lemma_5_11 (in Devissage, which
imports FoxHeisenberg) — the import runs the other way, the TrivialSelfDual.lean pattern.
Card bookkeeping for the simple case #
For a nontrivial simple module the invariants H⁰w(A) = A^C vanish, so the normal form
H¹w ≅ A (lemma_5_13) forces #Z¹w = #A² and #H²w = 1 — clauses 1 and 2 of IsSelfDual.
H¹w ≅ A from the normal form: when every x₀-supported tuple is a cocycle and every
cocycle is uniquely x₀-supported modulo coboundaries (lemma_5_13), the class map A → H¹w,
c ↦ [x₀Supported c], is a bijection, so #H¹w = #A.
No invariants for a nontrivial simple module: H⁰w(A) = A^C = 0. H⁰w is the C-fixed
space (H0w_eq_fixedPts, using hgen), a C-submodule, so ⊥ or ⊤ by simplicity; ⊤ would
make the action trivial, contradicting hnt.
Card clauses for a nontrivial simple module (feeding IsSelfDual): #H²w = 1 and
#Z¹w = #A², from #H¹w = #A (card_H1w_of_normalForm), #H⁰w = 1, and the Euler characteristic
card_H1w_eq / card_Z1w_eq_sq_mul_card_H2w.
No dual invariants for a nontrivial simple module: #(A^∨)^C = 1. A nonzero C-invariant
λ has C-stable kernel, which is ⊥ by simplicity, so λ is injective; but λ(c·a) = λ(a)
(invariance) then forces c·a = a, a trivial action — contradicting hnt.
Split/ramified dichotomy for a simple module: either τ acts trivially (split, V^T = V)
or V^T = 0 (ramified). The τ-fixed space V^T is C-stable — σ preserves it via the tame
relation σ⁻¹τσ = τ² (τ(σv) = σ(τ²v) = σv), x₀,x₁ act trivially (wild_acts_trivially), and
the stabilizer is a subgroup containing the generators, hence all of C (hgen) — so simplicity
forces V^T = ⊥ or ⊤.
mixedB descends to H¹w (the degree-one pairing) #
mixedB is invariant under changing the primal argument by a coboundary (against a cocycle
dual): B(x + d⁰a, y) = B(x, y) since B(d⁰a, y) = ⟨a, L(y)⟩ = 0 (prop_5_8_left, y a cocycle).
Uses mixedB bilinearity.
Dual version: B(x, y + d⁰λ) = B(x, y) (prop_5_8_right, x a cocycle).
Clause 3 (degree-one perfect pairing) from a normal form. Given that x₀-supported
cochains x0Supported c are cocycles and hit every H¹w class uniquely (the normal form of
lemma_5_13, for both A and A∨), and that the induced pairing c, λ ↦ B(x0Supported c, x0Supported λ) is nondegenerate on both sides, mixedB descends to a perfect pairing
H¹w(A) × H¹w(A∨) → 𝔽₂. Descent uses mixedB_left_congr/mixedB_right_congr; nondegeneracy
transports through the normal-form identification H¹w ≅ A.
Split simple case: Z¹w/B¹w shapes, normal form, x₀-support #
These are phrased against the split shapes (rather than lemma_5_13_split directly) so they
apply equally to A and its contragredient dual A∨: the dual is split with trivial wild action
whenever A is, without needing "the dual of a simple module is simple".
The split Z¹w/B¹w shapes from a trivial wild action (hx0, hx1) rather than from
simplicity — the body of lemma_5_13_split with wild_acts_trivially factored out as hypotheses,
so it is usable on A∨ (where wild-triviality comes from the contragredient of A's).
The x₀-supported cochains are cocycles, straight from the split Z¹w shape.
Split normal form: from the Z¹w/B¹w shapes and surjectivity of σ − 1 (from V^S = 0,
hVS), every degree-one class has a unique x₀-supported representative.
Split simple case: IsSelfDual #
Proposition 5.15, split simple case. A nontrivial simple module on which τ acts trivially
(htau) and σ acts nontrivially (hσ) is self-dual. The σ-tameness hU and fixed-point
freeness hVS come from the tame representation-theory proof; the contragredient dual A∨ inherits split + trivial-wild action
from A (via ElemDual.smul_apply), giving both normal forms; the cards close clauses 1–2 and
clause3_of_normalForm (with the split pairing (c,λ) ↦ λ(c)) closes clause 3.
Trivial-action case. If all four generators act trivially then (by hgen) every element of
C does, and the module is self-dual by trivialSelfDual. This is the split sub-case where σ
also acts trivially.
Ramified simple case #
Elementwise contragredient triviality: if g acts trivially on A it acts trivially on
A∨ ((g•λ)a = λ(g⁻¹•a) = λ(a)).
In the ramified case the x₀-supported cochains are cocycles: the tame row (d1Fun_tame)
involves only coordinates 0 and 1, the wild row is S⁻¹x₃
(liftMarking_wildValue_u_ramified), and all three coordinates vanish on x0Supported c.
Proposition 5.15, ramified simple case. A simple module with V^T = 0 is self-dual.
hTodd (τ odd-order) is derived (tau_powOmega2_smul_trivial); the dual A∨ inherits
wild-triviality and hTodd (contragredient) and τ-fixed-point-freeness ((τ⁻¹−1) surjective);
the pairing λ((1+U+U⁻¹)c) (lemma_5_13_pairing_ramified) is perfect because the operator
1+U+U⁻¹ is unipotent, hence bijective (sigma2_pairing_operator_injective) — no σ-tameness
hU anywhere (it is not derivable: S₃/C₅⋊C₄ admissible counterexamples).
Split case of a simple module (complete). When τ acts trivially, the simple module is
self-dual — whether σ acts nontrivially (selfDual_of_split) or trivially
(selfDual_of_trivial_action). This closes the entire V^T = V branch of the
tau_split_or_ramified dichotomy.
The simple case of prop_5_15, unconditional: every finite simple char-2 module at an
admissible-style marking is self-dual. Dispatches on the tau_split_or_ramified dichotomy —
selfDual_of_split_case for V^T = V, selfDual_of_ramified for V^T = 0. This is exactly
the hsimp input the dévissage induction (prop_5_15_of_simple) consumes.
Prop. 5.15 (candidate deformation duality): the Fox–Heisenberg chain map is a
quasi-isomorphism for every finite elementary module — packaged: the display-(56) numerics hold
and the descended B-pairing is perfect.
The composition: the dévissage strong induction prop_5_15_of_simple
(GQ2/DevissageInduction.lean, via lemma_5_11 along 0 → W → A → A/W → 0 for a proper
C-stable W) reduces to the simple case, which selfDual_of_simple closes by the
tau_split_or_ramified dichotomy — split (lemma_5_13_split + the tame representation-theory providers) or
ramified (lemma_5_13_ramified + hTodd derived + the unipotent pairing operator).
Relocated here from GQ2/FoxHeisenberg.lean (statement unchanged, same fully qualified name
GQ2.FoxH.prop_5_15): the proof needs the dévissage and the simple-case assembly, which import
that file.
Paper-tag ledger (auto-generated by paperforge; do not edit) #
- Prop 5.15 = ⟦prop-defduality⟧