Prop 5.8 / 5.10 and the duality package (5.11–5.15) #
Split off from GQ2.FoxHeisenberg, building on GQ2.FoxHeisenberg.Heisenberg. This file
provides:
- Prop 5.8 / Prop 5.10: the traced mixed central coordinate
mixedB t x y = β_t + β_wand the traced Stokes identities that are the Fox–Heisenberg chain map (section Traced); - the duality package
IsSelfDualand the statements of Lemmas 5.11, 5.12, 5.13 and 5.15 (section Duality); - Lemma 5.2, the exact class-two identity of the §5.1 ledger (
section ClassTwo).
See GQ2.FoxHeisenberg for the umbrella module docstring.
Prop 5.8 / Prop 5.10: the traced Stokes identities = the chain map #
The degree-0 endpoint component D⁰(a) = (a, a) of the Fox–Heisenberg chain map
(display (43)).
Equations
- GQ2.FoxH.traceD0 = AddMonoidHom.mk' (fun (a : A) => (a, a)) ⋯
Instances For
The degree-2 endpoint component D²(u_t, u_w) = u_t + u_w (display (45), the scalar
trace).
Equations
- GQ2.FoxH.traceD2 = AddMonoidHom.mk' (fun (p : A × A) => p.1 + p.2) ⋯
Instances For
The tame relator-word bridge (Lemma 5.7 ⇒ the tame row of Prop 5.8) #
heisMarking/liftMarking evaluate the paper's relators directly in the target; stokesEval
evaluates the free relator word. They agree because both are the pushforward of the free
marking ⟨g₀,g₁,g₂,g₃⟩ on Fin 4 along the classifying hom, and Marking.map_tameValue is
natural. Since the tame word carries no ω₂, no finiteness is needed — so bridge_tame is
unconditional, and feeding it into Lemma 5.7 computes the tame relator's z-coordinate at d⁰a
in closed form (the tame row of display (41)).
The wild row is genuinely harder: Marking.map_wildValue needs the source finite, but the
universal source FreeGroup (Fin 4) is infinite (and freeMarking.wildValue's ω₂-powers are
degenerate there). The wild bridge therefore needs the target-dependent integer-ω₂
representative of the wild word — the separate "wild-row" computation.
The four marked values ⟨t.σ, t.τ, t.x₀, t.x₁⟩ as a vector — the lower map of stokesEval.
Equations
- GQ2.FoxH.markVec t = ![t.σ, t.τ, t.x₀, t.x₁]
Instances For
The free marking ⟨g₀, g₁, g₂, g₃⟩ on FreeGroup (Fin 4) (the universal source).
Equations
- GQ2.FoxH.freeMarking = { σ := FreeGroup.of 0, τ := FreeGroup.of 1, x₀ := FreeGroup.of 2, x₁ := FreeGroup.of 3 }
Instances For
The wild relator word with the ω₂-powers replaced by an explicit integer exponent e (the
paper's ω₂ becomes (·)^e for a concrete e = omega2Exp N, a multiple of the relevant orders).
Mirrors Marking.wildValue's ledger exactly; only sigma2, u0, u1 carry the exponent.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The wild word's mod-2 exponent vector is (0, e, 0, e+1) (the wild analogue of
expMod2_fgTame). Because expMod2 lands in the abelian Multiplicative (ZMod 2),
conjugations are exponent-invariant and commutators vanish; in h₀ the two x₀-letters and the
two d₀-occurrences (d_g and the bare d₀) cancel and d₀² is even, so ε(h₀) = 0 for
every e (paper Prop 5.8's proof), leaving ε(r_w) = ε(u₁⁻¹) + ε(x₁^σ) = (0, e, 0, e+1).
At the odd representatives of ω₂ (omega2Exp of any even exponent is odd) this is (0,1,0,0),
matching the tame vector — so condition (40) holds for the (1,1) trace and the Stokes
corrections of Lemma 5.7 cancel in Prop 5.8. (Cf. docs/erratum-h0-transcription.md: for the
pre-erratum h₀ missing the bare d₀, the vector was (0, 0, e+1, e+1) and they did not.)
wildValueExp is natural in group homomorphisms — it uses only mul, inv, pow, conjP,
commP (no ω₂), so no finiteness is needed.
For finite G, wildValueExp at omega2Exp (Monoid.exponent G) is Marking.wildValue:
only sigma2, u0, u1 carry ω₂, and each such element's order divides the exponent, so
powOmega2_pow_eq rewrites the three ω₂-powers to the explicit omega2Exp-power.
Divisibility form of wildValueExp_eq_wildValue: wildValueExp t (omega2Exp N) = t.wildValue
for any N ≠ 0 that is a multiple of the three ω₂-subword orders (σ, x₀τ, x₁τ). Used
to run the bridge at N = exponent (H(A)⋊C) on the lower groups C and A^∨⋊C (whose element
orders divide that exponent via the injective section homs).
The projection ⟨a,λ,z,g⟩ ↦ ⟨λ, g⟩ : H(A) ⋊ C →* A^∨ ⋊ C onto the dual lift group.
Equations
- GQ2.FoxH.lgHom = { toFun := fun (p : GQ2.FoxH.HeisLift A C) => { u := p.l, g := p.g }, map_one' := ⋯, map_mul' := ⋯ }
Instances For
heisMarking t x y is the free marking pushed through stokesEval (markVec t) x y.
liftMarking t y (dual coefficients) is the free marking pushed through
lgHom ∘ stokesEval.
Tame bridge: the paper's tame relator value at heisMarking equals the free-word
evaluation stokesEval … fgTame.
The .l-coordinate of the y-only tame evaluation is d¹'s tame row on the dual.
The tame row of Prop 5.8 (41): Lemma 5.7 applied to the actual tame relator computes its
mixed central coordinate at the coboundary d⁰a — the pairing ⟨a, L^{A^∨}_t(y)⟩ plus the tame
ε-correction y_τ(τ·a) (exponent vector (0,1,0,0)). The wild row (and hence full Prop 5.8)
awaits the wild bridge.
Wild bridge: the paper's wild relator value at heisMarking equals the free-word
evaluation stokesEval … fgWild, where fgWild = wildValueExp freeMarking (omega2Exp (exponent H(A)⋊C)) is the target-dependent integer-ω₂ representative of the wild word. This is the wild
analogue of bridge_tame; unlike the tame case it is genuinely target-dependent (the exponent is
Monoid.exponent (HeisLift A C)), because freeMarking.wildValue's ω₂ is degenerate in the
infinite free group. Feeding this into Lemma 5.7 is what the wild row of Prop 5.8
and the normal-form Lemma 5.13 consume.
The wild row of Prop 5.8 #
The wild summand (heisMarking t (d⁰a) y).wildValue.z is computed exactly like the tame row
(mixedB_tameRow), but the free relator word is fgWild = wildValueExp freeMarking (omega2Exp N)
with N = exponent (H(A)⋊C), and Lemma 5.7's hypotheses need wildValueExp _ (omega2Exp N) = _
on the lower groups C (for hr) and A^∨⋊C (for the .l-bridge). Both hold because C and
A^∨⋊C embed into H(A)⋊C by injective section homs, so their element orders divide N.
The section g ↦ ⟨0,0,0,g⟩ : C →* H(A) ⋊ C of the base projection (injective).
Equations
- GQ2.FoxH.secHom = { toFun := fun (g : C) => { a := 0, l := 0, z := 0, g := g }, map_one' := ⋯, map_mul' := ⋯ }
Instances For
The section ⟨λ,g⟩ ↦ ⟨0,λ,0,g⟩ : A^∨ ⋊ C →* H(A) ⋊ C (injective).
Equations
- GQ2.FoxH.secWL = { toFun := fun (p : GQ2.FoxH.WordLift (GQ2.FoxH.ElemDual A) C) => { a := 0, l := p.u, z := 0, g := p.g }, map_one' := ⋯, map_mul' := ⋯ }
Instances For
Every order in the lower group C divides exponent (H(A) ⋊ C).
2 ∣ exponent (H(A) ⋊ C): the central element z(1) = ⟨0,0,1,1⟩ has order 2.
The ω₂-representative at N = exponent (H(A)⋊C) is odd (its 𝔽₂-cast is 1), because
N is even. This is what makes the wild ε-correction reduce to y_τ(τ·a), matching the tame.
The wild hr: fgWild has trivial lower value, from WildRel (via the paper's ω₂-ledger
evaluated at the target exponent).
The wild .l-bridge: the .l-coordinate of the y-only wild evaluation is d¹'s wild row
on the dual (the analogue of stokesEval_tame_l).
The wild row of Prop 5.8 (41): the wild summand at the coboundary d⁰a equals the pairing
⟨a, L^{A^∨}_w(y)⟩ plus the ε-correction y_τ(τ·a) — the same correction as the tame row (the
wild ε-vector (0, e, 0, e+1) reduces to (0,1,0,0) at the odd ω₂-representative).
Prop 5.8, display (41) (= chain identity (47) of Prop 5.10 under the canonical
identifications): B_{ρ,A}(d⁰a, y) = ⟨a, L^{A^∨}_t(y) + L^{A^∨}_w(y)⟩, where the dual
first relation differentials are d1Fun on A^∨.
The proof follows the paper's statement on p. 17. The tame summand is
mixedB_tameRow — ⟨a, L^{A^∨}_t(y)⟩ + y_τ(τ·a) (tame ε-vector (0,1,0,0), expMod2_fgTame);
the wild summand comes from bridge_wild + lemma_5_7_left with ε-vector
(0, e, 0, e+1) = (0,1,0,0) at the odd ω₂-representative (expMod2_wildValueExp), i.e.
⟨a, L^{A^∨}_w(y)⟩ + y_τ(τ·a); the two y_τ(τ·a) corrections cancel (char 2), which is exactly
condition (40) for the (1,1) trace. (An earlier apparent inconsistency here was a repo-side
h₀ transcription bug, resolved — see docs/erratum-h0-transcription.md.)
The dual (right) row of Prop 5.8 #
Mirror of the left row with the A-coordinate projection agHom : H(A)⋊C →* A⋊C in place of the
dual lgHom, and the section secWA : A⋊C ↪ H(A)⋊C for the exponent divisibilities. Lemma 5.7's
right form supplies the pairing ⟨L^A_r(x), λ⟩ and the ε-correction Σᵢ εᵢ(r)·λ(xᵢ).
The projection ⟨a,λ,z,g⟩ ↦ ⟨a, g⟩ : H(A) ⋊ C →* A ⋊ C onto the A-lift group.
Equations
- GQ2.FoxH.agHom = { toFun := fun (p : GQ2.FoxH.HeisLift A C) => { u := p.a, g := p.g }, map_one' := ⋯, map_mul' := ⋯ }
Instances For
The section ⟨u,g⟩ ↦ ⟨u,0,0,g⟩ : A ⋊ C →* H(A) ⋊ C (injective).
Equations
- GQ2.FoxH.secWA = { toFun := fun (p : GQ2.FoxH.WordLift A C) => { a := p.u, l := 0, z := 0, g := p.g }, map_one' := ⋯, map_mul' := ⋯ }
Instances For
liftMarking t x (over A) is the free marking pushed through agHom ∘ stokesEval.
The .a-coordinate of the x-only tame evaluation is d¹'s tame row on A.
The .a-coordinate of the x-only wild evaluation is d¹'s wild row on A.
The tame row of Prop 5.8 (42) (dual form): ⟨L^A_t(x), λ⟩ + λ(x_τ).
The wild row of Prop 5.8 (42) (dual form): ⟨L^A_w(x), λ⟩ + λ(x_τ) — same correction as
the tame row.
Prop 5.8, display (42) (= chain identity (48)): B_{ρ,A}(x, d⁰λ) = ⟨L_t(x)+L_w(x), λ⟩.
Proved as stated: mixedB = tameRow + wildRow, and the two λ(x_τ) corrections cancel (char 2).
Lemma 5.6 (strict coefficient naturality), in the traced form Prop 5.10 uses: for an
equivariant f : A → A', B_{A'}(f∗x, y') = B_A(x, f^∨ y').
Proof (the paper's "evaluate in the mixed Heisenberg group"): the two markings live in
H(A') ⋊ C and H(A) ⋊ C, related by f on the A-slot and f^∨ on the dual slot. They both
sit inside the mixed subgroup S ≤ H(A') ⋊ C × H(A) ⋊ C cut out by "f-related a/λ,
equal z, equal g" — a subgroup precisely because f is C-equivariant. The two projections
π₁, π₂ : S →* … carry the mixed marking to the two sides (Marking.map_tameValue/map_wildValue,
the latter needing S finite for the ω₂-powers), and S's defining z-equation makes the two
relator z-coordinates agree — which is exactly the claim.
(Requires A, A', C finite, the paper's finite setting: map_wildValue's ω₂ push needs the
source group finite.)
The duality package: IsSelfDual, 5.11, 5.12, 5.13, 5.15 #
The C-fixed points of a module (the invariants M^C, as a Set — Nat.card needs no
subgroup structure).
Equations
- GQ2.FoxH.fixedPts C M = {m : M | ∀ (g : C), g • m = m}
Instances For
The Prop 5.15 conclusion, packaged (candidate side, at a marking t and module A):
the display-(56) numerics and a perfect degree-one pairing descending the traced mixed
coordinate B_{ρ,A}. "Perfect" is encoded as two-sided nondegeneracy (equivalent for finite
elementary groups given the card clauses). Lemma 5.11 is two-out-of-three for this
predicate.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Simplicity of a 𝔽₂[C]-module, subgroup form: nonzero, and the only C-stable additive
subgroups are ⊥ and ⊤ (no Module instances, per the repo convention).
Equations
- GQ2.FoxH.IsSimpleModTwo C V = (Nontrivial V ∧ ∀ (W : AddSubgroup V), (∀ (g : C), ∀ w ∈ W, g • w ∈ W) → W = ⊥ ∨ W = ⊤)
Instances For
Lemma 5.12 (simple characteristic-two modules are tame): a normal 2-subgroup L ◁ C
acts trivially on every simple 𝔽₂[C]-module. Proof: the L-fixed subspace is nonzero (the
p-group congruence #V ≡ #Vᴸ (mod 2) with #V even) and C-stable (L normal), so
simplicity forces it to be all of V. (Proved for the §5 proof layer, as part of the Heisenberg
word-evaluation core — d1Fun_add, d1Fun_comp_d0, Lemma 5.6, Lemma 5.7 both forms, and the
tame row of Prop 5.8; the wild row (Prop 5.8/Lemma 5.13, needing the target-dependent
integer-ω₂ representative of the wild word) and the mapping-cone dévissage Lemma 5.11
followed later in the §5 proof layer and are also proved.)
Lemma 5.2: the exact class-two identity (§5.1 ledger) #
The auxiliary word h₀ = (x₀^{g₀})·x₀·d_g·d₀·d₀²·[d_g,d₀] (Marking.h0) has the class-two shape
h_ϕ(X,D) = ϕ(X)·X·ϕ(D)·D·D²·[ϕ(D),D] with ϕ = (·)^{g₀} (conjugation by g₀), X = x₀,
D = d₀. Paper Lemma 5.2 collapses it to ϕ(X)·X·D⁻¹·ϕ(D) (display (32)) in any group in which
[ϕ(D),D] is central of order ≤ 2 and D⁴ = 1 — the class-two setting of the coefficient
Heisenberg/extraspecial groups. This is the algebraic heart of the h₀-shadow (Lemma 5.3) and the
mixed Hessian (Lemma 5.14): h₀ may replace x₀² in every first-order, cup, and central ledger.
Lemma 5.2, core cancellation. If the commutator k = [A,B] (commP convention
A⁻¹B⁻¹AB) is central and satisfies k² = 1, and B⁴ = 1, then A·B·B²·[A,B] = B⁻¹·A.
This is display (32) after cancelling the common prefix ϕ(X)·X (with A = ϕ(D), B = D).
The proof is the paper's: from A·B = B·A·k (hcomm), k central and k² = 1 give that A
commutes with B², and B³ = B⁻¹; then A·B·B²·k = B·A·B² = B³·A = B⁻¹·A. The associativity
bookkeeping is discharged by right-normalising with simp only [mul_assoc, …], feeding the
commutator relation in the right-associated form A·(B·x) = B·(A·(k·x)) so it fires under the
normal form.
Lemma 5.2, display (32): h_ϕ(X,D) = ϕ(X)·X·ϕ(D)·D·D²·[ϕ(D),D] = ϕ(X)·X·D⁻¹·ϕ(D),
whenever [ϕ(D),D] is central of order ≤ 2 and D⁴ = 1. (ϕ need not be a homomorphism for the
identity; the paper's ϕ is a Z-fixing automorphism, which is what makes the hypotheses hold for
the actual h₀.)
Lemma 5.2(ii): when ϕ = id, h_ϕ(X,D) = X² for every D ([D,D] = 1). Used in the
split (P = 1) branch of the h₀-shadow, where g₀ = σ₂² acts trivially.