Free pro-C groups on a type

For a class C of finite groups, the free pro-C group on X is the pro-C completion of the free profinite group on X.

The construction has the expected universal property: a map from X to a pro-C profinite group in the same universe extends uniquely to a continuous homomorphism. Extensionality for homomorphisms out of the free pro-C group only requires a Hausdorff group target, which may live in any universe. The generators generate the free pro-C group topologically, so for finite X it is topologically finitely generated. The file also records functoriality in X and the fact that a surjection of generating types induces a surjection of free groups.

Main definitions

• TauCeti.freeProC: the free pro-C group on a type.
• TauCeti.freeProC.of: its canonical generators.
• TauCeti.freeProC.lift: extension from the generators.
• TauCeti.freeProC.map: functoriality in the generating type.

Main results

• TauCeti.isProC_freeProC: a free pro-C group is pro-C.
• TauCeti.freeProC.topologicalClosure_closure_range_of_eq_top: the generators generate the free pro-C group topologically.
• TauCeti.isTopologicallyFinitelyGenerated_freeProC: for finite X, the free pro-C group on X is topologically finitely generated.
• TauCeti.freeProC.hom_ext: homomorphisms agreeing on the generators are equal.
• TauCeti.freeProC.existsUnique_lift: the universal property.
• TauCeti.freeProC.lift_surjective: a topologically generating map lifts to a surjection.
• TauCeti.freeProC.map_surjective: a surjection of generating types induces a surjection.
• TauCeti.freeProC.existsUnique_continuousMulEquiv: the free pro-C group is unique up to a unique topological isomorphism matching the generators.

References

• L. Ribes and P. Zalesskii, Profinite Groups, Chapter 3.

Free pro-C groups

@[reducible, inline]

noncomputable abbrev TauCeti.freeProC (C : FiniteGroupClass) (X : Type u) : Type u

The free pro-C group on X, obtained by taking the pro-C completion of the free profinite group on X.

Equations

• TauCeti.freeProC C X = TauCeti.proCCompletion C ↑(TauCeti.freeProfiniteGroup X).toProfinite.toTop

theorem TauCeti.isProC_freeProC (C : FiniteGroupClass) (X : Type u) : IsProC C (freeProC C X)

A free pro-C group is pro-C.

noncomputable def TauCeti.freeProC.fromFreeProfiniteGroup (C : FiniteGroupClass) (X : Type u) : ↑(freeProfiniteGroup X).toProfinite.toTop →ₜ* freeProC C X

The canonical continuous quotient map from the free profinite group to the free pro-C group.

Equations

• TauCeti.freeProC.fromFreeProfiniteGroup x✝¹ x✝ = { toMonoidHom := TauCeti.proCCompletion.mk x✝¹ ↑(TauCeti.freeProfiniteGroup x✝).toProfinite.toTop, continuous_toFun := ⋯ }

@[simp]

theorem TauCeti.freeProC.fromFreeProfiniteGroup_apply (C : FiniteGroupClass) (X : Type u) (x : ↑(freeProfiniteGroup X).toProfinite.toTop) : (fromFreeProfiniteGroup C X) x = (proCCompletion.mk C ↑(freeProfiniteGroup X).toProfinite.toTop) x

Evaluation of the canonical quotient map agrees with the underlying quotient homomorphism.

noncomputable def TauCeti.freeProC.of {C : FiniteGroupClass} {X : Type u} (x : X) : freeProC C X

The canonical map from the generating type into the free pro-C group.

Equations

• TauCeti.freeProC.of x = (TauCeti.freeProC.fromFreeProfiniteGroup C X) (TauCeti.freeProfiniteGroup.of x)

@[simp]

theorem TauCeti.freeProC.fromFreeProfiniteGroup_of {C : FiniteGroupClass} {X : Type u} (x : X) : (fromFreeProfiniteGroup C X) (freeProfiniteGroup.of x) = of x

