Shapiro finiteness: H¹(U, 𝔽₂) is finite for an open subgroup U ≤ G_ℚ₂

The [Finite (H¹(G_K, 𝔽₂))] instance threaded through the whole deep-part counting layer (DeepCount, DimClose, DimAssembly, ResidueLift, AdmissibleCount) is discharged here from the existing axiom budget — no new axiom.

For U an open (hence finite-index) subgroup of G_ℚ₂, Shapiro's lemma identifies H¹(U, 𝔽₂) with H¹(G_ℚ₂, 𝔽₂[G/U]) where 𝔽₂[G/U] = Map(G ⧸ U, 𝔽₂) is the finite coinduced/permutation module (coinduced action (g • f) x = f (g⁻¹ • x), trivial coefficient action). We build the Shapiro comparison map

θ : H¹(G_ℚ₂, 𝔽₂[G/U]) → H¹(U, 𝔽₂), θ = mapCoeff₁(ev) ∘ res₁

(restrict to U, then evaluate at the base coset ⟦1⟧), and prove it surjective via the explicit Shapiro section σ(c)(g)(x) = c(w(g,x)) built from the transversal word w(g,x) = sect(g⁻¹•x)⁻¹ · g⁻¹ · sect x ∈ U — whose cocycle identity w(g₁g₂,x) = w(g₂, g₁⁻¹•x)·w(g₁,x) is a pure group computation, and which collapses to u⁻¹ at the base coset (so the round-trip is the identity, 𝔽₂-inversion being trivial).

Since 𝔽₂[G/U] is finite, H¹(G_ℚ₂, 𝔽₂[G/U]) is finite by B7 (finite_H1, the local Euler characteristic — already in the census), and the surjection transports finiteness to H¹(U, 𝔽₂).

#print axioms finite_H1_open = std-3 + B7 (absGalQ2_localEulerCharacteristic). No sorryAx, no new axiom.

def GQ2.PermMod (U : Subgroup AbsGalQ2) : Type

The finite coinduced / permutation module 𝔽₂[G/U] for Shapiro's lemma: functions G ⧸ U → 𝔽₂ with the coinduced G-action (g • f) x = f (g⁻¹ • x). An instance-opaque synonym (plain def) so the coinduced action is not shadowed by the global pointwise (trivial) Pi-action on raw function types.

Equations

• GQ2.PermMod U = (GQ2.AbsGalQ2 ⧸ U → ZMod 2)

@[implicit_reducible]

noncomputable instance GQ2.PermMod.instAddCommGroup {U : Subgroup AbsGalQ2} : AddCommGroup (PermMod U)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance GQ2.PermMod.instTopologicalSpace {U : Subgroup AbsGalQ2} : TopologicalSpace (PermMod U)

Equations

• GQ2.PermMod.instTopologicalSpace = ⊥

instance GQ2.PermMod.instDiscreteTopology {U : Subgroup AbsGalQ2} : DiscreteTopology (PermMod U)

instance GQ2.PermMod.instFiniteOfQuotientAbsGalQ2Subgroup {U : Subgroup AbsGalQ2} [Finite (AbsGalQ2 ⧸ U)] : Finite (PermMod U)

instance GQ2.PermMod.instIsTopologicalAddGroup {U : Subgroup AbsGalQ2} : IsTopologicalAddGroup (PermMod U)

@[implicit_reducible]

noncomputable instance GQ2.PermMod.instSMulAbsGalQ2 {U : Subgroup AbsGalQ2} : SMul AbsGalQ2 (PermMod U)

Equations

• GQ2.PermMod.instSMulAbsGalQ2 = { smul := fun (g : GQ2.AbsGalQ2) (f : GQ2.PermMod U) (x : GQ2.AbsGalQ2 ⧸ U) => f (g⁻¹ • x) }

theorem GQ2.PermMod.smul_apply {U : Subgroup AbsGalQ2} (g : AbsGalQ2) (f : PermMod U) (x : AbsGalQ2 ⧸ U) : (g • f) x = f (g⁻¹ • x)

theorem GQ2.PermMod.add_apply {U : Subgroup AbsGalQ2} (f₁ f₂ : PermMod U) (x : AbsGalQ2 ⧸ U) : (f₁ + f₂) x = f₁ x + f₂ x

@[implicit_reducible]

noncomputable instance GQ2.PermMod.instDistribMulActionAbsGalQ2 {U : Subgroup AbsGalQ2} : DistribMulAction AbsGalQ2 (PermMod U)

Equations

• GQ2.PermMod.instDistribMulActionAbsGalQ2 = { toSMul := GQ2.PermMod.instSMulAbsGalQ2, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }

theorem GQ2.PermMod.continuous_orbit {U : Subgroup AbsGalQ2} (x : AbsGalQ2 ⧸ U) : Continuous fun (g : AbsGalQ2) => g • x

The orbit map g ↦ g • x on the coset space is continuous.

theorem GQ2.PermMod.continuous_smul_left {U : Subgroup AbsGalQ2} (hU : IsOpen ↑U) [Finite (AbsGalQ2 ⧸ U)] (f : PermMod U) : Continuous fun (g : AbsGalQ2) => g • f

For fixed f, the map g ↦ g • f into the discrete module is continuous.

theorem GQ2.PermMod.continuousSMul {U : Subgroup AbsGalQ2} (hU : IsOpen ↑U) [Finite (AbsGalQ2 ⧸ U)] : ContinuousSMul AbsGalQ2 (PermMod U)

The coinduced action is (jointly) continuous.

noncomputable def GQ2.PermMod.basePt (U : Subgroup AbsGalQ2) : AbsGalQ2 ⧸ U

