Free pro-C groups

Mathematical statement

Let $C$ be a class of finite groups. Let $X$ be a topological space, $F$ a profinite group, and $\iota:X\to F$ a continuous map. The predicate says that $F$ is pro-$C$, the image of $\iota$ topologically generates $F$, and every continuous map $\varphi:X\to H$ to a pro-$C$ group extends uniquely to a continuous group homomorphism $f:F\to H$.

The required equation is $$f(\iota(x))=\varphi(x)\qquad(x\in X).$$ There is no requirement that $\varphi(X)$ generate $H$: the universal property quantifies over all continuous choices of generator images.

Lean code

`ProCGroups.FreeProC.IsFreeProCGroup`

Published library source ↗Same source in NYLL ↗

structure IsFreeProCGroup
    {X : Type u} [TopologicalSpace X]
    {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
    [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
    (ι : X → F) : Prop where
  /--
  Open normal subgroups with quotients in `C` form a neighborhood basis at one in `F`.
  -/
  hasOpenNormalBasisInClass : ProCGroups.ProC.HasOpenNormalBasisInClass C F
  /-- The canonical map from the generating space into `F` is continuous. -/
  continuous_ι : Continuous ι
  /-- The image of the canonical map topologically generates `F`. -/
  generates_range : Generation.TopologicallyGenerates (G := F) (Set.range ι)
  /--
  Every continuous map from `X` to a pro-`C` target extends to a unique continuous group
  homomorphism from `F`.
  -/
  existsUnique_lift :
    ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
      [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G],
    ProCGroups.ProC.HasOpenNormalBasisInClass C (G) →
      ∀ (φ : X → G), Continuous φ →
        ∃! f : F →* G, Continuous f ∧ ∀ x, f (ι x) = φ x

In-scope Lean context

open Set

open scoped Topology

namespace ProCGroups.FreeProC

universe u v w

open ProCGroups

open ProCGroups.FiniteGeneration

section

variable {C : ProCGroups.FiniteGroupClass}

Full declaration and proof

/--
Free pro-\(C\) groups via a strengthened universal property. The lifting property quantifies
over all continuous maps into pro-\(C\) groups, rather than only maps whose image generates the
target.
-/
structure IsFreeProCGroup
    {X : Type u} [TopologicalSpace X]
    {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
    [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
    (ι : X → F) : Prop where
  /--
  Open normal subgroups with quotients in `C` form a neighborhood basis at one in `F`.
  -/
  hasOpenNormalBasisInClass : ProCGroups.ProC.HasOpenNormalBasisInClass C F
  /-- The canonical map from the generating space into `F` is continuous. -/
  continuous_ι : Continuous ι
  /-- The image of the canonical map topologically generates `F`. -/
  generates_range : Generation.TopologicallyGenerates (G := F) (Set.range ι)
  /--
  Every continuous map from `X` to a pro-`C` target extends to a unique continuous group
  homomorphism from `F`.
  -/
  existsUnique_lift :
    ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
      [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G],
    ProCGroups.ProC.HasOpenNormalBasisInClass C (G) →
      ∀ (φ : X → G), Continuous φ →
        ∃! f : F →* G, Continuous f ∧ ∀ x, f (ι x) = φ x

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.