The free profinite group on a type

The free profinite group on a type X is the profinite completion of the discrete free group on X. This file constructs it together with the data that pins it down: the canonical map freeProfiniteGroup.of from X, the universal property that a map from X to a profinite group extends uniquely to a continuous homomorphism, and the resulting functoriality in X.

The universal property is stated for an unbundled profinite target, so that it applies without first packaging the target as an object of ProfiniteGrp; the target must nevertheless live in the same universe as X, because the completion of a group in Type u is again in Type u. Uniqueness is separated into freeProfiniteGroup.hom_ext, whose target need only be a Hausdorff topological space carrying a group structure, with no IsTopologicalGroup instance required: two continuous homomorphisms that agree on the generators agree on the dense subgroup the generators generate.

Main definitions

• freeProfiniteGroup X: the free profinite group on X, as an object of ProfiniteGrp.
• freeProfiniteGroup.of: the canonical map from X to the free profinite group.
• freeProfiniteGroup.fromFreeGroup: the canonical homomorphism from the discrete free group.
• freeProfiniteGroup.lift: the continuous homomorphism extending a map on generators.
• freeProfiniteGroup.map: the continuous homomorphism induced by a map of generating types.

Main results

• freeProfiniteGroup.dense_closure_range_of: the generators generate topologically.
• freeProfiniteGroup.hom_ext: continuous homomorphisms agreeing on the generators are equal.
• freeProfiniteGroup.existsUnique_lift: the universal property.
• freeProfiniteGroup.map_surjective: a surjection of generating types induces a surjection.
• freeProfiniteGroup.existsUnique_continuousMulEquiv: the free profinite group is unique up to a unique topological isomorphism matching the generators.

References

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

@[reducible, inline]

noncomputable abbrev TauCeti.freeProfiniteGroup (X : Type u) : ProfiniteGrp.{u}

The free profinite group on a type X: the profinite completion of the discrete free group on X. What pins this construction down is its universal property, freeProfiniteGroup.existsUnique_lift.

Equations

• TauCeti.freeProfiniteGroup X = ProfiniteGrp.ProfiniteCompletion.completion ↧(FreeGroup X)

noncomputable def TauCeti.freeProfiniteGroup.fromFreeGroup (X : Type u) : FreeGroup X →* ↑(freeProfiniteGroup X).toProfinite.toTop

The canonical homomorphism from the discrete free group on X to the free profinite group on X. It is Mathlib's unit ProfiniteGrp.ProfiniteCompletion.eta at FreeGroup X, read as a plain monoid homomorphism rather than as a morphism of GrpCat.

Equations

• TauCeti.freeProfiniteGroup.fromFreeGroup X = GrpCat.Hom.hom (ProfiniteGrp.ProfiniteCompletion.eta ↧(FreeGroup X))

noncomputable def TauCeti.freeProfiniteGroup.of {X : Type u} (x : X) : ↑(freeProfiniteGroup X).toProfinite.toTop

The canonical map from the generating type into the free profinite group.

Equations

• TauCeti.freeProfiniteGroup.of x = (TauCeti.freeProfiniteGroup.fromFreeGroup X) (FreeGroup.of x)

@[simp]

theorem TauCeti.freeProfiniteGroup.fromFreeGroup_of {X : Type u} (x : X) : (fromFreeGroup X) (FreeGroup.of x) = of x

fromFreeGroup carries the free-group generator at x to the generator of x.

theorem TauCeti.freeProfiniteGroup.coe_fromFreeGroup (X : Type u) : ⇑(fromFreeGroup X) = ProfiniteGrp.ProfiniteCompletion.etaFn ↧(FreeGroup X)

The underlying function of fromFreeGroup is the unit map into the profinite completion.

theorem TauCeti.freeProfiniteGroup.range_fromFreeGroup (X : Type u) : (fromFreeGroup X).range = Subgroup.closure (Set.range of)

The image of the discrete free group is the subgroup generated by the generators.

theorem TauCeti.freeProfiniteGroup.dense_closure_range_of (X : Type u) : Dense ↑(Subgroup.closure (Set.range of))