The canonical quotient map sends a free profinite generator to the corresponding free pro-C generator.

theorem TauCeti.freeProC.fromFreeProfiniteGroup_surjective {C : FiniteGroupClass} {X : Type u} : Function.Surjective ⇑(fromFreeProfiniteGroup C X)

The canonical map from the free profinite group to the free pro-C group is surjective.

theorem TauCeti.freeProC.topologicalClosure_closure_range_of_eq_top (C : FiniteGroupClass) (X : Type u) : (Subgroup.closure (Set.range of)).topologicalClosure = ⊤

The canonical generators of a free pro-C group generate it topologically.

theorem TauCeti.isTopologicallyFinitelyGenerated_freeProC (C : FiniteGroupClass) (X : Type u) [Finite X] : IsTopologicallyFinitelyGenerated (freeProC C X)

The free pro-C group on a finite type is topologically finitely generated.

theorem TauCeti.freeProC.hom_ext {C : FiniteGroupClass} {X : Type u} {Q : Type v} [Group Q] [TopologicalSpace Q] [T2Space Q] {f g : freeProC C X →ₜ* Q} (h : ∀ (x : X), f (of x) = g (of x)) : f = g

Two continuous homomorphisms out of a free pro-C group that agree on the generators are equal.

theorem TauCeti.freeProC.hom_ext_iff {C : FiniteGroupClass} {X : Type u} {Q : Type v} [Group Q] [TopologicalSpace Q] [T2Space Q] {f g : freeProC C X →ₜ* Q} : f = g ↔ ∀ (x : X), f (of x) = g (of x)

noncomputable def TauCeti.freeProC.lift {C : FiniteGroupClass} {X P : Type u} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProC C P) (f : X → P) : freeProC C X →ₜ* P

The continuous homomorphism from a free pro-C group extending a map on its generators.

Equations

• TauCeti.freeProC.lift hP f = { toMonoidHom := TauCeti.proCCompletion.lift hP (TauCeti.freeProfiniteGroup.lift f).toMonoidHom ⋯, continuous_toFun := ⋯ }

@[simp]

theorem TauCeti.freeProC.lift_comp_fromFreeProfiniteGroup {C : FiniteGroupClass} {X P : Type u} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProC C P) (f : X → P) : (lift hP f).comp (fromFreeProfiniteGroup C X) = freeProfiniteGroup.lift f

The free pro-C lift recovers the free profinite lift along the quotient map.

@[simp]

theorem TauCeti.freeProC.lift_fromFreeProfiniteGroup {C : FiniteGroupClass} {X P : Type u} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProC C P) (f : X → P) (x : ↑(freeProfiniteGroup X).toProfinite.toTop) : (lift hP f) ↑x = (freeProfiniteGroup.lift f) x

The free pro-C lift evaluates on the image of the free profinite group as the free profinite lift.

@[simp]

theorem TauCeti.freeProC.lift_of {C : FiniteGroupClass} {X P : Type u} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProC C P) (f : X → P) (x : X) : (lift hP f) (of x) = f x

The lift of f agrees with f on every canonical generator.

theorem TauCeti.freeProC.lift_unique {C : FiniteGroupClass} {X P : Type u} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProC C P) (f : X → P) (g : freeProC C X →ₜ* P) (hg : ∀ (x : X), g (of x) = f x) : g = lift hP f

A continuous homomorphism restricting to f on the generators is the canonical lift of f.

theorem TauCeti.freeProC.existsUnique_lift {C : FiniteGroupClass} {X P : Type u} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProC C P) (f : X → P) : ∃! g : freeProC C X →ₜ* P, ∀ (x : X), g (of x) = f x

The universal property of the free pro-C group. Every map from X to a profinite pro-C group extends uniquely to a continuous homomorphism from freeProC C X.

@[simp]

