Documentation

TauCeti.Topology.Algebra.Group.Profinite.Free.Automorphism

Continuous automorphisms of a free pro-p group of finite rank #

Let F be a topological group with a topological isomorphism e : F ≃ₜ* freeProP p X to the free pro-p group on a finite type X, so that x i := e.symm (freeProP.of i) is a basis of F. A continuous automorphism of F is prescribed by its values on the basis, and any family of values that topologically generates F is attained: the endomorphism x i ↦ y i given by the universal property is surjective, hence bijective by the Hopf property of topologically finitely generated profinite groups.

The main source of such families is the following: if each y i is a conjugate of the p-adic power of x i by a unit u i, then the y i generate by Burnside's basis theorem, since modulo the Frattini subgroup conjugation is trivial and x i ^ u i generates the same closed subgroup as x i. So for every family of units u i and every choice of conjugators c i there is a continuous automorphism with x i ↦ (c i)⁻¹ * x i ^ u i * c i. This is the automorphism criterion by which endomorphisms of a free pro-p group given on a basis by conjugated unit powers, such as the automorphisms of free pro-p groups preserving the peripheral conjugacy classes up to a common exponent, are shown to be automorphisms.

Burnside's basis theorem also shows that every abstract automorphism σ of the Frattini quotient freeProP p X ⧸ proPFrattini p (freeProP p X) comes from a continuous automorphism: lifts of the images under σ of the classes of the generators of i generate the free group, so the automorphism sending each of i to such a lift induces σ. Hence the map ContinuousAut (freeProP p X) →* MulAut (freeProP p X ⧸ proPFrattini p _) is surjective. Its target is the automorphism group of the 𝔽_p-vector space with basis the classes of the generators (TauCeti.freeProP.frattiniQuotientBasis), that is GL_n(𝔽_p) for X = Fin n.

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.freeProP.finSuccExtend {p n : ℕ} (e : freeProP p (Fin n) ≃ₜ* freeProP p (Fin n)) :
freeProP p (Fin (n + 1)) ≃ₜ* freeProP p (Fin (n + 1))

