§5.11 dévissage on the r_R spine: the long exact sequence — SES of complexes and connecting maps #
Mechanical R-spine clone of GQ2/Devissage/LESCore.lean (campaign decision,
docs/orchestration/roe-r20-recon.md); proofs ported verbatim. Spine renames Z1w → Z1wR, H1w → H1wR, H2w → H2wR, d1Fun → d1FunR, d1 → d1R, mixedB → mixedB_R, WildRel → WildRelR,
IsSelfDual(W) → IsSelfDual(W)_R, with R-suffixed public names. The (A) degreewise-exactness
helpers pi_g_surjective, pi_exact, prod_g_surjective, prod_exact are reused from
GQ2.Devissage.LESCore, never cloned.
The long exact sequence #
A module SES 0 → A' --f--> A --g--> A'' → 0 (with C-equivariant f, g) induces a short
exact sequence of word complexes; the degreewise functors (·)⁴ and (·)² are exact. From this
we build the connecting maps and the nine-term LES.
The connecting map δ¹ : H¹w(A'') → H²w(A') (snake) #
A chosen lift of a degree-1 A''-cochain to A⁴ (via g surjective).
Equations
- GQ2.FoxH.snakeLift_R g hsurj c'' i = ⋯.choose
Instances For
For a cocycle c'' ∈ Z¹w(A''), d¹ of its lift lands in ker(g × g).
The A'²-element the snake extracts: (f × f)(snakeZ_R) = d¹(lift c'').
Equations
- GQ2.FoxH.snakeZ_R f g hg hsurj hexact t c'' = ⋯.choose
Instances For
Well-definedness of the snake: for any lift c of c'' and any z with
(f×f)(z) = d¹(c), the class [z] ∈ H²w(A') equals [snakeZ_R c''] — so δ¹ will not depend on
the chosen lift, hence descends to a hom on H¹w(A'').
The connecting map on cocycles, Z¹w(A'') →+ H²w(A'), c'' ↦ [snakeZ_R c''] (a hom by
snakeZ_welldef_R, using additive lifts).
Equations
- GQ2.FoxH.delta1raw_R f g hf hg hinj hsurj hexact t = { toFun := fun (c'' : ↥(GQ2.FoxH.Z1wR t)) => ↑(GQ2.FoxH.snakeZ_R f g hg hsurj hexact t c''), map_zero' := ⋯, map_add' := ⋯ }
Instances For
The snake connecting map δ¹ : H¹w(A'') → H²w(A'). Descends delta1raw_R through the
B¹w-quotient: a coboundary c'' = d⁰(a'') lifts to d⁰(â), whose d¹ is 0, so its class
is 0.
Equations
- GQ2.FoxH.delta1_R f g hf hg hinj hsurj hexact t ht hw = QuotientAddGroup.lift ((GQ2.FoxH.B1wR t).addSubgroupOf (GQ2.FoxH.Z1wR t)) (GQ2.FoxH.delta1raw_R f g hf hg hinj hsurj hexact t) ⋯
Instances For
The connecting map δ⁰ : H⁰w(A'') → H¹w(A') (snake) #
The mirror of δ¹ one degree down. Lift a'' ∈ H⁰w(A'') to a ∈ A; then d⁰a ∈ ker(g∘·)
(as g∘d⁰a = d⁰(g a) = d⁰a'' = 0), so d⁰a = f∘w for a unique w : A'⁴, which is a cocycle
(f∘d¹w = d¹(f∘w) = d¹d⁰a = 0, f injective). δ⁰(a'') := [w] ∈ H¹w(A'); the class is
independent of the lift a (a different lift shifts w by a coboundary). The domain H⁰w is an
honest subgroup (no quotient), so — unlike δ¹ — no descent is needed, only lift-independence.
For a'' ∈ H⁰w(A''), d⁰ of the chosen lift lands in ker(g∘·) (degree 1).
The A'⁴-cochain the degree-0 snake extracts: f∘(snake0Z'_R) = d⁰(lift a'').
Equations
- GQ2.FoxH.snake0Z'_R f g hg hsurj hexact t a'' = ⋯.choose
Instances For
snake0Z'_R ∈ Z¹w(A'): its d¹ vanishes (pull d¹∘d⁰ = 0 back through the injection f).
Lift-independence of δ⁰: any lift a of a'' with cocycle w (f∘w = d⁰a) gives the
same class [w] = δ⁰(a''). A second lift differs by f a', shifting w by d⁰a'.
The degree-0 connecting map δ⁰ : H⁰w(A'') →+ H¹w(A').
Equations
- GQ2.FoxH.delta0_R f g hf hg hinj hsurj hexact t ht hw = { toFun := fun (a'' : ↥(GQ2.FoxH.H0w t)) => ↑⟨GQ2.FoxH.snake0Z'_R f g hg hsurj hexact t a'', ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }