FamiliesExtend from the Lemma 6.11 package

FamiliesExtend ρ (GQ2/LocalKummer.lean) — every admissible family V^∨ → H¹(N, 𝔽₂) is the scalar-restriction family of a class in H¹(ℚ₂, V) — is the H²(H_V, V) = 0 input of the lemma_6_17_dim chain (the paper's (78) projectivity logic). This file discharges it from the Lemma 6.11 regular-summand package alone (familiesExtend_of_package), with no counting and no graded filtration:

1. Inverse Shapiro at the free module. For the regular coefficients RegMod C Nr (𝔽₂[C]^{Nr} with the left-translation action, pulled back to G_ℚ₂ through ρ), every admissible family extends. The extension is the explicit coinduced-module cocycle b(g)(n, x) := u_n(s(x)⁻¹ · g · s(ρ(g)⁻¹x)) where s is a normalized set-section of ρ and u_n represents the family's value at the evaluation functional ev_{n,1}; the cocycle identity is the middle-insertion factorization of the shapiroWord, and the family is recovered on all of R^∨ from the single seed ev_{n,1} by conjugation-equivariance (ρ surjective) plus the finite ev-span of R^∨.
2. Retract transfer. phiRes is natural in the coefficient module (phiRes_mapCoeff1), so along the package (ι, r) with r ∘ ι = id a family on V is pushed to RegMod (ψ ↦ ξ(ψ ∘ ι)), extended there, and the extending class is pulled back through mapCoeff1 r — FamiliesExtend for V itself.

RegMod C Nr is an instance-opaque type synonym (a plain def) for Fin Nr → C → ZMod 2: the repo's global trivial action of G_ℚ₂ on ZMod 2 (GQ2/SectionSix.lean) lifts pointwise over raw function types and would clash with the translation action; the synonym hides the pi-shape from instance search, so the actions declared here are the only candidates. Everything here is #print axioms ⊆ std-3.

Consumer: GQ2/DimAssembly.lean (lemma_6_17_dim_of_hduality), which obtains the V-side package from lemma_6_11_of_tame_pair and thereby removes hext from the lemma_6_17_dim parameter list (leaving only the deep-part proof's hduality).

The normalized section and the Shapiro word

noncomputable def GQ2.ShapiroExtend.sec1 {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 →ₜ* C) (hρsurj : Function.Surjective ⇑ρ) (c : C) : AbsGalQ2

A set-theoretic section of ρ, normalized so that sec1 ρ hρsurj 1 = 1.

Equations

• GQ2.ShapiroExtend.sec1 ρ hρsurj c = if c = 1 then 1 else Function.surjInv hρsurj c

theorem GQ2.ShapiroExtend.shapiroWord_mem {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 →ₜ* C) (hρsurj : Function.Surjective ⇑ρ) (g : AbsGalQ2) (x : C) : (sec1 ρ hρsurj x)⁻¹ * g * sec1 ρ hρsurj ((ρ g)⁻¹ * x) ∈ ρ.ker

The Shapiro word s(x)⁻¹ · g · s(ρ(g)⁻¹x) lies in N = ker ρ.

noncomputable def GQ2.ShapiroExtend.shapiroWord {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 →ₜ* C) (hρsurj : Function.Surjective ⇑ρ) (g : AbsGalQ2) (x : C) : ↥ρ.ker

The inverse-Shapiro word s(x)⁻¹ · g · s(ρ(g)⁻¹x), as an element of ↥N. This is the (g, x)-entry of the coinduced-module extension cocycle.

Equations

• GQ2.ShapiroExtend.shapiroWord ρ hρsurj g x = ⟨(GQ2.ShapiroExtend.sec1 ρ hρsurj x)⁻¹ * g * GQ2.ShapiroExtend.sec1 ρ hρsurj ((ρ g)⁻¹ * x), ⋯⟩

theorem GQ2.ShapiroExtend.shapiroWord_mul {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 →ₜ* C) (hρsurj : Function.Surjective ⇑ρ) (g h : AbsGalQ2) (x : C) : shapiroWord ρ hρsurj (g * h) x = shapiroWord ρ hρsurj g x * shapiroWord ρ hρsurj h ((ρ g)⁻¹ * x)

Middle-insertion factorization — the source of the cocycle identity for the extension.

theorem GQ2.ShapiroExtend.shapiroWord_ker_one {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 →ₜ* C) (hρsurj : Function.Surjective ⇑ρ) (n₀ : ↥ρ.ker) : shapiroWord ρ hρsurj (↑n₀) 1 = n₀

On the kernel, at the base point x = 1, the word is the element itself.

theorem GQ2.ShapiroExtend.continuous_shapiroWord {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] (ρ : AbsGalQ2 →ₜ* C) (hρsurj : Function.Surjective ⇑ρ) (x : C) : Continuous fun (g : AbsGalQ2) => shapiroWord ρ hρsurj g x

Continuity of the word in g (the C-inputs are discrete, so the section legs are free).

The regular coefficient module, instance-opaque

def GQ2.ShapiroExtend.RegMod (C : Type) (Nr : ℕ) : Type

The regular coefficients 𝔽₂[C]^{Nr}, as an instance-opaque synonym of Fin Nr → C → ZMod 2: a plain def, so the ambient pointwise-action instances on raw function types (via the repo's global trivial G_ℚ₂-action on ZMod 2) cannot fire on it; the left-translation C-action below is the unique action in scope.

Equations

• GQ2.ShapiroExtend.RegMod C Nr = (Fin Nr → C → ZMod 2)

@[implicit_reducible]

instance GQ2.ShapiroExtend.instAddCommGroupRegMod {α : Type} {Nr : ℕ} : AddCommGroup (RegMod α Nr)

Equations

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

@[implicit_reducible]

instance GQ2.ShapiroExtend.instTopologicalSpaceRegMod {α : Type} {Nr : ℕ} : TopologicalSpace (RegMod α Nr)

Equations

• GQ2.ShapiroExtend.instTopologicalSpaceRegMod = GQ2.ShapiroExtend.instTopologicalSpaceRegMod._aux_1

instance GQ2.ShapiroExtend.instDiscreteTopologyRegModOfFinite {α : Type} {Nr : ℕ} [Finite α] : DiscreteTopology (RegMod α Nr)

instance GQ2.ShapiroExtend.instFiniteRegMod {α : Type} {Nr : ℕ} [Finite α] : Finite (RegMod α Nr)

instance GQ2.ShapiroExtend.instIsTopologicalAddGroupRegModOfFinite {α : Type} {Nr : ℕ} [Finite α] : IsTopologicalAddGroup (RegMod α Nr)

@[implicit_reducible]

instance GQ2.ShapiroExtend.instDistribMulActionRegMod {G' : Type} [Group G'] {Nr : ℕ} : DistribMulAction G' (RegMod G' Nr)

The left-translation action of C on the regular coefficients.

Equations

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

The evaluation span of the regular module's dual

def GQ2.ShapiroExtend.evReg {C : Type} (Nr : ℕ) (n : Fin Nr) (x : C) : RegMod C Nr →+ ZMod 2

The evaluation functional at (n, x) on the regular coefficients.

Equations

• GQ2.ShapiroExtend.evReg Nr n x = { toFun := fun (F : GQ2.ShapiroExtend.RegMod C Nr) => F n x, map_zero' := ⋯, map_add' := ⋯ }

theorem GQ2.ShapiroExtend.addHom_eq_sum_evReg {C : Type} (Nr : ℕ) [Fintype C] (φ : RegMod C Nr →+ ZMod 2) : φ = ∑ p : Fin Nr × C with φ (Pi.single p.1 (Pi.single p.2 1)) = 1, evReg Nr p.1 p.2

The ev-span: every functional on the regular module is the (finite) sum of the evaluations it supports — R^∨ is spanned by the point evaluations.

Naturality of the scalar restriction in the coefficient module

theorem GQ2.ShapiroExtend.phiRes_mapCoeff1 {C : Type} [Group C] [TopologicalSpace C] {ρ : AbsGalQ2 →ₜ* C} {W₁ W₂ : Type} [AddCommGroup W₁] [TopologicalSpace W₁] [DiscreteTopology W₁] [DistribMulAction AbsGalQ2 W₁] [ContinuousSMul AbsGalQ2 W₁] [DistribMulAction C W₁] [AddCommGroup W₂] [TopologicalSpace W₂] [DiscreteTopology W₂] [DistribMulAction AbsGalQ2 W₂] [ContinuousSMul AbsGalQ2 W₂] [DistribMulAction C W₂] [IsTopologicalAddGroup W₁] [IsTopologicalAddGroup W₂] (hρ₁ : ∀ (g : AbsGalQ2) (w : W₁), g • w = ρ g • w) (hρ₂ : ∀ (g : AbsGalQ2) (w : W₂), g • w = ρ g • w) (f : W₁ →+ W₂) (hf : Continuous ⇑f) (hcompat : ∀ (g : AbsGalQ2) (w : W₁), f (g • w) = g • f w) (x : ContCoh.H1 AbsGalQ2 W₁) (φ : W₂ →+ ZMod 2) : LocalKummer.phiRes ρ ((ContCoh.mapCoeff1 f hf hcompat) x) φ = LocalKummer.phiRes ρ x (φ.comp f)

phiRes is natural in the coefficient module: restricting a pushed-forward class is pre-composing the functional. The workhorse of the retract transfer.

The main theorem: FamiliesExtend from the regular-summand package

theorem GQ2.ShapiroExtend.familiesExtend_of_package {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] [Finite C] {ρ : AbsGalQ2 →ₜ* C} {V : Type} [AddCommGroup V] [TopologicalSpace V] [DiscreteTopology V] [DistribMulAction AbsGalQ2 V] [ContinuousSMul AbsGalQ2 V] [DistribMulAction C V] (hρ : ∀ (g : AbsGalQ2) (v : V), g • v = ρ g • v) (hρsurj : Function.Surjective ⇑ρ) {Nr : ℕ} (ι : V →+ Fin Nr → C → ZMod 2) (r : (Fin Nr → C → ZMod 2) →+ V) (hι : ∀ (h : C) (v : V) (n : Fin Nr) (x : C), ι (h • v) n x = ι v n (h⁻¹ * x)) (hr : ∀ (h : C) (F : Fin Nr → C → ZMod 2), (r fun (n : Fin Nr) (x : C) => F n (h⁻¹ * x)) = h • r F) (hri : ∀ (v : V), r (ι v) = v) : LocalKummer.FamiliesExtend ρ

FamiliesExtend from the Lemma 6.11 package (the deep-part proof): given the equivariant split-summand package (ι, r) embedding V into the regular module 𝔽₂[C]^{Nr} (the lemma_6_11/lemma_6_11_of_tame_pair output shape), every admissible family extends to a class of H¹(ℚ₂, V).

Inverse Shapiro at the regular module (the explicit coinduced-coefficient cocycle out of the family's evaluation seeds), then the retract transfer along mapCoeff1 r. The statement is V-side only; the regular module and its actions live inside the proof.

Paper-tag ledger (auto-generated by paperforge; do not edit)

• Lemma 6.11 = ⟦lem-faithfulprojective⟧