The graph tie-in, affineness and the keystone assembly

Split off from GQ2.KeystoneDelta (design §6). This file provides:

• the graph tie-in (graph_pmul, tDef_eq_JDefT) and the affineness haff (betaChi_affine): the cup part is additive, the g-part a coboundary killed by ι_Γ, the inflated scalar cancels four-fold;
• Stage D — the keystone assembly: the χ-edge γ''_χ (gamma2), the total edge γtot_χ, the polar-inverse shear family a_χ (achi) and its crossed-cocycle law, and the Ψ_χ-normal form (psi_decomp).

See GQ2.KeystoneDelta for the umbrella module docstring.

The graph tie-in and the affineness haff (the master count's threaded hypothesis)

theorem GQ2.SectionEight.AffineTLift.graph_pmul {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] {D : RadicalCoverData Bg} {DD : DescData D} {Γ : Type} [Group Γ] [TopologicalSpace Γ] {ρ : Γ →ₜ* Bg ⧸ D.M} (c : VCocycle DD ρ) (γ δ : Γ) : pmul (c.c γ, (rho0 DD ρ) γ) (c.c δ, (rho0 DD ρ) δ) = (c.c (γ * δ), (rho0 DD ρ) (γ * δ))

The graph of a crossed cocycle is pmul-multiplicative.

theorem GQ2.SectionEight.AffineTLift.tDef_eq_JDefT {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] {D : RadicalCoverData Bg} {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) {Γ : Type} [Group Γ] [TopologicalSpace Γ] {ρ : Γ →ₜ* Bg ⧸ D.M} (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (c : VCocycle DD ρ) (p : Γ × Γ) : tDef S hσ c p = JDefT S hσ (c.c p.1, (rho0 DD ρ) p.1) (c.c p.2, (rho0 DD ρ) p.2)

The T-defect of fLift is the J-defect at the graph.

noncomputable def GQ2.SectionEight.AffineTLift.cupChi {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] {D : RadicalCoverData Bg} (DD : DescData D) {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) {Γ : Type} [Group Γ] [TopologicalSpace Γ] (ρ : Γ →ₜ* Bg ⧸ D.M) (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (gχ : DD.Vmod → ZMod 2) (χ : ↥(TCharC D)) (c : VCocycle DD ρ) (p : Γ × Γ) : ZMod 2

The cup part of the χ-obstruction cochain: the c-additive component of the ω_χ-decomposition at the graph.

Equations

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

theorem GQ2.SectionEight.AffineTLift.chiDef_decomp {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] {D : RadicalCoverData Bg} {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) {Γ : Type} [Group Γ] [TopologicalSpace Γ] {ρ : Γ →ₜ* Bg ⧸ D.M} (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (χ : ↥(TCharC D)) (gχ : DD.Vmod → ZMod 2) (hg : ∀ (v w : DD.Vmod), ↑χ (mDef DD S v w) = gχ (v + w) + gχ v + gχ w) (c : VCocycle DD ρ) (p : Γ × Γ) : chiDef S hσ χ c p = cupChi DD S ρ hσ gχ χ c p + (gχ (c.c (p.1 * p.2)) + gχ (c.c p.1) + gχ (c.c p.2)) + ↑χ (uDef DD S ((rho0 DD ρ) p.1) ((rho0 DD ρ) p.2))

The chiDef-decomposition at a splitting of f_χ: cup part + g-coboundary part + inflated scalar.

theorem GQ2.SectionEight.AffineTLift.cupChi_add {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] {D : RadicalCoverData Bg} {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) {Γ : Type} [Group Γ] [TopologicalSpace Γ] {ρ : Γ →ₜ* Bg ⧸ D.M} (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (χ : ↥(TCharC D)) (gχ : DD.Vmod → ZMod 2) (hg : ∀ (v w : DD.Vmod), ↑χ (mDef DD S v w) = gχ (v + w) + gχ v + gχ w) (c c' : VCocycle DD ρ) (p : Γ × Γ) : cupChi DD S ρ hσ gχ χ (c + c') p = cupChi DD S ρ hσ gχ χ c p + cupChi DD S ρ hσ gχ χ c' p

The cup part is additive in the cocycle.

theorem GQ2.SectionEight.AffineTLift.cupChi_zero {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] {D : RadicalCoverData Bg} {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) {Γ : Type} [Group Γ] [TopologicalSpace Γ] {ρ : Γ →ₜ* Bg ⧸ D.M} (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (χ : ↥(TCharC D)) (gχ : DD.Vmod → ZMod 2) (hg0 : gχ 0 = 0) (p : Γ × Γ) : cupChi DD S ρ hσ gχ χ 0 p = 0

The cup part vanishes at the zero cocycle.

theorem GQ2.SectionEight.AffineTLift.gPart_mem_B2 {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] {D : RadicalCoverData Bg} {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} {Γ : Type} [Group Γ] [TopologicalSpace Γ] {ρ : Γ →ₜ* Bg ⧸ D.M} [DistribMulAction Γ (ZMod 2)] (_hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m) (gχ : DD.Vmod → ZMod 2) (cx : VCocycle DD ρ) : (fun (p : Γ × Γ) => gχ (cx.c (p.1 * p.2)) + gχ (cx.c p.1) + gχ (cx.c p.2)) ∈ ContCoh.B2 Γ (ZMod 2)

The g-coboundary part of the chiDef-decomposition is a continuous coboundary.

theorem GQ2.SectionEight.AffineTLift.betaChi_affine {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] {D : RadicalCoverData Bg} {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) {Γ : Type} [Group Γ] [TopologicalSpace Γ] {ρ : Γ →ₜ* Bg ⧸ D.M} (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) [IsTopologicalGroup Γ] [DistribMulAction Γ (ZMod 2)] (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m) (hH2 : Nat.card (ContCoh.H2 Γ (ZMod 2)) = 2) (χ : ↥(TCharC D)) (c c' : VCocycle DD ρ) : betaChi S hσ χ (c + c') = betaChi S hσ χ c + betaChi S hσ χ c' + betaChi S hσ χ 0

The affineness haff (the master count's threaded hypothesis, design §6): β_χ is affine in the cocycle — the cup part is additive, the g-part is a coboundary killed by ι_Γ, and the inflated scalar cancels four-fold.

Stage D: the keystone assembly (design §6)

theorem GQ2.SectionEight.AffineTLift.gchi_exists {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (χ : ↥(TCharC D)) : ∃ (g : DD.Vmod → ZMod 2), g 0 = 0 ∧ ∀ (v w : DD.Vmod), ↑χ (mDef DD S v w) = g (v + w) + g v + g w

The splitting data for f_χ = χ ∘ mDef exists.

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

A fixed splitting g_χ of f_χ.

Equations

• GQ2.SectionEight.AffineTLift.gchi S hσ χ = Classical.choose ⋯

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

The χ-edge γ''_χ of the zero-form normal form.

Equations

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

theorem GQ2.SectionEight.AffineTLift.gamma2_add {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (χ : ↥(TCharC D)) (cc : DD.C0) (x y : DD.Vmod) : gamma2 S hσ χ cc (x + y) = gamma2 S hσ χ cc x + gamma2 S hσ χ cc y

γ''_χ(cc) is additive.

theorem GQ2.SectionEight.AffineTLift.gamma2_dual_crossed {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (χ : ↥(TCharC D)) (cc dd : DD.C0) (x : DD.Vmod) : gamma2 S hσ χ (cc * dd) x = gamma2 S hσ χ cc x + gamma2 S hσ χ dd (cc⁻¹ • x)

The dual-crossed law for γ''_χ.

The total edge and the polar-inverse shear

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

The total edge γtot_χ := γ''_χ + γκ.

Equations

• GQ2.SectionEight.AffineTLift.gammatot S Dsc hσ χ cc x = GQ2.SectionEight.AffineTLift.gamma2 S hσ χ cc x + GQ2.SectionEight.AffineTLift.gammakap σ Dsc hσ cc x

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

theorem GQ2.SectionEight.AffineTLift.exists_polar_inverse' {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} {q : DD.Vmod → ZMod 2} (hq : QuadraticFp2.IsQuadraticFp2 q) (hns : QuadraticFp2.Nonsingular q) (φ : DD.Vmod → ZMod 2) (hφ : ∀ (x y : DD.Vmod), φ (x + y) = φ x + φ y) : ∃ (a : DD.Vmod), ∀ (v : DD.Vmod), QuadraticFp2.polar q a v = φ v

Polar-inverse for additive functionals (module-free wrapper).

theorem GQ2.SectionEight.AffineTLift.polar_inj {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} {q : DD.Vmod → ZMod 2} (hq : QuadraticFp2.IsQuadraticFp2 q) (hns : QuadraticFp2.Nonsingular q) {a b : DD.Vmod} (h : ∀ (v : DD.Vmod), QuadraticFp2.polar q a v = QuadraticFp2.polar q b v) : a = b

Polar injectivity: nonsingular forms separate points through the polar pairing.

The shear family a_χ and the total scalar phase

theorem GQ2.SectionEight.AffineTLift.polar_smul_inv {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} {q : DD.Vmod → ZMod 2} (hinvQ : QuadraticFp2.IsInvariant DD.C0 q) (cc : DD.C0) (u v : DD.Vmod) : QuadraticFp2.polar q (cc • u) v = QuadraticFp2.polar q u (cc⁻¹ • v)

Polar equivariance for an invariant form: B(cc•u, v) = B(u, cc⁻¹•v).

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

The shear family a_χ(cc) := B♭⁻¹(γtot_χ(cc)).

Equations

• GQ2.SectionEight.AffineTLift.achi S Dsc hσ χ cc = Classical.choose ⋯

theorem GQ2.SectionEight.AffineTLift.achi_crossed {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) (Dsc : Descent D) (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (hinvQ : QuadraticFp2.IsInvariant DD.C0 DD.qbar) (χ : ↥(TCharC D)) (cc dd : DD.C0) : achi S Dsc hσ χ (cc * dd) = achi S Dsc hσ χ cc + cc • achi S Dsc hσ χ dd

a_χ is a crossed 1-cocycle (the ha of prop_8_8_target).

theorem GQ2.SectionEight.AffineTLift.achi_kill {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) (Dsc : Descent D) (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (χ : ↥(TCharC D)) (cc : DD.C0) (v : DD.Vmod) : QuadraticFp2.polar DD.qbar (achi S Dsc hσ χ cc) v + (AddMonoidHom.mk' (gammatot S Dsc hσ χ cc) ⋯) v = 0

The kill condition (hkill of prop_8_8_target).

The Ψ_χ-normal form

theorem GQ2.SectionEight.AffineTLift.kappa0_datChi_decomp {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (χ : ↥(TCharC D)) (p q : DD.Vmod × DD.C0) : kappa0 (datChi DD S hσ χ) p q = gamma2 S hσ χ p.2 (p.2 • q.1) + (gchi S hσ χ (pmul p q).1 + gchi S hσ χ p.1 + gchi S hσ χ q.1)

The zero-form kappa0 in γ'' + ∂g-normal form (pair level).

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

The total scalar phase input δtot_χ := e_χ + δκ.

Equations

• GQ2.SectionEight.AffineTLift.deltatot S Dsc hσ χ cc dd = ↑χ (GQ2.SectionEight.AffineTLift.uDef DD S cc dd) + GQ2.SectionEight.AffineTLift.dkap σ Dsc hσ cc dd

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

The combined coboundary potential W_χ.

Equations

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

theorem GQ2.SectionEight.AffineTLift.psi_decomp {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) (Dsc : Descent D) (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (χ : ↥(TCharC D)) (p q : DD.Vmod × DD.C0) : ↑χ (JDefT S hσ p q) + kfull σ Dsc p q = kappa0 DD.dat p q + gammatot S Dsc hσ χ p.2 (p.2 • q.1) + deltatot S Dsc hσ χ p.2 q.2 + (wtot S Dsc hσ χ (pmul p q) + wtot S Dsc hσ χ p + wtot S Dsc hσ χ q)

The Ψ_χ-normal form (design §6): the full obstruction cochain is κ⁰ + Γγtot + inf δtot + ∂W_χ, pointwise.