Documentation

GQ2.Devissage

§5.11 dévissage: two-out-of-three for IsSelfDual along a module SES #

lemma_5_11 (proved at the bottom of this file; the IsSelfDual package is defined in GQ2/FoxHeisenberg/Traced.lean) is the two-out-of-three property of the IsSelfDual package along a short exact sequence 0 → A' → A → A'' → 0 of finite elementary 𝔽₂[C]-modules. The proof device is the long exact cohomology sequence of the word complex C(A) : A --d⁰--> A⁴ --d¹--> A² (displays (30)/(49)/(50)): the degreewise functors A ↦ A, A ↦ Fin 4 → A, A ↦ A × A are exact (identity / finite products), and d⁰, d¹ are natural in the coefficient module (this file's d0_natural/d1_natural), so the module SES induces a short exact sequence of complexes, whence a nine-term LES

0 → H⁰(A') → H⁰(A) → H⁰(A'') → H¹(A') → H¹(A) → H¹(A'') → H²(A') → H²(A) → H²(A'') → 0.

A key simplification: rank-nullity on d¹ gives dim Z¹w = 2·dim A + dim H²w for every A (Z1w = ker d¹, H2w = coker d¹), so the two card clauses of IsSelfDual are equivalent — the card part reduces to the single clause #H²w(A) = #fixedPts(ElemDual A).

The word-complex theorem #

selfdualW_two_of_three is the master theorem: two-out-of-three for IsSelfDualW, the word-internal form of the package with #H⁰w(A^∨) in place of #fixedPts C (A^∨). The proof runs two nine-term LESs (the word complex of the SES, and of its dualization — exact by the elementary-dual pack) tied into a duality ladder by six χ-maps whose squares all commute (lemma_5_6, the evaluation squares, and the two δ-square cores), and closes with nine four-lemma windows. Free inputs: χ⁰/χ⁰ᵀ are always injective (separation), χ²/χ²ᵀ always surjective (extension/biduality), and the Euler-characteristic swap #H⁰w(A) = #H²w(A^∨) converts the given card clauses into full bijectivity.

Relating word invariants to fixed points #

ker d⁰ is the fixed set of the four marked elements, whereas IsSelfDual uses fixedPts C — all of C. These agree exactly for a generating marking: H0w_eq_fixedPts (hgen : t.Generates), whence isSelfDual_iff_W. Accordingly lemma_5_11 now carries hgen : t.Generates and lives at the bottom of this file (the proof needs this file's machinery; imports run FoxHeisenberg → Devissage), proved by splicing selfdualW_two_of_three through isSelfDual_iff_W. Its consumer prop_5_15 (FoxHeisenberg.lean, the Prop. 5.15 proof) gained the same hypothesis — admissible markings supply it.

Paper-tag ledger (auto-generated by paperforge; do not edit) #