Elementary automorphisms of a free pro-p group and the exponent vector of a relator

Let F = freeProP p X be the free pro-p group on a type X. This file studies the two kinds of elementary automorphisms of F that act on the exponent vector TauCeti.freeProP.exponentSum in ℤ_p^X through elementary matrices, computes that action, and uses them, for X finite, to normalise the exponent vector of an arbitrary element of F:

• TauCeti.freeProP.congr σ, for a bijection σ of the generating type, permutes the generators; it permutes the coordinates of the exponent vector.
• TauCeti.freeProP.transvection x₀ x hx a, for x ≠ x₀ and a p-adic exponent a, sends the generator at x₀ to x₀ · x ^ a and fixes the other generators; its inverse is the transvection with exponent -a, and it adds a times the coordinate at x₀ to the coordinate at x of the exponent vector.
• TauCeti.freeProP.dilation x₀ u, for a unit u of ℤ_p, raises the generator at x₀ to its p-adic power u and fixes the other generators; its inverse is the dilation by u⁻¹, and it multiplies the coordinate at x₀ of the exponent vector by u.

It also defines the composite TauCeti.freeProP.symplecticTransvection hn3 c of two transvections of the free pro-p group on n ≥ 4 generators, x₂ ↦ x₂ x₄^c and x₃ ↦ x₃ x₁^{-c}, which fixes the other generators; this is the change of basis of Labute's classification of the dyadic Demushkin groups of even rank, where it preserves the class of the relator modulo λ_2.

The normalisation is the elimination step of Labute's classification of Demushkin groups: if the exponent vector of r ∈ F is q • w with w x₀ = 1, then some automorphism e of F has exponentSum (e r) = q e_{x₀}, that is e r ∈ x₀ ^ q · [F, F] by TauCeti.freeProP.toAdd_exponentSum_eq_single_iff (TauCeti.freeProP.exists_continuousMulEquiv_toAdd_exponentSum_eq_single_of_eq_smul). Since ℤ_p is a valuation ring, some coordinate of the exponent vector divides all the others, so every r admits such a normalisation, with the pivot coordinate placed at any prescribed generator (TauCeti.freeProP.exists_continuousMulEquiv_toAdd_exponentSum_eq_single_of_forall_dvd, TauCeti.freeProP.exists_continuousMulEquiv_toAdd_exponentSum_eq_single). For a one-relator pro-p group ⟨X ∣ r⟩ this is the statement that, after a change of basis of F, the relator is x₀ ^ q times an element of the closed commutator subgroup, where q generates the ideal of ℤ_p spanned by the exponent sums of r; the abelianization of the group is then ℤ_p^{X ∖ {x₀}} × ℤ_p ⧸ q ℤ_p, so q is the coordinate whose p-adic valuation the one-relator abelianization structure theorem reads off.

Main definitions

• TauCeti.freeProP.transvection: the automorphism x₀ ↦ x₀ · x ^ a of freeProP p X.
• TauCeti.freeProP.dilation: the automorphism x₀ ↦ x₀ ^ u of freeProP p X, for a unit u.
• TauCeti.freeProP.symplecticTransvection: the automorphism x₂ ↦ x₂ x₄^c, x₃ ↦ x₃ x₁^{-c} of freeProP p (Fin n), for n ≥ 4.

Main results

• TauCeti.freeProP.transvection_symm, TauCeti.freeProP.transvection_zero, TauCeti.freeProP.transvection_add: the transvections at fixed x₀, x form a one-parameter group of automorphisms.
• TauCeti.freeProP.dilation_symm, TauCeti.freeProP.dilation_one, TauCeti.freeProP.dilation_mul: the dilations at a fixed generator form a group of automorphisms indexed by ℤ_pˣ.
• TauCeti.freeProP.toAdd_exponentSum_congr, TauCeti.freeProP.toAdd_exponentSum_transvection, TauCeti.freeProP.toAdd_exponentSum_dilation: the exponent vectors of the images under the three elementary automorphisms.
• TauCeti.freeProP.symplecticTransvection_freeProPGen_one, TauCeti.freeProP.symplecticTransvection_freeProPGen_two, TauCeti.freeProP.symplecticTransvection_freeProPGen_of_ne: the values of the symplectic transvection pair on the generators.
• TauCeti.freeProP.exists_continuousMulEquiv_toAdd_exponentSum_eq_single_of_eq_smul: if the exponent vector of r is q • w with w x₀ = 1, an automorphism of freeProP p X carries r to an element with exponent vector q e_{x₀}.
• TauCeti.freeProP.exists_continuousMulEquiv_toAdd_exponentSum_eq_single: every element of freeProP p X, for X finite, is carried by an automorphism to an element whose exponent vector is supported at a prescribed generator, with value a coordinate of the original exponent vector dividing all the others.

