The free pro-C group on a pointed topological space

For a class C of finite groups and a pointed topological space (X, x₀), the free pro-C group on (X, x₀) is the pro-C group F_C(X, x₀) with a continuous map X → F_C(X, x₀) sending x₀ to 1 such that every continuous map X → P to a profinite pro-C group P with x₀ ↦ 1 extends uniquely to a continuous homomorphism F_C(X, x₀) → P. When X is a profinite space this is the free pro-C group on a pointed profinite space of Ribes and Zalesskii, §3.3, the object on which the infinite-rank theory of free pro-C groups is built.

The construction quotients the free pro-C group freeProC C X on the underlying type of X by the intersection of its admissible open normal subgroups, those U through which the generator map X → freeProC C X ⧸ U is continuous and kills x₀. Nothing in the construction uses compactness of X, so the definitions and theorems are stated for an arbitrary pointed topological space.

For a discrete X the object is the free pro-C group on the type X ∖ {x₀}. For the one-point compactification S⁺ of a space S, pointed at ∞, the inclusion S → S⁺ induces a continuous surjection freeProC C S → F_C(S⁺, ∞), and for discrete S the images of the points of S converge to 1.

Main definitions

• TauCeti.freeProCPointed: the free pro-C group on a pointed topological space.
• TauCeti.freeProCPointed.of: the canonical continuous map from the space.
• TauCeti.freeProCPointed.lift: the extension of a base-point-preserving continuous map.
• TauCeti.freeProCPointed.map, TauCeti.freeProCPointed.congr: the continuous homomorphism induced by a continuous map of pointed spaces, and the topological isomorphism induced by a homeomorphism of pointed spaces.
• TauCeti.freeProCPointed.equivFreeProC: for a discrete space, the identification with the free pro-C group on the complement of the base point.
• TauCeti.freeProCPointed.fromFreeProC: the surjection from the free pro-C group on S onto the free pro-C group on the pointed one-point compactification of S.

Main results

• TauCeti.isProC_freeProCPointed: the free pro-C group on a pointed space is pro-C; TauCeti.freeProCPointed.isProP_finiteGroupClassP: for C the class of finite p-groups it is pro-p.
• TauCeti.freeProCPointed.continuous_of, TauCeti.freeProCPointed.of_basePoint: the canonical map is continuous and kills the base point.
• TauCeti.freeProCPointed.existsUnique_lift: the universal property.
• TauCeti.freeProCPointed.topologicalClosure_closure_range_of_eq_top: the image of X generates topologically.
• TauCeti.freeProCPointed.fromFreeProC_surjective: the free pro-C group on a type maps onto the free pro-C group on its pointed one-point compactification.
• TauCeti.freeProCPointed.tendsto_of_coe_cofinite_nhds_one: for a discrete space S, the images of the points of S in F_C(S⁺, ∞) converge to 1 along the cofinite filter on S.

References

• L. Ribes and P. Zalesskii, Profinite Groups, Section 3.3.

def TauCeti.freeProCPointed.IsAdmissible (C : FiniteGroupClass) {X : Type u} [TopologicalSpace X] (x₀ : X) (U : OpenNormalSubgroup (freeProC C X)) : Prop

An open normal subgroup U of the free pro-C group on the type X is admissible for the base point x₀ when the composite X → freeProC C X → freeProC C X ⧸ U is continuous and sends x₀ to 1. The admissible subgroups are exactly the finite-quotient shadows of the continuous base-point-preserving maps from X to pro-C groups.

Equations

• TauCeti.freeProCPointed.IsAdmissible C x₀ U = ((Continuous fun (x : X) => ↑(TauCeti.freeProC.of x)) ∧ TauCeti.freeProC.of x₀ ∈ ↑U.toOpenSubgroup)

noncomputable def TauCeti.freeProCPointed.kernel (C : FiniteGroupClass) {X : Type u} [TopologicalSpace X] (x₀ : X) : Subgroup (freeProC C X)

The kernel of the free pro-C group on the pointed space (X, x₀): the intersection of the admissible open normal subgroups of the free pro-C group on the type X.

