The splitting lemma, ξ-calculus and the Θ-extraction

Split off from GQ2.KeystoneDelta (design §§3–5). This file provides:

• Stage B — the V-splitting lemma exists_splitting_of_symm_zero_diag (a symmetric zero-diagonal normalized 2-cocycle on a finite elementary-abelian 2-group is a coboundary);
• Stage C.1 — the ξ-normalization lemmas and the cover-commutator = polar lemma (xi_polar);
• Stage C.2 — the descended-cover cocycle κfull and the Θ-facts (theta_facts);
• Stage C.3 — Θ', the four-chase extraction (theta'_decomp) and the dual-crossed law for the edge γκ (gammakap_dual_crossed).

See GQ2.KeystoneDelta for the umbrella module docstring.

Stage B: the V-splitting lemma (design §3)

A symmetric, zero-diagonal, normalized 2-cocycle on a finite elementary-abelian 2-group is a coboundary: the twisted extension it classifies is an 𝔽₂-vector space, so the projection has a linear section, whose first coordinate is the splitting cochain.

theorem GQ2.SectionEight.AffineTLift.exists_splitting_of_symm_zero_diag {V : Type} [AddCommGroup V] [Finite V] (hV2 : ∀ (v : V), v + v = 0) (φ : V → V → ZMod 2) (hcoc : ∀ (v w x : V), φ (v + w) x + φ v w = φ v (w + x) + φ w x) (hsymm : ∀ (v w : V), φ v w = φ w v) (hdiag : ∀ (v : V), φ v v = 0) (hzl : ∀ (v : V), φ 0 v = 0) : ∃ (g : V → ZMod 2), g 0 = 0 ∧ ∀ (v w : V), φ v w = g (v + w) + g v + g w

The splitting lemma (design §3): a symmetric zero-diagonal normalized 2-cocycle on a finite elementary-abelian 2-group is ∂g for a normalized g.

Stage C, part 1: ξ-normalization and the cover-commutator = polar lemma (design §5)

theorem GQ2.SectionEight.AffineTLift.ker_sq_one {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} (Dsc : Descent D) {x : covQ Dsc} (hx : x ∈ (descP Dsc).ker) : x * x = 1

Kernel elements of descP are involutions.

theorem GQ2.SectionEight.AffineTLift.xi_diag_sq {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} (Dsc : Descent D) {x : Bg ⧸ D.T} (hx : x * x = 1) : xi Dsc (x, x) = ccZsign Dsc (s0 Dsc x * s0 Dsc x)

The diagonal of ξ at an involution is the section-square sign.

theorem GQ2.SectionEight.AffineTLift.xi_polar {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} (Dsc : Descent D) (v w : DD.Vmod) : xi Dsc ((iV DD) (Multiplicative.ofAdd v), (iV DD) (Multiplicative.ofAdd w)) + xi Dsc ((iV DD) (Multiplicative.ofAdd w), (iV DD) (Multiplicative.ofAdd v)) = QuadraticFp2.polar DD.qbar v w

The cover-commutator = polar lemma (design §5): the symmetry defect of ξ on the V-fibre is the polar form of the descended square map q̄.

Stage C, part 2: the descended-cover cocycle and the Θ-extraction (design §4)

noncomputable def GQ2.SectionEight.AffineTLift.kfull {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} (σ : DD.C0 →* Bg ⧸ D.T) (Dsc : Descent D) (p q : DD.Vmod × DD.C0) : ZMod 2

The descended central class κfull, transported to the raw semidirect pairs.

Equations

• GQ2.SectionEight.AffineTLift.kfull σ Dsc p q = GQ2.SectionEight.AffineTLift.xi Dsc (GQ2.SectionEight.AffineTLift.jmap DD σ p, GQ2.SectionEight.AffineTLift.jmap DD σ q)

