The keystone and the phase-cover data #
Split off from GQ2.KeystoneDelta (design §6). This file provides:
- Stage E — the shear cocycle
shChi, the total scalar phaseDeltaChi, the generic-Γ graph-pullback/coboundary memberships, and the keystone (keystone): the (135)-Γ completed square, whose only Γ-residues arehtrivandhH2; - Stage F — the phase-cover data for
centralCoverOfCocycle: the Serre identityDeltaChi_cocycleand the normalizationsDeltaChi_one_left/DeltaChi_one_right.
See GQ2.KeystoneDelta for the umbrella module docstring.
Stage E: the keystone (design §6 — the (135)-Γ completed square) #
Pulling the Ψ_χ-normal form back along the graph of c and completing the square with
prop_8_8_target at the shear family a_χ yields the master count's hkey:
β_χ(c) + β_ξ(c) = Q⁰(c + sh_χ) + ι_Γ(ρ'^* Δ_χ)
at Δ_χ := DeltaScalar (γtot_χ, δtot_χ, a_χ) and sh_χ := a_χ ∘ ρ'. The only Γ-residues
are htriv and hH2; everything else is the C-level data proved above.
The shear cocycle sh_χ := a_χ ∘ ρ': the (133) shift-vector family as a crossed
V-cocycle (continuity through the discrete Bg ⧸ M).
Equations
- GQ2.SectionEight.AffineTLift.shChi S Dsc hσ hinvQ χ = { c := fun (γ : Γ) => GQ2.SectionEight.AffineTLift.achi S Dsc hσ χ ((GQ2.SectionEight.AffineTLift.rho0 DD ρ) γ), cont := ⋯, crossed := ⋯ }
Instances For
The total scalar phase family Δ_χ (the (134) total phase Δ_{χ,κ}, C-level).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Generic-Γ well-formedness of the graph pullback (Lemma 6.1/(62); the G_ℚ₂-bound
ancestor is SectionSix.graphPullback_mem_Z2): along a crossed cocycle, the pullback of the
equivariant base datum is a continuous 2-cocycle.
The graph-coboundary of any pair potential along a crossed cocycle is a continuous
coboundary (the ∂-terms of the Ψ_χ-pullback).
The keystone (Prop 8.8's completed square (135) at Γ-level, design §6): the master
count's hkey at Δ := DeltaChi and sh := shChi. Only htriv and hH2 are Γ-residues.
Stage F: the phase-cover data (design §6, c2) #
centralCoverOfCocycle consumes a normalized raw 2-cocycle on C₀. Here we supply the
three inputs for Δ_χ: the Serre identity (DeltaChi_cocycle — the completed square on the
(0,·)-section minus the bundle/base/coboundary Serre identities) and the two normalizations
(DeltaChi_one_left/right — from the proved normalization atoms). All C-level.
uσ-defect normalization, left.
uσ-defect normalization, right.
γtot_χ(cc) kills 0.
γtot_χ(1) = 0 (the edge is normalized at the identity).
The shear family is normalized: a_χ(1) = 0.
δtot_χ is normalized on the left.
δtot_χ is normalized on the right.
Serre identity for χ ∘ JDefT: the associativity defect of the product lift Jmap
conjugates by Jmap p, and the C-invariance of χ kills the conjugation.
Serre identity for the Ψ_χ-bundle κ⁰ + Γγtot + inf δtot, by the psi_decomp
normal form and the three component Serre identities.
The phase-cover cocycle law (hcoc of centralCoverOfCocycle): Δ_χ satisfies the
raw Serre identity on C₀ — the completed square on the (0,·)-section, minus the
bundle/base/coboundary Serre identities.
Left normalization (hl of centralCoverOfCocycle): Δ_χ(1, ·) = 0.
Right normalization (hr of centralCoverOfCocycle): Δ_χ(·, 1) = 0.