Transgression splitting for Lemma 6.21

Proof layer for GQ2.SectionSix.lemma_6_21: an extension 1 → V → B → C → 1 carrying a global 𝔽₂-valued 2-cocycle ξ whose fibre diagonal is a nonsingular quadratic form q splits. The paper's mechanism is the transgression formula d₂(q) = B_q^♭ ∘ η (eq. (116)); this file fixes a direct cochain-level design with no spectral sequences:

The design

Fix a set-section σ : C → B with σ 1 = 1 (Function.surjInv patched at 1) and its factor set f c d := i⁻¹(σ c · σ d · σ (c·d)⁻¹) ∈ V (values in i.range = ker p). Define the explicit mixed cochain

A : C → V → ZMod 2, A c v := ξ (σ c, i (c⁻¹ • v)) + ξ (i v, σ c).

The key transgression identity (key_transgression, the cochain-level (116)) is

polar q (f c d) v = A c v + A d (c⁻¹ • v) + A (c*d) v — i.e. B_q^♭ ∘ f = δA in the C-module V^∨ = (V → 𝔽₂) with (c • φ) v = φ (c⁻¹ • v),

proved by expanding hcocycle on mixed triples from {σ c, σ d, i v} (the grind is lemma_6_22-flavoured: linear_combination (norm := (ring_nf; simp [CharTwo.two_eq_zero])) over the cocycle instances, after normalizing arguments with hconj/hσ).

A c is not additive in v (defect = the conjugation defect of the fibre restriction R := ξ∘(i×i), mixedA_defect), so B_q^♭⁻¹ cannot be applied to it directly. The paper's Lemma 6.21 resolves this obstruction with its "fixed equivariant class κ⁰_q" hypothesis: in cochain avatar, a family t : C → V → 𝔽₂ with

(i) δ_V(t c) = R(c•, c•) + R (each t c is a central automorphism datum of 𝔽₂ ×_R V over the c-action), and (ii) t (c·d) = t c (d•·) + t d (the automorphisms compose coherently, eq. (60)),

which is exactly Lemma 6.1's IsEquivariantFactorSet correction family m, transported from dat.f to R along a primitive θ of the symmetric zero-diagonal 2-cocycle dat.f + R (symm_cocycle_is_coboundary, equivariant_lift_of_factorSet). Then à c := A c + t c⁻¹ is additive with the same δ (by (i) the defects cancel; by (ii) the correction telescopes), g := B_q^♭⁻¹ ∘ Ã satisfies f = δg (bijectivity + C-equivariance of B_q^♭), and s c := i (g c)⁻¹ · σ c is the splitting homomorphism.

Facts derived, not assumed

• V has exponent 2: polar q (v+v) w = 2·polar q v w = 0 for all w, so hns forces v + v = 0 (exponent_two_of_nonsingular, proved below).
• ξ is normalized at 1: cocycle instances give ξ(g,1) = ξ(1,k) = ξ(1,1), and hξq at v = 0 gives ξ(1,1) = q 0 = 0.
• q (c • v) = q v and polar q (c•v) (c•w) = polar q v w: conjugating a 2-cocycle changes it by an explicit coboundary δ(k_b); diagonals and antisymmetrizations of coboundaries vanish (δa is symmetric with zero diagonal), so both are conjugation-invariant.

Result

The theorem splitting_of_global_cocycle implements the complete assembly, and SectionSix.lemma_6_21 applies it through equivariant_lift_of_factorSet. The κ⁰_q hypothesis (t, ht_quad, ht_mul) restores the paper's "relative to the fixed equivariant class" clause dropped by the consequence-form extraction — see docs/orchestration/p15i-transgression-gap.md.

theorem GQ2.Transgression.exponent_two_of_nonsingular {V : Type} [AddCommGroup V] {q : V → ZMod 2} (hq : QuadraticFp2.IsQuadraticFp2 q) (hns : QuadraticFp2.Nonsingular q) (v : V) : v + v = 0

Exponent 2 of the fibre is forced by nonsingularity (no h2 hypothesis needed): polar q (v+v) w = 2·polar q v w = 0 for every w.