The base coset ⟦1⟧ ∈ G ⧸ U.

Equations

• GQ2.PermMod.basePt U = ↑1

noncomputable def GQ2.PermMod.ev (U : Subgroup AbsGalQ2) : PermMod U →+ ZMod 2

Evaluation at the base coset f ↦ f ⟦1⟧, a U-equivariant additive map to 𝔽₂.

Equations

• GQ2.PermMod.ev U = { toFun := fun (f : GQ2.PermMod U) => f (GQ2.PermMod.basePt U), map_zero' := ⋯, map_add' := ⋯ }

theorem GQ2.PermMod.ev_continuous {U : Subgroup AbsGalQ2} : Continuous ⇑(ev U)

theorem GQ2.PermMod.ev_compat {U : Subgroup AbsGalQ2} (u : ↥U) (n : PermMod U) : (ev U) (u • n) = u • (ev U) n

ev intertwines the U-actions (both trivial on the base value).

noncomputable def GQ2.PermMod.theta (U : Subgroup AbsGalQ2) (hU : IsOpen ↑U) [Finite (AbsGalQ2 ⧸ U)] : ContCoh.H1 AbsGalQ2 (PermMod U) →+ ContCoh.H1 (↥U) (ZMod 2)

The Shapiro map θ : H¹(G, 𝔽₂[G/U]) → H¹(U, 𝔽₂): restrict to U, then evaluate at the base coset. We prove it surjective; since the source is finite (B7, 𝔽₂[G/U] finite), so is H¹(U, 𝔽₂).

Equations

• GQ2.PermMod.theta U hU = (GQ2.ContCoh.mapCoeff1 (GQ2.PermMod.ev U) ⋯ ⋯).comp (GQ2.ContCoh.res1 GQ2.AbsGalQ2 (GQ2.PermMod U) U)

noncomputable def GQ2.PermMod.thetaZ1 (U : Subgroup AbsGalQ2) (hU : IsOpen ↑U) [Finite (AbsGalQ2 ⧸ U)] : ↥(ContCoh.Z1 AbsGalQ2 (PermMod U)) →+ ↥(ContCoh.Z1 (↥U) (ZMod 2))

The Z¹-level Shapiro map underlying theta.

Equations

• One or more equations did not get rendered due to their size.

The Shapiro section (surjectivity)

noncomputable def GQ2.PermMod.sect {U : Subgroup AbsGalQ2} (x : AbsGalQ2 ⧸ U) : AbsGalQ2

A set-theoretic section of G → G ⧸ U normalized so the base coset lifts to 1.

Equations

• GQ2.PermMod.sect x = if x = GQ2.PermMod.basePt U then 1 else Quotient.out x

theorem GQ2.PermMod.wElt_mem {U : Subgroup AbsGalQ2} (g : AbsGalQ2) (x : AbsGalQ2 ⧸ U) : (sect (g⁻¹ • x))⁻¹ * g⁻¹ * sect x ∈ U

The Shapiro word w(g,x) = sect(g⁻¹•x)⁻¹ · g⁻¹ · sect x lies in U.

noncomputable def GQ2.PermMod.wElt {U : Subgroup AbsGalQ2} (g : AbsGalQ2) (x : AbsGalQ2 ⧸ U) : ↥U

The Shapiro word as an element of U.

Equations

• GQ2.PermMod.wElt g x = ⟨(GQ2.PermMod.sect (g⁻¹ • x))⁻¹ * g⁻¹ * GQ2.PermMod.sect x, ⋯⟩

theorem GQ2.PermMod.wElt_mul {U : Subgroup AbsGalQ2} (g₁ g₂ : AbsGalQ2) (x : AbsGalQ2 ⧸ U) : wElt (g₁ * g₂) x = wElt g₂ (g₁⁻¹ • x) * wElt g₁ x

The cocycle identity for the Shapiro word: w(g₁g₂, x) = w(g₂, g₁⁻¹•x) · w(g₁, x).

noncomputable def GQ2.PermMod.sigmaFun {U : Subgroup AbsGalQ2} (c : ↥(ContCoh.Z1 (↥U) (ZMod 2))) : AbsGalQ2 → PermMod U

The section cochain σ(c)(g) = (x ↦ c(w(g,x))).

Equations

• GQ2.PermMod.sigmaFun c g x = ↑c (GQ2.PermMod.wElt g x)

theorem GQ2.PermMod.sigma_eval {U : Subgroup AbsGalQ2} (c : ↥(ContCoh.Z1 (↥U) (ZMod 2))) (u : ↥U) : ↑c (wElt (↑u) (basePt U)) = ↑c u

The Shapiro round-trip on the base coset: c(w(u, ⟦1⟧)) = c(u). The word collapses to u⁻¹ (since sect ⟦1⟧ = 1), and 𝔽₂-inversion is the identity.

theorem GQ2.PermMod.theta_surjective {U : Subgroup AbsGalQ2} (hU : IsOpen ↑U) [Finite (AbsGalQ2 ⧸ U)] : Function.Surjective ⇑(theta U hU)

Shapiro surjectivity.

theorem GQ2.finite_H1_open (U : Subgroup AbsGalQ2) (hU : IsOpen ↑U) [Finite (AbsGalQ2 ⧸ U)] : Finite (ContCoh.H1 (↥U) (ZMod 2))

Finiteness of H¹(U, 𝔽₂) for an open subgroup U ≤ G_ℚ₂ — Shapiro's lemma reduces it to H¹(G_ℚ₂, 𝔽₂[G/U]), finite by B7. Discharges the [Finite (H¹(G_K, 𝔽₂))] instance threaded through the deep-part counting layer. No new axiom (std-3 + B7).