What a pro-C completion means

Mathematical statement

Let $C$ be a class of finite groups. Let $G$ be a topological group and let $\widehat G_C$ be a profinite group. A continuous homomorphism $\iota:G\to\widehat G_C$ is a pro-$C$ completion when its image is dense, its target has an open normal basis with quotients in $C$, and every continuous homomorphism $\varphi:G\to H$ to a pro-$C$ group has a unique continuous factorization.

Composition with $\iota$ therefore gives $$\operatorname{Hom}_{\mathrm{cont}}(\widehat G_C,H)\cong\operatorname{Hom}_{\mathrm{cont}}(G,H).$$ The quantification is over profinite targets with the specified open normal basis, in the universe used by the declaration.

Lean code

`ProCGroups.Completion.IsProCCompletion`

Published library source ↗Same source in NYLL ↗

structure IsProCCompletion
    (C : ProCGroups.FiniteGroupClass)
    (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (Ghat : Type u) [Group Ghat] [TopologicalSpace Ghat] [IsTopologicalGroup Ghat]
      [CompactSpace Ghat] [T2Space Ghat] [TotallyDisconnectedSpace Ghat]
    (ι : G →ₜ* Ghat) : Prop where
  /--
  Open normal subgroups with quotients in `C` form a neighborhood basis at one in the completed
  group.
  -/
  hasOpenNormalBasisInClass : ProCGroups.ProC.HasOpenNormalBasisInClass C Ghat
  /-- The image of the original group under the completion map is dense in `Ghat`. -/
  denseRange : DenseRange ι
  /--
  Every continuous homomorphism from `G` to a pro-`C` target extends uniquely to a continuous
  homomorphism from `Ghat`.
  -/
  existsUnique_lift :
    ∀ {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
      [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H],
    ProCGroups.ProC.HasOpenNormalBasisInClass C (H) →
      ∀ (φ : G →ₜ* H), ∃! φbar : Ghat →ₜ* H, φbar.comp ι = φ

In-scope Lean context

open scoped Topology

namespace ProCGroups.Completion

universe u v

variable {C : ProCGroups.FiniteGroupClass}

Full declaration and proof

/-- An abstract pro-\(C\) completion of a topological group. -/
structure IsProCCompletion
    (C : ProCGroups.FiniteGroupClass)
    (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (Ghat : Type u) [Group Ghat] [TopologicalSpace Ghat] [IsTopologicalGroup Ghat]
      [CompactSpace Ghat] [T2Space Ghat] [TotallyDisconnectedSpace Ghat]
    (ι : G →ₜ* Ghat) : Prop where
  /--
  Open normal subgroups with quotients in `C` form a neighborhood basis at one in the completed
  group.
  -/
  hasOpenNormalBasisInClass : ProCGroups.ProC.HasOpenNormalBasisInClass C Ghat
  /-- The image of the original group under the completion map is dense in `Ghat`. -/
  denseRange : DenseRange ι
  /--
  Every continuous homomorphism from `G` to a pro-`C` target extends uniquely to a continuous
  homomorphism from `Ghat`.
  -/
  existsUnique_lift :
    ∀ {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
      [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H],
    ProCGroups.ProC.HasOpenNormalBasisInClass C (H) →
      ∀ (φ : G →ₜ* H), ∃! φbar : Ghat →ₜ* H, φbar.comp ι = φ

Source credits and license

Copyright (c) 2026 Naganori Yamaguchi (https://github.com/n-yamaguchi-0729). All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Naganori Yamaguchi (assisted by OpenAI Codex)

References

Luis Ribes and Pavel Zalesskii. Profinite Groups. Springer-Verlag Berlin Heidelberg, 2010. Second edition; Ergebnisse der Mathematik und ihrer Grenzgebiete, 3. Folge, volume 40.