Symmetric zero-diagonal 2-cocycles on an elementary-abelian group are coboundaries

The injectivity half of H²(V, 𝔽₂) ≅ {quadratic forms}; used to transport the Lemma 6.1 correction family m from the datum's factor set dat.f to ξ's own fibre restriction.

theorem GQ2.Transgression.symm_cocycle_is_coboundary {V : Type} [AddCommGroup V] (h2 : ∀ (v : V), v + v = 0) (S : V → V → ZMod 2) (hcoc : ∀ (v w x : V), S (v + w) x + S v w = S v (w + x) + S w x) (hsymm : ∀ (v w : V), S v w = S w v) (hdiag : ∀ (v : V), S v v = 0) : ∃ (θ : V → ZMod 2), θ 0 = 0 ∧ ∀ (v w : V), S v w = θ (v + w) + θ v + θ w

Symmetric zero-diagonal 2-cocycles on an elementary-abelian group are coboundaries: if S satisfies the trivial-coefficient 2-cocycle identity, is symmetric and has zero diagonal, then S = δθ for some θ with θ 0 = 0. Proof: the twisted product 𝔽₂ ×_S V is an abelian group of exponent 2 (commutativity = symmetry, inverses = zero diagonal), hence an 𝔽₂-vector space; the projection to V is linear and surjective, so it has a linear section, whose central coordinate is θ.

theorem GQ2.Transgression.bflat_bijective {V : Type} [AddCommGroup V] [Finite V] (q : V → ZMod 2) (hq : QuadraticFp2.IsQuadraticFp2 q) (hns : QuadraticFp2.Nonsingular q) (φ : V → ZMod 2) : (∀ (x y : V), φ (x + y) = φ x + φ y) → ∃! v : V, ∀ (w : V), QuadraticFp2.polar q v w = φ w

The polar adjoint B_q^♭ : V → (V → 𝔽₂) is bijective onto the additive functionals: for every additive φ : V → 𝔽₂ there is a unique v with polar q v · = φ. The polar of a nonsingular q on the finite elementary abelian V is a nondegenerate 𝔽₂-bilinear form, so V ≃ₗ Module.Dual (ZMod 2) V (LinearMap.BilinForm.toDual); additivity ⟹ 𝔽₂-linearity via AddMonoidHom.toZModLinearMap.

theorem GQ2.Transgression.polar_fibre {V : Type} [AddCommGroup V] {B : Type} [Group B] (i : Multiplicative V →* B) (q : V → ZMod 2) (hq : QuadraticFp2.IsQuadraticFp2 q) (hns : QuadraticFp2.Nonsingular q) (ξ : B × B → ZMod 2) (hcocycle : ∀ (g h k : B), ξ (h, k) + ξ (g, h * k) = ξ (g * h, k) + ξ (g, h)) (hξq : ∀ (v : V), ξ (i (Multiplicative.ofAdd v), i (Multiplicative.ofAdd v)) = q v) (u w : V) : QuadraticFp2.polar q u w = ξ (i (Multiplicative.ofAdd u), i (Multiplicative.ofAdd w)) + ξ (i (Multiplicative.ofAdd w), i (Multiplicative.ofAdd u))

The fibre antisymmetrization computes the polar: for u w : V, polar q u w = ξ(iu, iw) + ξ(iw, iu). Proof: expand q(u+w) = ξ(iu·iw, iu·iw) by the cocycle on the (commuting, involutive) fibre elements iu, iw, using normalization ξ(1, ·) = 0.

theorem GQ2.Transgression.xi_conj_cobound {B : Type} [Group B] (ξ : B × B → ZMod 2) (hcocycle : ∀ (g h k : B), ξ (h, k) + ξ (g, h * k) = ξ (g * h, k) + ξ (g, h)) (s x y : B) : ξ (s * x * s⁻¹, s * y * s⁻¹) + ξ (x, y) = ξ (s, x) + ξ (s * x * s⁻¹, s) + (ξ (s, y) + ξ (s * y * s⁻¹, s)) + (ξ (s, x * y) + ξ (s * (x * y) * s⁻¹, s))

