The rank of the free pro-p group on a pointed space

Let (X, x₀) be a pointed topological space and F = F_p(X, x₀) the free pro-p group on it, the free pro-C group freeProCPointed (finiteGroupClassP p) x₀ for C the class of finite p-groups. By the universal property, a continuous 𝔽_p-valued character of F is the same as a continuous map X → 𝔽_p vanishing at x₀, so the continuous 𝔽_p-dual of F is the space of such maps (TauCeti.freeProCPointed.continuousZModDualEquiv), and Burnside's basis theorem in cardinal form gives the rank of F as the 𝔽_p-dimension of that space (TauCeti.freeProCPointed.topologicalGeneratorRank_eq_rank).

For the one-point compactification S⁺ of a discrete space S, pointed at ∞, the continuous maps S⁺ → 𝔽_p vanishing at ∞ are the finitely supported functions on S, so the rank of F_p(S⁺, ∞) is #S (TauCeti.freeProCPointed.topologicalGeneratorRank_onePoint). The free pro-p group on the type S, whose universal property quantifies over all maps S → P, has rank p ^ #S instead when S is infinite (TauCeti.topologicalGeneratorRank_freeProP_of_infinite). Since a topological isomorphism preserves the rank, the continuous surjection freeProC C S → F_C(S⁺, ∞) induced by S → S⁺ is therefore not injective for infinite discrete S at C the class of finite p-groups (TauCeti.freeProCPointed.not_injective_fromFreeProC): the two candidate "free pro-p groups on an infinite set" are different groups, and the one with a basis converging to 1 is the proper quotient.

Main definitions

• TauCeti.freeProCPointed.characterOfContinuousMap: the continuous 𝔽_p-valued character of F_p(X, x₀) extending a continuous map X → 𝔽_p that vanishes at x₀.
• TauCeti.freeProCPointed.continuousZModDualEquiv: the continuous 𝔽_p-dual of F_p(X, x₀) is the space of continuous maps X → 𝔽_p vanishing at x₀.

Main results

• TauCeti.freeProCPointed.topologicalGeneratorRank_eq_rank: the rank of F_p(X, x₀) is the 𝔽_p-dimension of the continuous maps X → 𝔽_p vanishing at x₀.
• TauCeti.freeProCPointed.topologicalGeneratorRank_onePoint: the rank of F_p(S⁺, ∞) is #S for a discrete space S.
• TauCeti.freeProCPointed.not_injective_fromFreeProC: for an infinite discrete S, the surjection from the free pro-p group on the type S onto F_p(S⁺, ∞) is not injective.

References

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

Continuous characters

noncomputable def TauCeti.freeProCPointed.characterOfContinuousMap (p : ℕ) [Fact (Nat.Prime p)] {X : Type u} [TopologicalSpace X] (x₀ : X) (f : C(X, ZMod p)) (hf : f x₀ = 0) : freeProCPointed (finiteGroupClassP p) x₀ →ₜ* Multiplicative (ZMod p)

The continuous 𝔽_p-valued character of the free pro-p group on (X, x₀) extending a continuous map f : X → 𝔽_p with f x₀ = 0: the universal property applied to the finite p-group ℤ/p, lifted to the universe of X.

Equations

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

@[simp]

theorem TauCeti.freeProCPointed.characterOfContinuousMap_of (p : ℕ) [Fact (Nat.Prime p)] {X : Type u} [TopologicalSpace X] (x₀ : X) (f : C(X, ZMod p)) (hf : f x₀ = 0) (x : X) : (characterOfContinuousMap p x₀ f hf) (of (finiteGroupClassP p) x₀ x) = Multiplicative.ofAdd (f x)

The character extending f takes the value f x at the image of x.

noncomputable def TauCeti.freeProCPointed.continuousZModDualEquiv (p : ℕ) [Fact (Nat.Prime p)] {X : Type u} [TopologicalSpace X] (x₀ : X) : continuousZModDual p (freeProCPointed (finiteGroupClassP p) x₀) ≃ₗ[ZMod p] ↥(↑(ContinuousMap.evalCLM (ZMod p) x₀)).ker

The continuous 𝔽_p-dual of the free pro-p group on a pointed space is the space of continuous maps X → 𝔽_p vanishing at the base point, by restriction to the image of X; the inverse is TauCeti.freeProCPointed.characterOfContinuousMap.

Equations

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

@[simp]

theorem TauCeti.freeProCPointed.coe_continuousZModDualEquiv_apply_apply (p : ℕ) [Fact (Nat.Prime p)] {X : Type u} [TopologicalSpace X] (x₀ : X) (φ : continuousZModDual p (freeProCPointed (finiteGroupClassP p) x₀)) (x : X) : ↑((continuousZModDualEquiv p x₀) φ) x = Multiplicative.toAdd ((Additive.toMul φ) (of (finiteGroupClassP p) x₀ x))

@[simp]

theorem TauCeti.freeProCPointed.continuousZModDualEquiv_symm_apply (p : ℕ) [Fact (Nat.Prime p)] {X : Type u} [TopologicalSpace X] (x₀ : X) (f : ↥(↑(ContinuousMap.evalCLM (ZMod p) x₀)).ker) : (continuousZModDualEquiv p x₀).symm f = Additive.ofMul (characterOfContinuousMap p x₀ ↑f ⋯)

Rank

theorem TauCeti.freeProCPointed.topologicalGeneratorRank_eq_rank (p : ℕ) [Fact (Nat.Prime p)] {X : Type u} [TopologicalSpace X] (x₀ : X) : topologicalGeneratorRank (freeProCPointed (finiteGroupClassP p) x₀) = Module.rank (ZMod p) ↥(↑(ContinuousMap.evalCLM (ZMod p) x₀)).ker

The rank of the free pro-p group on a pointed space is the 𝔽_p-dimension of the space of continuous maps X → 𝔽_p vanishing at the base point: Burnside's basis theorem in cardinal form, read through TauCeti.freeProCPointed.continuousZModDualEquiv.

theorem TauCeti.freeProCPointed.topologicalGeneratorRank_onePoint (p : ℕ) [Fact (Nat.Prime p)] (S : Type u) [TopologicalSpace S] [DiscreteTopology S] : topologicalGeneratorRank (freeProCPointed (finiteGroupClassP p) OnePoint.infty) = Cardinal.mk S

The rank of the free pro-p group on the pointed one-point compactification of a discrete space S is #S: the continuous maps S⁺ → 𝔽_p vanishing at ∞ are the finitely supported functions on S.

theorem TauCeti.freeProCPointed.not_injective_fromFreeProC (p : ℕ) [Fact (Nat.Prime p)] (S : Type u) [TopologicalSpace S] [DiscreteTopology S] [Infinite S] : ¬Function.Injective ⇑(fromFreeProC (finiteGroupClassP p) S)

The canonical surjection from the free pro-p group on an infinite type onto the free pro-p group on its pointed one-point compactification is not injective. For an infinite discrete space S, the continuous surjection freeProC C S → F_C(S⁺, ∞) induced by S → S⁺ is not injective when C is the class of finite p-groups: an injective continuous surjection between profinite groups is a topological isomorphism, which would force the ranks p ^ #S of the source and #S of the target to agree.