Candidate deformation duality — the Fox–Heisenberg chain map and its boundaries #
This file formalises the candidate side of cor:adjointboundary
(reference/q2_manuscript.tex, §5, l.1687–2025): the four numerical/duality
endpoints attached to the finite word complex C_{ρ,A}^• of
Lifting/WordComplex.lean. These are the candidate-source values that Stage F
compares numerically with the local Galois cohomology — there is no map
between the two complexes, only an equality of dimensions, multiplicities and
perfect pairings.
1. The Fox–Heisenberg chain map D_{ρ,A} (prop:chainmap, eq:Dmap) #
Under the identifications Hom((A^∨)^k, F₂) ≅ A^k, the chain map
D_{ρ,A} : C_{ρ,A}^• → Hom(C_{ρ,A^∨}^•, F₂)[-2] has the explicit endpoints
D⁰(a) = (a, a) (eq:D0)
⟨D¹(x), y⟩ = 𝓑_{ρ,A}(x, y) (eq:D1)
D²(u_t, u_w) = u_t + u_w. (eq:D2)
Its degree-one component D¹ is the traced Fox–Heisenberg central form
𝓑_{ρ,A} = β_t + β_w (prop:tracedstokes). For the trivial module
(prop:defduality, l.1936) this traced form is exactly the scalar
cup–Bockstein table cupFormQ of Lifting/HeisenbergCup.lean.
2. Candidate deformation duality (prop:defduality) #
The chain map is a quasi-isomorphism, so the induced cup pairings
H^i_{A,ρ}(A) × H^{2-i}_{A,ρ}(A^∨) → F₂ are perfect. For the trivial
module the degree-one pairing on H¹ is cupFormQ, whose nondegeneracy
(cupFormQ_nondegenerate) we package as a self-duality isomorphism
H¹ ≃ₗ (H¹)^∨ and the resulting dimension equality.
3. The lift torsor (lem:affinelifting, l.4015) #
Z¹_{Γ,ρ} acts freely and transitively on each nonempty fibre of the map from
lifts to their T-quotient, so a nonempty lift set is a torsor under Z¹; its
cardinality is Nat.card Z¹ (lift_torsor_card).
4. The connecting homomorphism ∂_{Γ,ρ} (l.2005) and cor:adjointboundary #
∂_{Γ,ρ} : H¹_{Γ,ρ}(V) → H²_{Γ,ρ}(T) is the connecting homomorphism of the
coefficient short exact sequence 0 → T → M → V → 0, realised on the candidate
side as the snake map of the degreewise-exact sequence of word complexes
(lem:exactcoefffunctor, eq:coneshortexact). cor:adjointboundary
(eq:adjointboundary) is its adjointness ⟨∂c, χ⟩ = ⟨c, ρ*γ_χ⟩ against the
perfect cup pairing.
§1. The Fox–Heisenberg chain map endpoints (prop:chainmap, eq:Dmap) #
The degree-zero component of the chain map (prop:chainmap, eq:D0):
D⁰_{ρ,A}(a) = (a, a). Under Hom((A^∨)², F₂) ≅ A² this is the diagonal,
the dual of the degree-two trace D².
Instances For
The degree-two component of the chain map (prop:chainmap, eq:D2): the
scalar trace D²_{ρ,A}(u_t, u_w) = u_t + u_w on the two relator coordinates.
Instances For
The degree-two trace D² is the codiagonal that splits the degree-zero
diagonal D⁰ on each relator coordinate (prop:chainmap): D²(u, 0) = u and
D²(0, u) = u. D⁰ (diagonal) and D² (codiagonal) are transpose under the
identification Hom((A^∨)ᵏ, F₂) ≅ Aᵏ, the endpoint duality of prop:defduality.
§2. Candidate deformation duality (prop:defduality) — the perfect #
degree-one cup pairing on the trivial module.
The (σ, x₀, x₁)-coordinate model of H¹ for the trivial module A = F₂ is
F₂³ (prop:defduality, l.1936: dim H¹ = 3), and the degree-one cup pairing
is cupFormQ with nonsingular matrix [[0,0,1],[0,1,0],[1,0,0]].
The (σ, x₀, x₁)-coordinate model of H¹ for the trivial module A = F₂.
By prop:defduality (l.1936) the trivial-module H¹ is 3-dimensional with
this basis.
Instances For
The degree-one cup pairing of prop:defduality packaged as a
ZMod 2-bilinear form on the H¹-model F₂³ (the scalar cup–Bockstein table
cupFormQ).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The map H¹ → (H¹)^∨ induced by the cup pairing (x ↦ ⟨x, ·⟩).
Instances For
The degree-one component D¹ of the chain map for the trivial module
(prop:chainmap, eq:D1): ⟨D¹ x, y⟩ = 𝓑_{ρ,A}(x, y), and for A = F₂ the
traced Fox–Heisenberg form 𝓑 is the cup form, so D¹ = cupToDual
(prop:defduality, l.1936). Completes the visible triple D⁰, D¹, D² of §1.
Instances For
The cup pairing is nondegenerate / perfect: the induced map
H¹ → (H¹)^∨ is injective (prop:defduality, via cupFormQ_nondegenerate).
The degree-one cup pairing is perfect (prop:defduality): for the
trivial module it induces a self-duality H¹ ≃ₗ (H¹)^∨.
Equations
Instances For
Dimension equality from the perfect pairing (prop:defduality):
dim H¹ = dim (H¹)^∨.
Identification of the H¹-model with the actual word-complex cohomology #
For the trivial module B¹ = im d⁰ = 0 (d0_trivial), so H¹ = Z¹ = ker d¹,
and Z¹ = {(a, 0, c, d)} (the τ-coordinate vanishes, d1_trivial). The
(σ, x₀, x₁) = (a, c, d) projection is the manuscript's H¹-basis (l.1936).
Z¹ = H¹ for the trivial module is the (σ, x₀, x₁)-model F₂³
(prop:defduality, l.1936): the projection (a, 0, c, d) ↦ (a, c, d) is a linear
isomorphism ker d¹ ≃ₗ F₂³. Since B¹ = im d⁰ = 0 here (d0_trivial), this
ker d¹ is the genuine H¹, so the perfect cup pairing cupPairing lives on it.
Equations
- One or more equations did not get rendered due to their size.
Instances For
§3. The lift torsor (lem:affinelifting, eq:mumultiplicity) #
The lift count is the cocycle count (lem:affinelifting, l.4015): a
nonempty set L of lifts over a fixed lifting datum is a torsor under the
1-cocycles Z (AddTorsor bakes in nonemptiness), so |L| = |Z|. Applied
to Z = Z¹_{Γ,ρ} this is the |Z¹| factor of the lift multiplicity μ.
The lift torsor specialised to the candidate 1-cocycles Z¹ = ker d¹: a
nonempty lift set over a lifting datum has cardinality Nat.card Z¹.
§4. The connecting homomorphism ∂_{Γ,ρ} (l.2005) and cor:adjointboundary #
The candidate-side connecting homomorphism ∂_{Γ,ρ} : H¹_{Γ,ρ}(V) → H²_{Γ,ρ}(T)
of the coefficient short exact sequence 0 → T → M → V → 0 is the snake map
of the degreewise-short-exact sequence of word complexes
(lem:exactcoefffunctor, eq:coneshortexact). We construct it abstractly from
the degree-(1, 2) truncation: degree-two cohomology is the cokernel
H² = coker d¹, degree-one cocycles are Z¹ = ker d¹, and the connecting map
is Z¹(V) → coker d¹_T = H²(T). This is the candidate ∂_{Γ,ρ} at cocycle
level (it already descends to H¹; the manuscript uses it on Z¹ directly,
l.4015).
The submodule of degree-one M-cochains lying over a V-cocycle:
m with p₄ m ∈ ker d¹_V. On it, d¹_M lands in range i₂ (the T-part),
which is what makes the snake map defined.
Equations
- Q2Presentation.Lifting.obstrCochains dV p4 = Submodule.comap p4 dV.ker
Instances For
On obstrCochains, the degree-two differential d¹_M factors through the
T-part range i₂ (right naturality square + exactness).
The T-valued snake cochain g : obstrCochains → T2, characterised by
i₂ ∘ g = d¹_M (uses injectivity of i₂).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The snake map at cochain level obstrCochains → H²(T) = coker d¹_T,
m ↦ [g m] where i₂(g m) = d¹_M m.
Equations
- Q2Presentation.Lifting.snakeMapCochain dT dM dV p4 i2 p2 hi2 hex2 hnatV = dT.range.mkQ ∘ₗ Q2Presentation.Lifting.snakeT dM dV p4 i2 p2 hi2 hex2 hnatV
Instances For
The surjection obstrCochains ↠ Z¹(V) = ker d¹_V induced by p₄.
Equations
- Q2Presentation.Lifting.projToKer dV p4 = LinearMap.codRestrict dV.ker (p4 ∘ₗ (Q2Presentation.Lifting.obstrCochains dV p4).subtype) ⋯
Instances For
Well-definedness (independence of the M-lift): the snake cochain map
kills ker(p₄|) = range i₄ (left naturality square + degree-4 exactness),
hence descends along the surjection obstrCochains ↠ Z¹(V).
The candidate connecting homomorphism ∂_{Γ,ρ} : Z¹_{Γ,ρ}(V) → H²_{Γ,ρ}(T)
(cor:adjointboundary, l.2005), the snake map of the degreewise-short-exact
sequence of word complexes 0 → C(T) → C(M) → C(V) → 0
(lem:exactcoefffunctor, eq:coneshortexact). On a V-cocycle c, lift to
m̃ ∈ M⁴ with p₄ m̃ = c; then d¹_M m̃ = i₂ t for a unique t ∈ T², and
∂c = [t] ∈ H²(T).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The defining property of the connecting map (the snake recipe): for a
V-cocycle c, any M-lift m̃ with p₄ m̃ = c, and the unique t with
i₂ t = d¹_M m̃, one has ∂c = [t] in H²(T). This confirms connectingMap
is the genuine snake map of lem:exactcoefffunctor.
cor:adjointboundary — the adjoint-boundary relation (eq:adjointboundary) #
The adjoint-boundary relation (cor:adjointboundary, eq:adjointboundary).
The connecting map ∂ : H¹_{Γ,ρ}(V) → H²_{Γ,ρ}(T) is adjoint to the
dual-boundary map ρ*∘∂_C^∨ : H²(T)^∨ → H¹(V^∨) against the evaluation pairing
on H²(T) and the perfect cup pairing cup = ⟨·,·⟩_Γ on H¹(V) × H¹(V^∨):
⟨∂c, χ⟩ = ⟨c, ρ*γ_χ⟩_Γ for all c ∈ H¹(V), χ ∈ H²(T)^∨.
On the candidate side this holds by the naturality of the Fox–Heisenberg chain
map D_{ρ,A} (prop:chainmap, eq:chainid1/eq:chainid2, i.e. the traced
finite-word Stokes identity prop:tracedstokes); on the local side by the
compatibility of connecting homomorphisms with cup product and the invariant map
(prop:localduality). The two sources thus share the same connecting map.
Equations
- Q2Presentation.Lifting.IsAdjointBoundary boundary dualBoundary cup = ∀ (c : HV) (χ : Module.Dual (ZMod 2) H2T), χ (boundary c) = (cup c) (dualBoundary χ)
Instances For
The adjoint-boundary relation determines the connecting map. Against the
evaluation pairing on H²(T), eq:adjointboundary pins ∂ down uniquely from the
dual-boundary and cup data. This is the numerical force of cor:adjointboundary:
the candidate and local connecting maps — sharing the common dual boundary and the
common perfect cup pairing (prop:defduality = prop:localduality numerically) —
necessarily agree. (Uses only that linear functionals separate points of the
finite-dimensional H²(T).)