The generic Z¹ → H¹ reduction of the source-Gauss sum

The phase140_from_residues residue hGaussZ is ∑ᶠ c : VCocycle DD ρ', sign (QZero DD ρ' c) = #V · G0. This file reduces it — generically in Γ, source-free — to a Gauss sum over the #V-sized quotient Z¹ ⧸ B¹, whose value is the (83)-evaluation G0 (the Prop. 8.9 assembly). Design record: docs/orchestration/p16d6e4-gauss-design.md §2.

Contents:

• iotaB_add_mem_B2 — ι_Γ absorbs a B²-shift (no #H² = 2 needed);
• graphPullback_shift_mem_B2 — the base determinant graph pullback is unchanged mod B² under a vCob-shift (the generic-Γ form of RepIndependence.graphPullback_sub_mem_B2, reusing its innerConj conjugation identity and KeystoneDelta.graphCob_mem_B2 continuity);
• QZero_add_vCob — hence Q⁰ is B¹-invariant;
• vCobHom/vCobRange, hfix_of_simple (the V^{C₀} = 0 freeness), QZeroBar;
• gaussZ_reduction — ∑ᶠ c, sign(Q⁰ c) = #V · ∑ᶠ x : Z¹⧸B¹, sign(Q̄⁰ x), and card_quotient_vCobRange — #(Z¹⧸B¹) = #V.

Generic factor-set conjugation algebra (clean-context copies)

RepIndependence's kappa0_cocycle/etaS/innerConj are stated in an AbsGalQ2-bound section (their C/W carry [TopologicalSpace] and an AbsGalQ2-action), so they do not apply to DD.C0/DD.Vmod. These are the same identities in a clean generic context.

theorem GQ2.SectionEight.AffineTLift.kappa0_cocycle {C : Type u_1} [Group C] {W : Type u_2} [AddCommGroup W] [DistribMulAction C W] {q : W → ZMod 2} {dat : FactorSet C W} (hdat : IsEquivariantFactorSet q dat) (a b c : SectionSix.SemiProd C W) : kappa0 dat a b + kappa0 dat (a * b) c = kappa0 dat a (b * c) + kappa0 dat b c

κ⁰ is a 2-cocycle on V ⋊ C (display (61)/Lemma 6.1, from the factor-set axioms).

def GQ2.SectionEight.AffineTLift.etaS {C : Type u_1} [Group C] {W : Type u_2} [AddCommGroup W] [DistribMulAction C W] (dat : FactorSet C W) (s x : SectionSix.SemiProd C W) : ZMod 2

The inner-conjugation 1-cochain η_s(x) = κ⁰(s, x) + κ⁰(sxs⁻¹, s) on V ⋊ C.

Equations

• GQ2.SectionEight.AffineTLift.etaS dat s x = GQ2.kappa0 dat s x + GQ2.kappa0 dat (s * x * s⁻¹) s

theorem GQ2.SectionEight.AffineTLift.innerConj {C : Type u_1} [Group C] {W : Type u_2} [AddCommGroup W] [DistribMulAction C W] {q : W → ZMod 2} {dat : FactorSet C W} (hdat : IsEquivariantFactorSet q dat) (s x y : SectionSix.SemiProd C W) : etaS dat s y + etaS dat s (x * y) + etaS dat s x = kappa0 dat (s * x * s⁻¹) (s * y * s⁻¹) + kappa0 dat x y

Inner automorphisms act trivially on H²: c_s^*κ⁰ − κ⁰ = δ¹(η_s) pointwise.

theorem GQ2.SectionEight.AffineTLift.iotaB_add_mem_B2 {Γ : Type} [Group Γ] [TopologicalSpace Γ] [DistribMulAction Γ (ZMod 2)] {φ β : Γ × Γ → ZMod 2} (hβ : β ∈ ContCoh.B2 Γ (ZMod 2)) : iotaB (φ + β) = iotaB φ

ι_Γ is invariant under adding a continuous coboundary (B² is its zero fibre).

theorem GQ2.SectionEight.AffineTLift.graphPullback_shift_mem_B2 {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] {D : RadicalCoverData Bg} {DD : DescData D} {Γ : Type} [Group Γ] [TopologicalSpace Γ] {ρ : Γ →ₜ* Bg ⧸ D.M} [DistribMulAction Γ (ZMod 2)] (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m) (c : VCocycle DD ρ) (v : DD.Vmod) : graphPullback DD.dat (fun (γ : Γ) => (rho0 DD ρ) γ) (c + vCob DD ρ v).c - graphPullback DD.dat (fun (γ : Γ) => (rho0 DD ρ) γ) c.c ∈ ContCoh.B2 Γ (ZMod 2)

The base determinant graph pullback is B¹-shift-invariant mod B² (generic-Γ form of RepIndependence.graphPullback_sub_mem_B2): shifting the cocycle c by the principal coboundary vCob v changes (c, ρ')^* κ⁰ by the (−v, 1)-conjugation phase, a continuous 2-coboundary. Reuses the generic innerConj identity and graphCob_mem_B2's continuity.

theorem GQ2.SectionEight.AffineTLift.QZero_add_vCob {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] {D : RadicalCoverData Bg} {DD : DescData D} {Γ : Type} [Group Γ] [TopologicalSpace Γ] {ρ : Γ →ₜ* Bg ⧸ D.M} [DistribMulAction Γ (ZMod 2)] (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m) (c : VCocycle DD ρ) (v : DD.Vmod) : QZero DD ρ (c + vCob DD ρ v) = QZero DD ρ c

Q⁰ is B¹-invariant: the base determinant form is unchanged by a vCob-shift.

The B¹ ≅ V translation group and the freeness criterion

noncomputable def GQ2.SectionEight.AffineTLift.vCobHom {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] {D : RadicalCoverData Bg} (DD : DescData D) {Γ : Type} [Group Γ] [TopologicalSpace Γ] (ρ : Γ →ₜ* Bg ⧸ D.M) : DD.Vmod →+ VCocycle DD ρ

The principal-coboundary hom V →+ Z¹_{Γ,ρ}(V) (its image is B¹).

Equations

• GQ2.SectionEight.AffineTLift.vCobHom DD ρ = AddMonoidHom.mk' (GQ2.SectionEight.AffineTLift.vCob DD ρ) ⋯

@[simp]

theorem GQ2.SectionEight.AffineTLift.vCobHom_apply {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] {D : RadicalCoverData Bg} {DD : DescData D} {Γ : Type} [Group Γ] [TopologicalSpace Γ] {ρ : Γ →ₜ* Bg ⧸ D.M} (v : DD.Vmod) : (vCobHom DD ρ) v = vCob DD ρ v

noncomputable def GQ2.SectionEight.AffineTLift.vCobRange {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] {D : RadicalCoverData Bg} (DD : DescData D) {Γ : Type} [Group Γ] [TopologicalSpace Γ] (ρ : Γ →ₜ* Bg ⧸ D.M) : AddSubgroup (VCocycle DD ρ)

B¹_{Γ,ρ}(V) ≤ Z¹_{Γ,ρ}(V) as the range of the coboundary hom.

Equations

• GQ2.SectionEight.AffineTLift.vCobRange DD ρ = (GQ2.SectionEight.AffineTLift.vCobHom DD ρ).range

theorem GQ2.SectionEight.AffineTLift.hfix_of_simple {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] {D : RadicalCoverData Bg} {DD : DescData D} {Γ : Type} [Group Γ] [TopologicalSpace Γ] {ρ : Γ →ₜ* Bg ⧸ D.M} [Nontrivial DD.C0] (hsurj : Function.Surjective fun (γ : Γ) => (rho0 DD ρ) γ) (hsimple : ∀ (W : AddSubgroup DD.Vmod), (∀ (g : DD.C0), ∀ w ∈ W, g • w ∈ W) → W = ⊥ ∨ W = ⊤) (hfaith : ∀ (g : DD.C0), (∀ (v : DD.Vmod), g • v = v) → g = 1) (v : DD.Vmod) (hv : ∀ (γ : Γ), (rho0 DD ρ) γ • v = v) : v = 0

The V^{C₀} = 0 freeness (design §2 item 4): for a faithful simple C₀-module V with C₀ nontrivial and ρ' surjective, the only ρ'-fixed vector is 0. Discharges the hfix hypothesis of vCob_injective from the block's chief-factor data.

The descended Gauss form and the reduction

theorem GQ2.SectionEight.AffineTLift.vCobHom_injective {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] {D : RadicalCoverData Bg} {DD : DescData D} {Γ : Type} [Group Γ] [TopologicalSpace Γ] {ρ : Γ →ₜ* Bg ⧸ D.M} (hfix : ∀ (v : DD.Vmod), (∀ (γ : Γ), (rho0 DD ρ) γ • v = v) → v = 0) : Function.Injective ⇑(vCobHom DD ρ)

vCob is injective when V carries no nonzero ρ'-fixed vector, hence the coboundary hom is injective (|B¹| = #V).

noncomputable def GQ2.SectionEight.AffineTLift.QZeroBar {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] {D : RadicalCoverData Bg} (DD : DescData D) {Γ : Type} [Group Γ] [TopologicalSpace Γ] (ρ : Γ →ₜ* Bg ⧸ D.M) [DistribMulAction Γ (ZMod 2)] (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m) (x : VCocycle DD ρ ⧸ vCobRange DD ρ) : ZMod 2

The descended base determinant form Q̄⁰ on the #V-sized quotient Z¹ ⧸ B¹ (design §2 item 5): Q⁰ descends because it is B¹-invariant (QZero_add_vCob). Its Gauss sum is the (83)-value G0 (the Prop. 8.9 assembly).

Equations

• GQ2.SectionEight.AffineTLift.QZeroBar DD ρ htriv x = Quotient.liftOn' x (GQ2.SectionEight.AffineTLift.QZero DD ρ) ⋯

@[simp]

theorem GQ2.SectionEight.AffineTLift.QZeroBar_mk {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] {D : RadicalCoverData Bg} {DD : DescData D} {Γ : Type} [Group Γ] [TopologicalSpace Γ] {ρ : Γ →ₜ* Bg ⧸ D.M} [DistribMulAction Γ (ZMod 2)] (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m) (c : VCocycle DD ρ) : QZeroBar DD ρ htriv ↑c = QZero DD ρ c

theorem GQ2.SectionEight.AffineTLift.gaussZ_reduction {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] {D : RadicalCoverData Bg} {DD : DescData D} {Γ : Type} [Group Γ] [TopologicalSpace Γ] {ρ : Γ →ₜ* Bg ⧸ D.M} [DistribMulAction Γ (ZMod 2)] [Finite (VCocycle DD ρ)] (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m) (hfix : ∀ (v : DD.Vmod), (∀ (γ : Γ), (rho0 DD ρ) γ • v = v) → v = 0) : ∑ᶠ (c : VCocycle DD ρ), sign (QZero DD ρ c) = ↑(Nat.card DD.Vmod) * ∑ᶠ (x : VCocycle DD ρ ⧸ vCobRange DD ρ), sign (QZeroBar DD ρ htriv x)

The generic Z¹ → H¹ reduction (design §2 item 5): the source-Gauss sum over all of Z¹_{Γ,ρ}(V) is #V times the Gauss sum of the descended form Q̄⁰ on Z¹ ⧸ B¹. The free B¹-translation (vCob injective) makes every fibre of Z¹ ↠ Z¹⧸B¹ a #V-sized coset on which Q⁰ is constant. Finiteness of Z¹ is a hypothesis — supply finite_vcocycle (a splitting + t.f.g.) or, σ-free, a nonzero Nat.card-count such as hZcard_local (the Prop. 8.9 assembly composition).

theorem GQ2.SectionEight.AffineTLift.card_quotient_vCobRange {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] {D : RadicalCoverData Bg} {DD : DescData D} {Γ : Type} [Group Γ] [TopologicalSpace Γ] {ρ : Γ →ₜ* Bg ⧸ D.M} (hfix : ∀ (v : DD.Vmod), (∀ (γ : Γ), (rho0 DD ρ) γ • v = v) → v = 0) (hZcard : Nat.card (VCocycle DD ρ) = Nat.card DD.Vmod * Nat.card DD.Vmod) : Nat.card (VCocycle DD ρ ⧸ vCobRange DD ρ) = Nat.card DD.Vmod

The H¹-model is #V-sized (design §2 item 6): #(Z¹ ⧸ B¹) = #V, from #B¹ = #V (free translation) and #Z¹ = #V² (hZcard, the source's 5.15/5.16 numerics). Lets the Prop. 8.9 assembly exhibit the descended form as a form on a #V-space.

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

• Lemma 6.1 = ⟦lem-extraspecialconnecting⟧