The abelianization of a free pro-p group of finite rank

Let F = freeProP p X be the free pro-p group on a finite type X. Its topological abelianization F^{ab} = F ⧸ closure [F, F] is the free abelian pro-p group on X, namely ℤ_p^X. The isomorphism sends the class of the generator at x to the coordinate vector e_x, and its inverse sends u : X → ℤ_p to ∏ x, x_x ^ (u x), the product of the p-adic powers of the classes of the generators.

Both directions come from universal properties. The exponent-sum map exponentSum : F →ₜ* Multiplicative (X → ℤ_[p]) is the lift of x ↦ e_x; it reads off the p-adic exponent of each generator in an element of F, and being a continuous homomorphism to an abelian group it factors through F^{ab}. Conversely ℤ_p^X is topologically generated by the coordinate vectors, so a continuous homomorphism out of it is determined by their images, and this uniqueness shows that the two composites are identities.

For a presented pro-p group F ⧸ R the abelianization is the quotient of ℤ_p^X by the image of R; see TauCeti.Topology.Algebra.Group.Profinite.Presentation.Abelianization.

Main definitions

• TauCeti.freeProP.exponentSum: the exponent-sum map freeProP p X →ₜ* Multiplicative (X → ℤ_[p]), sending the generator at x to the coordinate vector at x.
• TauCeti.freeProP.abelianizationEquiv: the topological isomorphism TopologicalAbelianization (freeProP p X) ≃ₜ* Multiplicative (X → ℤ_[p]) induced by the exponent-sum map.
• TauCeti.freeProP.exponentSumZModPow: the i-th exponent sum modulo p ^ k, as a continuous character freeProP p X →ₜ* ULift (Multiplicative (ZMod (p ^ k))).

Main results

• TauCeti.freeProP.abelianizationEquiv_mk, TauCeti.freeProP.abelianizationEquiv_symm_ofAdd: the isomorphism is induced by exponentSum, and its inverse is u ↦ ∏ x, x_x ^ (u x).
• TauCeti.freeProP.exponentSum_surjective, TauCeti.freeProP.exponentSum_eq_one_iff: the exponent-sum map is surjective, and its kernel is the closed commutator subgroup.
• TauCeti.freeProP.toAdd_exponentSum_eq_single_iff: the exponent vector of y is q e_{x₀} exactly when y is x₀ ^ q times an element of the closed commutator subgroup.
• TauCeti.freeProP.dvd_exponentSum_of_mem_proPFrattini: the exponent sums of an element of the pro-p Frattini subgroup are divisible by p.
• TauCeti.freeProP.apply_eq_prod_padicPow_exponentSum: a continuous homomorphism to a commutative pro-p group is computed by the exponent sums, ψ y = ∏ x, ψ (x_x) ^ (u x) for u = exponentSum y.

References

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

noncomputable def TauCeti.freeProP.exponentSum (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) : freeProP p X →ₜ* Multiplicative (X → ℤ_[p])

The exponent-sum map of the free pro-p group on X: the continuous homomorphism to ℤ_p^X sending the generator at x to the coordinate vector e_x. On a word in the generators it records the total exponent of each generator; it induces the abelianization isomorphism TauCeti.freeProP.abelianizationEquiv.

Equations

• TauCeti.freeProP.exponentSum p X = TauCeti.freeProP.lift ⋯ fun (x : X) => Multiplicative.ofAdd (Pi.single x 1)

@[simp]

theorem TauCeti.freeProP.exponentSum_of (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) [DecidableEq X] (x : X) : (exponentSum p X) (of x) = Multiplicative.ofAdd (Pi.single x 1)

theorem TauCeti.freeProP.toAdd_exponentSum_of_pow_apply (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) [DecidableEq X] (i : X) (n : ℕ) (k : X) : Multiplicative.toAdd ((exponentSum p X) (of i ^ n)) k = ↑(if k = i then n else 0)

The exponent vector of the power x_i ^ n of a generator is n at i and 0 elsewhere.

@[simp]

