ProfinitePowerTransfer

Abstract

Continuous finite quotients transfer uniform width to profinite groups.

Definition 1.1 (Bounded algebraic generators).

$$\mathrm{GeneratedByAtMost}(G,d)⟺\exists (S:\mathrm{Finset}(G)),\mathrm{Card}(S)\le d\wedge \mathrm{SubgroupClosure}(S)=\mathrm{TopSubgroup}(G)$$

Formalization. D5/S3/Factorization/Galois/ProfinitePowerTransfer.GeneratedByAtMost (✓ std3).

Source. Repository-derived.

Commentary.

A finite set of at most d elements generates the whole group algebraically. The carrier is arbitrary; the finite-group premise appears in the uniform width proposition.

Definition 1.2 (Uniform width in finite groups).

$$\mathrm{FinitePowerWidth}(d,m,w)⟺\forall (Q:Type),\mathrm{Group}(Q)\wedge \mathrm{Finite}(Q)\Rightarrow \mathrm{GeneratedByAtMost}(Q,d)\Rightarrow \mathrm{HasPowerWidth}(Q,m,w)$$

Formalization. D5/S3/Factorization/Galois/ProfinitePowerTransfer.FinitePowerWidth (✓ std3).

Source. Repository-derived.

Commentary.

For fixed d, m and w, every finite group generated by at most d elements has ordered mth-power width at most w. This definition supplies no proof of that uniform finite-group result.

Theorem 1.3 (Powers descend along homomorphisms).

$$\forall (f:\mathrm{GroupHom}(G,Q)),\forall (g:G),g\in \mathrm{powerSubgroup}(G,m)\Rightarrow f(g)\in \mathrm{powerSubgroup}(Q,m)$$

Proof. Machine-checked in Lean as D5/S3/Factorization/Galois/ProfinitePowerTransfer.map_mem_powerSubgroup (✓ std3). ∎

Source. Repository-derived.

Commentary.

A group homomorphism maps the generated power subgroup into the corresponding power subgroup of its target.

Theorem 1.4 (Ordered products commute with homomorphisms).

$$\forall (f:\mathrm{GroupHom}(G,Q)),\forall (a:\mathrm{Functions}(\mathrm{Fin}(w),G)),f(\mathrm{powerProduct}(m,w,a))=\mathrm{powerProduct}(m,w,i\mapsto f(a(i)))$$

Proof. Machine-checked in Lean as D5/S3/Factorization/Galois/ProfinitePowerTransfer.map_powerProduct (✓ std3). ∎

Source. Repository-derived.

Commentary.

A homomorphism carries an ordered product of powers to the same ordered product of the images.

Theorem 1.5 (Dense generators in finite quotients).

$$\mathrm{CompactTopologicalGroup}(G)\Rightarrow \mathrm{TopologicalClosure}(\mathrm{SubgroupClosure}(S))=\mathrm{TopSubgroup}(G)\Rightarrow \forall (N:\mathrm{OpenNormalSubgroup}(G)),\mathrm{GeneratedByAtMost}(\mathrm{Quotient}(G,N),\mathrm{Card}(S))$$

Proof. Machine-checked in Lean as D5/S3/Factorization/Galois/ProfinitePowerTransfer.finite_quotient_generated (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a compact topological group with a finite set S generating a dense subgroup, the image of S generates each quotient by an open normal subgroup algebraically, with at most S.card generators. These quotient maps are continuous and their targets are finite and discrete.

Theorem 1.6 (Closed-set membership detected by finite quotients).

$$\mathrm{CompactTotallyDisconnectedTopologicalGroup}(G)\Rightarrow \mathrm{IsClosed}(K)\Rightarrow \forall (N:\mathrm{OpenNormalSubgroup}(G)),\exists (k:K),\mathrm{QuotientMap}(N,g)=\mathrm{QuotientMap}(N,k)\Rightarrow g\in K$$

Proof. Machine-checked in Lean as D5/S3/Factorization/Galois/ProfinitePowerTransfer.mem_closed_of_finite_quotients (✓ std3). ∎

Source. Repository-derived.

Commentary.

In a compact totally disconnected topological group, an element lies in a closed set K whenever every quotient by an open normal subgroup identifies it with some element of K. The representatives may depend on the quotient. Open normal neighbourhoods supply separation.

Theorem 1.7 (Uniform finite width transfers to the group).

$$\mathrm{CompactTotallyDisconnectedTopologicalGroup}(G)\Rightarrow \mathrm{TopologicalClosure}(\mathrm{SubgroupClosure}(S))=\mathrm{TopSubgroup}(G)\Rightarrow \mathrm{FinitePowerWidth}(\mathrm{Card}(S),m,w)\Rightarrow \mathrm{HasPowerWidth}(G,m,w)$$

Proof. Machine-checked in Lean as D5/S3/Factorization/Galois/ProfinitePowerTransfer.profinite_hasPowerWidth_of_finite (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a compact totally disconnected topological group with dense generators S, a uniform width bound for all finite groups generated by at most S.card elements gives that same ordered width in the group. Compactness closes the product image; continuous finite quotients detect membership. Hausdorff separation follows from the stated group and disconnectedness assumptions.

Theorem 1.8 (Closed power subgroup from finite width).

$$\mathrm{CompactTotallyDisconnectedTopologicalGroup}(G)\Rightarrow \mathrm{TopologicalClosure}(\mathrm{SubgroupClosure}(S))=\mathrm{TopSubgroup}(G)\Rightarrow \mathrm{FinitePowerWidth}(\mathrm{Card}(S),m,w)\Rightarrow \mathrm{IsClosed}(\mathrm{powerSubgroup}(G,m))$$

Proof. Machine-checked in Lean as D5/S3/Factorization/Galois/ProfinitePowerTransfer.isClosed_powerSubgroup_of_finite_width (✓ std3). ∎

Source. Repository-derived.

Commentary.

Under the preceding compactness, disconnectedness and dense-generation assumptions, uniform width in finite groups implies closedness of the power subgroup.

References

• Truth anchor: D5/S3/Factorization/Galois/ProfinitePowerTransfer.FinitePowerWidth
• Truth anchor: D5/S3/Factorization/Galois/ProfinitePowerTransfer.GeneratedByAtMost
• Truth anchor: D5/S3/Factorization/Galois/ProfinitePowerTransfer.finite_quotient_generated
• Truth anchor: D5/S3/Factorization/Galois/ProfinitePowerTransfer.isClosed_powerSubgroup_of_finite_width
• Truth anchor: D5/S3/Factorization/Galois/ProfinitePowerTransfer.map_mem_powerSubgroup
• Truth anchor: D5/S3/Factorization/Galois/ProfinitePowerTransfer.map_powerProduct
• Truth anchor: D5/S3/Factorization/Galois/ProfinitePowerTransfer.mem_closed_of_finite_quotients
• Truth anchor: D5/S3/Factorization/Galois/ProfinitePowerTransfer.profinite_hasPowerWidth_of_finite
• Dependency: D5/S3/Factorization/Galois/PowerCompactness