Equations

• TauCeti.freeProCPointed.kernel C x₀ = ⨅ (U : { U : OpenNormalSubgroup (TauCeti.freeProC C X) // TauCeti.freeProCPointed.IsAdmissible C x₀ U }), ↑(↑U).toOpenSubgroup

theorem TauCeti.freeProCPointed.mem_kernel_iff (C : FiniteGroupClass) {X : Type u} [TopologicalSpace X] (x₀ : X) {y : freeProC C X} : y ∈ kernel C x₀ ↔ ∀ (U : OpenNormalSubgroup (freeProC C X)), IsAdmissible C x₀ U → y ∈ ↑U.toOpenSubgroup

Membership in the kernel, unfolded over the admissible subgroups.

instance TauCeti.freeProCPointed.kernel_normal (C : FiniteGroupClass) {X : Type u} [TopologicalSpace X] (x₀ : X) : (kernel C x₀).Normal

The kernel is a normal subgroup.

instance TauCeti.freeProCPointed.isClosed_kernel (C : FiniteGroupClass) {X : Type u} [TopologicalSpace X] (x₀ : X) : IsClosed ↑(kernel C x₀)

The kernel is closed, so its quotient is profinite.

@[reducible, inline]

abbrev TauCeti.freeProCPointed (C : FiniteGroupClass) {X : Type u} [TopologicalSpace X] (x₀ : X) : Type u

The free pro-C group on the pointed topological space (X, x₀), the quotient of the free pro-C group on the type X by the intersection of the admissible open normal subgroups. What pins it down is its universal property freeProCPointed.existsUnique_lift: continuous maps from X to a profinite pro-C group sending x₀ to 1 correspond to continuous homomorphisms out of it. For a profinite space X this is F_C(X, x₀) of Ribes and Zalesskii, §3.3.

Equations

• TauCeti.freeProCPointed C x₀ = (TauCeti.freeProC C X ⧸ TauCeti.freeProCPointed.kernel C x₀)

theorem TauCeti.isProC_freeProCPointed (C : FiniteGroupClass) {X : Type u} [TopologicalSpace X] (x₀ : X) : IsProC C (freeProCPointed C x₀)

The free pro-C group on a pointed space is pro-C.

theorem TauCeti.freeProCPointed.isProP_finiteGroupClassP {X : Type u} [TopologicalSpace X] (x₀ : X) (p : ℕ) : IsProP p (freeProCPointed (finiteGroupClassP p) x₀)

The free pro-C group on a pointed space, for C the class of finite p-groups, is pro-p.

noncomputable def TauCeti.freeProCPointed.mk (C : FiniteGroupClass) {X : Type u} [TopologicalSpace X] (x₀ : X) : freeProC C X →ₜ* freeProCPointed C x₀

The canonical continuous quotient map from the free pro-C group on the type X to the free pro-C group on the pointed space (X, x₀).

Equations

• TauCeti.freeProCPointed.mk C x₀ = TauCeti.ContinuousMonoidHom.quotientMk (TauCeti.freeProCPointed.kernel C x₀)

theorem TauCeti.freeProCPointed.mk_apply (C : FiniteGroupClass) {X : Type u} [TopologicalSpace X] (x₀ : X) (y : freeProC C X) : (mk C x₀) y = ↑y

The canonical quotient map sends an element to its class.

@[simp]

theorem TauCeti.freeProCPointed.coe_mk (C : FiniteGroupClass) {X : Type u} [TopologicalSpace X] (x₀ : X) : ↑(mk C x₀) = QuotientGroup.mk' (kernel C x₀)

The canonical quotient map, as a monoid homomorphism, is the quotient projection.

theorem TauCeti.freeProCPointed.mk_surjective (C : FiniteGroupClass) {X : Type u} [TopologicalSpace X] (x₀ : X) : Function.Surjective ⇑(mk C x₀)

The canonical quotient map is surjective.

noncomputable def TauCeti.freeProCPointed.of (C : FiniteGroupClass) {X : Type u} [TopologicalSpace X] (x₀ x : X) : freeProCPointed C x₀

The canonical map from the pointed space to its free pro-C group.

Equations

• TauCeti.freeProCPointed.of C x₀ x = (TauCeti.freeProCPointed.mk C x₀) (TauCeti.freeProC.of x)

@[simp]

theorem TauCeti.freeProCPointed.mk_of (C : FiniteGroupClass) {X : Type u} [TopologicalSpace X] (x₀ x : X) : (mk C x₀) (freeProC.of x) = of C x₀ x

The canonical quotient map sends a generator of the free pro-C group on the type X to the image of the corresponding point.

@[simp]

theorem TauCeti.freeProCPointed.coe_freeProC_of (C : FiniteGroupClass) {X : Type u} [TopologicalSpace X] (x₀ x : X) : ↑(freeProC.of x) = of C x₀ x

The class of a generator of the free pro-C group on the type X is the image of the corresponding point.

@[simp]

theorem TauCeti.freeProCPointed.of_basePoint (C : FiniteGroupClass) {X : Type u} [TopologicalSpace X] (x₀ : X) : of C x₀ x₀ = 1

The canonical map kills the base point.

theorem TauCeti.freeProCPointed.continuous_of (C : FiniteGroupClass) {X : Type u} [TopologicalSpace X] (x₀ : X) : Continuous (of C x₀)

The canonical map from the pointed space to its free pro-C group is continuous.

theorem TauCeti.freeProCPointed.topologicalClosure_closure_range_of_eq_top (C : FiniteGroupClass) {X : Type u} [TopologicalSpace X] (x₀ : X) : (Subgroup.closure (Set.range (of C x₀))).topologicalClosure = ⊤

The image of the space generates its free pro-C group topologically.

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

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

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

noncomputable def TauCeti.freeProCPointed.lift {C : FiniteGroupClass} {X : Type u} [TopologicalSpace X] {x₀ : X} {P : Type u} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProC C P) (f : X → P) (hf : Continuous f) (hf₀ : f x₀ = 1) : freeProCPointed C x₀ →ₜ* P

The continuous homomorphism from the free pro-C group on a pointed space to a profinite pro-C group extending a continuous map that kills the base point.

Equations

• TauCeti.freeProCPointed.lift hP f hf hf₀ = TauCeti.ContinuousMonoidHom.quotientLift (TauCeti.freeProCPointed.kernel C x₀) (TauCeti.freeProC.lift hP f) ⋯

@[simp]

theorem TauCeti.freeProCPointed.lift_comp_mk {C : FiniteGroupClass} {X : Type u} [TopologicalSpace X] {x₀ : X} {P : Type u} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProC C P) (f : X → P) (hf : Continuous f) (hf₀ : f x₀ = 1) : (lift hP f hf hf₀).comp (mk C x₀) = freeProC.lift hP f

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

@[simp]

theorem TauCeti.freeProCPointed.lift_mk {C : FiniteGroupClass} {X : Type u} [TopologicalSpace X] {x₀ : X} {P : Type u} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProC C P) (f : X → P) (hf : Continuous f) (hf₀ : f x₀ = 1) (y : freeProC C X) : (lift hP f hf hf₀) ((mk C x₀) y) = (freeProC.lift hP f) y

The lift evaluates on classes as the free pro-C lift.

@[simp]

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

The lift of f agrees with f on the image of the space.

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

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

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

The universal property of the free pro-C group on a pointed space. Every continuous map from X to a profinite pro-C group that sends x₀ to 1 extends uniquely to a continuous homomorphism from freeProCPointed C x₀.

@[simp]

theorem TauCeti.freeProCPointed.comp_lift {C : FiniteGroupClass} {X : Type u} [TopologicalSpace X] {x₀ : 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) (hf : Continuous f) (hf₀ : f x₀ = 1) : g.comp (lift hP f hf hf₀) = lift hQ (⇑g ∘ f) ⋯ ⋯

The lift is natural in its target.

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

A continuous base-point-preserving map whose range generates the target topologically lifts to a surjection.

Functoriality in the pointed space

noncomputable def TauCeti.freeProCPointed.map (C : FiniteGroupClass) {X : Type u} [TopologicalSpace X] {x₀ : X} {Y : Type u} [TopologicalSpace Y] {y₀ : Y} (f : X → Y) (hf : Continuous f) (hf₀ : f x₀ = y₀) : freeProCPointed C x₀ →ₜ* freeProCPointed C y₀

