The closed lower central series of a free pro-p group in degrees zero and one

Let F = freeProP p X be the free pro-p group on a finite type X, with generators x_i = freeProP.of i, and let gr_n(F) = γ_n(F) ⧸ γ_{n+1}(F) be the graded pieces of its closed lower central series, the lower p-series at p = 0. Each gr_n(F) is an abelian pro-p group, hence a ℤ_p-module, and the bracket gr_j(F) × gr_k(F) → gr_{j+k+1}(F) is ℤ_p-bilinear. This file computes the first two pieces:

• gr_0(F) is free over ℤ_p on the classes x_i of the generators: the map a ↦ Σ_i [x_i ^ a_i], (X → ℤ_p) → gr_0(F), is a bijection;
• for X linearly ordered, gr_1(F) is free over ℤ_p on the brackets [x_i, x_j] for i < j: the map c ↦ Σ_{i<j} [⁅x_i, x_j⁆ ^ c_ij] is a bijection. So the bracket identifies gr_1(F) with the exterior square of gr_0(F), of rank #X (#X - 1) / 2;
• in particular [x_i, x_j] ≠ 0 for i ≠ j.

Here g ^ a is the p-adic power TauCeti.IsProP.padicPow. Both maps are ℤ_p-linear, because the class of g ^ a is a times the class of g (TauCeti.IsProP.gradedMk_padicPow), so they exhibit ℤ_p-bases. In contrast to the lower p-series, whose graded pieces are 𝔽_p-vector spaces (TauCeti.freeProP.degreeOneBasis), the p-th powers are not divided out, so the bases are over ℤ_p and gr_1(F) has no p-power part.

Both degrees are proved by detecting homomorphisms supplied by the universal property of F. In degree zero the detector is the exponent-sum map F → ℤ_p^X, through the identification of gr_0(F) with the topological abelianization. In degree one, spanning is the one-term spanning theorem TauCeti.exists_sum_gradedBracket_eq_of_range together with bilinearity and alternation, and the coefficient of [x_i, x_j] is read off by the continuous homomorphism to the Heisenberg group over ℤ_p sending x_i ↦ (1, 0, 0), x_j ↦ (0, 1, 0) and the other generators to 1 (TauCeti.freeProP.exists_heisenberg_detect): its closed lower central series stops at γ_2 = 1, and the commutator of the two images is (0, 0, 1). The exterior square is then recognized by LinearMap.IsAlt.exteriorSquareEquiv, since the alternating bracket carries the ordered pairs of the degree-zero basis to the degree-one basis.

Main definitions

• TauCeti.freeProP.lcsDegreeZeroBasis, TauCeti.freeProP.lcsDegreeOneBasis: the ℤ_p-bases x_i of gr_0(F) and [x_i, x_j], i < j, of gr_1(F) (classes of the generators and their brackets), for the ℤ_p-module structure TauCeti.freeProP.instModulePadicIntLcsGradedPiece.
• TauCeti.freeProP.exteriorSquareEquivLcsGradedPieceOne: the isomorphism ⋀²gr_0(F) ≃ gr_1(F), x ∧ y ↦ [x, y].

Main results

• TauCeti.lcsGradedPiece_zero_freeProP_bijective: the classes of the generators form a ℤ_p-basis of gr_0(F).
• TauCeti.freeProP.exists_heisenberg_detect: the detecting homomorphisms to the Heisenberg group.
• TauCeti.lcsGradedPiece_one_freeProP_bijective: the brackets [x_i, x_j], i < j, form a ℤ_p-basis of gr_1(F).
• TauCeti.lcsBracket_freeProP_ne_zero: the bracket of two distinct generator classes is nonzero.
• TauCeti.freeProP.finrank_lcsGradedPiece_zero, TauCeti.freeProP.finrank_lcsGradedPiece_one: gr_0(F) and gr_1(F) are free of ranks #X and #X choose 2.

References

