The abelianization B_R = D_R^{ab} (Roe note §3.1, eq. (3.4)–(3.6))

The marked pro-2 abelianization of the Roe group D_R (GQ2/Roe/DRPresentation.lean):

B_R = D_R^{ab} = ⟨s̄, x̄, ȳ | −4x̄ + 2ȳ = 0⟩_{ℤ₂} = C₂·t ⊕ ℤ₂·s̄ ⊕ ℤ₂·x̄, t = ȳ·x̄⁻² (⟦eq:BR⟧/⟦eq:tR⟧/⟦eq:BRsplit⟧),

a 1:1 clone of GQ2/SectionThree.lean's BDecomposition for D₀ (the B = D₀^{ab} bundle of paper eq. (11)). The abelianized relation is drWord_comm: in B_R the relator collapses to (x̄⁴)⁻¹ȳ² = 1, i.e. 2ȳ = 4x̄. In the coordinate system (t, s̄, x̄) the torsion generator t = ȳ·x̄⁻² is 2-torsion and ȳ ↦ t·x̄² is forced (ȳ-row (1, 0, 2)).

Contents

• BRDecomposition / br_decomposition: the continuous isomorphism B_R ≅ Multiplicative (ZMod 2 × ℤ₂ × ℤ₂) pinning t ↦ (1,0,0), s̄ ↦ (0,1,0), x̄ ↦ (0,0,1) (and ȳ ↦ (1,0,2), forced). Built from the coordinate homs sHomR/xHomR/tHomR (abLiftG ∘ drLiftHom), shown bijective — the phiEquiv route.
• Topological generation dr_topGen: {s, x, y} topologically generate D_R; the hom-extensionality corollaries dr_hom_ext (homs out of D_R) and drab_hom_ext (homs out of B_R). Consumed by R9 (isLabuteOrientation_ext), R12 (drH1_bijective), R15.
• demushkinQ_DR_eq_two: the q-invariant feed for DRDemushkin.demushkinQ_DR — the torsion subgroup of B_R is C₂ (ℤ₂ is torsion-free), so demushkinQ D_R = 2.

The pro-2 topAbelianization instances are cloned local from GQ2/SectionThree.lean:112–160 (direct local instance, not wrapped in a def — that breaks the group structure).

Pro-2 instances on B_R = topAbelianization D_R

Cloned local from GQ2/SectionThree.lean:112–160 (the block there is file-scoped, so it does not leak to importers; we re-register for topAbelianization D_R).

@[implicit_reducible]

