Shapiro coordinates + scalar deepness (the hvanish producers) #
The two per-orbit hypotheses of OrbitVanish.Q0loc_vanish_of_datum_decomp for the deep half
x ∈ deepPart ρ:
hcoh— each per-orbit graph pullback is cohomologous to itscor2Funcorestriction. This is a direct application of the bankedSectionSix.lemma_6_15_{square,free,involution}; the Lemma 6.17 vanishing proof (OrbitDecomp.lean) structures eachdatf oas a definitionalcomapof the literal orbit datum so the pullbacks are syntactically the Lemma-6.15 inputs — the instantiation is done at f2d.hvanish— each corestriction's inner cocycle vanishes in its subgroup'sH². For square/free orbits the inner cocycle is a cupα ⌣ α'of scalar Shapiro coordinates, which vanish because those coordinates are deep (x ∈ deepPart⟹ every scalar restriction is a deep Kummer class,LocalKummer.mem_deepPart_iff), via the eq.-(94) orthogonalityLocalKummer.cup_deepClasses. This file proves that reduction —hvanish_cup— the self-contained core of the square and free cases. (The involution case,hvanishvialemma_6_16's Evens-norm vanishing, is the remaining piece; design recorddocs/orchestration/p15f2c-design.md.)
Axioms: B9, B11a (through cup_deepClasses/(94)).
The H²mk → H²ofFun vanishing bridge: a 2-cocycle whose H²mk class is 0 has trivial
H²ofFun. The shared tail of both hvanish cases.
The deep-class cup vanishing (the Lemma 6.17 vanishing proof, the square/free hvanish core): if two scalar
cocycles a, b over k.fixingSubgroup have deep classes, their cup 2-cochain
α ⌣ β has trivial H²ofFun class. Composes the eq.-(94) orthogonality
LocalKummer.cup_deepClasses (trivialCupPairing = 0) with the cup11/H2mk identification
and B²-extraction. This is H2ofFun ↥(U o) (inner o) = 0 for the square orbit
(inner o = α ⌣ α, U o = k.fixingSubgroup = ker ρ) and, at a ≠ b, the free orbit.
The involution hvanish cochain bridge (the Lemma 6.17 vanishing proof): the Evens-norm class evensNormH2
being zero (its content is lemma_6_16, for a deep scalar coordinate) gives the required
H2ofFun (evensNormFun …) = 0 — the involution-orbit inner o = evensNormFun, U o = U₀.
f2d composes lemma_6_16 (with the block's concrete Kummer field data) with this bridge.
Deepness transport across the equivariant coefficient embedding (f2d) #
Deepness transports along an equivariant coefficient map (the Lemma 6.17 vanishing proof): if x ∈ deepPart ρ
over W₁ and f : W₁ →+ W₂ is a continuous AbsGalQ2-equivariant map, then the pushed-forward
class mapCoeff1 f x is in deepPart ρ over W₂. Every scalar restriction of mapCoeff1 f x
is a scalar restriction of x at the pre-composed functional (ShapiroExtend.phiRes_mapCoeff1),
which is deep because x is. This carries the deep half X₊ across the Lemma-6.14 regular
embedding ι : V →+ W (the deepness half of the transport, the companion of the isometry).
Reindexing the acting group of a factor-set datum (the C ↔ AbsGalQ2 ⧸ ker ρ bridge) #
Reindex a factor-set datum's acting group along φ : C' → C — only the correction m sees
the group, so f is unchanged and m pre-composes with φ.
Equations
- dat.reindexHom φ = { f := dat.f, m := fun (c' : C') (v : V) => dat.m (φ c') v }
Instances For
graphPullback reindexing (the Lemma 6.17 vanishing proof, the linchpin of the C ↔ AbsGalQ2 ⧸ ker ρ bridge):
pulling back the φ-reindexed datum along ρ' : Γ → C' equals pulling back the original datum
along φ ∘ ρ', provided the C'-action on V is the φ-pullback of the C-action (hφ).
f2b's orbit datum lives over G ⧸ N while the ambient Q0loc/Lemma-6.14 transport is over C;
with φ = e : C → AbsGalQ2 ⧸ ker ρ and e ∘ ρ = mk' (ker ρ) this identifies the two graph
pullbacks so the banked lemma_6_15_* (stated at mk' N) apply.
Q0loc reindexing (the Lemma 6.17 vanishing proof): lifts graphPullback_reindexHom from the raw cochain to the
base connecting map — Q⁰_loc of the φ-reindexed datum along ρ' equals Q⁰_loc of the datum
along φ ∘ ρ'. In the assembly, with φ = e : C → AbsGalQ2 ⧸ ker ρ (e ∘ ρ = mk' (ker ρ)), this
rewrites the C-level Lemma-6.14 output as the mk'-level orbit map so the orbit reducer fires.
The involution-orbit hvanish, assembled #
The involution-orbit hvanish, assembled from lemma_6_16 (the Lemma 6.17 vanishing proof, the spine's
assembly core): given the concrete Kummer field data of the deep unit A at an involution block
coordinate — the tower k ≤ L (index 2, unramified hunram), the √-generator (d, δ, hδ, hδL, hLδ), the coordinates A = u + vδ, and the deep-unit/side-condition witnesses — the involution
inner cochain evensNormFun (…) has trivial H²ofFun over ↥(k.fixingSubgroup). This is the
reducer's involution hvanish, stated in k.fixingSubgroup vocabulary (f2d bridges
k.fixingSubgroup = U₀ — the InfiniteGalois transport fixingSubgroup (fixedField U₀) = U₀ — to
the reducer's ↥U₀ form).
Proof: SectionSix.lemma_6_16 gives evensNormH2 … = 0; the banked hvanish_evensNorm descends
it to H²ofFun.
The field data is threaded as hypotheses — the c2a "abstract Kummer presentation package"
∃-interface (d, δ, hδ, hδL, hLδ, u, v, hAuv) plus the deep witness (A, β, hdeep, …) from
mem_deepPart_iff/deepClass_eq_kummerClassK (the f2d/plumbing step). hunram HOLDS for every
involution orbit (Step-0 decision, docs/orchestration/p15f2c-design.md): ρ(ĝ) is order 2 in C, but C's
tame inertia ⟨c tameTau⟩ has odd order (Tame.tame_odd_order), so ρ(ĝ) ∉ inertia ⟹ L/k
unramified; c2c discharges hunram in spectral-norm vocabulary.
Ax: B9, B11a (via lemma_6_16).
Deep class → involution hvanish (the Lemma 6.17 vanishing proof, the witness-plumbing step): given a deep
Kummer class ξ ∈ deepClasses (L.fixingSubgroup) at the involution block coordinate and the c2a
"abstract Kummer presentation package" hc2a (IsDeepUnit L.fixingSubgroup A ⟹ ∃ d δ u v, …),
the involution inner cochain vanishes for the class's own square root β.
Extracts the deep unit (A, β) from ξ (unpacking the deepClasses definition), derives the
mechanical side-conditions hα (additivity via kummerCocycleFun_hom_on on L.fixingSubgroup,
which fixes A) and hαc (continuity via kummerCocycleFun_continuous), and applies hc2a +
hvanish_involution. This is steps (2)–(5) of the Lemma 6.17 vanishing proof in L-vocabulary; the remaining
ker ρ = L.fixingSubgroup transport (to feed mem_deepPart_iff) and the c2a-package proof
(the Lemma 6.17 vanishing proof) are the last pieces. Ax: B9, B11a, B11b (via hvanish_involution/lemma_6_16).