theorem TauCeti.freeProC.comp_lift {C : FiniteGroupClass} {X P : Type u} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q] [CompactSpace Q] [TotallyDisconnectedSpace Q] (hP : IsProC C P) (hQ : IsProC C Q) (g : P →ₜ* Q) (f : X → P) : g.comp (lift hP f) = lift hQ (⇑g ∘ f)

The free pro-C lift is natural in its target.

theorem TauCeti.freeProC.lift_surjective {C : FiniteGroupClass} {X P : Type u} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProC C P) {f : X → P} (hf : Dense ↑(Subgroup.closure (Set.range f))) : Function.Surjective ⇑(lift hP f)

A map whose range generates the target topologically lifts to a surjection.

noncomputable def TauCeti.freeProC.map {C : FiniteGroupClass} {X Y : Type u} (f : X → Y) : freeProC C X →ₜ* freeProC C Y

The continuous homomorphism of free pro-C groups induced by a map of generating types.

Equations

• TauCeti.freeProC.map f = TauCeti.freeProC.lift ⋯ (TauCeti.freeProC.of ∘ f)

@[simp]

theorem TauCeti.freeProC.map_of {C : FiniteGroupClass} {X Y : Type u} (f : X → Y) (x : X) : (map f) (of x) = of (f x)

map f carries the generator at x to the generator at f x.

@[simp]

theorem TauCeti.freeProC.lift_comp_map {C : FiniteGroupClass} {X Y P : Type u} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProC C P) (f : Y → P) (g : X → Y) : (lift hP f).comp (map g) = lift hP (f ∘ g)

The free pro-C lift is natural in the generating type.

@[simp]

theorem TauCeti.freeProC.map_id {C : FiniteGroupClass} {X : Type u} : map id = ContinuousMonoidHom.id (freeProC C X)

Mapping the generating type by the identity induces the identity homomorphism.

@[simp]

theorem TauCeti.freeProC.map_comp {C : FiniteGroupClass} {X Y Z : Type u} (f : X → Y) (g : Y → Z) : map (g ∘ f) = (map g).comp (map f)

The maps induced by maps of generating types compose functorially.

@[simp]

theorem TauCeti.freeProC.map_comp_fromFreeProfiniteGroup {C : FiniteGroupClass} {X Y : Type u} (f : X → Y) : (map f).comp (fromFreeProfiniteGroup C X) = (fromFreeProfiniteGroup C Y).comp (freeProfiniteGroup.map f)

The map induced on free pro-C groups commutes with the canonical maps from the free profinite groups.

@[simp]

theorem TauCeti.freeProC.map_fromFreeProfiniteGroup {C : FiniteGroupClass} {X Y : Type u} (f : X → Y) (x : ↑(freeProfiniteGroup X).toProfinite.toTop) : (map f) ↑x = (fromFreeProfiniteGroup C Y) ((freeProfiniteGroup.map f) x)

The map induced on free pro-C groups evaluates compatibly with the map induced on free profinite groups.

theorem TauCeti.freeProC.map_surjective {C : FiniteGroupClass} {X Y : Type u} {f : X → Y} (hf : Function.Surjective f) : Function.Surjective ⇑(map f)

A surjection of generating types induces a surjection of free pro-C groups.

theorem TauCeti.freeProC.existsUnique_continuousMulEquiv {C : FiniteGroupClass} {X G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProC C G) (ι : X → G) (h : ∀ (P : Type u) [inst : Group P] [inst_1 : TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P], IsProC C P → ∀ (f : X → P), ∃! φ : G →ₜ* P, ∀ (x : X), φ (ι x) = f x) : ∃! e : freeProC C X ≃ₜ* G, ∀ (x : X), e (of x) = ι x

The free pro-C group is unique up to a unique isomorphism. A pro-C group G with a map ι : X → G through which every map from X to a pro-C profinite group factors uniquely is topologically isomorphic to freeProC C X by a unique isomorphism matching the two families of generators.