Conjugation is a coboundary: for a trivial-coefficient 2-cocycle ξ, conjugation by a fixed s changes ξ by the coboundary of the 1-cochain β_s(z) = ξ(s, z) + ξ(szs⁻¹, s): ξ(sxs⁻¹, sys⁻¹) + ξ(x, y) = β_s(x) + β_s(y) + β_s(xy). (Three cocycle instances, char 2.)

theorem GQ2.Transgression.polar_conj {C : Type} [Group C] {V : Type} [AddCommGroup V] [DistribMulAction C V] {B : Type} [Group B] (p : B →* C) (hp : Function.Surjective ⇑p) (i : Multiplicative V →* B) (hconj : ∀ (b : B) (v : V), b * i (Multiplicative.ofAdd v) * b⁻¹ = i (Multiplicative.ofAdd (p b • v))) (q : V → ZMod 2) (hq : QuadraticFp2.IsQuadraticFp2 q) (hns : QuadraticFp2.Nonsingular q) (ξ : B × B → ZMod 2) (hcocycle : ∀ (g h k : B), ξ (h, k) + ξ (g, h * k) = ξ (g * h, k) + ξ (g, h)) (hξq : ∀ (v : V), ξ (i (Multiplicative.ofAdd v), i (Multiplicative.ofAdd v)) = q v) (c : C) (v w : V) : QuadraticFp2.polar q (c • v) (c • w) = QuadraticFp2.polar q v w

Conjugation-invariance of the polar form: polar q (c•v) (c•w) = polar q v w. The polar is the fibre antisymmetrization (polar_fibre), and by xi_conj_cobound conjugation changes ξ by a coboundary; the antisymmetrization of a coboundary vanishes on the commuting fibre elements, so the polar is C-invariant.

noncomputable def GQ2.Transgression.sigma {C : Type} [Group C] {B : Type} [Group B] (p : B →* C) (hp : Function.Surjective ⇑p) : C → B

The normalized section: Function.surjInv hp patched to send 1 ↦ 1.

Equations

• GQ2.Transgression.sigma p hp c = if c = 1 then 1 else Function.surjInv hp c

noncomputable def GQ2.Transgression.factorSet {C : Type} [Group C] {V : Type} [AddCommGroup V] {B : Type} [Group B] (p : B →* C) (hp : Function.Surjective ⇑p) (i : Multiplicative V →* B) (c d : C) : V

The factor set of sigma, valued in V through i⁻¹ (well-defined: σc·σd·σ(cd)⁻¹ ∈ ker p = i.range). [O: define via Function.invFun i + hrange; prove i (ofAdd (factorSet c d)) = sigma c * sigma d * (sigma (c*d))⁻¹.]

Equations

• One or more equations did not get rendered due to their size.

theorem GQ2.Transgression.factorSet_spec {C : Type} [Group C] {V : Type} [AddCommGroup V] {B : Type} [Group B] (p : B →* C) (hp : Function.Surjective ⇑p) (i : Multiplicative V →* B) (hrange : i.range = p.ker) (c d : C) : i (Multiplicative.ofAdd (factorSet p hp i c d)) = sigma p hp c * sigma p hp d * (sigma p hp (c * d))⁻¹

Defining property of the factor set: i (ofAdd (f c d)) = σc · σd · σ(cd)⁻¹ (well-defined since σc·σd·σ(cd)⁻¹ ∈ ker p = i.range).

noncomputable def GQ2.Transgression.mixedA {C : Type} [Group C] {V : Type} [AddCommGroup V] [DistribMulAction C V] {B : Type} [Group B] (p : B →* C) (hp : Function.Surjective ⇑p) (i : Multiplicative V →* B) (ξ : B × B → ZMod 2) (c : C) (v : V) : ZMod 2

The mixed transgression cochain A c v = ξ(σc, i(c⁻¹•v)) + ξ(iv, σc).

Equations