The continuous homomorphism F_C(X, x₀) → F_C(Y, y₀) induced by a continuous map of pointed spaces f : X → Y with f x₀ = y₀: the lift of x ↦ of C y₀ (f x).

Equations

• TauCeti.freeProCPointed.map C f hf hf₀ = TauCeti.freeProCPointed.lift ⋯ (fun (x : X) => TauCeti.freeProCPointed.of C y₀ (f x)) ⋯ ⋯

@[simp]

theorem TauCeti.freeProCPointed.map_of (C : FiniteGroupClass) {X : Type u} [TopologicalSpace X] {x₀ : X} {Y : Type u} [TopologicalSpace Y] {y₀ : Y} (f : X → Y) (hf : Continuous f) (hf₀ : f x₀ = y₀) (x : X) : (map C f hf hf₀) (of C x₀ x) = of C y₀ (f x)

The map induced by f sends the image of a point to the image of its f-image.

@[simp]

theorem TauCeti.freeProCPointed.map_id (C : FiniteGroupClass) {X : Type u} [TopologicalSpace X] {x₀ : X} : map C id ⋯ ⋯ = ContinuousMonoidHom.id (freeProCPointed C x₀)

The identity of the pointed space induces the identity.

theorem TauCeti.freeProCPointed.map_comp (C : FiniteGroupClass) {X : Type u} [TopologicalSpace X] {x₀ : X} {Y : Type u} [TopologicalSpace Y] {y₀ : Y} {Z : Type u} [TopologicalSpace Z] {z₀ : Z} (g : Y → Z) (hg : Continuous g) (hg₀ : g y₀ = z₀) (f : X → Y) (hf : Continuous f) (hf₀ : f x₀ = y₀) : map C (g ∘ f) ⋯ ⋯ = (map C g hg hg₀).comp (map C f hf hf₀)

The map induced by a composite of pointed maps is the composite of the induced maps.

noncomputable def TauCeti.freeProCPointed.congr (C : FiniteGroupClass) {X : Type u} [TopologicalSpace X] {x₀ : X} {Y : Type u} [TopologicalSpace Y] {y₀ : Y} (e : X ≃ₜ Y) (he : e x₀ = y₀) : freeProCPointed C x₀ ≃ₜ* freeProCPointed C y₀

A homeomorphism of pointed spaces induces a topological isomorphism of free pro-C groups F_C(X, x₀) ≃ₜ* F_C(Y, y₀), sending the image of a point to the image of its e-image.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.freeProCPointed.congr_of (C : FiniteGroupClass) {X : Type u} [TopologicalSpace X] {x₀ : X} {Y : Type u} [TopologicalSpace Y] {y₀ : Y} (e : X ≃ₜ Y) (he : e x₀ = y₀) (x : X) : (congr C e he) (of C x₀ x) = of C y₀ (e x)

The isomorphism induced by a pointed homeomorphism e sends the image of a point to the image of its e-image.

@[simp]

theorem TauCeti.freeProCPointed.congr_symm_of (C : FiniteGroupClass) {X : Type u} [TopologicalSpace X] {x₀ : X} {Y : Type u} [TopologicalSpace Y] {y₀ : Y} (e : X ≃ₜ Y) (he : e x₀ = y₀) (y : Y) : (congr C e he).symm (of C y₀ y) = of C x₀ (e.symm y)

The inverse of the isomorphism induced by a pointed homeomorphism e sends the image of a point to the image of its e⁻¹-image.

Discrete spaces

