§5.11 dévissage: the dualized SES, δ-squares, and the master two-of-three #
Part of the §5.11 dévissage development (split from GQ2/Devissage.lean).
The dualized SES and the δ-squares #
Dualizing the SES gives 0 → A''^∨ --g^∨--> A^∨ --f^∨--> A'^∨ → 0; the LES machinery
instantiates on it verbatim. The δ-squares — the genuinely new commutativity content of the
ladder — reduce to two snake-vs-snake core computations, each a chain of Prop 5.8 and
Lemma 5.6 through the chosen lifts.
δ⁰ of the dualized SES: H⁰w(A'^∨) →+ H¹w(A''^∨).
Equations
- GQ2.FoxH.delta0D f g hf hg hinj hsurj hexact hA₂ t ht hw = GQ2.FoxH.delta0 (GQ2.FoxH.dualMap g) (GQ2.FoxH.dualMap f) ⋯ ⋯ ⋯ ⋯ ⋯ t ht hw
Instances For
δ¹ of the dualized SES: H¹w(A'^∨) →+ H²w(A''^∨).
Equations
- GQ2.FoxH.delta1D f g hf hg hinj hsurj hexact hA₂ t ht hw = GQ2.FoxH.delta1 (GQ2.FoxH.dualMap g) (GQ2.FoxH.dualMap f) ⋯ ⋯ ⋯ ⋯ ⋯ t ht hw
Instances For
δ-square core 1: evaluating λ ∈ H⁰w(A'^∨) on the δ¹-snake of c'' equals pairing
c'' against the dual δ⁰-snake word of λ. (Lift λ to Λ along f^∨; both sides equal
B(lift c'', d⁰Λ) by Prop 5.8 right resp. Lemma 5.6.)
δ-square core 2: pairing the primal δ⁰-snake word of a'' against a dual cocycle y'
equals evaluating the dual δ¹-snake of y' on a''. (Mirror of core 1: Prop 5.8 left +
Lemma 5.6 through the lifts.)
δ-square (1,2): χ²_{A'} ∘ δ¹ = (δ⁰ of the dual SES)^∨ ∘ χ¹_{A''}.
δ-square (0,1): χ¹_{A'} ∘ δ⁰ = (δ¹ of the dual SES)^∨ ∘ χ⁰_{A''}.
δ-square (0,1), transposed: χ¹ᵀ_{A''} ∘ δ⁰_dual = (δ¹)^∨ ∘ χ⁰ᵀ_{A'}.
δ-square (1,2), transposed: χ²ᵀ_{A''} ∘ δ¹_dual = (δ⁰)^∨ ∘ χ¹ᵀ_{A'}.
Lemma 5.11, word-internal form (exact-cone dévissage): two-out-of-three for
IsSelfDualW along the module SES. Proof: translate each IsSelfDualW into
χ-bijectivities (isSelfDualW_iff, chi_bij_of_selfdualW), then chase the duality ladder —
nine four-lemma windows across the two LESs (word complex of the SES, and of its dualization)
tied by the lemma_5_6-squares, the evaluation squares and the δ-squares.