Peripheral automorphisms in rank one

Let F be a free pro-p group of rank one, presented by a marked isomorphism e : F ≃ₜ* freeProP p (Fin 1), with basis element x = basis e 0. Then F is isomorphic to ℤ_[p], hence commutative, so its conjugacy classes are singletons, and the cusp is x⁻¹. The peripheral conditions therefore collapse: a continuous automorphism is peripheral of exponent u exactly when it sends x to x ^ u.

Every continuous automorphism φ is of this form. Its value φ x topologically generates F, and two topological generators of a procyclic pro-p group differ by a unit exponent. So in rank one the peripheral automorphism group is all of ContinuousAut F, and the exponent character is injective, since an automorphism is determined by its value on x. Together with the peripheral-power theorem this identifies ContinuousAut F with ℤ_[p]ˣ: the exponent is a topological group isomorphism ContinuousAut F ≃ₜ* ℤ_[p]ˣ, whose inverse sends u to the automorphism x ↦ x ^ u.

Main definitions

• TauCeti.Peripheral.continuousAutEquivUnits: for a marked free pro-p group of rank one, the topological group isomorphism ContinuousAut F ≃ₜ* ℤ_[p]ˣ sending φ to the unit u with φ x = x ^ u.

Main results

• TauCeti.Peripheral.isConj_iff_eq_rank_one: conjugacy in F is equality.
• TauCeti.Peripheral.isPeripheralAut_iff_apply_basis_eq_padicPow_rank_one: an automorphism is peripheral of exponent u exactly when it sends x to x ^ u.
• TauCeti.Peripheral.exists_isPeripheralAut_rank_one, TauCeti.Peripheral.mem_peripheralAut_rank_one, TauCeti.Peripheral.peripheralAut_eq_top_rank_one: every continuous automorphism is peripheral.
• TauCeti.Peripheral.exponent_bijective_rank_one: the exponent character is bijective.
• TauCeti.Peripheral.apply_basis_continuousAutEquivUnits, TauCeti.Peripheral.continuousAutEquivUnits_eq_iff: the isomorphism with ℤ_[p]ˣ is characterized by φ x = x ^ u.

References

• L. Ribes and P. Zalesskii, Profinite Groups, 2nd ed., Section 4.3 for procyclic pro-p groups and Section 4.5 for automorphisms of free pro-p groups.

theorem TauCeti.Peripheral.topologicalClosure_closure_basis_zero {p : ℕ} {F : Type u_1} [Group F] [TopologicalSpace F] [IsTopologicalGroup F] (e : F ≃ₜ* freeProP p (Fin 1)) : (Subgroup.closure {basis e 0}).topologicalClosure = ⊤

In rank one the basis element topologically generates F.

theorem TauCeti.Peripheral.isConj_iff_eq_rank_one {p : ℕ} {F : Type u_1} [Group F] [TopologicalSpace F] [Fact (Nat.Prime p)] (e : F ≃ₜ* freeProP p (Fin 1)) {y z : F} : IsConj y z ↔ y = z

In a free pro-p group of rank one, conjugacy is equality: the group is commutative.

theorem TauCeti.Peripheral.isPeripheralAut_iff_apply_basis_eq_padicPow_rank_one {p : ℕ} {F : Type u_1} [Group F] [TopologicalSpace F] [Fact (Nat.Prime p)] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F] (hF : IsProP p F) (e : F ≃ₜ* freeProP p (Fin 1)) (u : ℤ_[p]ˣ) (φ : ContinuousAut F) : IsPeripheralAut hF (basis e) u φ ↔ φ (basis e 0) = hF.padicPow (basis e 0) ↑u

Peripheral automorphisms in rank one. A continuous automorphism of a free pro-p group of rank one is peripheral of exponent u exactly when it sends the basis element x to x ^ u.

theorem TauCeti.Peripheral.exists_isPeripheralAut_rank_one {p : ℕ} {F : Type u_1} [Group F] [TopologicalSpace F] [Fact (Nat.Prime p)] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F] (hF : IsProP p F) (e : F ≃ₜ* freeProP p (Fin 1)) (φ : ContinuousAut F) : ∃ (u : ℤ_[p]ˣ), IsPeripheralAut hF (basis e) u φ

Every automorphism is peripheral in rank one. A continuous automorphism of a free pro-p group of rank one sends the basis element x to a topological generator, which is x ^ u for a unit u, and it is then peripheral of exponent u.

theorem TauCeti.Peripheral.mem_peripheralAut_rank_one {p : ℕ} {F : Type u_1} [Group F] [TopologicalSpace F] [Fact (Nat.Prime p)] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F] (hF : IsProP p F) (e : F ≃ₜ* freeProP p (Fin 1)) (φ : ContinuousAut F) : φ ∈ peripheralAut hF (basis e)