theorem GQ2.SectionEight.AffineTLift.kfull_serre {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} (σ : DD.C0 →* Bg ⧸ D.T) (Dsc : Descent D) (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (p q r : DD.Vmod × DD.C0) : kfull σ Dsc q r + kfull σ Dsc p (pmul q r) = kfull σ Dsc (pmul p q) r + kfull σ Dsc p q

κfull satisfies the raw Serre identity for pmul.

theorem GQ2.SectionEight.AffineTLift.m_zero {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} {q : DD.Vmod → ZMod 2} {dat : FactorSet DD.C0 DD.Vmod} (hdat : IsEquivariantFactorSet q dat) (cc : DD.C0) : dat.m cc 0 = 0

m_c(0) = 0 for an equivariant factor-set datum.

theorem GQ2.SectionEight.AffineTLift.kappa0_serre {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} {q : DD.Vmod → ZMod 2} {dat : FactorSet DD.C0 DD.Vmod} (hdat : IsEquivariantFactorSet q dat) (p q' r : DD.Vmod × DD.C0) : kappa0 dat q' r + kappa0 dat p (pmul q' r) = kappa0 dat (pmul p q') r + kappa0 dat p q'

The raw Serre identity for kappa0 of any equivariant factor-set datum.

theorem GQ2.SectionEight.AffineTLift.pcob_serre {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} (G : DD.Vmod × DD.C0 → ZMod 2) (p q r : DD.Vmod × DD.C0) : G (pmul q r) + G q + G r + (G (pmul p (pmul q r)) + G p + G (pmul q r)) = G (pmul (pmul p q) r) + G (pmul p q) + G r + (G (pmul p q) + G p + G q)

The pmul-coboundary of a 1-cochain satisfies the raw Serre identity.

theorem GQ2.SectionEight.AffineTLift.theta_facts {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} (σ : DD.C0 →* Bg ⧸ D.T) (Dsc : Descent D) : (∀ (v : DD.Vmod), kfull σ Dsc (v, 1) (v, 1) + kappa0 DD.dat (v, 1) (v, 1) = 0) ∧ ∀ (v w : DD.Vmod), kfull σ Dsc (v, 1) (w, 1) + kappa0 DD.dat (v, 1) (w, 1) = kfull σ Dsc (w, 1) (v, 1) + kappa0 DD.dat (w, 1) (v, 1)

Θ := κfull + κ⁰ has zero diagonal and symmetric V×V-part.

Stage C, part 3: Θ' and the four-chase extraction (design §4)

noncomputable def GQ2.SectionEight.AffineTLift.theta {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} (σ : DD.C0 →* Bg ⧸ D.T) (Dsc : Descent D) (p q : DD.Vmod × DD.C0) : ZMod 2

Θ := κfull + κ⁰.

Equations

• GQ2.SectionEight.AffineTLift.theta σ Dsc p q = GQ2.SectionEight.AffineTLift.kfull σ Dsc p q + GQ2.kappa0 DD.dat p q

theorem GQ2.SectionEight.AffineTLift.theta_pone_left {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} (σ : DD.C0 →* Bg ⧸ D.T) (Dsc : Descent D) (q : DD.Vmod × DD.C0) : theta σ Dsc pone q = 0

theorem GQ2.SectionEight.AffineTLift.theta_pone_right {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} (σ : DD.C0 →* Bg ⧸ D.T) (Dsc : Descent D) (p : DD.Vmod × DD.C0) : theta σ Dsc p pone = 0

theorem GQ2.SectionEight.AffineTLift.gkappa_exists {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} (σ : DD.C0 →* Bg ⧸ D.T) (Dsc : Descent D) (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) : ∃ (g : DD.Vmod → ZMod 2), g 0 = 0 ∧ ∀ (v w : DD.Vmod), theta σ Dsc (v, 1) (w, 1) = g (v + w) + g v + g w

The splitting data for Θ|_{V×V} exists.

noncomputable def GQ2.SectionEight.AffineTLift.gkappa {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} (σ : DD.C0 →* Bg ⧸ D.T) (Dsc : Descent D) (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) : DD.Vmod → ZMod 2

The V×V-splitting cochain gκ.

Equations

• GQ2.SectionEight.AffineTLift.gkappa σ Dsc hσ = Classical.choose ⋯

theorem GQ2.SectionEight.AffineTLift.gkappa_zero {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} (σ : DD.C0 →* Bg ⧸ D.T) (Dsc : Descent D) (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) : gkappa σ Dsc hσ 0 = 0

noncomputable def GQ2.SectionEight.AffineTLift.theta' {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} (σ : DD.C0 →* Bg ⧸ D.T) (Dsc : Descent D) (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (p q : DD.Vmod × DD.C0) : ZMod 2

Θ' — Θ with the V×V-part killed by the gκ-coboundary.

Equations

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

theorem GQ2.SectionEight.AffineTLift.theta'_VV {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} (σ : DD.C0 →* Bg ⧸ D.T) (Dsc : Descent D) (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (v w : DD.Vmod) : theta' σ Dsc hσ (v, 1) (w, 1) = 0

The extraction data

noncomputable def GQ2.SectionEight.AffineTLift.ukap {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} (σ : DD.C0 →* Bg ⧸ D.T) (Dsc : Descent D) (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (v : DD.Vmod) (cc : DD.C0) : ZMod 2

uκ(v, cc) := Θ'((v,1),(0,cc)).

Equations

• GQ2.SectionEight.AffineTLift.ukap σ Dsc hσ v cc = GQ2.SectionEight.AffineTLift.theta' σ Dsc hσ (v, 1) (0, cc)

noncomputable def GQ2.SectionEight.AffineTLift.dkap {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} (σ : DD.C0 →* Bg ⧸ D.T) (Dsc : Descent D) (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (cc dd : DD.C0) : ZMod 2

δκ(cc, dd) := Θ'((0,cc),(0,dd)) — the scalar part of the descended class.

Equations

• GQ2.SectionEight.AffineTLift.dkap σ Dsc hσ cc dd = GQ2.SectionEight.AffineTLift.theta' σ Dsc hσ (0, cc) (0, dd)

noncomputable def GQ2.SectionEight.AffineTLift.gkraw {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} (σ : DD.C0 →* Bg ⧸ D.T) (Dsc : Descent D) (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (cc : DD.C0) (w : DD.Vmod) : ZMod 2

γκ-raw: Θ'((0,cc),(w,1)).

Equations

• GQ2.SectionEight.AffineTLift.gkraw σ Dsc hσ cc w = GQ2.SectionEight.AffineTLift.theta' σ Dsc hσ (0, cc) (w, 1)

noncomputable def GQ2.SectionEight.AffineTLift.gammakap {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} (σ : DD.C0 →* Bg ⧸ D.T) (Dsc : Descent D) (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (cc : DD.C0) (x : DD.Vmod) : ZMod 2

The edge γκ of the descended class (gammaEdge-calibrated).

Equations

• GQ2.SectionEight.AffineTLift.gammakap σ Dsc hσ cc x = GQ2.SectionEight.AffineTLift.gkraw σ Dsc hσ cc (cc⁻¹ • x) + GQ2.SectionEight.AffineTLift.ukap σ Dsc hσ x cc

theorem GQ2.SectionEight.AffineTLift.chaseE2 {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} (σ : DD.C0 →* Bg ⧸ D.T) (Dsc : Descent D) (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (v x : DD.Vmod) (ee : DD.C0) : theta' σ Dsc hσ (v, 1) (x, ee) = ukap σ Dsc hσ (v + x) ee + ukap σ Dsc hσ x ee

Chase E2: Θ' on a V-row.

theorem GQ2.SectionEight.AffineTLift.chaseE1 {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} (σ : DD.C0 →* Bg ⧸ D.T) (Dsc : Descent D) (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (v : DD.Vmod) (cc : DD.C0) (w : DD.Vmod) (dd : DD.C0) : theta' σ Dsc hσ (v, cc) (w, dd) = theta' σ Dsc hσ (0, cc) (w, dd) + theta' σ Dsc hσ (v, 1) (cc • w, cc * dd) + ukap σ Dsc hσ v cc

Chase E1: peel the V-coordinate off the first argument.

theorem GQ2.SectionEight.AffineTLift.chaseE3 {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} (σ : DD.C0 →* Bg ⧸ D.T) (Dsc : Descent D) (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (cc : DD.C0) (w : DD.Vmod) (dd : DD.C0) : theta' σ Dsc hσ (0, cc) (w, dd) = ukap σ Dsc hσ w dd + theta' σ Dsc hσ (cc • w, cc) (0, dd) + gkraw σ Dsc hσ cc w

Chase E3: peel the V-coordinate off the second argument.

theorem GQ2.SectionEight.AffineTLift.chaseE4 {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} (σ : DD.C0 →* Bg ⧸ D.T) (Dsc : Descent D) (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (cc dd : DD.C0) (y : DD.Vmod) : theta' σ Dsc hσ (y, cc) (0, dd) = dkap σ Dsc hσ cc dd + ukap σ Dsc hσ y (cc * dd) + ukap σ Dsc hσ y cc

Chase E4: reduce the mixed corner to δκ and uκ.

theorem GQ2.SectionEight.AffineTLift.theta'_decomp {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} (σ : DD.C0 →* Bg ⧸ D.T) (Dsc : Descent D) (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (v : DD.Vmod) (cc : DD.C0) (w : DD.Vmod) (dd : DD.C0) : theta' σ Dsc hσ (v, cc) (w, dd) = gkraw σ Dsc hσ cc w + ukap σ Dsc hσ (cc • w) cc + dkap σ Dsc hσ cc dd + (ukap σ Dsc hσ (v + cc • w) (cc * dd) + ukap σ Dsc hσ v cc + ukap σ Dsc hσ w dd)

The extraction (design §4): Θ' in Γγκ + inf δκ + ∂uκ normal form (raw values).

theorem GQ2.SectionEight.AffineTLift.chaseE5 {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} (σ : DD.C0 →* Bg ⧸ D.T) (Dsc : Descent D) (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (cc : DD.C0) (a b : DD.Vmod) : gkraw σ Dsc hσ cc (a + b) = gkraw σ Dsc hσ cc a + gkraw σ Dsc hσ cc b + ukap σ Dsc hσ (cc • (a + b)) cc + ukap σ Dsc hσ (cc • b) cc + ukap σ Dsc hσ (cc • a) cc

Chase E5: gkraw additivity up to uκ-corrections.

theorem GQ2.SectionEight.AffineTLift.gammakap_add {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} (σ : DD.C0 →* Bg ⧸ D.T) (Dsc : Descent D) (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (cc : DD.C0) (x y : DD.Vmod) : gammakap σ Dsc hσ cc (x + y) = gammakap σ Dsc hσ cc x + gammakap σ Dsc hσ cc y

γκ is additive.

theorem GQ2.SectionEight.AffineTLift.chaseE6 {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} (σ : DD.C0 →* Bg ⧸ D.T) (Dsc : Descent D) (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (cc dd : DD.C0) (w : DD.Vmod) : gkraw σ Dsc hσ (cc * dd) w = gkraw σ Dsc hσ dd w + gkraw σ Dsc hσ cc (dd • w) + ukap σ Dsc hσ (dd • w) dd + ukap σ Dsc hσ (cc • dd • w) (cc * dd) + ukap σ Dsc hσ (cc • dd • w) cc

Chase E6: the gkraw-composition law.

theorem GQ2.SectionEight.AffineTLift.gammakap_dual_crossed {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} (σ : DD.C0 →* Bg ⧸ D.T) (Dsc : Descent D) (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (cc dd : DD.C0) (x : DD.Vmod) : gammakap σ Dsc hσ (cc * dd) x = gammakap σ Dsc hσ cc x + gammakap σ Dsc hσ dd (cc⁻¹ • x)

The dual-crossed law for γκ (design §6): γκ(cc·dd)(x) = γκ(cc)(x) + γκ(dd)(cc⁻¹•x).