noncomputable def TauCeti.freeProCPointed.equivFreeProC (C : FiniteGroupClass) {X : Type u} [TopologicalSpace X] (x₀ : X) [DiscreteTopology X] : freeProCPointed C x₀ ≃ₜ* freeProC C { x : X // x ≠ x₀ }

For a discrete space, the free pro-C group on (X, x₀) is the free pro-C group on the type X ∖ {x₀}, matching the image of a point other than the base point with the corresponding generator.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.freeProCPointed.equivFreeProC_symm_apply (C : FiniteGroupClass) {X : Type u} [TopologicalSpace X] (x₀ : X) [DiscreteTopology X] (y : freeProC C { x : X // x ≠ x₀ }) : (equivFreeProC C x₀).symm y = (freeProC.lift ⋯ fun (y : { x : X // x ≠ x₀ }) => of C x₀ ↑y) y

The inverse of the identification with the free pro-C group on X ∖ {x₀} is the free pro-C lift of the canonical map.

@[simp]

theorem TauCeti.freeProCPointed.equivFreeProC_symm_of (C : FiniteGroupClass) {X : Type u} [TopologicalSpace X] (x₀ : X) [DiscreteTopology X] (y : { x : X // x ≠ x₀ }) : (equivFreeProC C x₀).symm (freeProC.of y) = of C x₀ ↑y

The inverse of the identification with the free pro-C group on X ∖ {x₀} sends a generator to the image of the corresponding point.

@[simp]

theorem TauCeti.freeProCPointed.equivFreeProC_of (C : FiniteGroupClass) {X : Type u} [TopologicalSpace X] (x₀ : X) [DiscreteTopology X] {x : X} (hx : x ≠ x₀) : (equivFreeProC C x₀) (of C x₀ x) = freeProC.of ⟨x, hx⟩

The identification with the free pro-C group on X ∖ {x₀} sends the image of a point other than the base point to the corresponding generator.

The one-point compactification

noncomputable def TauCeti.freeProCPointed.fromFreeProC (C : FiniteGroupClass) (S : Type u) [TopologicalSpace S] : freeProC C S →ₜ* freeProCPointed C OnePoint.infty

The continuous homomorphism from the free pro-C group on the type S to the free pro-C group on the one-point compactification S⁺ pointed at ∞, induced by the inclusion S → S⁺.

Equations

• TauCeti.freeProCPointed.fromFreeProC C S = TauCeti.freeProC.lift ⋯ fun (s : S) => TauCeti.freeProCPointed.of C OnePoint.infty ↑s

@[simp]

theorem TauCeti.freeProCPointed.fromFreeProC_of (C : FiniteGroupClass) (S : Type u) [TopologicalSpace S] (s : S) : (fromFreeProC C S) (freeProC.of s) = of C OnePoint.infty ↑s

The map from the free pro-C group on S sends a generator to the image of the corresponding point of the one-point compactification.

theorem TauCeti.freeProCPointed.fromFreeProC_surjective (C : FiniteGroupClass) (S : Type u) [TopologicalSpace S] : Function.Surjective ⇑(fromFreeProC C S)

The free pro-C group on S maps onto the free pro-C group on (S⁺, ∞).

theorem TauCeti.freeProCPointed.tendsto_of_coe_cofinite_nhds_one (C : FiniteGroupClass) (S : Type u) [TopologicalSpace S] [DiscreteTopology S] : Filter.Tendsto (fun (s : S) => of C OnePoint.infty ↑s) Filter.cofinite (nhds 1)

The images of the points of a discrete space converge to 1 in the free pro-C group on its pointed one-point compactification: the map s ↦ of C ∞ s tends to 1 along the cofinite filter on S, that is every neighbourhood of 1 contains the images of all but finitely many points of S.

theorem TauCeti.freeProCPointed.convergesToOne_range_of_coe (C : FiniteGroupClass) (S : Type u) [TopologicalSpace S] [DiscreteTopology S] : ConvergesToOne (Set.range fun (s : S) => of C OnePoint.infty ↑s)

The set of images of the points of a discrete space converges to one in the free pro-C group on its pointed one-point compactification, in the sense of TauCeti.ConvergesToOne.