The generators generate the free profinite group topologically.

theorem TauCeti.freeProfiniteGroup.hom_ext {X : Type u} {Q : Type v} [Group Q] [TopologicalSpace Q] [T2Space Q] {φ ψ : ↑(freeProfiniteGroup X).toProfinite.toTop →ₜ* Q} (h : ∀ (x : X), φ (of x) = ψ (of x)) : φ = ψ

Two continuous homomorphisms out of the free profinite group that agree on the generators are equal. The target need only be a Hausdorff topological space carrying a group structure; no IsTopologicalGroup Q instance is required.

theorem TauCeti.freeProfiniteGroup.hom_ext_iff {X : Type u} {Q : Type v} [Group Q] [TopologicalSpace Q] [T2Space Q] {φ ψ : ↑(freeProfiniteGroup X).toProfinite.toTop →ₜ* Q} : φ = ψ ↔ ∀ (x : X), φ (of x) = ψ (of x)

noncomputable def TauCeti.freeProfiniteGroup.lift {X P : Type u} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (f : X → P) : ↑(freeProfiniteGroup X).toProfinite.toTop →ₜ* P

The continuous homomorphism to a profinite group P extending a map X → P on the generators.

Equations

• TauCeti.freeProfiniteGroup.lift f = (TauCeti.ProfiniteCompletion.continuousMonoidHomEquiv (FreeGroup X) P).symm (FreeGroup.lift f)

@[simp]

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

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

theorem TauCeti.freeProfiniteGroup.lift_unique {X P : Type u} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (f : X → P) (φ : ↑(freeProfiniteGroup X).toProfinite.toTop →ₜ* P) (hφ : ∀ (x : X), φ (of x) = f x) : φ = lift f

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

theorem TauCeti.freeProfiniteGroup.existsUnique_lift {X P : Type u} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (f : X → P) : ∃! φ : ↑(freeProfiniteGroup X).toProfinite.toTop →ₜ* P, ∀ (x : X), φ (of x) = f x

The universal property of the free profinite group. A map from X to a profinite group extends uniquely to a continuous homomorphism from freeProfiniteGroup X.

@[simp]

theorem TauCeti.freeProfiniteGroup.comp_lift {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] (g : P →ₜ* Q) (f : X → P) : g.comp (lift f) = lift (⇑g ∘ f)

The lift is natural in the target.

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

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

noncomputable def TauCeti.freeProfiniteGroup.map {X Y : Type u} (u : X → Y) : ↑(freeProfiniteGroup X).toProfinite.toTop →ₜ* ↑(freeProfiniteGroup Y).toProfinite.toTop

The continuous homomorphism induced by a map of generating types.

Equations

• TauCeti.freeProfiniteGroup.map u = TauCeti.freeProfiniteGroup.lift (TauCeti.freeProfiniteGroup.of ∘ u)

@[simp]

theorem TauCeti.freeProfiniteGroup.map_of {X Y : Type u} (u : X → Y) (x : X) : (map u) (of x) = of (u x)

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

@[simp]

theorem TauCeti.freeProfiniteGroup.map_id {X : Type u} : map id = ContinuousMonoidHom.id ↑(freeProfiniteGroup X).toProfinite.toTop

map sends the identity to the identity.

@[simp]

theorem TauCeti.freeProfiniteGroup.map_comp {X Y Z : Type u} (u : X → Y) (v : Y → Z) : map (v ∘ u) = (map v).comp (map u)

map is functorial in the generating type.

theorem TauCeti.freeProfiniteGroup.map_surjective {X Y : Type u} {u : X → Y} (hu : Function.Surjective u) : Function.Surjective ⇑(map u)

A surjection of generating types induces a surjection of free profinite groups.

instance TauCeti.freeProfiniteGroup.instSubsingletonCarrierToTopTotallyDisconnectedSpaceToProfiniteOfIsEmpty {X : Type u} [IsEmpty X] : Subsingleton ↑(freeProfiniteGroup X).toProfinite.toTop

The free profinite group on an empty type is trivial.

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

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