Prop 3.10, local half: (Π, ν₂) ≅ (G_{ℚ₂}(2), ν_ur)

Compose prop_1_1 (G_{ℚ₂}(2) ≅ D₀ with ν_ur(a,s,y) = (−2,1,0), GQ2/PropOneOneAssembly.lean) with the Nielsen isomorphism d0PiEquiv : D₀ ≅ Π (GQ2/DyadicNielsen.lean), and use the seam ztwoEquivPadic : Ztwo ≅ Multiplicative ℤ₂ (the ℤ₂-powering development) for ι. The ν-compatibility is a density argument on D₀'s three generators, matching the prop_1_1 unramified coordinates against ν₂(σ,x₀,x₁) = (1,0,0) transported through d0PiEquiv (d0A ↦ x₀⁻¹σ⁻², d0S ↦ σ, d0Y ↦ x₁).

theorem GQ2.SectionThree.ztwoEquivPadic_ztwoOne : ztwoEquivPadic ztwoOne = Multiplicative.ofAdd 1

ζ = ztwoEquivPadic ztwoOne = ofAdd 1.

noncomputable def GQ2.SectionThree.zetaNuTwo : ↑PiBd.toProfinite.toTop →ₜ* Multiplicative ℤ_[2]

The composite H = ζ ∘ ν₂ : Π → Multiplicative ℤ₂. Pushing H (rather than ζ) through a product avoids the Ztwo-def barrier: H's map_* never expose the Ztwo intermediate.

Equations

• GQ2.SectionThree.zetaNuTwo = { toMonoidHom := GQ2.ztwoEquivPadic.toMonoidHom, continuous_toFun := GQ2.SectionThree.zetaNuTwo._proof_3 }.comp GQ2.nuTwo

theorem GQ2.SectionThree.prop_3_10_local_marked_proved [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] (R : LocalReciprocity) : ∃ (ι : ↑Ztwo.toProfinite.toTop ≃ₜ* Multiplicative ℤ_[2]), ι ztwoOne = Multiplicative.ofAdd ↑1 ∧ ∃ (e : ↑(maxProPQuotient 2 AbsGalQ2).toProfinite.toTop ≃ₜ* ↑PiBd.toProfinite.toTop), ∀ (g : AbsGalQ2), R.nu_ur (toAb g) = ι (nuTwo (e ((maxProPMk 2 AbsGalQ2) g)))

Prop 3.10, local half (proved): the boundary group Π with ν₂ is the fully unramified marked pair (G_{ℚ₂}(2), ν_ur).

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

• Prop 3.10 = ⟦prop-pro2⟧