References

• J. P. Labute, Classification of Demushkin groups, Canad. J. Math. 19 (1967), 106–132.
• L. Ribes and P. Zalesskii, Profinite Groups, Section 3.3.

Permuting the generators

@[simp]

theorem TauCeti.freeProP.toAdd_exponentSum_congr {p : ℕ} [Fact (Nat.Prime p)] {X Y : Type u} (σ : X ≃ Y) (y : freeProP p X) : Multiplicative.toAdd ((exponentSum p Y) ((congr σ) y)) = Multiplicative.toAdd ((exponentSum p X) y) ∘ ⇑σ.symm

Permuting the generators permutes the exponent vector: the exponent vector of congr σ y is the exponent vector of y composed with σ⁻¹.

Transvections

noncomputable def TauCeti.freeProP.transvection {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} (x₀ x : X) (hx : x ≠ x₀) (a : ℤ_[p]) : freeProP p X ≃ₜ* freeProP p X

The transvection x₀ ↦ x₀ · x ^ a of the free pro-p group on X, for generators x ≠ x₀ and a p-adic exponent a: the continuous automorphism sending the generator at x₀ to x₀ · x ^ a and fixing every other generator. Its inverse is the transvection with exponent -a (TauCeti.freeProP.transvection_symm). On the exponent vectors in ℤ_p^X it is the elementary matrix adding a times the coordinate at x₀ to the coordinate at x (TauCeti.freeProP.toAdd_exponentSum_transvection).

Equations

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

theorem TauCeti.freeProP.coe_transvection {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} {x₀ x : X} (hx : x ≠ x₀) (a : ℤ_[p]) [DecidableEq X] : ⇑(transvection x₀ x hx a) = ⇑(lift ⋯ (Function.update of x₀ (of x₀ * ⋯.padicPow (of x) a)))

The transvection x₀ ↦ x₀ · x ^ a is the lift of the family sending x₀ to x₀ · x ^ a and every other generator to itself.

@[simp]

theorem TauCeti.freeProP.transvection_of_self {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} {x₀ x : X} (hx : x ≠ x₀) (a : ℤ_[p]) : (transvection x₀ x hx a) (of x₀) = of x₀ * ⋯.padicPow (of x) a

The transvection x₀ ↦ x₀ · x ^ a sends the generator at x₀ to x₀ · x ^ a.

@[simp]

theorem TauCeti.freeProP.transvection_of_of_ne {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} {x₀ x : X} (hx : x ≠ x₀) (a : ℤ_[p]) {x' : X} (hx' : x' ≠ x₀) : (transvection x₀ x hx a) (of x') = of x'

The transvection x₀ ↦ x₀ · x ^ a fixes the generators other than x₀.

@[simp]

theorem TauCeti.freeProP.transvection_symm {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} {x₀ x : X} (hx : x ≠ x₀) (a : ℤ_[p]) : (transvection x₀ x hx a).symm = transvection x₀ x hx (-a)

The inverse of the transvection x₀ ↦ x₀ · x ^ a is the transvection x₀ ↦ x₀ · x ^ (-a).

@[simp]

theorem TauCeti.freeProP.transvection_zero {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} {x₀ x : X} (hx : x ≠ x₀) : transvection x₀ x hx 0 = ContinuousMulEquiv.refl (freeProP p X)

The transvection with exponent 0 is the identity.

theorem TauCeti.freeProP.transvection_add {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} {x₀ x : X} (hx : x ≠ x₀) (a b : ℤ_[p]) : transvection x₀ x hx (a + b) = (transvection x₀ x hx a).trans (transvection x₀ x hx b)

Transvections at fixed x₀, x compose by adding the exponents.

@[simp]

theorem TauCeti.freeProP.toAdd_exponentSum_transvection {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} {x₀ x : X} (hx : x ≠ x₀) (a : ℤ_[p]) [DecidableEq X] (y : freeProP p X) : Multiplicative.toAdd ((exponentSum p X) ((transvection x₀ x hx a) y)) = Multiplicative.toAdd ((exponentSum p X) y) + Pi.single x (a * Multiplicative.toAdd ((exponentSum p X) y) x₀)

The exponent vector under a transvection. The transvection x₀ ↦ x₀ · x ^ a adds a times the coordinate at x₀ to the coordinate at x of the exponent vector, and leaves the other coordinates unchanged.

