§5.2 definitions: the Heisenberg lift H(A) ⋊ C and the finite Stokes formula #
Split off from GQ2.FoxHeisenberg, building on GQ2.FoxHeisenberg.Basic. This file provides:
- the Heisenberg lift group
H(A) ⋊ C(HeisLift A C) onA × A^∨ × 𝔽₂ × Cwith the §5.2 multiplication(a,λ,z)(a',λ',z') = (a+a', λ+λ', z+z'+λ(a'))twisted by the diagonalC-action, and its API; - the mixed central coordinate machinery (
section Mixed); - Lemma 5.7, the finite-word Stokes formula in its general free-group form (
stokesEval,expMod2, and the proved tame exponent vectorexpMod2_fgTame).
See GQ2.FoxHeisenberg for the umbrella module docstring.
The Heisenberg lift group H(A) ⋊ C (§5.2) #
H(A) ⋊ C: quadruples (a, λ, z, g) with the §5.2 multiplication
(a,λ,z)(a',λ',z') = (a+a', λ+λ', z+z'+λ(a')) twisted by the diagonal C-action. The
central coordinate z is the carrier of the mixed derivatives.
- a : A
The
A-coordinate (the first derivativeD_u). - l : ElemDual A
The dual coordinate (
D^∨_u). - z : ZMod 2
The central coordinate (
β_u). - g : C
The base value in
C.
Instances For
Equations
- GQ2.FoxH.HeisLift.instOne = { one := { a := 0, l := 0, z := 0, g := 1 } }
Equations
- One or more equations did not get rendered due to their size.
H(A) ⋊ C is finite when A and C are (all four coordinates range over finite types).
The base projection HeisLift A C →* C.
Equations
- GQ2.FoxH.HeisLift.gHom = { toFun := GQ2.FoxH.HeisLift.g, map_one' := ⋯, map_mul' := ⋯ }
Instances For
The central element ⟨0, 0, w, 1⟩ (the paper's z(w)). It is genuinely central.
Equations
- GQ2.FoxH.HeisLift.zc w = { a := 0, l := 0, z := w, g := 1 }
Instances For
The central factor z(·) as a homomorphism Multiplicative (ZMod 2) →* H(A) ⋊ C.
Equations
- GQ2.FoxH.HeisLift.zcHom = { toFun := fun (w : Multiplicative (ZMod 2)) => GQ2.FoxH.HeisLift.zc (Multiplicative.toAdd w), map_one' := ⋯, map_mul' := ⋯ }
Instances For
The conjugation computation p_a⁻¹ · ⟨0,λ,0,g⟩ · p_a = ⟨g·a − a, λ, λ(g·a), g⟩, where
p_a = ⟨a,0,0,1⟩. This is the algebraic heart of Lemma 5.7's left form: conjugating a
g=1-slot generator by the A-translation p_a shifts its A-coordinate by the coboundary
g·a − a and drops the central defect λ(g·a).
The dual conjugation computation q_λ⁻¹ · ⟨a,0,0,g⟩ · q_λ = ⟨a, g·λ − λ, −λ(a), g⟩, where
q_λ = ⟨0,λ,0,1⟩. This is the algebraic heart of Lemma 5.7's right form: conjugating a
g=1-slot generator by the dual translation q_λ shifts its dual coordinate by the coboundary
g·λ − λ and records the central defect −λ(a).
The Heisenberg commutator central coordinate (symplectic B-form), in the g = 1 fiber
H(A) = A × A^∨ × 𝔽₂. For p, q with trivial base value, the central coordinate of the
commutator [p,q] = p⁻¹q⁻¹pq is the alternating pairing p.l(q.a) + q.l(p.a) (the sign is
absorbed in char 2). This is the extraspecial/Heisenberg central kernel B of Lemma 5.14: it
supplies the [d₀,z₀] mixed contribution λ(U⁻¹c) + (U^∨λ)(c) = λ((U⁻¹+U)c).
The trivially-based toolkit for the mixed Hessian (Lemma 5.14) #
Mirror of the WordLift toolkit for the central coordinate. On elements whose base g acts
trivially on the module, .a and .l are additive homs and .z follows the Heisenberg cocycle
(p*q).z = p.z + q.z + p.l(q.a). This drives the h₀ ↦ λ(c) / [d₀,z₀] ↦ 0 central ledger.
A C-element acting trivially on the module acts trivially on its 𝔽₂-dual
(contragredient).
Conjugation by a g-slice element g (g.a = 0, g.l = 0, g.z = 0) with trivially-acting
base preserves all three Heisenberg coordinates — it only conjugates the base. This is φ = conj by g₀ in the h₀-shadow (g₀ = σ₂² lands in the base slice on the x₀-supported rep).
Conjugation by a base-slice element g (g.a = 0), whose base may act nontrivially:
(conjP p g).a = g.g⁻¹ • p.a. Generalises conjP_a_of_gslice (drops the base-triviality; used in
the ramified Hessian where g₀ = σ₂² acts by U²).
Conjugation by a base-slice element g (a = l = z = 0) fixes the central coordinate, even
when the base g.g acts nontrivially: (conjP p g).z = p.z.
The commutator symplectic B-form for trivially-based elements (not just the g = 1
fiber): [p,q].z = p.l(q.a) + q.l(p.a). Gives c₀ = [d₀,z₀] ↦ 0 once d₀.a = d₀.l = 0.
The Heisenberg-lifted marking over t with offsets x and dual offsets y.
Equations
- One or more equations did not get rendered due to their size.
Instances For
B_{ρ,A} (Prop 5.8): the traced mixed central coordinate — the sum of the central
coordinates of the two evaluated relators (not the central coordinate of their product).
Equations
- GQ2.FoxH.mixedB t x y = (GQ2.FoxH.heisMarking t x y).tameValue.z + (GQ2.FoxH.heisMarking t x y).wildValue.z
Instances For
Lemma 5.7: the finite-word Stokes formula (general form) #
Evaluation of an ordinary free-group word after the substitution
gᵢ ↦ (xᵢ, yᵢ, 0; cᵢ) ∈ H(A) ⋊ C (Lemma 5.7).
Equations
- GQ2.FoxH.stokesEval c x y = FreeGroup.lift fun (i : Fin n) => { a := x i, l := y i, z := 0, g := c i }
Instances For
The mod-2 total exponent ε_i(r) of the i-th generator in an ordinary word.
Equations
- GQ2.FoxH.expMod2 i = FreeGroup.lift fun (j : Fin n) => Multiplicative.ofAdd (if j = i then 1 else 0)
Instances For
The base coordinate of a Stokes evaluation is the underlying word value in C.
With zero A-offsets, the A- and central coordinates of a Stokes evaluation vanish (the
elements ⟨0, λ, 0, g⟩ form a subgroup on which the central defect is inert).
The conjugation model of the coboundary evaluation (Lemma 5.7, left form) #
The generic coboundary substitution x = d⁰a factors, one generator at a time, as
⟨cᵢa−a, yᵢ, 0, cᵢ⟩ = p_a⁻¹ · ⟨0, yᵢ, 0, cᵢ⟩ · p_a · z(yᵢ(cᵢa)) (with p_a = ⟨a,0,0,1⟩).
Because z(·) is central, the per-generator central factors telescope into a single
z(Σᵢ εᵢ(r)·yᵢ(cᵢa)), and the conjugation commutes with word evaluation. This makes
stokesEval c (d⁰a) y = conjPa a ∘ stokesEval c 0 y · z ∘ epsWord an identity of homomorphisms,
which we prove by FreeGroup.ext_hom and then read off the z-coordinate.
Conjugation q ↦ p_a⁻¹ · q · p_a by the A-translation p_a = ⟨a,0,0,1⟩, as a group hom.
Equations
- GQ2.FoxH.conjPa a = { toFun := fun (q : GQ2.FoxH.HeisLift A C) => { a := a, l := 0, z := 0, g := 1 }⁻¹ * q * { a := a, l := 0, z := 0, g := 1 }, map_one' := ⋯, map_mul' := ⋯ }
Instances For
The z-coordinate of p_a⁻¹ · q · p_a when q sits in the g-slice (q.a = 0, q.z = 0):
conjugation records the central defect q.l (q.g · a).
The central exponent word r ↦ ∏ᵢ z(εᵢ(r)·fᵢ) for a mod-2 coefficient vector f,
packaged as a hom to Multiplicative (ZMod 2) so that z ∘ freeExp f is the telescoped
central factor of a Stokes evaluation.
Equations
- GQ2.FoxH.freeExp f = FreeGroup.lift fun (i : Fin n) => Multiplicative.ofAdd (f i)
Instances For
The additive value of freeExp f is the ε-counting sum Σᵢ εᵢ(r)·fᵢ (mod 2): each generator
i contributes fᵢ once per occurrence, so mod 2 exactly εᵢ(r) times.
The central ε-word of the left form: r ↦ ∏ᵢ z(εᵢ(r)·yᵢ(cᵢa)).
Equations
- GQ2.FoxH.epsWord c a y = GQ2.FoxH.freeExp fun (i : Fin n) => (y i) (c i • a)
Instances For
epsWord's additive value is the ε-counting sum Σᵢ εᵢ(r)·yᵢ(cᵢa) (mod 2).
The RHS conjugation model of stokesEval c (d⁰a) y: conjugate the y-only evaluation by
p_a and multiply by the telescoped central factor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Lemma 5.7 factorization (identity of homomorphisms): stokesEval at the coboundary
d⁰a equals conjPa a of the y-only evaluation, corrected by the central ε-word.
Lemma 5.7, display (38): for a word r with trivial lower value, evaluating at the
generic coboundary x = d⁰a = ((cᵢ−1)a)ᵢ gives
β_r(d⁰a, y) = ⟨a, L^{A^∨}_r(y)⟩ + Σᵢ εᵢ(r)·yᵢ(cᵢa).
The dual conjugation model (Lemma 5.7, right form) #
The dual coboundary substitution y = d⁰λ factors, one generator at a time, as
⟨xᵢ, cᵢλ−λ, 0, cᵢ⟩ = q_λ⁻¹ · ⟨xᵢ, 0, 0, cᵢ⟩ · q_λ · z(λ(xᵢ)) (with q_λ = ⟨0,λ,0,1⟩),
mirroring the left form with the roles of the A- and dual coordinates exchanged.
Conjugation q ↦ q_λ⁻¹ · q · q_λ by the dual translation q_λ = ⟨0,λ,0,1⟩.
Equations
- GQ2.FoxH.conjQlam lam = { toFun := fun (q : GQ2.FoxH.HeisLift A C) => { a := 0, l := lam, z := 0, g := 1 }⁻¹ * q * { a := 0, l := lam, z := 0, g := 1 }, map_one' := ⋯, map_mul' := ⋯ }
Instances For
The z-coordinate of q_λ⁻¹ · q · q_λ when q sits in the g-slice (q.l = 0, q.z = 0):
conjugation records the central defect λ(q.a) (the sign is absorbed mod 2).
With zero dual offsets, the dual- and central coordinates of a Stokes evaluation vanish.
The RHS conjugation model of stokesEval c x (d⁰λ) (dual form).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Lemma 5.7 factorization (dual form): stokesEval at the dual coboundary d⁰λ equals
conjQlam lam of the x-only evaluation, corrected by the central ε-word.
Lemma 5.7, display (39): the dual-variable form,
β_r(x, d⁰λ) = ⟨L^A_r(x), λ⟩ + Σᵢ εᵢ(r)·λ(xᵢ). (The lower-value hypothesis hr is recorded for
symmetry with the left form; the dual central defect is g-independent, so it is not needed
here.)
The free-group tame word τ^σ · (τ²)⁻¹ on four letters (for the exponent stress test).
Equations
- GQ2.FoxH.fgTame = GQ2.conjP (FreeGroup.of 1) (FreeGroup.of 0) * (FreeGroup.of 1 ^ 2)⁻¹
Instances For
Stress test (Prop 5.8's proof, exponent claim): the tame word's mod-2 exponent vector
is (0, 1, 0, 0) — odd total τ-exponent, even everything else.