Documentation

TauCeti.Topology.Algebra.Group.Profinite.ProP.CompletedGroupAlgebraModule

Abelian pro-p groups with a continuous action as modules over ℤ_p[[Γ]] #

An abelian pro-p group A is a ℤ_p-module through the p-adic power (TauCeti.IsProP.module), and with its topology it is a compact ℤ_p-module in the sense of TauCeti.IsCompactModule. When a profinite group Γ acts continuously on A by group automorphisms, the action is ℤ_p-linear, because a continuous homomorphism of pro-p groups commutes with p-adic powers, so A is a compact ℤ_p-module with a continuous Γ-action and the general construction of TauCeti.IsCompactModule.completedGroupAlgebraModule makes it a topological module over the completed group algebra ℤ_p[[Γ]], in which each γ : Γ acts as it does on A.

This is the shape of Labute's relation module in the classification of Demushkin groups: for X the kernel of the orientation character on a free pro-p group F, the topological abelianization E = X ⧸ (X, X) is an abelian pro-p group on which Γ = F ⧸ X acts continuously by conjugation, and the module structure over Λ = ℤ_p[[Γ]] used in his Theorems 5 and 6 is the one constructed here (Labute, §4, p. 121).

Main definitions #

Main results #

References #

source
@[instance_reducible]
noncomputable def TauCeti.IsProP.completedGroupAlgebraModule {p : ℕ} [Fact (Nat.Prime p)] {A : Type u_1} [CommGroup A] [TopologicalSpace A] [IsTopologicalGroup A] [CompactSpace A] [TotallyDisconnectedSpace A] (Γ : Type u_2) [Group Γ] [MulDistribMulAction Γ A] [TopologicalSpace Γ] [CompactSpace Γ] [SeparatelyContinuousMul Γ] [ContinuousSMul Γ A] (hA : IsProP p A) :
Module (completedGroupAlgebra ℤ_[p] Γ) (Additive A)

An abelian pro-p group with a continuous action of a profinite group Γ is a module over the completed group algebra ℤ_p[[Γ]], in which a group element acts as it does on the group (TauCeti.IsProP.completedGroupAlgebraModule_of_smul). This is the general construction TauCeti.IsCompactModule.completedGroupAlgebraModule for the compact ℤ_p-module TauCeti.IsProP.module; the prime and the acting group are not determined by A, so it is a definition rather than an instance, introduced with letI := hA.completedGroupAlgebraModule Γ.

Equations
Instances For
    source
    theorem TauCeti.IsProP.completedGroupAlgebraModule_of_smul {p : ℕ} [Fact (Nat.Prime p)] {A : Type u_1} [CommGroup A] [TopologicalSpace A] [IsTopologicalGroup A] [CompactSpace A] [TotallyDisconnectedSpace A] {Γ : Type u_2} [Group Γ] [MulDistribMulAction Γ A] [TopologicalSpace Γ] [CompactSpace Γ] [SeparatelyContinuousMul Γ] [ContinuousSMul Γ A] (hA : IsProP p A) (γ : Γ) (x : Additive A) :
    (completedGroupAlgebra.of ℤ_[p] Γ) γ • x = γ • x

    A group element acts as itself: of ℤ_[p] Γ γ • x = γ • x. Not a simp lemma: simp already proves it through TauCeti.IsCompactModule.completedGroupAlgebraModule_smul and TauCeti.IsCompactModule.completedSMul_of, since the module structure is instance-reducible.

    source
    theorem TauCeti.IsProP.isScalarTower_completedGroupAlgebraModule {p : ℕ} [Fact (Nat.Prime p)] {A : Type u_1} [CommGroup A] [TopologicalSpace A] [IsTopologicalGroup A] [CompactSpace A] [TotallyDisconnectedSpace A] (Γ : Type u_2) [Group Γ] [MulDistribMulAction Γ A] [TopologicalSpace Γ] [CompactSpace Γ] [SeparatelyContinuousMul Γ] [ContinuousSMul Γ A] (hA : IsProP p A) :
    IsScalarTower ℤ_[p] (completedGroupAlgebra ℤ_[p] Γ) (Additive A)

    The ℤ_p[[Γ]]-module structure extends the ℤ_p-module structure TauCeti.IsProP.module.

    source
    theorem TauCeti.IsProP.continuousSMul_completedGroupAlgebraModule {p : ℕ} [Fact (Nat.Prime p)] {A : Type u_1} [CommGroup A] [TopologicalSpace A] [IsTopologicalGroup A] [CompactSpace A] [TotallyDisconnectedSpace A] (Γ : Type u_2) [Group Γ] [MulDistribMulAction Γ A] [TopologicalSpace Γ] [CompactSpace Γ] [SeparatelyContinuousMul Γ] [ContinuousSMul Γ A] (hA : IsProP p A) :
    ContinuousSMul (completedGroupAlgebra ℤ_[p] Γ) (Additive A)

    The ℤ_p[[Γ]]-module structure on an abelian pro-p group is topological.

    source
    theorem TauCeti.IsProP.span_completedGroupAlgebraModule_eq_top {p : ℕ} [Fact (Nat.Prime p)] {A : Type u_1} [CommGroup A] [TopologicalSpace A] [IsTopologicalGroup A] [CompactSpace A] [TotallyDisconnectedSpace A] (Γ : Type u_2) [Group Γ] [MulDistribMulAction Γ A] [TopologicalSpace Γ] [CompactSpace Γ] [SeparatelyContinuousMul Γ] [ContinuousSMul Γ A] (hA : IsProP p A) {T : Set A} (hT : T.Finite) (hgen : Dense ↑(Subgroup.closure (Set.univ • T))) :
    Submodule.span (completedGroupAlgebra ℤ_[p] Γ) (⇑Additive.ofMul '' T) = ⊤

    Generation over ℤ_p[[Γ]]. If the Γ-orbit of a finite subset T of an abelian pro-p group A generates a dense subgroup, then the additive classes of the elements of T span Additive A over ℤ_p[[Γ]]. This is the general TauCeti.IsCompactModule.span_completedGroupAlgebraModule_eq_top_of_dense_closure_univ_smul, with the generation hypothesis read on the multiplicative group A, where its topology lives.

    source
    theorem TauCeti.IsProP.module_finite_completedGroupAlgebraModule {p : ℕ} [Fact (Nat.Prime p)] {A : Type u_1} [CommGroup A] [TopologicalSpace A] [IsTopologicalGroup A] [CompactSpace A] [TotallyDisconnectedSpace A] (Γ : Type u_2) [Group Γ] [MulDistribMulAction Γ A] [TopologicalSpace Γ] [CompactSpace Γ] [SeparatelyContinuousMul Γ] [ContinuousSMul Γ A] (hA : IsProP p A) {T : Set A} (hT : T.Finite) (hgen : Dense ↑(Subgroup.closure (Set.univ • T))) :
    Module.Finite (completedGroupAlgebra ℤ_[p] Γ) (Additive A)

    Finite generation over ℤ_p[[Γ]]. If the Γ-orbit of a finite subset T of an abelian pro-p group A generates a dense subgroup, then Additive A is a finitely generated ℤ_p[[Γ]]-module, spanned by the classes of the elements of T (TauCeti.IsProP.span_completedGroupAlgebraModule_eq_top).