B4: the rank-3 dyadic Demushkin presentation D₀ = ⟨A, S, Y | A²S⁴[S,Y]⟩

The paper's Prop. 1.1 / Lemma 3.4 normalizes the maximal pro-2 quotient G_{ℚ₂}(2) as the Demushkin group D₀ = ⟨A, S, Y | A²S⁴[S,Y] = 1⟩ (Labute's classification at d = 1). This file constructs D₀ as a GQ2.profinitePresentation and provides the relator; the actual isomorphism G_{ℚ₂}(2) ≅ D₀ is axiom B4 in GQ2/Foundations/Axioms.lean.

• GQ2.d0Relator : FreeProfiniteGroup (Fin 3) — the relator A²S⁴[S,Y] with A = of 0, S = of 1, Y = of 2, commutator [S,Y] = S⁻¹Y⁻¹SY (the paper's commP, GQ2/Words.lean). It is ω₂-free, hence a bare word in the free profinite group on three generators.
• GQ2.D0 : ProfiniteGrp — the presented group profinitePresentation {d0Relator}.

Stress test (homEquiv + a decide-able finite 2-group): the concrete marking A ↦ (reflection), S ↦ (order-4 rotation), Y ↦ (rotation²) of DihedralGroup 4 classifies a continuous hom F₃ ⟶ DihedralGroup 4 sending the generators as specified (homD4_toMonoidHom_of) and killing the relator (homD4_d0Relator, by decide) — so the relation is satisfiable in a genuine finite 2-group, and (d0Relator_quotientMk_eq_one) it holds in D₀.

The relator and the presented group

noncomputable def GQ2.d0Relator : ↑(FreeProfiniteGroup (Fin 3)).toProfinite.toTop

The dyadic Demushkin relator r₀ = A²S⁴[S,Y] (Labute [2], Thm 8 at d = 1; the paper's D₀ relation), as a word in the free profinite group on Fin 3 with A = of 0, S = of 1, Y = of 2. Commutator convention: [S,Y] = S⁻¹Y⁻¹SY (GQ2.commP, matching GQ2/Words.lean).

Equations

• GQ2.d0Relator = GQ2.FreeProfiniteGroup.of 0 ^ 2 * GQ2.FreeProfiniteGroup.of 1 ^ 4 * GQ2.commP (GQ2.FreeProfiniteGroup.of 1) (GQ2.FreeProfiniteGroup.of 2)

noncomputable def GQ2.D0Full : ProfiniteGrp.{0}

The full profinite presentation ⟨A, S, Y | A²S⁴[S,Y]⟩ (before taking the pro-2 quotient). The paper's D₀ = G_{ℚ₂}(2) is pro-2, so D₀ is the maximal pro-2 quotient of this (D0 below); the bare presentation is not pro-2 — e.g. A,S ↦ 0, Y ↦ 1 gives a surjection onto ℤ/3 (the relator dies in an abelian target), so its abelianization carries an odd part. Working with the pro-2 quotient is what makes topAbelianization D₀ ≅ ℤ/2 × ℤ₂ × ℤ₂ (paper (11)) and keeps axiom B4 (G_{ℚ₂}(2) ≅ D₀, a pro-2 ≅ pro-2 statement) faithful.

Equations

• GQ2.D0Full = GQ2.profinitePresentation {GQ2.d0Relator}

noncomputable def GQ2.D0 : ProfiniteGrp.{0}

D₀ (paper Prop. 1.1): the pro-2 group presented by ⟨A, S, Y | A²S⁴[S,Y] = 1⟩, i.e. the maximal pro-2 quotient of the free profinite presentation. This is the rank-3 dyadic Demushkin group; axiom B4 asserts G_{ℚ₂}(2) ≅ D₀.

Equations

• GQ2.D0 = GQ2.maxProPQuotient 2 ↑GQ2.D0Full.toProfinite.toTop

theorem GQ2.d0Relator_quotientMk_eq_one : (quotientMk (relatorSubgroup {d0Relator})) d0Relator = 1

The relator holds in the full presentation: A²S⁴[S,Y] = 1.

The marked generators

noncomputable def GQ2.d0FullA : ↑D0Full.toProfinite.toTop

The generator A in the full presentation D0Full (image of of 0).

Equations

• GQ2.d0FullA = (GQ2.quotientMk (GQ2.relatorSubgroup {GQ2.d0Relator})) (GQ2.FreeProfiniteGroup.of 0)

noncomputable def GQ2.d0FullS : ↑D0Full.toProfinite.toTop

The generator S in the full presentation D0Full (image of of 1).

Equations

• GQ2.d0FullS = (GQ2.quotientMk (GQ2.relatorSubgroup {GQ2.d0Relator})) (GQ2.FreeProfiniteGroup.of 1)

noncomputable def GQ2.d0FullY : ↑D0Full.toProfinite.toTop

The generator Y in the full presentation D0Full (image of of 2).

Equations

• GQ2.d0FullY = (GQ2.quotientMk (GQ2.relatorSubgroup {GQ2.d0Relator})) (GQ2.FreeProfiniteGroup.of 2)

theorem GQ2.d0Full_relation : d0FullA ^ 2 * d0FullS ^ 4 * commP d0FullS d0FullY = 1

The Demushkin relation A²S⁴[S,Y] = 1 already in the full presentation D0Full.

noncomputable def GQ2.d0A : ↑D0.toProfinite.toTop

The generator A ∈ D₀ (image of A under the pro-2 quotient map).

Equations

• GQ2.d0A = (GQ2.maxProPMk 2 ↑GQ2.D0Full.toProfinite.toTop) GQ2.d0FullA

noncomputable def GQ2.d0S : ↑D0.toProfinite.toTop

The generator S ∈ D₀.

Equations

• GQ2.d0S = (GQ2.maxProPMk 2 ↑GQ2.D0Full.toProfinite.toTop) GQ2.d0FullS

noncomputable def GQ2.d0Y : ↑D0.toProfinite.toTop

The generator Y ∈ D₀.

Equations

• GQ2.d0Y = (GQ2.maxProPMk 2 ↑GQ2.D0Full.toProfinite.toTop) GQ2.d0FullY

theorem GQ2.d0_relation : d0A ^ 2 * d0S ^ 4 * commP d0S d0Y = 1

The Demushkin relation on the named generators: A²S⁴[S,Y] = 1 in D₀. It holds already in the full presentation D0Full (d0Full_relation) and is pushed through the pro-2 quotient homomorphism maxProPMk (which commutes with *, ^, commP definitionally).

Stress test: a concrete finite 2-group marking (homEquiv + decide)

DihedralGroup 4 is a non-abelian group of order 8 = 2³. The marking A ↦ sr 0 (a reflection, order 2), S ↦ r 1 (a rotation of order 4), Y ↦ r 2 satisfies A² = S⁴ = 1 and [S,Y] = 1 (rotations commute), so the relator dies — witnessing that A²S⁴[S,Y] = 1 is realizable in a genuine finite 2-group.

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

• Lemma 3.4 = ⟦lem-standardorientation⟧
• Prop 1.1 = ⟦prop-markedDem⟧