Dilations

noncomputable def TauCeti.freeProP.dilation {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} (x₀ : X) (u : ℤ_[p]ˣ) : freeProP p X ≃ₜ* freeProP p X

The dilation x₀ ↦ x₀ ^ u of the free pro-p group on X, for a generator x₀ and a unit u of ℤ_p: the continuous automorphism raising the generator at x₀ to its p-adic power u and fixing every other generator. Its inverse is the dilation by u⁻¹ (TauCeti.freeProP.dilation_symm). On the exponent vectors in ℤ_p^X it is the diagonal matrix multiplying the coordinate at x₀ by u (TauCeti.freeProP.toAdd_exponentSum_dilation).

Equations

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

@[simp]

theorem TauCeti.freeProP.dilation_of_self {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} (x₀ : X) (u : ℤ_[p]ˣ) : (dilation x₀ u) (of x₀) = ⋯.padicPow (of x₀) ↑u

The dilation x₀ ↦ x₀ ^ u sends the generator at x₀ to x₀ ^ u.

@[simp]

theorem TauCeti.freeProP.dilation_of_of_ne {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} (x₀ : X) (u : ℤ_[p]ˣ) {x' : X} (hx' : x' ≠ x₀) : (dilation x₀ u) (of x') = of x'

The dilation x₀ ↦ x₀ ^ u fixes the generators other than x₀.

@[simp]

theorem TauCeti.freeProP.dilation_symm {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} (x₀ : X) (u : ℤ_[p]ˣ) : (dilation x₀ u).symm = dilation x₀ u⁻¹

The inverse of the dilation x₀ ↦ x₀ ^ u is the dilation x₀ ↦ x₀ ^ u⁻¹.

@[simp]

theorem TauCeti.freeProP.dilation_one {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} (x₀ : X) : dilation x₀ 1 = ContinuousMulEquiv.refl (freeProP p X)

The dilation by the unit 1 is the identity.

theorem TauCeti.freeProP.dilation_mul {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} (x₀ : X) (u v : ℤ_[p]ˣ) : dilation x₀ (u * v) = (dilation x₀ u).trans (dilation x₀ v)

Dilations at a fixed generator compose by multiplying the units.

@[simp]

theorem TauCeti.freeProP.toAdd_exponentSum_dilation {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} (x₀ : X) (u : ℤ_[p]ˣ) [Finite X] [DecidableEq X] (y : freeProP p X) : Multiplicative.toAdd ((exponentSum p X) ((dilation x₀ u) y)) = Function.update (Multiplicative.toAdd ((exponentSum p X) y)) x₀ (↑u * Multiplicative.toAdd ((exponentSum p X) y) x₀)

The exponent vector under a dilation. The dilation x₀ ↦ x₀ ^ u multiplies the coordinate at x₀ of the exponent vector by u and leaves the other coordinates unchanged.

The symplectic transvection pair

noncomputable def TauCeti.freeProP.symplecticTransvection {p : ℕ} [Fact (Nat.Prime p)] {n : ℕ} (hn3 : 3 < n) (c : ℤ_[p]) : freeProP p (Fin n) ≃ₜ* freeProP p (Fin n)

The symplectic transvection pair x₂ ↦ x₂ x₄^c, x₃ ↦ x₃ x₁^{-c} of the free pro-p group on n ≥ 4 generators, for a p-adic exponent c: the composite of the transvection at x₂ along x₄ with exponent c and the transvection at x₃ along x₁ with exponent -c (TauCeti.freeProP.transvection); it fixes the other generators. It is the change of basis of Labute's classification of the dyadic Demushkin groups of even rank: it preserves the class in gr_1(F) of the normal-form words x₁^q (x₁, x₂)(x₃, x₄) ⋯ (x_{n-1}, x_n) (TauCeti.freeProP.gradedMap_symplecticTransvection_gradedMk_demushkinWordNeTwo).

Equations

• TauCeti.freeProP.symplecticTransvection hn3 c = (TauCeti.freeProP.transvection ⟨1, ⋯⟩ ⟨3, hn3⟩ ⋯ c).trans (TauCeti.freeProP.transvection ⟨2, ⋯⟩ ⟨0, ⋯⟩ ⋯ (-c))

theorem TauCeti.freeProP.symplecticTransvection_def {p : ℕ} [Fact (Nat.Prime p)] {n : ℕ} (hn3 : 3 < n) (c : ℤ_[p]) : symplecticTransvection hn3 c = (transvection ⟨1, ⋯⟩ ⟨3, hn3⟩ ⋯ c).trans (transvection ⟨2, ⋯⟩ ⟨0, ⋯⟩ ⋯ (-c))

