Q⁰ over Γ_A as a relator value in the κ⁰-extension #
The evaluation brick of the (83)-for-Γ_A seam (docs/orchestration/p16d6e4aA-gammaA-gauss-design.md §2):
the graph pullback is, on the nose, the pullback of the base central cocycle κ⁰_q on the
semidirect product V ⋊ C (eq. (61)/(62): graphPullback dat ρ₀ b = κ⁰ ∘ (graph × graph),
where graph γ = (b γ, ρ₀ γ) is a homomorphism exactly because b is a crossed cocycle).
Hence, by A-2 (QZero_eq_levelFactor_obs) and the level-change naturality
(relZPair_comap), the base determinant form evaluates as a relator value in the concrete
finite extension CentExt κ⁰:
Q⁰_{Γ_A,ρ'}(c) = relZPair (graph-marking) κ⁰-cocycle |₁ + |₂
where the graph marking is the image of the Γ_A-generator marking gammaGen under the
graph homomorphism — the four explicit pairs (c(gᵢ), ρ'₀(gᵢ)) ∈ V ⋊ C. This is the A-4
interface: the two relator words evaluated at those pairs in CentExt κ⁰ ARE the paper's
(83) quadratic in the generator values.
Contents: the semidirect group Sd C V (isolated carrier, no Prod-instance pollution);
kappa0Cocycle (κ⁰ as a normalized WordCoh2.TwoCocycle — Lemma 6.1's associativity from
the IsEquivariantFactorSet clauses); graphSdHom (the crossed-cocycle graph hom) and its
continuity; the explicit LevelFactor for the graph pullback (kernel level of the graph
hom); and the assembled QZero_eq_relZPair_kappa0.
All std-3; no axioms, no sorries.
The semidirect product V ⋊ C as an isolated group carrier #
The carrier of V ⋊ C — a def (not an abbrev), so the group structure below does
not leak onto raw products.
Equations
- GQ2.SectionEight.AffineTLift.Sd C V = (V × C)
Instances For
Equations
- One or more equations did not get rendered due to their size.
κ⁰_q as a normalized TwoCocycle on V ⋊ C (Lemma 6.1's associativity) #
m_c(0) = 0 (from m_quad at v = w = 0 in characteristic 2).
The base central cocycle κ⁰_q as a normalized TwoCocycle on V ⋊ C (eq. (61);
the cocycle identity is Lemma 6.1's "associativity of E_f", assembled from f_cocycle,
m_quad, and m_mul).
Equations
- GQ2.SectionEight.AffineTLift.kappa0Cocycle dat hdat = { κ := fun (p r : GQ2.SectionEight.AffineTLift.Sd C V) => GQ2.kappa0 dat (p.v, p.cc) (r.v, r.cc), norm := ⋯, cocyc := ⋯ }
Instances For
The graph homomorphism of a crossed cocycle #
The graph homomorphism γ ↦ (c(γ), ρ'₀(γ)) : Γ →* V ⋊ C — the crossed-cocycle
condition is exactly the homomorphism law.
Equations
- GQ2.SectionEight.AffineTLift.graphSdHom c = { toFun := fun (γ : Γ) => (c.c γ, (GQ2.SectionEight.AffineTLift.rho0 DD ρM) γ), map_one' := ⋯, map_mul' := ⋯ }
Instances For
The graph pullback is the κ⁰-pullback along the graph hom (eq. (62), on the
nose).
The explicit level factorization over Γ_A and the assembled relator value #
A crossed cocycle's underlying function is continuous into the (discrete) module: its
composition with the injective iV ∘ ofAdd is continuous into the discrete Bg ⧸ T, so
every fiber is open.
The A-3 keystone: over Γ_A, the base determinant form Q⁰ of a crossed V-cocycle
is the relator value in the concrete κ⁰-extension: the (tame + wild) relator-z pair of
the κ⁰-cocycle on V ⋊ C at the marking graph(gammaGen) — the four explicit pairs
(c(gᵢ), ρ'₀(gᵢ)). (A-2's QZero_eq_levelFactor_obs at the kernel level of the graph hom,
transported by relZPair_comap.)
Paper-tag ledger (auto-generated by paperforge; do not edit) #
- eq. (61) = ⟦eq-basekappacochain⟧
- eq. (62) = ⟦eq-baseconnectingcochain⟧
- Lemma 6.1 = ⟦lem-extraspecialconnecting⟧