The Fox–Heisenberg cup calculation (manuscript §5, l.1488–2025) #
This file formalises the class-2 second-derivative layer of the candidate
linear-lifting theory: the mixed Heisenberg/extraspecial coefficient group, the
exact class-two collector identity, the bilinear commutator (cup) pairing it
carries, the ω₂-twisted mixed-Hessian pairing operator 1 + U + U⁻¹
(U = S^{ω₂}), and the scalar cup/Bockstein Hilbert form on H¹.
It sits on top of Lifting/WordComplex.lean (the word complex d⁰, d¹, the
cohomology H¹, H²) and Foundation/Omega2.lean (powOmega2 = (·)^{ω₂}).
The mixed Heisenberg coefficient group H(A) (manuscript l.1490–1510) #
For an elementary F₂[C]-module A with dual A^∨ = Hom_{F₂}(A, F₂), set
H(A) = A × A^∨ × F₂ with (a,λ,z)(a',λ',z') = (a+a', λ+λ', z+z'+λ(a')). This
is a genuine (non-abelian) Heisenberg 2-group; its multiplication and inversion
are the finite Fox recursion formulas (eq:heisrules1, eq:heisrules2).
The exact class-two identity (lem:class2square, l.1301, eq:class2collector) #
In any class-≤2 group with squares/commutators central, commutators of order
≤2, and g⁴=1, the collector 𝔥_φ(X,D) = φ(X)·X · φ(D)·D · D²·[φ(D),D]
collapses to φ(X)·X·D⁻¹·φ(D); for φ=1 it is X² (the h₀ ↦ x₀² replacement
of lem:h0shadow, central coordinate λ(c)).
The cup / Hilbert form (manuscript l.1125–1133, l.1944) #
For the trivial module A=F₂, d¹(a,b,c,d)=(b,b), so H¹ is 3-dimensional on
(σ,x₀,x₁), and the traced Fox–Heisenberg form is ad'+da'+cc', i.e. the scalar
cup/Bockstein table ac'+ca'+bb' (eq:HilbertTable) with quadratic initial form
b²+ac+ca.
Part 0 — char-2 helpers #
In a ZMod 2-module every element is its own additive inverse.
-x = x in a ZMod 2-module (used to discharge the char-2 sign bookkeeping).
Part 1 — the mixed Heisenberg coefficient group H(A) #
The F₂-linear dual A^∨ = Hom_{F₂}(A, F₂).
Equations
- Q2Presentation.Lifting.Dual A = Module.Dual (ZMod 2) A
Instances For
The mixed Heisenberg coefficient group H(A) = A × A^∨ × F₂
(manuscript l.1490): primal coordinate v = D_u, dual coordinate dl = D^∨_u,
central coordinate z = β_u.
- v : A
The primal
A-coordinateD_u. - dl : Dual A
The dual
A^∨-coordinateD^∨_u. - z : ZMod 2
The central
F₂-coordinateβ_u.
Instances For
The collector multiplication (eq:heisrules1, eq:heisrules2):
(a,λ,z)(a',λ',z') = (a+a', λ+λ', z+z'+λ(a')).
Inversion: (a,λ,z)⁻¹ = (-a, -λ, -z + λ(a)) (eq:heisrules2, second line).
Equations
- One or more equations did not get rendered due to their size.
The square diagonal (lem:h0shadow(ii)): u² = (0, 0, λ(v)). For the
normalized representative supported on x₀ with value c and dual λ, the
central coordinate of x₀² (hence of h₀, by lem:h0shadow) is λ(c).
The bilinear commutator (cup) pairing b_cl (lem:fullwordledger) #
The bilinear commutator pairing of the class-two coefficient group
(lem:fullwordledger, l.1411): the central coordinate of the commutator
⁅u, w⁆ = u⁻¹ w⁻¹ u w (project convention, matching Q2Word.commExpr) is
b_cl(u, w) = (D^∨_u)(D_w) + (D^∨_w)(D_u).
Instances For
b_cl is symmetric.
Part 2 — the diagonal C-action (manuscript l.1499; lem:heisnatural) #
The diagonal C-action by a linear automorphism g : A ≃ₗ[F₂] A
(manuscript l.1499, "The C-action is diagonal"): (a, λ, z) ↦ (g a, λ∘g⁻¹, z).
It preserves the pairing λ(a') because (λ∘g⁻¹)(g a') = λ(a'), hence is a group
automorphism of H(A).
Equations
Instances For
Part 3 — the exact class-two identity (lem:class2square, eq:class2collector) #
The class-two collector word 𝔥_φ(X,D) = φ(X)·X · φ(D)·D · D²·[φ(D),D]
(manuscript lem:class2square, l.1311), with the project commutator convention
[A,B] = A⁻¹B⁻¹AB (= Q2Word.commExpr).
Equations
Instances For
The exact class-two identity (lem:class2square, eq:class2collector):
in a group where squares (hsq) and commutators (hk) are central, commutators
have order ≤2 (hk2), and every element has 4th power 1 (h4),
𝔥_φ(X,D) = φ(X)·X·D⁻¹·φ(D).
Consequence (ii) (lem:class2square(ii)): if φ = 1, then 𝔥_φ(X,D) = X²
for every D. This is the h₀ ↦ x₀² replacement of lem:h0shadow.
Part 4 — the ω₂-twisted mixed-Hessian pairing operator 1 + U + U⁻¹ #
(lem:mixedhessian eq:pairingoperator, lem:simplenormalforms, l.1862–1888.)
With U = S^{ω₂} the 2-primary part of the σ-action, the degree-one cup
pairing on a nontrivial simple module is induced by 1 + U + U⁻¹, which the
manuscript shows is invertible because U has 2-power order, so its minimal
polynomial divides a power of X+1, coprime to X²+X+1. We capture this as: a
unipotent U (i.e. U−1 nilpotent) makes 1 + U + U⁻¹ a unit, and U = S^{ω₂}
is unipotent because it has 2-power order.
End A is finite when A is (needed to form S^{ω₂} via powOmega2).
The automorphism group (End A)ˣ is finite when A is.
A 2-power-order endomorphism is unipotent: if U^{2^k} = 1 then U − 1
is nilpotent (its 2^k-th power is U^{2^k} − 1 = 0).
The mixed-Hessian pairing operator is invertible (lem:mixedhessian,
lem:simplenormalforms): for a unipotent unit U (i.e. U−1 nilpotent),
1 + U + U⁻¹ is a unit of End A. Indeed U·(1+U+U⁻¹) = 1+U+U² = 1+(N+N²)
with N = U−1 nilpotent, hence a unit; and U is a unit.
The mixed-Hessian central value (lem:mixedhessian, l.1871–1915,
ramified case P=0): assembling the central ledger of lem:fullwordledger, the
h₀ square diagonal λ(c) plus the [d₀,z₀] commutator pairing b_cl of the
d₀-shadow (c, λ, 0) and z₀-shadow (U⁻¹c, U^∨λ, 0) equals λ((1+U+U⁻¹)c).
Together with pairingOp_isUnit this is the perfect degree-one cup pairing.
powOmega2 g = g^{ω₂} has 2-power order (manuscript: U = S^{ω₂} has
2-power order, lem:simplenormalforms): (g^{ω₂})^{ordProj[2](orderOf g)} = 1.
The exponent ordProj[2] (orderOf g) = 2^{v₂(orderOf g)} is a power of 2.
The mixed-Hessian pairing operator for U = S^{ω₂} is invertible
(lem:mixedhessian + lem:simplenormalforms): for any unit S of End A (the
σ-action; A finite), the operator 1 + S^{ω₂} + (S^{ω₂})⁻¹ is a unit, because
S^{ω₂} has 2-power order, hence is unipotent.
Part 5 — the scalar cup / Bockstein Hilbert form on H¹ (l.1125–1133, l.1944) #
The Hilbert / cup–Bockstein bilinear form on F₂³ (manuscript eq:HilbertTable,
l.1131): ℋ((a,b,c),(a',b',c')) = a·c' + c·a' + b·b', in coordinates dual to
(σ, x₀, x₁). This is the traced Fox–Heisenberg form ad'+da'+cc' on the
(σ,x₀,x₁)-basis of H¹ for the trivial module (l.1944, under the relabel
(a,b,c)↦(a,c,d)), with matrix [[0,0,1],[0,1,0],[1,0,0]].
Instances For
The Hilbert pairing is nondegenerate (perfect): if x pairs to 0 with
every vector then x = 0. Equivalently its matrix [[0,0,1],[0,1,0],[1,0,0]] is
nonsingular — the perfect cup pairing of prop:defduality.
Connection to the word complex d⁰, d¹ for the trivial module #
For the trivial module d⁰ = 0, so B¹ = 0 and H¹ = Z¹ = ker d¹.
The normalized H¹ representatives for the trivial module are {(a,0,c,d)}
(τ-coordinate 0), i.e. exactly ker d¹. On the (σ,x₀,x₁)=(a,c,d) coordinates
the cup pairing is cupFormQ (the traced Fox–Heisenberg form ad'+da'+cc').