The lower 2-central tower λₖ of a topological group (L-campaign ticket L1/L2)

Statements final (ticket L1); fills ticket L2. Design record: docs/orchestration/labute-l1-design.md; mathematical sources: docs/orchestration/ labute-plan.md §2.4 (Tier F) and docs/orchestration/labute-spike.md §1, §2.1, §4.1.

The lower exponent-2 central series (Serre, Bourbaki 252, §6–7: F₁ = F, F_{i+1} = (F_i)² (F, F_i); the spike's λ-series) of a topological group G:

• λ₁ = G, λ_{k+1} = cl(λₖ² [λₖ, G]) — twoCentralSeries G k, 1-based to match the memos' numerology (k₀ = 3, m(k) = k, calculus threshold k ≥ 3, 2^{k-1}-tails). The index 0 is a junk value (λ₀ := ⊤) so that every statement at k ≥ 1 reads exactly as in the memos. All layers are closed by construction.
• Qₖ = G/λₖ — levelQuot G k, with projections levelProj : Q_{k+1} →* Qₖ, the canonical (non-homomorphic) section canonLift, and the two-index images lambdaImage G j k = λⱼλₖ/λₖ ≤ Qₖ.
• Zₖ = λₖ/λ_{k+1} — zLayer G k := lambdaImage G k (k+1) ≤ Q_{k+1}, central and elementary abelian (spike §2.1).
• For topologically f.g. pro-2 G: each λₖ is open, each Qₖ a finite 2-group, the tower is a neighborhood basis of 1, and ⨅ λₖ = ⊥ (plan §2.4). The categorical limit statement G ≅ lim G/λₖ of plan §2.4 is deliberately not frozen here: no L-campaign consumer needs it (the assembly runs through the cofinality statement exists_twoCentralSeries_le + GQ2/Reconstruction.lean) — see the design memo §3.
• Functoriality: the series is verbal, so continuous homs map λₖ into λₖ, with equality for continuous epis of compact groups.
• The χ-shadow layer (spike §2.7.5, §4.1): λₖ(ℤ₂ˣ) ⊆ 1 + 2^{k+1}ℤ₂ for k ≥ 2 (twoCentralSeries_units_le, stated as containment in the kernel of reduction mod 2^{k+1}), and for any continuous χ : G → ℤ₂ˣ the level shadow chiLevel χ k : Qₖ →* (ZMod 2^k)ˣ — precision 2^k, the modulus of the invariant P (m(k) = k, spike §2.4). The spike's finer shadow χ̂ₖ (precision 2^{k+1} on Qₖ) is not a frozen definition; fills needing the extra digit build it locally from twoCentralSeries_units_le (design memo §4).

Commutator conventions (board §10; read before filling)

Two commutator conventions coexist in this development, deliberately:

• Repo convention (GQ2/Words.lean): commP x y = x⁻¹y⁻¹xy, conjP x g = g⁻¹xg. Every word-shape statement of the campaign — the relators drWord/d0Word, the defect, the shift formulas dbarWordR0/dbarWordR2 (StageLemma.lean), and all LS-memo tables — is in commP form; L3/L4 consume the spike's data with no sign translation.
• Mathlib convention: ⁅g, h⁆ = g*h*g⁻¹*h⁻¹ (scoped instance commutatorElement), and the subgroup-level ⁅H, K⁆. It appears in exactly one place: the generating set of twoCentralSucc uses ⁅H, ⊤⁆, to inherit mathlib's commutator-subgroup API (Subgroup.map_commutator etc.) for the functoriality fills.

The two choices generate the same subgroups: commP v g = ⁅v⁻¹, g⁻¹⁆, so with v ranging over a subgroup both families give the same step — the translation lemma is commP_mem_twoCentralSucc below (proved, not sorried). λ-series statements are convention-independent; only element-level formulas care, and those are all commP.

Skeleton discipline: sorrys below are the L2 fill contract (exact inventory in the design memo); the non-sorry lemmas are L1 smoke tests.

The series

def GQ2.Roe.Labute.twoCentralSucc {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (H : Subgroup G) : Subgroup G

One step of the lower 2-central series: H ↦ cl(H²[H, G]), the topological closure of the subgroup generated by the squares of H and the commutators [H, G]. (Serre 252 §6: F_{i+1} = (F_i)^q (F, F_i) at q = 2; spike §1.) Mathlib's commutator subgroup ⁅H, ⊤⁆ is used; it agrees with the subgroup generated by the repo-convention commutators commP v g (commP_mem_twoCentralSucc below).

Equations

• GQ2.Roe.Labute.twoCentralSucc H = (Subgroup.closure ((fun (v : G) => v ^ 2) '' ↑H) ⊔ ⁅H, ⊤⁆).topologicalClosure

theorem GQ2.Roe.Labute.sq_mem_twoCentralSucc {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Subgroup G} {v : G} (hv : v ∈ H) : v ^ 2 ∈ twoCentralSucc H

A square from H lies in twoCentralSucc H.

theorem GQ2.Roe.Labute.commutator_mem_twoCentralSucc {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Subgroup G} {v : G} (hv : v ∈ H) (g : G) : ⁅v, g⁆ ∈ twoCentralSucc H

A mathlib-convention commutator ⁅v, g⁆ with v ∈ H lies in twoCentralSucc H.

theorem GQ2.Roe.Labute.commP_mem_twoCentralSucc {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Subgroup G} {v : G} (hv : v ∈ H) (g : G) : commP v g ∈ twoCentralSucc H

Convention bridge (smoke): a repo-convention commutator commP v g = v⁻¹g⁻¹vg (GQ2/Words.lean) with v ∈ H lies in twoCentralSucc H — so the generating sets of the memos (stated with commP) and the mathlib bracket generate the same step.

theorem GQ2.Roe.Labute.sqClosure_normal {G : Type u_1} [Group G] {H : Subgroup G} (hH : H.Normal) : (Subgroup.closure ((fun (v : G) => v ^ 2) '' ↑H)).Normal

The subgroup of squares of a normal subgroup is normal ((gvg⁻¹)² = gv²g⁻¹).

theorem GQ2.Roe.Labute.twoCentralSuccGen_normal {G : Type u_1} [Group G] {H : Subgroup G} (hH : H.Normal) : (Subgroup.closure ((fun (v : G) => v ^ 2) '' ↑H) ⊔ ⁅H, ⊤⁆).Normal

The generating subgroup H²[H, G] of one step, before taking the closure.

theorem GQ2.Roe.Labute.twoCentralSucc_normal {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Subgroup G} (hH : H.Normal) : (twoCentralSucc H).Normal

One step of the series preserves normality.

theorem GQ2.Roe.Labute.twoCentralSucc_le {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Subgroup G} (hH : H.Normal) (hc : IsClosed ↑H) : twoCentralSucc H ≤ H

One step of the series is contained in its input, for a closed normal subgroup.

theorem GQ2.Roe.Labute.twoCentralSucc_mono {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H K : Subgroup G} (h : H ≤ K) : twoCentralSucc H ≤ twoCentralSucc K

One step of the series is monotone in its input.

def GQ2.Roe.Labute.twoCentralSeries (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : ℕ → Subgroup G

The lower 2-central series λₖ of G, 1-based as in the memos: λ₁ = G, λ_{k+1} = cl(λₖ²[λₖ, G]) (twoCentralSucc). Index 0 is a junk value (λ₀ := ⊤ = λ₁); the recursion genuinely starts at k = 1, so twoCentralSeries_succ below carries the hypothesis 1 ≤ k.

Equations

• GQ2.Roe.Labute.twoCentralSeries G 0 = ⊤
• GQ2.Roe.Labute.twoCentralSeries G 1 = ⊤
• GQ2.Roe.Labute.twoCentralSeries G k.succ.succ = GQ2.Roe.Labute.twoCentralSucc (GQ2.Roe.Labute.twoCentralSeries G (k + 1))

@[simp]

theorem GQ2.Roe.Labute.twoCentralSeries_zero (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : twoCentralSeries G 0 = ⊤

@[simp]

theorem GQ2.Roe.Labute.twoCentralSeries_one (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : twoCentralSeries G 1 = ⊤

theorem GQ2.Roe.Labute.twoCentralSeries_succ (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} (hk : 1 ≤ k) : twoCentralSeries G (k + 1) = twoCentralSucc (twoCentralSeries G k)

The defining recursion, valid from k = 1 (at k = 0 the junk convention breaks it).

theorem GQ2.Roe.Labute.isClosed_twoCentralSeries (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) : IsClosed ↑(twoCentralSeries G k)

Every layer is closed (λ₁ = G and closures thereafter).

theorem GQ2.Roe.Labute.twoCentralSeries_normal (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) : (twoCentralSeries G k).Normal

Each λₖ is a normal subgroup (it is verbal: generated by the values of the words v², [v, g] over λ_{k-1} × G, a conjugation-stable family). Fill: L2.

instance GQ2.Roe.Labute.instNormalTwoCentralSeries (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) : (twoCentralSeries G k).Normal

theorem GQ2.Roe.Labute.twoCentralSeries_antitone (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Antitone (twoCentralSeries G)

The series is decreasing: λ_{k+1} ≤ λₖ and generally antitone. Fill: L2.

theorem GQ2.Roe.Labute.sq_mem_twoCentralSeries_succ (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} {v : G} (hv : v ∈ twoCentralSeries G k) : v ^ 2 ∈ twoCentralSeries G (k + 1)

Squares of λₖ land in λ_{k+1} (also at the junk index k = 0, where λ₁ = ⊤).

theorem GQ2.Roe.Labute.commutator_mem_twoCentralSeries_succ (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} {v : G} (hv : v ∈ twoCentralSeries G k) (g : G) : ⁅v, g⁆ ∈ twoCentralSeries G (k + 1)

Commutators ⁅λₖ, G⁆ land in λ_{k+1} (also at the junk index k = 0).

The level quotients Qₖ, projections, and layer images

@[reducible, inline]

abbrev GQ2.Roe.Labute.levelQuot (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) : Type u_1

The level-k quotient Qₖ = G/λₖ of the memos (finite for topologically f.g. pro-2 G, finite_levelQuot). Q₀ = Q₁ = 1 by the junk convention.

Equations

• GQ2.Roe.Labute.levelQuot G k = (G ⧸ GQ2.Roe.Labute.twoCentralSeries G k)

def GQ2.Roe.Labute.levelMk (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) : G →* levelQuot G k

The canonical projection G →* Qₖ.

Equations

• GQ2.Roe.Labute.levelMk G k = QuotientGroup.mk' (GQ2.Roe.Labute.twoCentralSeries G k)

theorem GQ2.Roe.Labute.levelMk_surjective (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) : Function.Surjective ⇑(levelMk G k)

def GQ2.Roe.Labute.levelProj (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) : levelQuot G (k + 1) →* levelQuot G k

The tower projection Q_{k+1} →* Qₖ (along λ_{k+1} ≤ λₖ).

Equations

• GQ2.Roe.Labute.levelProj G k = QuotientGroup.map (GQ2.Roe.Labute.twoCentralSeries G (k + 1)) (GQ2.Roe.Labute.twoCentralSeries G k) (MonoidHom.id G) ⋯

@[simp]

theorem GQ2.Roe.Labute.levelProj_levelMk (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) (g : G) : (levelProj G k) ((levelMk G (k + 1)) g) = (levelMk G k) g

theorem GQ2.Roe.Labute.levelProj_surjective (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) : Function.Surjective ⇑(levelProj G k)

noncomputable def GQ2.Roe.Labute.canonLift (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) : levelQuot G k → levelQuot G (k + 1)

A canonical set-theoretic section Qₖ → Q_{k+1} of levelProj (not a homomorphism); the canonical lift through which the defect and the stage lemma are stated (GQ2/Roe/Labute/Levelwise.lean, StageLemma.lean). Lift-independence of everything built from it is part of the frozen contract (defectR0_eq_of_lift etc.).

Equations

• GQ2.Roe.Labute.canonLift G k = Function.surjInv ⋯

@[simp]

theorem GQ2.Roe.Labute.levelProj_canonLift (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) (q : levelQuot G k) : (levelProj G k) (canonLift G k q) = q

def GQ2.Roe.Labute.lambdaImage (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (j k : ℕ) : Subgroup (levelQuot G k)

The image λⱼλₖ/λₖ of λⱼ in the level-k quotient Qₖ (interesting for j < k). For j = k - 1 these are the modification spaces of the stage calculus (spike §2.1).

Equations

• GQ2.Roe.Labute.lambdaImage G j k = Subgroup.map (GQ2.Roe.Labute.levelMk G k) (GQ2.Roe.Labute.twoCentralSeries G j)

theorem GQ2.Roe.Labute.levelProj_mem_lambdaImage (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {j k : ℕ} {q : levelQuot G (k + 1)} (hq : q ∈ lambdaImage G j (k + 1)) : (levelProj G k) q ∈ lambdaImage G j k

Projections respect the layer images (smoke).

@[reducible, inline]

abbrev GQ2.Roe.Labute.zLayer (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) : Subgroup (levelQuot G (k + 1))

The graded layer Zₖ = λₖ/λ_{k+1}, realized as a subgroup of Q_{k+1} (the encoding in which the defect, the shift formulas, and the span theorem are stated).

Equations

• GQ2.Roe.Labute.zLayer G k = GQ2.Roe.Labute.lambdaImage G k (k + 1)

theorem GQ2.Roe.Labute.zLayer_eq_ker_levelProj (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) : zLayer G k = (levelProj G k).ker

Zₖ is exactly the kernel of the tower projection. Fill: L2.

theorem GQ2.Roe.Labute.zLayer_le_center (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) : zLayer G k ≤ Subgroup.center (levelQuot G (k + 1))

Zₖ is central in Q_{k+1} (spike §2.1: [λₖ, G] ⊆ λ_{k+1}). Fill: L2.

theorem GQ2.Roe.Labute.zLayer_sq (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} {z : levelQuot G (k + 1)} (hz : z ∈ zLayer G k) : z ^ 2 = 1

Zₖ is elementary abelian: every element squares to 1 (spike §2.1: λₖ² ⊆ λ_{k+1}). Fill: L2.

theorem GQ2.Roe.Labute.levelMk_mul_canonLift_inv_mem_zLayer (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) (g : G) : (levelMk G (k + 1)) g * (canonLift G k ((levelMk G k) g))⁻¹ ∈ zLayer G k

The residue of g in Q_{k+1} and the canonical lift of its residue in Qₖ differ by an element of the central involutive layer Zₖ.

theorem GQ2.Roe.Labute.sq_levelMk_eq_sq_canonLift (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) (g : G) : (levelMk G (k + 1)) g ^ 2 = canonLift G k ((levelMk G k) g) ^ 2

Squaring in Q_{k+1} only depends on the class in Qₖ (Zₖ is central of exponent 2).

theorem GQ2.Roe.Labute.commutator_levelMk_eq_commutator_canonLift (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) (g : G) (y : levelQuot G (k + 1)) : ⁅(levelMk G (k + 1)) g, y⁆ = ⁅canonLift G k ((levelMk G k) g), y⁆

Commutators in Q_{k+1} with a fixed second slot only depend on the class in Qₖ.

Finitely generated elementary abelian subgroups

theorem GQ2.Roe.Labute.finite_closure_of_central_sq {T : Type u_1} [Group T] {K : Subgroup T} (hKc : K ≤ Subgroup.center T) (hK2 : ∀ z ∈ K, z ^ 2 = 1) (F : Finset T) : ↑F ⊆ ↑K → (↑(Subgroup.closure ↑F)).Finite

The subgroup generated by finitely many central involutions is finite.

Functoriality

theorem GQ2.Roe.Labute.map_twoCentralSucc_le {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {A : Subgroup G} {B : Subgroup H} (φ : G →* H) (hφ : Continuous ⇑φ) (hAB : Subgroup.map φ A ≤ B) : Subgroup.map φ (twoCentralSucc A) ≤ twoCentralSucc B

One step of the series is functorial along a continuous homomorphism: if φ carries A into B, it carries cl(A²[A, G]) into cl(B²[B, H]).

theorem GQ2.Roe.Labute.map_twoCentralSeries_le {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (φ : G →* H) (hφ : Continuous ⇑φ) (k : ℕ) : Subgroup.map φ (twoCentralSeries G k) ≤ twoCentralSeries H k

The series is verbal, hence functorial: a continuous homomorphism maps λₖ into λₖ. Fill: L2.

theorem GQ2.Roe.Labute.isClosed_map_of_isClosed {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [Group H] [TopologicalSpace H] [CompactSpace G] [T2Space H] {A : Subgroup G} (φ : G →* H) (hφ : Continuous ⇑φ) (hA : IsClosed ↑A) : IsClosed ↑(Subgroup.map φ A)

The image of a closed subgroup of a compact group under a continuous homomorphism into a Hausdorff group is closed.

theorem GQ2.Roe.Labute.twoCentralSucc_map_le {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace G] [T2Space H] {A : Subgroup G} (φ : G →* H) (hφc : Continuous ⇑φ) (hφs : Function.Surjective ⇑φ) : twoCentralSucc (Subgroup.map φ A) ≤ Subgroup.map φ (twoCentralSucc A)

Reverse containment for one step along a continuous epimorphism of a compact group onto a Hausdorff group: cl((φA)²[φA, H]) ≤ φ(cl(A²[A, G])).

theorem GQ2.Roe.Labute.map_twoCentralSeries_eq {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace G] [T2Space H] (φ : G →* H) (hφc : Continuous ⇑φ) (hφs : Function.Surjective ⇑φ) (k : ℕ) : Subgroup.map φ (twoCentralSeries G k) = twoCentralSeries H k

For a continuous epimorphism of a compact group onto a Hausdorff topological group, the image of λₖ is exactly λₖ (verbal + closed map; the descent mechanism of the span theorem, spike §2.3). Fill: L2.

Finite 2-groups: the tower reaches the trivial subgroup

theorem GQ2.Roe.Labute.twoCentralSucc_eq_bot_of_le_center {Q : Type u_1} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q] [T1Space Q] {N : Subgroup Q} (hNc : N ≤ Subgroup.center Q) (hN2 : ∀ x ∈ N, x ^ 2 = 1) : twoCentralSucc N = ⊥

One step past a central subgroup of exponent 2 is trivial.

theorem GQ2.Roe.Labute.exists_twoCentralSeries_eq_bot_aux (n : ℕ) (Q : Type u_1) [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q] [DiscreteTopology Q] [Finite Q] : IsPGroup 2 Q → Nat.card Q ≤ n → ∃ (k : ℕ), twoCentralSeries Q k = ⊥

The tower of a finite discrete 2-group reaches ⊥. Induction on the order: a nontrivial finite 2-group has a central involution w; the tower of Q ⧸ ⟨w⟩ reaches ⊥, so the tower of Q reaches ⟨w⟩ (central of exponent 2) and one further step kills it.

theorem GQ2.Roe.Labute.exists_twoCentralSeries_eq_bot (Q : Type u_1) [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q] [DiscreteTopology Q] [Finite Q] (hQ : IsPGroup 2 Q) : ∃ (k : ℕ), twoCentralSeries Q k = ⊥

The tower of a finite discrete 2-group reaches ⊥.

Openness, finiteness, and the neighborhood basis (topologically f.g. pro-2 G)

theorem GQ2.Roe.Labute.finite_levelQuot_succ (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) (h1 : Finite (levelQuot G k)) (h2 : Finite ↥(zLayer G k)) : Finite (levelQuot G (k + 1))

Q_{k+1} embeds into Qₖ × Zₖ, so it is finite as soon as both factors are.

theorem GQ2.Roe.Labute.finite_closure_subset_zLayer (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) {F : Set (levelQuot G (k + 1))} (hFfin : F.Finite) (hFZ : F ⊆ ↑(zLayer G k)) : (↑(Subgroup.closure F)).Finite

A subgroup of Q_{k+1} generated by a finite subset of the layer Zₖ is finite.

theorem GQ2.Roe.Labute.isClosed_closure_subset_zLayer (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) {F : Set (levelQuot G (k + 1))} (hFfin : F.Finite) (hFZ : F ⊆ ↑(zLayer G k)) : IsClosed ↑(Subgroup.closure F)

A subgroup generated by a finite subset of Zₖ is closed in Q_{k+1}.

theorem GQ2.Roe.Labute.isClosed_comap_closure_zLayer (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) {F : Set (levelQuot G (k + 1))} (hFfin : F.Finite) (hFZ : F ⊆ ↑(zLayer G k)) : IsClosed ↑(Subgroup.comap (levelMk G (k + 1)) (Subgroup.closure F))

The preimage in G of a subgroup generated by a finite subset of Zₖ is closed.

theorem GQ2.Roe.Labute.zLayer_le_of_le_comap (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) {K : Subgroup (levelQuot G (k + 1))} (h : twoCentralSeries G k ≤ Subgroup.comap (levelMk G (k + 1)) K) : zLayer G k ≤ K

Transfer a containment of λₖ in a preimage to a containment of the layer Zₖ.

theorem GQ2.Roe.Labute.commutator_levelMk_mem_zLayer (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} {v : G} (hv : v ∈ twoCentralSeries G k) (g : G) : (levelMk G (k + 2)) ⁅v, g⁆ ∈ zLayer G (k + 1)

For v ∈ λₖ, the values ⁅v, g⁆ mod λ_{k+2} lie in the central layer Z_{k+1}.

theorem GQ2.Roe.Labute.commLayerHom_mul (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} {v : G} (hv : v ∈ twoCentralSeries G k) (a b : G) : (levelMk G (k + 2)) ⁅v, a * b⁆ = (levelMk G (k + 2)) ⁅v, a⁆ * (levelMk G (k + 2)) ⁅v, b⁆

Bilinearity of the commutator modulo λ_{k+2}: for v ∈ λₖ the map g ↦ ⁅v, g⁆ mod λ_{k+2} is a homomorphism, because its values are central in Q_{k+2}.

def GQ2.Roe.Labute.commLayerHom (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} {v : G} (hv : v ∈ twoCentralSeries G k) : G →* levelQuot G (k + 2)

The homomorphism g ↦ ⁅v, g⁆ mod λ_{k+2} attached to v ∈ λₖ.

Equations

• GQ2.Roe.Labute.commLayerHom G hv = MonoidHom.mk' (fun (h : G) => (GQ2.Roe.Labute.levelMk G (k + 2)) ⁅v, h⁆) ⋯

@[simp]

theorem GQ2.Roe.Labute.commLayerHom_apply (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} {v : G} (hv : v ∈ twoCentralSeries G k) (g : G) : (commLayerHom G hv) g = (levelMk G (k + 2)) ⁅v, g⁆

theorem GQ2.Roe.Labute.continuous_commLayerHom (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} {v : G} (hv : v ∈ twoCentralSeries G k) : Continuous ⇑(commLayerHom G hv)

theorem GQ2.Roe.Labute.finite_levelQuot_two (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (hfg : ∃ (s : Finset G), (Subgroup.closure ↑s).topologicalClosure = ⊤) : Finite (levelQuot G 2)

Base of the finiteness induction: Q₂ = G/λ₂ is generated by the residues of a topological generating set, and is abelian of exponent 2, hence finite.

theorem GQ2.Roe.Labute.finite_levelQuot_step (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (hfg : ∃ (s : Finset G), (Subgroup.closure ↑s).topologicalClosure = ⊤) {k : ℕ} (hk : 1 ≤ k) (h : Finite (levelQuot G (k + 1))) : Finite (levelQuot G (k + 2))

Inductive step of the finiteness statement (k ≥ 1): the layer Z_{k+1} is generated by the finitely many square- and commutator-classes coming from Q_{k+1} and the generating set.

theorem GQ2.Roe.Labute.finite_levelQuot (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] (hfg : ∃ (s : Finset G), (Subgroup.closure ↑s).topologicalClosure = ⊤) (hpro : IsProP 2 G) (k : ℕ) : Finite (levelQuot G k)

The level quotients of a topologically f.g. pro-2 group are finite. Fill: L2.

theorem GQ2.Roe.Labute.isOpen_twoCentralSeries (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] (hfg : ∃ (s : Finset G), (Subgroup.closure ↑s).topologicalClosure = ⊤) (hpro : IsProP 2 G) (k : ℕ) : IsOpen ↑(twoCentralSeries G k)

For a topologically finitely generated pro-2 group, every λₖ is open. (Openness at each step: λₖ/λ_{k+1} is generated by finitely many square/commutator classes of exponent 2 — plan §2.4.) Fill: L2.

theorem GQ2.Roe.Labute.isPGroup_levelQuot (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] (hfg : ∃ (s : Finset G), (Subgroup.closure ↑s).topologicalClosure = ⊤) (hpro : IsProP 2 G) (k : ℕ) : IsPGroup 2 (levelQuot G k)

The level quotients are 2-groups. Fill: L2.

theorem GQ2.Roe.Labute.exists_twoCentralSeries_le (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] (hfg : ∃ (s : Finset G), (Subgroup.closure ↑s).topologicalClosure = ⊤) (hpro : IsProP 2 G) {U : Subgroup G} (hU : IsOpen ↑U) : ∃ (k : ℕ), twoCentralSeries G k ≤ U

Neighborhood-basis / cofinality (plan §2.1 item 2, §2.4): every open subgroup of a topologically f.g. pro-2 group contains some λₖ (via: the finite 2-group G/core is nilpotent with 2-central series reaching 1). This is the statement through which the λ-tower levelwise data reaches all open normal subgroups in the assembly (GQ2/Roe/Labute/Assembly.lean). Fill: L2.

theorem GQ2.Roe.Labute.iInf_twoCentralSeries (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] (hfg : ∃ (s : Finset G), (Subgroup.closure ↑s).topologicalClosure = ⊤) (hpro : IsProP 2 G) : ⨅ (k : ℕ), twoCentralSeries G k = ⊥

The tower separates points: ⨅ λₖ = ⊥ (plan §2.4's ⋂ λₖ = 1). Fill: L2.

The χ-shadow layer (spike §2.7.5, §4.1)

The λ-series of ℤ₂ˣ sits inside the principal-unit filtration one step deeper than the index (λₖ(ℤ₂ˣ) = 1 + 2^{k+1}ℤ₂ for k ≥ 2; only ⊆ is frozen — the reverse inclusion has no consumer). Consequently every continuous character χ : G → ℤ₂ˣ has a level-k shadow Qₖ →* (ZMod 2^k)ˣ: the invariant P's χ-clause at modulus 2^k = 2^{m(k)} (spike §2.4) is stated through it.

theorem GQ2.Roe.Labute.mem_ker_units_toZModPow_iff {n : ℕ} {u : ℤ_[2]ˣ} : u ∈ (Units.map ↑(PadicInt.toZModPow n)).ker ↔ ↑2 ^ n ∣ ↑u - 1

Membership in the mod-2ⁿ kernel of ℤ₂ˣ, spelled as a divisibility (u ≡ 1 mod 2ⁿ).

theorem GQ2.Roe.Labute.ker_units_toZModPow_antitone {m n : ℕ} (h : m ≤ n) {u : ℤ_[2]ˣ} (hu : u ∈ (Units.map ↑(PadicInt.toZModPow n)).ker) : u ∈ (Units.map ↑(PadicInt.toZModPow m)).ker

The mod-2ⁿ kernels of ℤ₂ˣ decrease with n.

theorem GQ2.Roe.Labute.isClosed_ker_units_toZModPow (n : ℕ) : IsClosed ↑(Units.map ↑(PadicInt.toZModPow n)).ker

The mod-2ⁿ kernel of ℤ₂ˣ is closed: it is the preimage of a closed ball of ℤ₂.

theorem GQ2.Roe.Labute.twoCentralSeries_units_le (k : ℕ) (hk : 2 ≤ k) : twoCentralSeries ℤ_[2]ˣ k ≤ (Units.map ↑(PadicInt.toZModPow (k + 1))).ker

The modulus lemma (spike §2.4, "exact, elementary" — only the containment direction is frozen): for k ≥ 2, λₖ(ℤ₂ˣ) ⊆ 1 + 2^{k+1}ℤ₂, encoded as the kernel of the unit-group reduction mod 2^{k+1}. Fill: L2.

theorem GQ2.Roe.Labute.chiShadow_eq_one_of_mem {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (χ : G →ₜ* ℤ_[2]ˣ) (k : ℕ) {g : G} (hg : g ∈ twoCentralSeries G k) : (Units.map ↑(PadicInt.toZModPow k)) (χ g) = 1

The λ-layers die in the mod-2^k shadow of any continuous character: for g ∈ λₖ(G), χ g ≡ 1 (mod 2^k). (For k ≤ 1 the target (ZMod 2^k)ˣ is trivial; for k ≥ 2 this is map_twoCentralSeries_le + twoCentralSeries_units_le one precision step down.) Fill: L2.

noncomputable def GQ2.Roe.Labute.chiLevel {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (χ : G →ₜ* ℤ_[2]ˣ) (k : ℕ) : levelQuot G k →* (ZMod (2 ^ k))ˣ

The level-k χ-shadow χ̄ₖ : Qₖ →* (ZMod 2^k)ˣ of a continuous character χ : G → ℤ₂ˣ — precision 2^k, the modulus m(k) = k of the invariant P (spike §2.4). Total in k (no side condition): for k ≤ 1 the target is trivial.

Equations

• GQ2.Roe.Labute.chiLevel χ k = QuotientGroup.lift (GQ2.Roe.Labute.twoCentralSeries G k) ((Units.map ↑(PadicInt.toZModPow k)).comp χ.toMonoidHom) ⋯

@[simp]

theorem GQ2.Roe.Labute.chiLevel_levelMk {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (χ : G →ₜ* ℤ_[2]ˣ) (k : ℕ) (g : G) : (chiLevel χ k) ((levelMk G k) g) = (Units.map ↑(PadicInt.toZModPow k)) (χ g)

Evaluation of the shadow on residues (smoke).

theorem GQ2.Roe.Labute.chiLevel_levelProj {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (χ : G →ₜ* ℤ_[2]ˣ) (k : ℕ) (q : levelQuot G (k + 1)) : (chiLevel χ k) ((levelProj G k) q) = (Units.map ↑(ZMod.castHom ⋯ (ZMod (2 ^ k)))) ((chiLevel χ (k + 1)) q)

Naturality of the shadows in k: reading the level-(k+1) shadow mod 2^k recovers the level-k shadow through the tower projection. (The mod-2^{k+1} clause of P at level k+1 weakens to the mod-2^k clause at level k — the restriction-map direction of the levelwise sets.) Fill: L2.