• J. Labute, Algèbres de Lie et pro-p-groupes définis par une seule relation, Invent. Math. 4 (1967), 142–158.
• J.-P. Serre, Lie Algebras and Lie Groups, Part I, Chapter IV, for discrete free groups.

theorem TauCeti.freeProP.exists_heisenberg_detect {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} {i j : X} (hij : i ≠ j) : ∃ (f : freeProP p X →* HeisenbergGroup ℤ_[p]), Continuous ⇑f ∧ f (of i) = { x := 1, y := 0, z := 0 } ∧ f (of j) = { x := 0, y := 1, z := 0 } ∧ ∀ (k : X), k ≠ i → k ≠ j → f (of k) = 1

The Heisenberg detecting homomorphisms. For distinct i and j there is a continuous homomorphism from the free pro-p group to the Heisenberg group over ℤ_p sending x_i to (1, 0, 0), x_j to (0, 1, 0) and every other generator to 1.

theorem TauCeti.lcsBracket_freeProP_ne_zero {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} {i j : X} (hij : i ≠ j) : ((lcsBracket (freeProP p X) 0 0) (gradedMkZero 0 (freeProP p X) (freeProP.of i))) (gradedMkZero 0 (freeProP p X) (freeProP.of j)) ≠ 0

Nonvanishing of the brackets of generators. In the degree-one piece of the closed lower central series of a free pro-p group, the bracket of the classes of two distinct generators is nonzero.

theorem TauCeti.lcsGradedPiece_zero_freeProP_bijective (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) [Fintype X] : Function.Bijective fun (a : X → ℤ_[p]) => ∑ i : X, gradedMkZero 0 (freeProP p X) (⋯.padicPow (freeProP.of i) (a i))

The degree-zero basis of a free pro-p group. For the free pro-p group F on a finite type X, the classes of the generators form a ℤ_p-basis of the degree-zero piece of the closed lower central series: a ↦ Σ_i [x_i ^ a_i] is a bijection (X → ℤ_p) → gr_0(F). Through TauCeti.lcsGradedPieceZeroEquiv this is the identification of the topological abelianization of F with ℤ_p^X.

