The Nielsen isomorphism D₀ ≅ Π

D₀ = ⟨A,S,Y ∣ A²S⁴[S,Y]⟩ (the dyadic Demushkin presentation, GQ2/DyadicPresentation.lean) and Π = ⟨σ,x₀,x₁ ∣ x₀^{σ²}·x₀·[x₁,σ]⟩ (the boundary-frame presentation, GQ2/BoundaryFrame.lean) are isomorphic pro-2 groups via an explicit Nielsen change of generators (paper Cor 3.12):

• Π → D₀: σ ↦ S, x₀ ↦ S⁻²A⁻¹, x₁ ↦ Y — kills piRelator (since (S⁻²A⁻¹)^{S²}·(S⁻²A⁻¹) = S⁻⁴A⁻² = [S,Y] by d0_relation).
• D₀ → Π: A ↦ x₀⁻¹σ⁻², S ↦ σ, Y ↦ x₁ — kills d0Relator (using piRelator = 1).

These are mutually inverse, giving d0PiEquiv : D₀ ≅ Π matching the marked generators. Composed with prop_1_1 (G_{ℚ₂}(2) ≅ D₀) this yields the local half of Prop 3.10. Structure mirrors GQ2/BoundaryConstruction.lean's prop_3_10_gammaA (presentation maps + density mutual inverse), but with no word collapse — the relators match by pure group algebra + d0_relation.

theorem GQ2.SectionThree.d0_isProP : IsProP 2 ↑D0.toProfinite.toTop

D₀ is a pro-2 group.

Topological generation of D₀

noncomputable def GQ2.SectionThree.evalD0 : ↑(FreeProfiniteGroup (Fin 3)).toProfinite.toTop →ₜ* ↑D0.toProfinite.toTop

The evaluation F₃ → D₀, A ↦ A, S ↦ S, Y ↦ Y.

Equations

• GQ2.SectionThree.evalD0 = (GQ2.maxProPMk 2 ↑GQ2.D0Full.toProfinite.toTop).comp (GQ2.quotientMk (GQ2.relatorSubgroup {GQ2.d0Relator}))

theorem GQ2.SectionThree.topGen_d0 : (Subgroup.closure {d0A, d0S, d0Y}).topologicalClosure = ⊤

D₀ is topologically generated by A, S, Y.

[Y,S] = A²S⁴ in D₀ (rearranged d0_relation)

theorem GQ2.SectionThree.commP_d0Y_d0S : commP d0Y d0S = d0A ^ 2 * d0S ^ 4

commP d0Y d0S = d0A² d0S⁴ (rearrange A²S⁴[S,Y] = 1).

The forward map Π → D₀

noncomputable def GQ2.SectionThree.piToD0Base : FreeProfiniteGroup (Fin 3) ⟶ D0

σ ↦ S, x₀ ↦ S⁻²A⁻¹, x₁ ↦ Y.

Equations

• GQ2.SectionThree.piToD0Base = (GQ2.FreeProfiniteGroup.homEquiv (Fin 3) GQ2.D0).symm ![GQ2.d0S, (GQ2.d0S ^ 2)⁻¹ * GQ2.d0A⁻¹, GQ2.d0Y]

The backward map D₀ → Π

noncomputable def GQ2.SectionThree.d0ToPiBase : FreeProfiniteGroup (Fin 3) ⟶ PiBd

A ↦ x₀⁻¹σ⁻², S ↦ σ, Y ↦ x₁.

Equations

• GQ2.SectionThree.d0ToPiBase = (GQ2.FreeProfiniteGroup.homEquiv (Fin 3) GQ2.PiBd).symm ![GQ2.piX0⁻¹ * (GQ2.piSigma ^ 2)⁻¹, GQ2.piSigma, GQ2.piX1]

The two descents and the isomorphism D₀ ≅ Π

noncomputable def GQ2.SectionThree.PiToD0 : ↑PiBd.toProfinite.toTop →ₜ* ↑D0.toProfinite.toTop

Π → D₀ (through the presentation + max pro-2 universal property).

Equations

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

noncomputable def GQ2.SectionThree.D0ToPi : ↑D0.toProfinite.toTop →ₜ* ↑PiBd.toProfinite.toTop

D₀ → Π (through the presentation + max pro-2 universal property).

Equations

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

theorem GQ2.SectionThree.D0ToPi_PiToD0 (x : ↑PiBd.toProfinite.toTop) : D0ToPi (PiToD0 x) = x

D₀ToPi ∘ PiToD0 = id on Π (density on πσ, πx₀, πx₁).

theorem GQ2.SectionThree.PiToD0_D0ToPi (x : ↑D0.toProfinite.toTop) : PiToD0 (D0ToPi x) = x

PiToD0 ∘ D0ToPi = id on D₀ (density on A, S, Y).

noncomputable def GQ2.SectionThree.d0PiEquiv : ↑D0.toProfinite.toTop ≃ₜ* ↑PiBd.toProfinite.toTop

The Nielsen isomorphism D₀ ≅ Π (paper Cor 3.12).

Equations

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

@[simp]

theorem GQ2.SectionThree.d0PiEquiv_d0A : d0PiEquiv d0A = piX0⁻¹ * (piSigma ^ 2)⁻¹

@[simp]

theorem GQ2.SectionThree.d0PiEquiv_d0S : d0PiEquiv d0S = piSigma

@[simp]

theorem GQ2.SectionThree.d0PiEquiv_d0Y : d0PiEquiv d0Y = piX1

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

• Cor 3.12 = ⟦cor-relativeDemushkin⟧
• Prop 3.10 = ⟦prop-pro2⟧