In rank one every continuous automorphism is a peripheral automorphism.

theorem TauCeti.Peripheral.peripheralAut_eq_top_rank_one {p : ℕ} {F : Type u_1} [Group F] [TopologicalSpace F] [Fact (Nat.Prime p)] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F] (hF : IsProP p F) (e : F ≃ₜ* freeProP p (Fin 1)) : peripheralAut hF (basis e) = ⊤

In rank one the peripheral automorphism group is the whole group of continuous automorphisms.

theorem TauCeti.Peripheral.apply_basis_exponent_rank_one {p : ℕ} {F : Type u_1} [Group F] [TopologicalSpace F] [Fact (Nat.Prime p)] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F] (hF : IsProP p F) (e : F ≃ₜ* freeProP p (Fin 1)) (φ : ↥(peripheralAut hF (basis e))) : ↑φ (basis e 0) = hF.padicPow (basis e 0) ↑((exponent hF e ⋯) φ)

In rank one a peripheral automorphism φ sends the basis element x to x ^ u, with u its exponent.

theorem TauCeti.Peripheral.exponent_bijective_rank_one {p : ℕ} {F : Type u_1} [Group F] [TopologicalSpace F] [Fact (Nat.Prime p)] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F] (hF : IsProP p F) (e : F ≃ₜ* freeProP p (Fin 1)) : Function.Bijective ⇑(exponent hF e ⋯)

The exponent character is bijective in rank one. It is injective because an automorphism is determined by its value x ^ u on the basis element, and surjective by the peripheral-power theorem.

noncomputable def TauCeti.Peripheral.continuousAutEquivUnits {p : ℕ} {F : Type u_1} [Group F] [TopologicalSpace F] [Fact (Nat.Prime p)] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F] (hF : IsProP p F) (e : F ≃ₜ* freeProP p (Fin 1)) : ContinuousAut F ≃ₜ* ℤ_[p]ˣ

The continuous automorphisms of a free pro-p group of rank one are the units of ℤ_[p]. The topological group isomorphism ContinuousAut F ≃ₜ* ℤ_[p]ˣ sending a continuous automorphism φ to the unique unit u with φ x = x ^ u, for the basis element x. It is the exponent character, every automorphism being peripheral in rank one.

@[simp]

theorem TauCeti.Peripheral.continuousAutEquivUnits_coe {p : ℕ} {F : Type u_1} [Group F] [TopologicalSpace F] [Fact (Nat.Prime p)] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F] (hF : IsProP p F) (e : F ≃ₜ* freeProP p (Fin 1)) (φ : ↥(peripheralAut hF (basis e))) : (continuousAutEquivUnits hF e) ↑φ = (exponent hF e ⋯) φ

On peripheral automorphisms, the isomorphism with ℤ_[p]ˣ is the exponent character.

theorem TauCeti.Peripheral.continuousAutEquivUnits_eq_iff {p : ℕ} {F : Type u_1} [Group F] [TopologicalSpace F] [Fact (Nat.Prime p)] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F] (hF : IsProP p F) (e : F ≃ₜ* freeProP p (Fin 1)) (φ : ContinuousAut F) (u : ℤ_[p]ˣ) : (continuousAutEquivUnits hF e) φ = u ↔ φ (basis e 0) = hF.padicPow (basis e 0) ↑u

The image of φ in ℤ_[p]ˣ is u exactly when φ sends the basis element x to x ^ u.

@[simp]

theorem TauCeti.Peripheral.apply_basis_continuousAutEquivUnits {p : ℕ} {F : Type u_1} [Group F] [TopologicalSpace F] [Fact (Nat.Prime p)] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F] (hF : IsProP p F) (e : F ≃ₜ* freeProP p (Fin 1)) (φ : ContinuousAut F) : φ (basis e 0) = hF.padicPow (basis e 0) ↑((continuousAutEquivUnits hF e) φ)

The automorphism φ sends the basis element x to x ^ u, where u is its image in ℤ_[p]ˣ.

@[simp]

theorem TauCeti.Peripheral.continuousAutEquivUnits_symm_apply_basis {p : ℕ} {F : Type u_1} [Group F] [TopologicalSpace F] [Fact (Nat.Prime p)] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F] (hF : IsProP p F) (e : F ≃ₜ* freeProP p (Fin 1)) (u : ℤ_[p]ˣ) : ((continuousAutEquivUnits hF e).symm u) (basis e 0) = hF.padicPow (basis e 0) ↑u

The inverse isomorphism sends a unit u to the automorphism x ↦ x ^ u.