noncomputable def GQ2.instCommGroupTopAbR {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : CommGroup (topAbelianization G)

G^{ab} is commutative (local clone).

Equations

• GQ2.instCommGroupTopAbR = { toGroup := inferInstance, mul_comm := ⋯ }

theorem GQ2.instCompactSpaceTopAbR {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] : CompactSpace (topAbelianization G)

theorem GQ2.instT2SpaceTopAbR {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] : T2Space (topAbelianization G)

theorem GQ2.instTotallyDisconnectedSpaceTopAbR {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] : TotallyDisconnectedSpace (topAbelianization G)

theorem GQ2.isProP_two_topAb_DR : IsProP 2 (topAbelianization ↑DR.toProfinite.toTop)

B_R = topAbelianization D_R is pro-2 (image of the pro-2 group D_R under abMk).

Topological generation of D_R by {s, x, y}

noncomputable def GQ2.qDR : ↑(FreeProfiniteGroup (Fin 3)).toProfinite.toTop →* ↑DR.toProfinite.toTop

The composite surjection F₃ ↠ D_R (through the full presentation and the pro-2 quotient), sending of 0, of 1, of 2 to drS, drX, drY.

Equations

• GQ2.qDR = (GQ2.maxProPMk 2 ↑GQ2.DRFull.toProfinite.toTop).comp (GQ2.quotientMk (GQ2.relatorSubgroup {GQ2.drRelator})).toMonoidHom

theorem GQ2.qDR_of (i : Fin 3) : qDR (FreeProfiniteGroup.of i) = ![drS, drX, drY] i

theorem GQ2.continuous_qDR : Continuous ⇑qDR

theorem GQ2.qDR_surjective : Function.Surjective ⇑qDR

theorem GQ2.freeProfinite_topGen : (Subgroup.closure (Set.range FreeProfiniteGroup.of)).topologicalClosure = ⊤

The free generators of F₃ topologically generate.

theorem GQ2.dr_topGen : (Subgroup.closure {drS, drX, drY}).topologicalClosure = ⊤

Topological generation of D_R ⟦lem:pro2word⟧: the marked generators {s, x, y} topologically generate D_R. This is the pushforward of freeProfinite_topGen through the surjection qDR : F₃ ↠ D_R. Consumed by R9 (isLabuteOrientation_ext), R12 (drH1 surjectivity), R15, and by dr_hom_ext/drab_hom_ext below.

theorem GQ2.dr_hom_ext {A : Type} [Group A] [TopologicalSpace A] [IsTopologicalGroup A] [T2Space A] (φ ψ : ↑DR.toProfinite.toTop →ₜ* A) (hS : φ drS = ψ drS) (hX : φ drX = ψ drX) (hY : φ drY = ψ drY) : φ = ψ

Hom-extensionality for D_R: two continuous homs into a pro-2 (Hausdorff) group agreeing on s, x, y agree everywhere ({s, x, y} topologically generate, dr_topGen). The DR-level density argument consumed by R9's isLabuteOrientation_ext and R15's marked matching.

The coordinate surjection Φ_R : ℤ₂³ → B_R and coordinate surjectivity

noncomputable def GQ2.PhiR : Multiplicative (ℤ_[2] × ℤ_[2] × ℤ_[2]) →* topAbelianization ↑DR.toProfinite.toTop

The coordinate hom Φ_R(s,x,y) = s̄^s · x̄^x · ȳ^y on B_R.

Equations

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

theorem GQ2.DRab_coord (z : topAbelianization ↑DR.toProfinite.toTop) : ∃ (s : ℤ_[2]) (x : ℤ_[2]) (y : ℤ_[2]), z = zpowZtwo isProP_two_topAb_DR (SectionThree.abMk drS) s * zpowZtwo isProP_two_topAb_DR (SectionThree.abMk drX) x * zpowZtwo isProP_two_topAb_DR (SectionThree.abMk drY) y

Coordinate surjectivity of B_R: every element is s̄^s x̄^x ȳ^y.

theorem GQ2.drab_hom_ext {A : Type} [Group A] [TopologicalSpace A] [IsTopologicalGroup A] [CompactSpace A] [T2Space A] [TotallyDisconnectedSpace A] (hA : IsProP 2 A) (φ ψ : topAbelianization ↑DR.toProfinite.toTop →ₜ* A) (hS : φ (SectionThree.abMk drS) = ψ (SectionThree.abMk drS)) (hX : φ (SectionThree.abMk drX) = ψ (SectionThree.abMk drX)) (hY : φ (SectionThree.abMk drY) = ψ (SectionThree.abMk drY)) (z : topAbelianization ↑DR.toProfinite.toTop) : φ z = ψ z

Hom-extensionality for B_R: continuous homs B_R → A (A pro-2) agreeing on s̄, x̄, ȳ agree everywhere (the d0ab_hom_ext analogue, via DRab_coord).

The three coordinate homs s̄-coord, x̄-coord, t-coord

Each is abLiftG (drLiftHom …); the relator check is drWord_comm (drWord = (x⁴)⁻¹y²), which holds because the generator values (s, x, y) satisfy −4x + 2y = 0.

noncomputable def GQ2.sHomR : topAbelianization ↑DR.toProfinite.toTop →ₜ* Multiplicative ℤ_[2]

The s̄-coordinate hom B_R → ℤ₂, with s̄ ↦ 1, x̄ ↦ 0, ȳ ↦ 0.

Equations

• GQ2.sHomR = GQ2.SectionThree.abLiftG (GQ2.drLiftHom GQ2.PropOneOne.isProP_two_multPadicInt ![Multiplicative.ofAdd 1, Multiplicative.ofAdd 0, Multiplicative.ofAdd 0] GQ2.sHomR._proof_4)

noncomputable def GQ2.xHomR : topAbelianization ↑DR.toProfinite.toTop →ₜ* Multiplicative ℤ_[2]

The x̄-coordinate hom B_R → ℤ₂, with s̄ ↦ 0, x̄ ↦ 1, ȳ ↦ 2.

Equations

• GQ2.xHomR = GQ2.SectionThree.abLiftG (GQ2.drLiftHom GQ2.PropOneOne.isProP_two_multPadicInt ![Multiplicative.ofAdd 0, Multiplicative.ofAdd 1, Multiplicative.ofAdd 2] GQ2.xHomR._proof_1)

noncomputable def GQ2.tHomR : topAbelianization ↑DR.toProfinite.toTop →ₜ* Multiplicative (ZMod 2)

The t-coordinate hom B_R → ZMod 2, with s̄ ↦ 0, x̄ ↦ 0, ȳ ↦ 1.

Equations

• GQ2.tHomR = GQ2.SectionThree.abLiftG (GQ2.drLiftHom GQ2.SectionThree.isProP_two_multZMod2 ![Multiplicative.ofAdd 0, Multiplicative.ofAdd 0, Multiplicative.ofAdd 1] GQ2.tHomR._proof_1)

The combined coordinate hom φ_R = (t, s̄, x̄)

noncomputable def GQ2.phiHomR : topAbelianization ↑DR.toProfinite.toTop →* Multiplicative (ZMod 2 × ℤ_[2] × ℤ_[2])

The combined coordinate map φ_R : B_R → ZMod 2 × ℤ₂ × ℤ₂.

Equations

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

theorem GQ2.continuous_phiHomR : Continuous ⇑phiHomR

Coordinate computations on s̄^s x̄^x ȳ^y

φ_R is injective

theorem GQ2.abMk_relR : SectionThree.abMk drX ^ 4 = SectionThree.abMk drY ^ 2

The abelianized relation x̄⁴ = ȳ² in B_R (from dr_relation + drWord_comm).

theorem GQ2.tbarR_sq : (SectionThree.abMk drX ^ (-2) * SectionThree.abMk drY) ^ 2 = 1

t = ȳ·x̄⁻² is 2-torsion (t² = ȳ²x̄⁻⁴ = 1).

theorem GQ2.phiHomR_injective : Function.Injective ⇑phiHomR

φ_R is surjective

theorem GQ2.phiHomR_surjective : Function.Surjective ⇑phiHomR

Assembly: the coordinate isomorphism

noncomputable def GQ2.phiEquivR : topAbelianization ↑DR.toProfinite.toTop ≃ₜ* Multiplicative (ZMod 2 × ℤ_[2] × ℤ_[2])

The coordinate isomorphism φ_R : B_R ≃ₜ* ZMod 2 × ℤ₂ × ℤ₂.

Equations

• GQ2.phiEquivR = GQ2.continuousMulEquivOfBijective { toMonoidHom := GQ2.phiHomR, continuous_toFun := GQ2.continuous_phiHomR } GQ2.phiEquivR._proof_2

The bundled decomposition ⟦eq:BR⟧/⟦eq:tR⟧/⟦eq:BRsplit⟧

structure GQ2.BRDecomposition : Type

Equation (3.4)–(3.6), bundled: a continuous isomorphism B_R = D_R^{ab} ≅ ℤ/2 × ℤ₂ × ℤ₂ sending the torsion generator t = ȳ·x̄⁻², s̄, x̄ to the standard basis. In coordinates (t, s̄, x̄) the row ȳ ↦ (1, 0, 2) is forced (ȳ = t·x̄²).

• e : topAbelianization ↑DR.toProfinite.toTop ≃ₜ* Multiplicative (ZMod 2 × ℤ_[2] × ℤ_[2])

  The coordinate isomorphism B_R ≅ C₂ ⊕ ℤ₂ ⊕ ℤ₂ of ⟦eq:BRsplit⟧.

• map_t : self.e (SectionThree.abMk (drY * (drX ^ 2)⁻¹)) = Multiplicative.ofAdd (1, 0, 0)

  The torsion coordinate: t = ȳ·x̄⁻² ↦ (1,0,0) ⟦eq:tR⟧.

• map_s : self.e (SectionThree.abMk drS) = Multiplicative.ofAdd (0, 1, 0)

  s̄ ↦ (0,1,0).

• map_x : self.e (SectionThree.abMk drX) = Multiplicative.ofAdd (0, 0, 1)

  x̄ ↦ (0,0,1).

theorem GQ2.br_decomposition : Nonempty BRDecomposition

The Roe abelianization decomposition exists ⟦eq:BR⟧/⟦eq:tR⟧/⟦eq:BRsplit⟧: the marked pro-2 abelianization B_R ≅ ℤ/2 × ℤ₂ × ℤ₂ via the coordinate homs t, s̄, x̄.

theorem GQ2.br_decomposition_Y (B : BRDecomposition) : B.e (SectionThree.abMk drY) = Multiplicative.ofAdd (1, 0, 2)

The ȳ-row of the decomposition, forced: ȳ ↦ (1, 0, 2) (ȳ = t·x̄²).

Stress lemmas

theorem GQ2.phiEquivR_generators : phiEquivR (SectionThree.abMk drS) = Multiplicative.ofAdd (0, 1, 0) ∧ phiEquivR (SectionThree.abMk drX) = Multiplicative.ofAdd (0, 0, 1) ∧ phiEquivR (SectionThree.abMk drY) = Multiplicative.ofAdd (1, 0, 2) ∧ phiEquivR (SectionThree.abMk (drY * (drX ^ 2)⁻¹)) = Multiplicative.ofAdd (1, 0, 0)

Stress test (four explicit generators): φ_R sends s̄, x̄, ȳ, t to their coordinate vectors (0,1,0), (0,0,1), (1,0,2), (1,0,0).

theorem GQ2.phiEquivR_relation : phiEquivR ((SectionThree.abMk drX ^ 4)⁻¹ * SectionThree.abMk drY ^ 2) = 1

Stress test (relation collapses to the ZMod 2 component) ⟦eq:BR⟧: the abelianized relator x̄⁴ = ȳ² maps to the identity, i.e. 2ȳ = 4x̄ holds — and modulo s̄, x̄ (the torsion-free part) the only surviving content is the 2-torsion of t.

The C₂-torsion identification and the demushkinQ feed

The torsion subgroup of B_R ≅ ZMod 2 × ℤ₂ × ℤ₂ is the ZMod 2 factor (ℤ₂ is torsion-free), so q = #torsion = 2. This feeds DRDemushkin.demushkinQ_DR.

noncomputable def GQ2.torsionEquivZMod2 : { z : Multiplicative (ZMod 2 × ℤ_[2] × ℤ_[2]) // IsOfFinOrder z } ≃ ZMod 2

Torsion of the model ZMod 2 × ℤ₂ × ℤ₂: the finite-order subtype is in bijection with ZMod 2 (the torsion is exactly the ZMod 2 factor).

Equations

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

theorem GQ2.demushkinQ_DR_eq_two : demushkinQ ↑DR.toProfinite.toTop = 2

q-invariant feed for demushkinQ_DR: demushkinQ D_R = 2 ⟦eq:BR⟧/⟦eq:BRsplit⟧. The topological abelianization is B_R ≅ C₂ ⊕ ℤ₂ ⊕ ℤ₂, whose torsion subgroup is the C₂ factor (order 2). Consumed by GQ2/Roe/DRDemushkin.lean's demushkinQ_DR.

Paper-tag ledger (Roe note paper/roe-presentation-verification.tex; hand-maintained)

• eq. (3.4) = ⟦eq:BR⟧ (abMk_relR, phiEquivR_relation)
• eq. (3.5) = ⟦eq:tR⟧ (t = ȳ·x̄⁻²; map_t, tbarR_sq)
• eq. (3.6) = ⟦eq:BRsplit⟧ (BRDecomposition, br_decomposition, demushkinQ_DR_eq_two)