• GQ2.Transgression.mixedA p hp i ξ c v = ξ (GQ2.Transgression.sigma p hp c, i (Multiplicative.ofAdd (c⁻¹ • v))) + ξ (i (Multiplicative.ofAdd v), GQ2.Transgression.sigma p hp c)

theorem GQ2.Transgression.mixedA_defect {C : Type} [Group C] {V : Type} [AddCommGroup V] [DistribMulAction C V] {B : Type} [Group B] (p : B →* C) (hp : Function.Surjective ⇑p) (i : Multiplicative V →* B) (hconj : ∀ (b : B) (v : V), b * i (Multiplicative.ofAdd v) * b⁻¹ = i (Multiplicative.ofAdd (p b • v))) (ξ : B × B → ZMod 2) (hcocycle : ∀ (g h k : B), ξ (h, k) + ξ (g, h * k) = ξ (g * h, k) + ξ (g, h)) (c : C) (v w : V) : mixedA p hp i ξ c (v + w) + mixedA p hp i ξ c v + mixedA p hp i ξ c w = ξ (i (Multiplicative.ofAdd (c⁻¹ • v)), i (Multiplicative.ofAdd (c⁻¹ • w))) + ξ (i (Multiplicative.ofAdd v), i (Multiplicative.ofAdd w))

The additivity defect of mixedA is the fibre-restriction conjugation defect (the D_c of the Lemma 6.21 proof gap analysis): mixedA c fails additivity in v by exactly ξ(i(c⁻¹v), i(c⁻¹w)) + ξ(iv, iw). Three hcocycle instances after two hconj moves; this is what blocks B_q^♭⁻¹ ∘ mixedA and forces the κ⁰_q hypothesis.

theorem GQ2.Transgression.key_transgression {C : Type} [Group C] {V : Type} [AddCommGroup V] [DistribMulAction C V] {B : Type} [Group B] (p : B →* C) (hp : Function.Surjective ⇑p) (i : Multiplicative V →* B) (hrange : i.range = p.ker) (hconj : ∀ (b : B) (v : V), b * i (Multiplicative.ofAdd v) * b⁻¹ = i (Multiplicative.ofAdd (p b • v))) (q : V → ZMod 2) (hq : QuadraticFp2.IsQuadraticFp2 q) (hns : QuadraticFp2.Nonsingular q) (ξ : B × B → ZMod 2) (hcocycle : ∀ (g h k : B), ξ (h, k) + ξ (g, h * k) = ξ (g * h, k) + ξ (g, h)) (hξq : ∀ (v : V), ξ (i (Multiplicative.ofAdd v), i (Multiplicative.ofAdd v)) = q v) (c d : C) (v : V) : QuadraticFp2.polar q (factorSet p hp i c d) v = mixedA p hp i ξ c v + mixedA p hp i ξ d (c⁻¹ • v) + mixedA p hp i ξ (c * d) v

The key transgression identity — the cochain-level eq. (116): B_q^♭(f c d) = (δA)(c,d) as functionals on V, i.e. polar q (f c d) v = A c v + A d (c⁻¹•v) + A (c*d) v. Proof: rewrite the polar as a fibre antisymmetrization (polar_fibre), the factor set through factorSet_spec, then close with a single char-2 linear_combination of nine hcocycle instances whose group arguments are normalized by three hconj-conjugation moves (m1/m2/m3).

theorem GQ2.Transgression.equivariant_lift_of_factorSet {C : Type} [Group C] {V : Type} [AddCommGroup V] [DistribMulAction C V] {B : Type} [Group B] (i : Multiplicative V →* B) (q : V → ZMod 2) (hq : QuadraticFp2.IsQuadraticFp2 q) (hns : QuadraticFp2.Nonsingular q) (ξ : B × B → ZMod 2) (hcocycle : ∀ (g h k : B), ξ (h, k) + ξ (g, h * k) = ξ (g * h, k) + ξ (g, h)) (hξq : ∀ (v : V), ξ (i (Multiplicative.ofAdd v), i (Multiplicative.ofAdd v)) = q v) (dat : FactorSet C V) (hdat : IsEquivariantFactorSet q dat) : ∃ (t : C → V → ZMod 2), (∀ (c : C) (v w : V), t c (v + w) + t c v + t c w = ξ (i (Multiplicative.ofAdd (c • v)), i (Multiplicative.ofAdd (c • w))) + ξ (i (Multiplicative.ofAdd v), i (Multiplicative.ofAdd w))) ∧ ∀ (c d : C) (v : V), t (c * d) v = t c (d • v) + t d v