theorem TauCeti.lcsGradedPiece_one_freeProP_bijective (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) [Fintype X] [LinearOrder X] : Function.Bijective fun (c : { ij : X × X // ij.1 < ij.2 } → ℤ_[p]) => ∑ ij : { ij : X × X // ij.1 < ij.2 }, gradedMk 0 (freeProP p X) 1 ⟨⋯.padicPow ⁅freeProP.of (↑ij).1, freeProP.of (↑ij).2⁆ (c ij), ⋯⟩

The degree-one basis of a free pro-p group. For the free pro-p group F on a finite linearly ordered type X, the brackets [x_i, x_j] of the generator classes for i < j form a ℤ_p-basis of the degree-one piece of the closed lower central series: the map c ↦ Σ_{i<j} [⁅x_i, x_j⁆ ^ c_ij] is a bijection ({(i, j) | i < j} → ℤ_p) → gr_1(F). It is ℤ_p-linear, because the class of g ^ u is u times the class of g (TauCeti.IsProP.gradedMk_padicPow), so gr_1(F) is the exterior square of gr_0(F), with x_i ∧ x_j ↦ [x_i, x_j].

The bases and the exterior square

@[instance_reducible]

noncomputable instance TauCeti.freeProP.instModulePadicIntLcsGradedPiece {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} (n : ℕ) : Module ℤ_[p] (lcsGradedPiece (freeProP p X) n)

The graded pieces of the closed lower central series of a free pro-p group are ℤ_p-modules, because the free pro-p group is pro-p (TauCeti.isProP_freeProP). This is TauCeti.IsProP.gradedPieceModule, the module structure of the abelian pro-p group γ_n(F) / γ_{n+1}(F).

noncomputable def TauCeti.freeProP.lcsDegreeZeroBasis (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) [Fintype X] : Module.Basis X ℤ_[p] (lcsGradedPiece (freeProP p X) 0)

The ℤ_p-basis of gr_0 of a free pro-p group of finite rank, formed by the classes of the generators x_i (TauCeti.lcsGradedPiece_zero_freeProP_bijective).

@[simp]

theorem TauCeti.freeProP.lcsDegreeZeroBasis_apply (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) [Fintype X] (i : X) : (lcsDegreeZeroBasis p X) i = gradedMkZero 0 (freeProP p X) (of i)

instance TauCeti.freeProP.instFreePadicIntLcsGradedPieceOfNatNatOfFinite (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) [Finite X] : Module.Free ℤ_[p] (lcsGradedPiece (freeProP p X) 0)

instance TauCeti.freeProP.instFinitePadicIntLcsGradedPieceOfNatNatOfFinite (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) [Finite X] : Module.Finite ℤ_[p] (lcsGradedPiece (freeProP p X) 0)

theorem TauCeti.freeProP.finrank_lcsGradedPiece_zero (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) [Fintype X] : Module.finrank ℤ_[p] (lcsGradedPiece (freeProP p X) 0) = Fintype.card X

gr_0 of the free pro-p group on X has rank #X over ℤ_p.

noncomputable def TauCeti.freeProP.lcsDegreeOneBasis (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) [Fintype X] [LinearOrder X] : Module.Basis { ij : X × X // ij.1 < ij.2 } ℤ_[p] (lcsGradedPiece (freeProP p X) 1)

The ℤ_p-basis of gr_1 of a free pro-p group of finite rank, formed by the brackets [x_i, x_j] of the generator classes for i < j (TauCeti.lcsGradedPiece_one_freeProP_bijective).

@[simp]

theorem TauCeti.freeProP.lcsDegreeOneBasis_apply (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) [Fintype X] [LinearOrder X] (ij : { ij : X × X // ij.1 < ij.2 }) : (lcsDegreeOneBasis p X) ij = ((lcsBracket (freeProP p X) 0 0) (gradedMkZero 0 (freeProP p X) (of (↑ij).1))) (gradedMkZero 0 (freeProP p X) (of (↑ij).2))

noncomputable def TauCeti.freeProP.exteriorSquareEquivLcsGradedPieceOne (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) [Fintype X] : ↥(⋀[ℤ_[p]]^2 (lcsGradedPiece (freeProP p X) 0)) ≃ₗ[ℤ_[p]] lcsGradedPiece (freeProP p X) 1

gr_1 of a free pro-p group is the exterior square of gr_0. For the free pro-p group F on a finite type, the graded bracket induces an isomorphism of ℤ_p-modules ⋀²gr_0(F) ≃ gr_1(F), x ∧ y ↦ [x, y] (exteriorSquareEquivLcsGradedPieceOne_ιMulti).

@[simp]

theorem TauCeti.freeProP.exteriorSquareEquivLcsGradedPieceOne_ιMulti (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) [Fintype X] (v : Fin 2 → lcsGradedPiece (freeProP p X) 0) : (exteriorSquareEquivLcsGradedPieceOne p X) ((exteriorPower.ιMulti ℤ_[p] 2) v) = ((lcsBracket (freeProP p X) 0 0) (v 0)) (v 1)

instance TauCeti.freeProP.instFreePadicIntLcsGradedPieceOfNatNatOfFinite_1 (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) [Finite X] : Module.Free ℤ_[p] (lcsGradedPiece (freeProP p X) 1)

instance TauCeti.freeProP.instFinitePadicIntLcsGradedPieceOfNatNatOfFinite_1 (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) [Finite X] : Module.Finite ℤ_[p] (lcsGradedPiece (freeProP p X) 1)

theorem TauCeti.freeProP.finrank_lcsGradedPiece_one (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) [Fintype X] : Module.finrank ℤ_[p] (lcsGradedPiece (freeProP p X) 1) = (Fintype.card X).choose 2

gr_1 of the free pro-p group on X has rank #X choose 2 over ℤ_p.