theorem TauCeti.freeProP.exponentSum_padicPow_of (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) [DecidableEq X] (x : X) (a : ℤ_[p]) : (exponentSum p X) (⋯.padicPow (of x) a) = Multiplicative.ofAdd (Pi.single x a)

The exponent vector of the p-adic power x ^ a of the generator at x is a e_x.

@[simp]

theorem TauCeti.freeProP.toAdd_exponentSum_freeProPGen_apply (p : ℕ) [Fact (Nat.Prime p)] {n : ℕ} (i : ℕ) (j : Fin n) : Multiplicative.toAdd ((exponentSum p (Fin n)) (freeProPGen p n i)) j = if ↑j = i then 1 else 0

The exponent vector of the i-th ℕ-indexed generator of freeProP p (Fin n) is the coordinate vector at i; out of range it is 0.

theorem TauCeti.freeProP.dvd_exponentSum_of_mem_proPFrattini (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) {y : freeProP p X} (hy : y ∈ proPFrattini p (freeProP p X)) (x : X) : ↑p ∣ Multiplicative.toAdd ((exponentSum p X) y) x

The exponent sums of an element of the Frattini subgroup are divisible by p. The reduction modulo p of the exponent sum at x is the continuous 𝔽_p-valued character TauCeti.freeProP.characterOfFun with value 1 at x and 0 at the other generators, and every such character kills the pro-p Frattini subgroup.

The exponent sums modulo p ^ k

noncomputable def TauCeti.freeProP.exponentSumZModPow (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) (k : ℕ) (i : X) : freeProP p X →ₜ* ULift.{u, 0} (Multiplicative (ZMod (p ^ k)))

The i-th exponent sum modulo p ^ k, as a continuous character of the free pro-p group into the discrete cyclic group ℤ/pᵏ, written multiplicatively and lifted to the universe of X: it sends y to the reduction modulo p ^ k of the exponent of the generator x_i in y. It takes the generator x_i to the standard generator of ℤ/pᵏ and kills the other generators, so it reads off the coefficient of x_i on the graded pieces of the lower p-series.

Equations

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

theorem TauCeti.freeProP.exponentSumZModPow_apply (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) (k : ℕ) (i : X) (y : freeProP p X) : (exponentSumZModPow p X k i) y = MulEquiv.ulift.symm (Multiplicative.ofAdd ((PadicInt.toZModPow k) (Multiplicative.toAdd ((exponentSum p X) y) i)))

@[simp]

theorem TauCeti.freeProP.exponentSumZModPow_eq_one_iff (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) (k : ℕ) (i : X) (y : freeProP p X) : (exponentSumZModPow p X k i) y = 1 ↔ ↑p ^ k ∣ Multiplicative.toAdd ((exponentSum p X) y) i

The i-th exponent sum modulo p ^ k of y vanishes exactly when p ^ k divides the i-th exponent sum of y.

@[simp]

theorem TauCeti.freeProP.exponentSumZModPow_of_self (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) (k : ℕ) (i : X) : (exponentSumZModPow p X k i) (of i) = MulEquiv.ulift.symm (Multiplicative.ofAdd 1)

The i-th exponent sum modulo p ^ k sends the generator x_i to the standard generator of ℤ/pᵏ.

@[simp]

theorem TauCeti.freeProP.exponentSumZModPow_of_of_ne (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) (k : ℕ) {i j : X} (hij : j ≠ i) : (exponentSumZModPow p X k i) (of j) = 1

The i-th exponent sum modulo p ^ k kills the generators other than x_i.

noncomputable def TauCeti.freeProP.abelianizationEquiv (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) [Finite X] : TopologicalAbelianization (freeProP p X) ≃ₜ* Multiplicative (X → ℤ_[p])

The abelianization of a free pro-p group of finite rank is ℤ_p^X. The topological abelianization of freeProP p X is topologically isomorphic to the additive group ℤ_p^X, by the isomorphism induced by the exponent-sum map: the class of the generator at x corresponds to the coordinate vector at x, and u : X → ℤ_p corresponds to ∏ x, x_x ^ (u x).

Equations

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

@[simp]

theorem TauCeti.freeProP.abelianizationEquiv_mk (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) [Finite X] (y : freeProP p X) : (abelianizationEquiv p X) ↑y = (exponentSum p X) y