The κ⁰_q-datum supplies the coherent equivariant lift (Lemma 6.1 → the paper's α_c-family): from an equivariant factor-set datum for q (IsEquivariantFactorSet), transport the correction family m along a primitive θ of dat.f + ξ|fibre (two 2-cocycles on V with the same diagonal q, so their difference is a symmetric zero-diagonal 2-cocycle — symm_cocycle_is_coboundary). The result satisfies the two identities of eqs. (59)/(60) with ξ's own fibre restriction in place of dat.f — the hypothesis shape consumed by splitting_of_global_cocycle.

theorem GQ2.Transgression.splitting_of_global_cocycle {C : Type} [Group C] {V : Type} [AddCommGroup V] [Finite V] [DistribMulAction C V] {B : Type} [Group B] (p : B →* C) (hp : Function.Surjective ⇑p) (i : Multiplicative V →* B) (hrange : i.range = p.ker) (hconj : ∀ (b : B) (v : V), b * i (Multiplicative.ofAdd v) * b⁻¹ = i (Multiplicative.ofAdd (p b • v))) (q : V → ZMod 2) (hq : QuadraticFp2.IsQuadraticFp2 q) (hns : QuadraticFp2.Nonsingular q) (ξ : B × B → ZMod 2) (hcocycle : ∀ (g h k : B), ξ (h, k) + ξ (g, h * k) = ξ (g * h, k) + ξ (g, h)) (hξq : ∀ (v : V), ξ (i (Multiplicative.ofAdd v), i (Multiplicative.ofAdd v)) = q v) (t : C → V → ZMod 2) (ht_quad : ∀ (c : C) (v w : V), t c (v + w) + t c v + t c w = ξ (i (Multiplicative.ofAdd (c • v)), i (Multiplicative.ofAdd (c • w))) + ξ (i (Multiplicative.ofAdd v), i (Multiplicative.ofAdd w))) (ht_mul : ∀ (c d : C) (v : V), t (c * d) v = t c (d • v) + t d v) : ∃ (s : C →* B), ∀ (cc : C), p (s cc) = cc

The assembled splitting (= lemma_6_21, relative to the fixed equivariant class). The κ⁰_q hypothesis is the family (t, ht_quad, ht_mul): each t c is the central-correction datum of an automorphism of the fibre extension 𝔽₂ ×_{ξ|fibre} V over the c-action (ht_quad), and the family composes coherently (ht_mul) — the paper's α_c α_d = α_{cd}; it is supplied by equivariant_lift_of_factorSet from Lemma 6.1's IsEquivariantFactorSet. Structure of the proof:

• Additive primitive: à c := mixedA c + t c⁻¹ is additive in v (mixedA_defect cancels against ht_quad at c⁻¹) and has the same C-coboundary as mixedA (ht_mul telescopes), so key_transgression + bflat_bijective produce a B_q^♭-representable transgression primitive g : C → V.
• Descent: polar-adjoint injectivity (bflat_bijective) together with polar_conj (equivariance) upgrades the primitive to the H²(C,V)-coboundary equation f c d = g c + c • g d + g (c*d).
• Section: from that coboundary equation, s c := i(ofAdd (g c))⁻¹ · σ c is a monoid homomorphism sectioning p (hconj + factorSet_spec + fibre 2-torsion).

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

• eq. (116) = ⟦eq-transgressionformula⟧
• eq. (59) = ⟦eq-mquadratic⟧
• eq. (60) = ⟦eq-mcoherent⟧
• Lemma 6.1 = ⟦lem-extraspecialconnecting⟧
• Lemma 6.21 = ⟦lem-transgression⟧