The defining equation of TauCeti.freeProP.symplecticTransvection.

theorem TauCeti.freeProP.symplecticTransvection_freeProPGen_of_ne {p : ℕ} [Fact (Nat.Prime p)] {n : ℕ} (hn3 : 3 < n) (c : ℤ_[p]) (m : ℕ) (hm₁ : m ≠ 1) (hm₂ : m ≠ 2) : (symplecticTransvection hn3 c) (freeProPGen p n m) = freeProPGen p n m

The symplectic transvection pair fixes the generators other than x₂ and x₃.

theorem TauCeti.freeProP.symplecticTransvection_freeProPGen_one {p : ℕ} [Fact (Nat.Prime p)] {n : ℕ} (hn3 : 3 < n) (c : ℤ_[p]) : (symplecticTransvection hn3 c) (freeProPGen p n 1) = freeProPGen p n 1 * ⋯.padicPow (freeProPGen p n 3) c

The symplectic transvection pair sends x₂ to x₂ x₄^c.

theorem TauCeti.freeProP.symplecticTransvection_freeProPGen_two {p : ℕ} [Fact (Nat.Prime p)] {n : ℕ} (hn3 : 3 < n) (c : ℤ_[p]) : (symplecticTransvection hn3 c) (freeProPGen p n 2) = freeProPGen p n 2 * ⋯.padicPow (freeProPGen p n 0) (-c)

The symplectic transvection pair sends x₃ to x₃ x₁^{-c}.

Normalising the exponent vector

theorem TauCeti.freeProP.exists_continuousMulEquiv_toAdd_exponentSum_eq_single_of_eq_smul {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} [Finite X] [DecidableEq X] {r : freeProP p X} {x₀ : X} {w : X → ℤ_[p]} {q : ℤ_[p]} (hw : w x₀ = 1) (hr : Multiplicative.toAdd ((exponentSum p X) r) = q • w) : ∃ (e : freeProP p X ≃ₜ* freeProP p X), Multiplicative.toAdd ((exponentSum p X) (e r)) = Pi.single x₀ q

Normalising the exponent vector of a relator. If the exponent vector of r ∈ freeProP p X is q • w with w x₀ = 1, then an automorphism of freeProP p X carries r to an element with exponent vector q e_{x₀}, that is to x₀ ^ q times an element of the closed commutator subgroup (TauCeti.freeProP.toAdd_exponentSum_eq_single_iff).

theorem TauCeti.freeProP.exists_continuousMulEquiv_toAdd_exponentSum_eq_single_of_forall_dvd {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} [Finite X] [DecidableEq X] {r : freeProP p X} {x₁ : X} (hx₁ : ∀ (x : X), Multiplicative.toAdd ((exponentSum p X) r) x₁ ∣ Multiplicative.toAdd ((exponentSum p X) r) x) (x₀ : X) : ∃ (e : freeProP p X ≃ₜ* freeProP p X), Multiplicative.toAdd ((exponentSum p X) (e r)) = Pi.single x₀ (Multiplicative.toAdd ((exponentSum p X) r) x₁)

Normalising the exponent vector, pivot form. If the coordinate at x₁ of the exponent vector v of r ∈ freeProP p X divides every coordinate, then for every generator x₀ an automorphism of freeProP p X carries r to an element with exponent vector v x₁ • e_{x₀}.

theorem TauCeti.freeProP.exists_continuousMulEquiv_toAdd_exponentSum_eq_single {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} [Finite X] [DecidableEq X] (r : freeProP p X) (x₀ : X) : ∃ (x₁ : X) (e : freeProP p X ≃ₜ* freeProP p X), (∀ (x : X), Multiplicative.toAdd ((exponentSum p X) r) x₁ ∣ Multiplicative.toAdd ((exponentSum p X) r) x) ∧ Multiplicative.toAdd ((exponentSum p X) (e r)) = Pi.single x₀ (Multiplicative.toAdd ((exponentSum p X) r) x₁)

Every element of a free pro-p group of finite rank has a normalisable exponent vector. For r ∈ freeProP p X and a generator x₀, some coordinate v x₁ of the exponent vector v of r divides all the others, and an automorphism of freeProP p X carries r to an element with exponent vector v x₁ • e_{x₀}, that is to x₀ ^ (v x₁) times an element of the closed commutator subgroup. The coordinate v x₁ generates the ideal of ℤ_p spanned by the exponent sums of r, so it is determined up to a unit of ℤ_p.