The Shapiro H¹ coordinate read (hcoh, the f2c keystone) #
The remaining cohomological input of the lemma_6_17_vanish orbit route (the Lemma 6.17 vanishing proof, handoff
docs/orchestration/p15f2-handoff.md §5): each block coordinate of a Z¹(G_ℚ₂, 𝔽₂[G/N]^K)-representative is
cohomologous to the Shapiro cochain of its scalar coordinate, so the banked
SectionSix.lemma_6_15_{square,free,involution} (stated at shapiroFun, acting map mk' N)
fire on the per-orbit graph pullbacks of OrbitDecomp's block datums.
The read (Shapiro's lemma for H¹(G, 𝔽₂[G/N]), explicit-witness form). For a 1-cocycle
β : G → 𝔽₂[G/N] w.r.t. the mk'-pulled-back left-regular action:
- the scalar coordinate
α := shapiroCoord β : n ↦ β(n)(1̄)is a 1-cocycle onN(trivial coefficients) — evaluation at the base coset; - the primitive
w := shapiroPrim β : u ↦ β(ũ)(u)(~=Quotient.out, the same canonical transversal asGQ2/Corestriction.lean) satisfies the pointwise identitySh(α)(g) = β(g) + (mk'(g)•w − w)(shapiroFun_shapiroCoord_eq).
Proof: evaluate the cocycle rule on both factorizations of g·(g⁻¹•u)~ = ũ·ℓ_u(g) at the coset
u; the ℓ-term is the Shapiro cochain, the two transversal terms are the primitive. No
choices beyond the canonical transversal, no sign bookkeeping (𝔽₂).
Per-orbit hcoh (§PerOrbit, at G := G_ℚ₂): the coboundary shift is transported through the
graph pullback by the banked RepIndependence.graphPullback_sub_mem_B2, the block datum is
converted to the literal orbit datum by graphPullback_comap (both are definitional
FactorSet.comaps along blockProj/blockProj₂), and Lemma 6.15 closes:
hcoh_square— eq. (103) at the block-jcoordinate;hcoh_free— eq. (104) at the block pair(j, k)with shiftmk' ĝ;hcoh_involution— eq. (105) at blockjwith involution liftĝ.
The deep coordinate (§DeepCoordinate): the scalar coordinate at block j is the scalar
restriction phiRes ρ x (evalW j) on the nose (phiRes_evalW, a rfl), so x ∈ deepPart ρ
hands each block coordinate a deep Kummer class (shapiroCoord_mem_deepClasses) — the f2d feed
for hvanish (ShapiroDeepness.hvanish_cup / lemma_6_16).
Paper: §6.2–§6.3, proof of Lemma 6.15 / eq. (102)–(105). Axioms: ∅ (std-3).
Preliminaries #
graphPullback functoriality along an equivariant comap: pulling the comapped datum back
along (ρ', b) is pulling the datum back along (ρ', i ∘ b). Turns the block datums of
OrbitDecomp (definitional comaps) into the literal orbit datums of Lemma 6.15.
The scalar read and its primitive #
The scalar Shapiro coordinate of a 𝔽₂[G/N]-valued 1-cochain: evaluate at the base
coset and restrict to N (the forward half of Shapiro's H¹(G, 𝔽₂[G/N]) ≅ H¹(N, 𝔽₂)).
Equations
- GQ2.ShapiroRead.shapiroCoord N β n = β (↑n) 1
Instances For
The Shapiro primitive: the explicit 0-cochain trivializing β − Sh(shapiroCoord β):
w(u) = β(ũ)(u) with ~ the canonical transversal (Quotient.out).
Equations
- GQ2.ShapiroRead.shapiroPrim N β u = β (Quotient.out u) u
Instances For
The scalar coordinate is multiplicative on N (the base coset is N-fixed).
The Shapiro read (pointwise): the Shapiro cochain of the scalar coordinate differs from
the cocycle by the explicit shapiroPrim coboundary. Evaluate the cocycle rule on the two
factorizations of g · (g⁻¹•u)~ = ũ · ℓ_u(g) at the coset u.
The Shapiro read, coboundary form: Sh(shapiroCoord β)(g) = β(g) + (mk'(g)•w − w) with
w = shapiroPrim β — the exact shift shape of RepIndependence.graphPullback_sub_mem_B2.
The Z¹-package of the scalar coordinate #
The scalar coordinate of a continuous mk'-cocycle is a continuous 1-cocycle on N
(trivial coefficients).
Per-orbit hcoh at G_ℚ₂ #
The block-level shift: b is replaced by b + δ⁰W₀ for the block-supported primitive W₀
(a B²-move on the graph pullback, graphPullback_sub_mem_B2), whose block coordinate is the
Shapiro cochain (shapiroFun_shapiroCoord_eq); then graphPullback_comap exposes the literal
orbit datum and Lemma 6.15 evaluates it as a corestriction.
Instance context: RegRep N is a type synonym with no registered topology, so the topological
instances (and the G_ℚ₂-action, the mk'-pullback of the left-regular action) enter as
instance arguments with the compatibility hypothesis hmk — the f2d assembly supplies them as
letIs (DistribMulAction.compHom along mk' N), for which hmk is rfl.
The block coordinate of a Z¹-representative is an mk'-cocycle (raw form).
The base-coset evaluation of a block coordinate is continuous (W is discrete).
the Lemma 6.17 vanishing proof, square-orbit hcoh (Lemma 6.15 eq. (103) at a block coordinate): the graph
pullback of the square block datum at any Z¹-representative is, in H², the corestriction of
the cup square of the block's scalar Shapiro coordinate.
the Lemma 6.17 vanishing proof, free-orbit hcoh (Lemma 6.15 eq. (104) at a block pair): the graph pullback
of the free block datum with shift mk' ĝ at any Z¹-representative is, in H², the
corestriction of α_j ⌣ ĝα_k (conjugated second coordinate).
the Lemma 6.17 vanishing proof, involution-orbit hcoh (Lemma 6.15 eq. (105) at a block coordinate): the
graph pullback of the involution block datum at any Z¹-representative is, in H², the
U₀-corestriction of the Evens norm of the block's scalar Shapiro coordinate.
The deep coordinate: shapiroCoord = phiRes at the block functional #
The block-coordinate evaluation functional F ↦ F j (1̄).
Equations
- GQ2.ShapiroRead.evalW N j = { toFun := fun (F : Fin K → GQ2.RegRep N) => F j 1, map_zero' := ⋯, map_add' := ⋯ }
Instances For
The deep-coordinate identification: the scalar restriction of a class at the block
functional evalW j is the H1ofFun of the Shapiro coordinate of its canonical
representative's block — on the nose.
The block coordinates of a deep class are deep (the f2d hvanish feed): for
x ∈ deepPart ρ on the block module, every block's scalar Shapiro coordinate has a deep
Kummer class.
Paper-tag ledger (auto-generated by paperforge; do not edit) #
- eq. (102) = ⟦eq-regularnaturality⟧
- eq. (103) = ⟦eq-shapirosquare⟧
- eq. (104) = ⟦eq-shapirofree⟧
- eq. (105) = ⟦eq-shapiroevens⟧
- Lemma 6.15 = ⟦lem-orbitshapiro⟧