The abelianization isomorphism is induced by the exponent-sum map.

theorem TauCeti.freeProP.abelianizationEquiv_mk_of (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) [Finite X] [DecidableEq X] (x : X) : (abelianizationEquiv p X) ↑(of x) = Multiplicative.ofAdd (Pi.single x 1)

The abelianization isomorphism sends the class of the generator at x to the coordinate vector at x.

theorem TauCeti.freeProP.abelianizationEquiv_symm_ofAdd (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) [Finite X] [Fintype X] (u : X → ℤ_[p]) : (abelianizationEquiv p X).symm (Multiplicative.ofAdd u) = ∏ x : X, ⋯.padicPow (↑(of x)) (u x)

The inverse of the abelianization isomorphism sends u : X → ℤ_p to ∏ x, x_x ^ (u x), the product of the p-adic powers of the classes of the generators.

@[simp]

theorem TauCeti.freeProP.abelianizationEquiv_symm_ofAdd_single (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) [Finite X] [DecidableEq X] (x : X) : (abelianizationEquiv p X).symm (Multiplicative.ofAdd (Pi.single x 1)) = ↑(of x)

The inverse of the abelianization isomorphism sends the coordinate vector at x to the class of the generator at x.

theorem TauCeti.freeProP.exponentSum_surjective (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) [Finite X] : Function.Surjective ⇑(exponentSum p X)

The exponent-sum map of a free pro-p group of finite rank is surjective.

theorem TauCeti.freeProP.exponentSum_eq_one_iff (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) [Finite X] (y : freeProP p X) : (exponentSum p X) y = 1 ↔ y ∈ (commutator (freeProP p X)).topologicalClosure

The kernel of the exponent-sum map is the closed commutator subgroup: for X finite, exponentSum y = 1 exactly when y lies in the closure of the commutator subgroup of the free pro-p group.

theorem TauCeti.freeProP.toAdd_exponentSum_eq_single_iff (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) [Finite X] [DecidableEq X] (y : freeProP p X) (x₀ : X) (q : ℤ_[p]) : Multiplicative.toAdd ((exponentSum p X) y) = Pi.single x₀ q ↔ (⋯.padicPow (of x₀) q)⁻¹ * y ∈ (commutator (freeProP p X)).topologicalClosure

Exponent vector supported at one generator. For X finite, the exponent vector of y is q e_{x₀} exactly when (x₀ ^ q)⁻¹ · y lies in the closed commutator subgroup, that is when y is x₀ ^ q times an element of the closed commutator subgroup of the free pro-p group.

theorem TauCeti.freeProP.apply_eq_prod_padicPow_exponentSum (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) [Finite X] [Fintype X] {A : Type u_1} [CommGroup A] [TopologicalSpace A] [IsTopologicalGroup A] [CompactSpace A] [TotallyDisconnectedSpace A] (hA : IsProP p A) (ψ : freeProP p X →ₜ* A) (y : freeProP p X) : ψ y = ∏ x : X, hA.padicPow (ψ (of x)) (Multiplicative.toAdd ((exponentSum p X) y) x)

A continuous homomorphism from a free pro-p group of finite rank to a commutative pro-p group is computed by the exponent sums: ψ y = ∏ x, ψ (x_x) ^ (u x) for u = exponentSum y, the powers being the p-adic powers of the target.

theorem TauCeti.freeProP.toAdd_exponentSum_apply_eq_sum_smul (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) [Finite X] [Fintype X] {Y : Type v} (φ : freeProP p X →ₜ* freeProP p Y) (y : freeProP p X) : Multiplicative.toAdd ((exponentSum p Y) (φ y)) = ∑ x : X, Multiplicative.toAdd ((exponentSum p X) y) x • Multiplicative.toAdd ((exponentSum p Y) (φ (of x)))

The exponent vector under a continuous homomorphism of free pro-p groups is the linear image of the exponent vector: exponentSum (φ y) = ∑ x, (exponentSum y)_x • exponentSum (φ x_x). The vectors exponentSum (φ x_x) are the columns of the matrix of the abelianization of φ.