Extension of an automorphism along Fin.succ. For a continuous automorphism e of the free pro-p group on Fin n, the continuous automorphism of the free pro-p group on Fin (n + 1) fixing the first generator x₀ and acting on the remaining generators x_{j+1}, j : Fin n, through e, read in freeProP p (Fin (n + 1)) along freeProP.map Fin.succ (TauCeti.freeProP.finSuccExtend_map_succ). Its inverse is the extension of e.symm.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.freeProP.finSuccExtend_of_zero {p n : ℕ} (e : freeProP p (Fin n) ≃ₜ* freeProP p (Fin n)) :
    (finSuccExtend e) (of 0) = of 0

    The extension of e along Fin.succ fixes the first generator.

    source
    @[simp]
    theorem TauCeti.freeProP.finSuccExtend_of_succ {p n : ℕ} (e : freeProP p (Fin n) ≃ₜ* freeProP p (Fin n)) (j : Fin n) :
    (finSuccExtend e) (of j.succ) = (map Fin.succ) (e (of j))

    The extension of e along Fin.succ acts on the generator at j.succ through e.

    source
    @[simp]
    theorem TauCeti.freeProP.finSuccExtend_map_succ {p n : ℕ} (e : freeProP p (Fin n) ≃ₜ* freeProP p (Fin n)) (y : freeProP p (Fin n)) :
    (finSuccExtend e) ((map Fin.succ) y) = (map Fin.succ) (e y)

    The extension of e along Fin.succ intertwines freeProP.map Fin.succ with e.

    source
    @[simp]
    theorem TauCeti.freeProP.finSuccExtend_symm {p n : ℕ} (e : freeProP p (Fin n) ≃ₜ* freeProP p (Fin n)) :
    (finSuccExtend e).symm = finSuccExtend e.symm

    The inverse of the extension of e along Fin.succ is the extension of e.symm.

    source
    @[simp]
    theorem TauCeti.freeProP.finSuccExtend_refl {p n : ℕ} :
    finSuccExtend (ContinuousMulEquiv.refl (freeProP p (Fin n))) = ContinuousMulEquiv.refl (freeProP p (Fin (n + 1)))

    The extension of the identity along Fin.succ is the identity.

    source
    @[simp]
    theorem TauCeti.freeProP.finSuccExtend_trans {p n : ℕ} (e₁ e₂ : freeProP p (Fin n) ≃ₜ* freeProP p (Fin n)) :
    finSuccExtend (e₁.trans e₂) = (finSuccExtend e₁).trans (finSuccExtend e₂)

    Extension along Fin.succ is compatible with composition.

    source
    theorem TauCeti.freeProP.finSuccExtend_freeProPGen_zero {p n : ℕ} (e : freeProP p (Fin n) ≃ₜ* freeProP p (Fin n)) :
    (finSuccExtend e) (freeProPGen p (n + 1) 0) = freeProPGen p (n + 1) 0

    The extension of e along Fin.succ fixes the first ℕ-indexed generator.

    source
    theorem TauCeti.freeProP.exists_continuousAut_of_topologicallyGenerates {p : ℕ} {X : Type u} [Finite X] {F : Type v} [Group F] [TopologicalSpace F] [IsTopologicalGroup F] (e : F ≃ₜ* freeProP p X) {y : X → F} (hy : (Subgroup.closure (Set.range y)).topologicalClosure = ⊤) :
    ∃ (φ : ContinuousAut F), ∀ (i : X), φ (e.symm (of i)) = y i

    Generating families are images of the basis under automorphisms. If F is a free pro-p group on the finite type X, with basis x i := e.symm (of i), then every family y : X → F that topologically generates F is the image of the basis under a continuous automorphism of F.

    source
    theorem TauCeti.freeProP.mapQuotient_proPFrattini_surjective {p : ℕ} {X : Type u} [Finite X] [Fact (Nat.Prime p)] :
    Function.Surjective ⇑(ContinuousAut.mapQuotient ⋯)

    Automorphisms of the Frattini quotient of a free pro-p group lift. For a prime p and a finite type X, every abstract automorphism σ of the Frattini quotient freeProP p X ⧸ proPFrattini p (freeProP p X) is induced by a continuous automorphism of the free pro-p group, namely one sending each generator of i to a lift of σ applied to its class.

    source
    theorem TauCeti.IsProP.exists_continuousAut_apply_eq_conj_padicPow {p : ℕ} {X : Type u} [Fact (Nat.Prime p)] [Finite X] {F : Type v} [Group F] [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F] (hF : IsProP p F) (e : F ≃ₜ* freeProP p X) (u : X → ℤ_[p]ˣ) (c : X → F) :
    ∃ (φ : ContinuousAut F), ∀ (i : X), φ (e.symm (freeProP.of i)) = (c i)⁻¹ * hF.padicPow (e.symm (freeProP.of i)) ↑(u i) * c i

    The automorphism criterion for conjugated unit powers. If F is a free pro-p group on the finite type X, with basis x i := e.symm (freeProP.of i), then for every family of units u : X → ℤ_[p]ˣ and every family of conjugators c : X → F there is a continuous automorphism of F sending each x i to (c i)⁻¹ * x i ^ u i * c i.

    source
    theorem TauCeti.IsProP.exists_continuousAut_apply_eq_conj_padicPow_const {p : ℕ} {X : Type u} [Fact (Nat.Prime p)] [Finite X] {F : Type v} [Group F] [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F] (hF : IsProP p F) (e : F ≃ₜ* freeProP p X) (u : ℤ_[p]ˣ) (c : X → F) :
    ∃ (φ : ContinuousAut F), ∀ (i : X), φ (e.symm (freeProP.of i)) = (c i)⁻¹ * hF.padicPow (e.symm (freeProP.of i)) ↑u * c i

    The automorphism criterion for conjugated powers with a common unit. The special case of exists_continuousAut_apply_eq_conj_padicPow in which every basis element x i is raised to the same unit u of ℤ_[p]: some continuous automorphism of F sends each x i to (c i)⁻¹ * x i ^ u * c i.