Compact modules over the completed group algebra

Let Γ be a compact topological group, R a compact topological ring and M a compact R-module (TauCeti.IsCompactModule R M) with a continuous R-linear action of Γ. This file extends the action of Γ on M to a continuous action of the completed group algebra R[[Γ]], making M a topological R[[Γ]]-module in which the group elements of R Γ γ act as γ does. This is the structure through which Iwasawa theory and Labute's classification of Demushkin groups study a compact abelian pro-p group with a continuous action of a profinite group: Labute's relation module E = X ⧸ (X, X), for X the kernel of the orientation character on a free pro-p group F, is a compact ℤ_p-module with a continuous action of Γ = F ⧸ X by conjugation, and its structure as a module over Λ = ℤ_p[[Γ]] is the setting of his Theorems 5 and 6.

The construction. Let V ≤ M be a Γ-invariant open submodule. The quotient M ⧸ V is a finite discrete R-module on which Γ acts through a finite quotient Γ ⧸ U, U open normal (Submodule.quotientActionKernel), so the group algebra R[Γ ⧸ U] acts on M ⧸ V, and hence so does R[[Γ]] through its projection onto R[Γ ⧸ U]; this is the algebra homomorphism completedGroupAlgebra.toQuotientEnd, and it does not depend on U. These actions are compatible with the factor maps M ⧸ V → M ⧸ V', and since the invariant open submodules form a basis of neighbourhoods of zero in the compact module M, the inverse-limit description of M assembles them into a unique action on M itself: x • m is the unique element of M whose class modulo every invariant open V is toQuotientEnd x applied to the class of m.

The module structure is a definition taking the compact-module hypothesis as an argument rather than an instance, in the same way as the ℤ_p-module structure TauCeti.IsProP.module of an abelian pro-p group; consumers introduce it with letI := hM.completedGroupAlgebraModule Γ.

Main definitions

• TauCeti.completedGroupAlgebra.toQuotientEnd: the action of R[[Γ]] on the quotient of M by an invariant submodule on which an open normal subgroup acts trivially.
• TauCeti.IsCompactModule.completedSMul: the scalar action of R[[Γ]] on a compact module with a continuous Γ-action.
• TauCeti.IsCompactModule.completedGroupAlgebraModule: the resulting R[[Γ]]-module structure.

Main results

• TauCeti.completedGroupAlgebra.toQuotientEnd_of, TauCeti.completedGroupAlgebra.toQuotientEnd_eq, TauCeti.completedGroupAlgebra.factor_toQuotientEnd, TauCeti.completedGroupAlgebra.continuous_toQuotientEnd: the level actions extend the action of Γ, are independent of the open normal subgroup, are compatible with the factor maps, and are continuous.
• TauCeti.IsCompactModule.mkQ_completedSMul: the defining property of the scalar action, its class modulo every invariant open submodule.
• TauCeti.IsCompactModule.completedSMul_of, TauCeti.IsCompactModule.completedSMul_algebraMap: the group elements act as Γ does and the scalars of R act as scalars.
• TauCeti.IsCompactModule.isScalarTower_completedGroupAlgebraModule, TauCeti.IsCompactModule.continuousSMul_completedGroupAlgebraModule: the module structure is compatible with the R-module structure and is topological.
• TauCeti.IsCompactModule.span_completedGroupAlgebraModule_eq_top_of_dense_closure_univ_smul, TauCeti.IsCompactModule.module_finite_completedGroupAlgebraModule_of_dense_closure_univ_smul: a finite set whose Γ-orbit generates a dense subgroup spans the module over R[[Γ]], so the module is finitely generated.

References

• L. Ribes and P. Zalesskii, Profinite Groups, Sections 5.1 and 5.3.
• J. P. Labute, Classification of Demushkin groups, Canad. J. Math. 19 (1967), Section 4, p. 121.

noncomputable def TauCeti.completedGroupAlgebra.toQuotientEnd {R : Type u} [CommRing R] {Γ : Type v} [Group Γ] [TopologicalSpace Γ] {M : Type w} [AddCommGroup M] [Module R M] [DistribMulAction Γ M] [SMulCommClass Γ R M] {V : Submodule R M} (hV : ∀ (γ : Γ), ∀ x ∈ V, γ • x ∈ V) (U : OpenNormalSubgroup Γ) (hU : ↑U.toOpenSubgroup ≤ (Submodule.quotientToModuleEnd hV).ker) : completedGroupAlgebra R Γ →ₐ[R] Module.End R (M ⧸ V)

The level action. For a Γ-invariant submodule V ≤ M and an open normal subgroup U of Γ acting trivially on M ⧸ V, the completed group algebra R[[Γ]] acts on M ⧸ V through its projection onto R[Γ ⧸ U] and the action of R[Γ ⧸ U] on M ⧸ V induced by that of Γ ⧸ U. The action does not depend on U (toQuotientEnd_eq), and a group element acts as it does on M ⧸ V (toQuotientEnd_of).

Equations

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

theorem TauCeti.completedGroupAlgebra.toQuotientEnd_apply {R : Type u} [CommRing R] {Γ : Type v} [Group Γ] [TopologicalSpace Γ] {M : Type w} [AddCommGroup M] [Module R M] [DistribMulAction Γ M] [SMulCommClass Γ R M] {V : Submodule R M} (hV : ∀ (γ : Γ), ∀ x ∈ V, γ • x ∈ V) (U : OpenNormalSubgroup Γ) (hU : ↑U.toOpenSubgroup ≤ (Submodule.quotientToModuleEnd hV).ker) (x : completedGroupAlgebra R Γ) : (toQuotientEnd hV U hU) x = ((MonoidAlgebra.lift R (Module.End R (M ⧸ V)) (Γ ⧸ ↑U.toOpenSubgroup)) (QuotientGroup.lift (↑U.toOpenSubgroup) (Submodule.quotientToModuleEnd hV) hU)) ((proj R Γ U) x)

The level action, unfolded: the projection to R[Γ ⧸ U] followed by the action of the group algebra on M ⧸ V.

@[simp]

theorem TauCeti.completedGroupAlgebra.toQuotientEnd_of {R : Type u} [CommRing R] {Γ : Type v} [Group Γ] [TopologicalSpace Γ] {M : Type w} [AddCommGroup M] [Module R M] [DistribMulAction Γ M] [SMulCommClass Γ R M] {V : Submodule R M} (hV : ∀ (γ : Γ), ∀ x ∈ V, γ • x ∈ V) (U : OpenNormalSubgroup Γ) (hU : ↑U.toOpenSubgroup ≤ (Submodule.quotientToModuleEnd hV).ker) (γ : Γ) : (toQuotientEnd hV U hU) ((of R Γ) γ) = (Submodule.quotientToModuleEnd hV) γ

A group element of R[[Γ]] acts on M ⧸ V as the group element does.

theorem TauCeti.completedGroupAlgebra.toQuotientEnd_eq_of_le {R : Type u} [CommRing R] {Γ : Type v} [Group Γ] [TopologicalSpace Γ] {M : Type w} [AddCommGroup M] [Module R M] [DistribMulAction Γ M] [SMulCommClass Γ R M] {V : Submodule R M} (hV : ∀ (γ : Γ), ∀ x ∈ V, γ • x ∈ V) {U U' : OpenNormalSubgroup Γ} (hU : ↑U.toOpenSubgroup ≤ (Submodule.quotientToModuleEnd hV).ker) (hUU' : U ≤ U') (hU' : ↑U'.toOpenSubgroup ≤ (Submodule.quotientToModuleEnd hV).ker) : toQuotientEnd hV U hU = toQuotientEnd hV U' hU'

The level actions through U ≤ U' agree, because the projections of R[[Γ]] are compatible along R[Γ ⧸ U] → R[Γ ⧸ U'].

theorem TauCeti.completedGroupAlgebra.toQuotientEnd_eq {R : Type u} [CommRing R] {Γ : Type v} [Group Γ] [TopologicalSpace Γ] {M : Type w} [AddCommGroup M] [Module R M] [DistribMulAction Γ M] [SMulCommClass Γ R M] {V : Submodule R M} (hV : ∀ (γ : Γ), ∀ x ∈ V, γ • x ∈ V) {U U' : OpenNormalSubgroup Γ} (hU : ↑U.toOpenSubgroup ≤ (Submodule.quotientToModuleEnd hV).ker) (hU' : ↑U'.toOpenSubgroup ≤ (Submodule.quotientToModuleEnd hV).ker) : toQuotientEnd hV U hU = toQuotientEnd hV U' hU'

Independence of the open normal subgroup. The level action on M ⧸ V is the same for every open normal subgroup acting trivially on M ⧸ V.

theorem TauCeti.completedGroupAlgebra.factor_toQuotientEnd {R : Type u} [CommRing R] {Γ : Type v} [Group Γ] [TopologicalSpace Γ] {M : Type w} [AddCommGroup M] [Module R M] [DistribMulAction Γ M] [SMulCommClass Γ R M] {V V' : Submodule R M} (hV : ∀ (γ : Γ), ∀ x ∈ V, γ • x ∈ V) (U : OpenNormalSubgroup Γ) (hU : ↑U.toOpenSubgroup ≤ (Submodule.quotientToModuleEnd hV).ker) (hV' : ∀ (γ : Γ), ∀ x ∈ V', γ • x ∈ V') (h : V ≤ V') (x : completedGroupAlgebra R Γ) (y : M ⧸ V) : (Submodule.factor h) (((toQuotientEnd hV U hU) x) y) = ((toQuotientEnd hV' U ⋯) x) ((Submodule.factor h) y)

Compatibility with the factor maps. For invariant V ≤ V', the level actions on M ⧸ V and M ⧸ V' commute with the factor map M ⧸ V → M ⧸ V'.

theorem TauCeti.completedGroupAlgebra.toQuotientEnd_apply_apply {R : Type u} [CommRing R] {Γ : Type v} [Group Γ] [TopologicalSpace Γ] {M : Type w} [AddCommGroup M] [Module R M] [DistribMulAction Γ M] [SMulCommClass Γ R M] {V : Submodule R M} (hV : ∀ (γ : Γ), ∀ x ∈ V, γ • x ∈ V) (U : OpenNormalSubgroup Γ) (hU : ↑U.toOpenSubgroup ≤ (Submodule.quotientToModuleEnd hV).ker) [Fintype (Γ ⧸ ↑U.toOpenSubgroup)] (x : completedGroupAlgebra R Γ) (y : M ⧸ V) : ((toQuotientEnd hV U hU) x) y = ∑ g : Γ ⧸ ↑U.toOpenSubgroup, ((proj R Γ U) x).coeff g • ((QuotientGroup.lift (↑U.toOpenSubgroup) (Submodule.quotientToModuleEnd hV) hU) g) y

The level action as a finite sum over the classes of Γ ⧸ U, weighted by the coefficients of the projection.

theorem TauCeti.completedGroupAlgebra.continuous_toQuotientEnd {R : Type u} [CommRing R] {Γ : Type v} [Group Γ] [TopologicalSpace Γ] {M : Type w} [AddCommGroup M] [Module R M] [DistribMulAction Γ M] [SMulCommClass Γ R M] {V : Submodule R M} (hV : ∀ (γ : Γ), ∀ x ∈ V, γ • x ∈ V) (U : OpenNormalSubgroup Γ) (hU : ↑U.toOpenSubgroup ≤ (Submodule.quotientToModuleEnd hV).ker) [TopologicalSpace R] [CompactSpace Γ] [SeparatelyContinuousMul Γ] [TopologicalSpace M] [SeparatelyContinuousAdd M] [ContinuousSMul R M] (hVo : IsOpen ↑V) : Continuous fun (p : completedGroupAlgebra R Γ × M ⧸ V) => ((toQuotientEnd hV U hU) p.1) p.2

Continuity of the level action for an invariant open submodule V of M, when M has separately continuous addition and a continuous scalar action of R: the action of R[[Γ]] on the discrete quotient M ⧸ V is jointly continuous.

theorem TauCeti.IsCompactModule.exists_le_ker_quotientToModuleEnd {R : Type u} [CommRing R] {Γ : Type v} [Group Γ] [TopologicalSpace Γ] {M : Type w} [AddCommGroup M] [Module R M] [DistribMulAction Γ M] [SMulCommClass Γ R M] {V : Submodule R M} [TopologicalSpace R] [SeparatelyContinuousMul Γ] [TopologicalSpace M] [ContinuousSMul Γ M] (hM : IsCompactModule R M) (hV : ∀ (γ : Γ), ∀ x ∈ V, γ • x ∈ V) (hVo : IsOpen ↑V) : ∃ (U : OpenNormalSubgroup Γ), ↑U.toOpenSubgroup ≤ (Submodule.quotientToModuleEnd hV).ker

Every invariant open submodule of a compact module admits an open normal subgroup of Γ acting trivially on the quotient.

theorem TauCeti.IsCompactModule.eq_of_forall_invariant_mkQ_eq {R : Type u} [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] {M : Type w} [AddCommGroup M] [Module R M] [DistribMulAction Γ M] [SMulCommClass Γ R M] [TopologicalSpace R] [CompactSpace R] [CompactSpace Γ] [TopologicalSpace M] [ContinuousSMul Γ M] (hM : IsCompactModule R M) {m m' : M} (h : ∀ (V : Submodule R M), IsOpen ↑V → (∀ (γ : Γ), ∀ x ∈ V, γ • x ∈ V) → V.mkQ m = V.mkQ m') : m = m'

Separation by the invariant open submodules, for a compact module: two elements that agree modulo every Γ-invariant open submodule are equal.

theorem TauCeti.IsCompactModule.existsUnique_forall_mkQ_eq_toQuotientEnd {R : Type u} [CommRing R] {Γ : Type v} [Group Γ] [TopologicalSpace Γ] {M : Type w} [AddCommGroup M] [Module R M] [DistribMulAction Γ M] [SMulCommClass Γ R M] [TopologicalSpace R] [CompactSpace R] [CompactSpace Γ] [SeparatelyContinuousMul Γ] [TopologicalSpace M] [ContinuousSMul Γ M] (hM : IsCompactModule R M) (x : completedGroupAlgebra R Γ) (m : M) : ∃! n : M, ∀ (V : Submodule R M) (hV : ∀ (γ : Γ), ∀ x ∈ V, γ • x ∈ V), IsOpen ↑V → ∀ (U : OpenNormalSubgroup Γ) (hU : ↑U.toOpenSubgroup ≤ (Submodule.quotientToModuleEnd hV).ker), V.mkQ n = ((completedGroupAlgebra.toQuotientEnd hV U hU) x) (V.mkQ m)

The inverse-limit construction of the scalar action. For x : R[[Γ]] and m : M there is exactly one element of M whose class modulo every Γ-invariant open submodule V is the level action of x on the class of m, for every open normal subgroup U acting trivially on M ⧸ V.

noncomputable def TauCeti.IsCompactModule.completedSMul {R : Type u} [CommRing R] {Γ : Type v} [Group Γ] [TopologicalSpace Γ] {M : Type w} [AddCommGroup M] [Module R M] [DistribMulAction Γ M] [SMulCommClass Γ R M] [TopologicalSpace R] [CompactSpace R] [CompactSpace Γ] [SeparatelyContinuousMul Γ] [TopologicalSpace M] [ContinuousSMul Γ M] (hM : IsCompactModule R M) (x : completedGroupAlgebra R Γ) (m : M) : M

The scalar action of the completed group algebra on a compact module M with a continuous R-linear action of Γ: hM.completedSMul x m is the unique element of M whose class modulo every Γ-invariant open submodule V is the level action of x on the class of m (TauCeti.IsCompactModule.mkQ_completedSMul). It extends the action of Γ (TauCeti.IsCompactModule.completedSMul_of), and it is the scalar action of the module structure TauCeti.IsCompactModule.completedGroupAlgebraModule.

Equations

• hM.completedSMul x m = ⋯.choose

theorem TauCeti.IsCompactModule.mkQ_completedSMul {R : Type u} [CommRing R] {Γ : Type v} [Group Γ] [TopologicalSpace Γ] {M : Type w} [AddCommGroup M] [Module R M] [DistribMulAction Γ M] [SMulCommClass Γ R M] {V : Submodule R M} [TopologicalSpace R] [CompactSpace R] [CompactSpace Γ] [SeparatelyContinuousMul Γ] [TopologicalSpace M] [ContinuousSMul Γ M] (hM : IsCompactModule R M) (hV : ∀ (γ : Γ), ∀ x ∈ V, γ • x ∈ V) (hVo : IsOpen ↑V) (U : OpenNormalSubgroup Γ) (hU : ↑U.toOpenSubgroup ≤ (Submodule.quotientToModuleEnd hV).ker) (x : completedGroupAlgebra R Γ) (m : M) : V.mkQ (hM.completedSMul x m) = ((completedGroupAlgebra.toQuotientEnd hV U hU) x) (V.mkQ m)

The defining property of the scalar action: modulo a Γ-invariant open submodule V, x • m is the level action of x on the class of m, computed through any open normal subgroup U acting trivially on M ⧸ V.

@[simp]

theorem TauCeti.IsCompactModule.completedSMul_of {R : Type u} [CommRing R] {Γ : Type v} [Group Γ] [TopologicalSpace Γ] {M : Type w} [AddCommGroup M] [Module R M] [DistribMulAction Γ M] [SMulCommClass Γ R M] [TopologicalSpace R] [CompactSpace R] [CompactSpace Γ] [SeparatelyContinuousMul Γ] [TopologicalSpace M] [ContinuousSMul Γ M] (hM : IsCompactModule R M) (γ : Γ) (m : M) : hM.completedSMul ((completedGroupAlgebra.of R Γ) γ) m = γ • m

A group element acts as itself: of R Γ γ • m = γ • m.

@[simp]

theorem TauCeti.IsCompactModule.completedSMul_algebraMap {R : Type u} [CommRing R] {Γ : Type v} [Group Γ] [TopologicalSpace Γ] {M : Type w} [AddCommGroup M] [Module R M] [DistribMulAction Γ M] [SMulCommClass Γ R M] [TopologicalSpace R] [CompactSpace R] [CompactSpace Γ] [SeparatelyContinuousMul Γ] [TopologicalSpace M] [ContinuousSMul Γ M] (hM : IsCompactModule R M) (r : R) (m : M) : hM.completedSMul ((algebraMap R (completedGroupAlgebra R Γ)) r) m = r • m

A scalar of R acts as a scalar: algebraMap R R[[Γ]] r • m = r • m.

@[simp]

theorem TauCeti.IsCompactModule.one_completedSMul {R : Type u} [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] {M : Type w} [AddCommGroup M] [Module R M] [DistribMulAction Γ M] [SMulCommClass Γ R M] [TopologicalSpace R] [CompactSpace R] [CompactSpace Γ] [SeparatelyContinuousMul Γ] [TopologicalSpace M] [ContinuousSMul Γ M] (hM : IsCompactModule R M) (m : M) : hM.completedSMul 1 m = m

The unit of R[[Γ]] acts as the identity on M.

theorem TauCeti.IsCompactModule.mul_completedSMul {R : Type u} [CommRing R] {Γ : Type v} [Group Γ] [TopologicalSpace Γ] {M : Type w} [AddCommGroup M] [Module R M] [DistribMulAction Γ M] [SMulCommClass Γ R M] [TopologicalSpace R] [CompactSpace R] [CompactSpace Γ] [SeparatelyContinuousMul Γ] [TopologicalSpace M] [ContinuousSMul Γ M] (hM : IsCompactModule R M) (x y : completedGroupAlgebra R Γ) (m : M) : hM.completedSMul (x * y) m = hM.completedSMul x (hM.completedSMul y m)

Multiplication in R[[Γ]] acts by successive scalar actions.

@[simp]

theorem TauCeti.IsCompactModule.completedSMul_zero {R : Type u} [CommRing R] {Γ : Type v} [Group Γ] [TopologicalSpace Γ] {M : Type w} [AddCommGroup M] [Module R M] [DistribMulAction Γ M] [SMulCommClass Γ R M] [TopologicalSpace R] [CompactSpace R] [CompactSpace Γ] [SeparatelyContinuousMul Γ] [TopologicalSpace M] [ContinuousSMul Γ M] (hM : IsCompactModule R M) (x : completedGroupAlgebra R Γ) : hM.completedSMul x 0 = 0

Every element of R[[Γ]] sends the zero element of M to zero.

theorem TauCeti.IsCompactModule.completedSMul_add {R : Type u} [CommRing R] {Γ : Type v} [Group Γ] [TopologicalSpace Γ] {M : Type w} [AddCommGroup M] [Module R M] [DistribMulAction Γ M] [SMulCommClass Γ R M] [TopologicalSpace R] [CompactSpace R] [CompactSpace Γ] [SeparatelyContinuousMul Γ] [TopologicalSpace M] [ContinuousSMul Γ M] (hM : IsCompactModule R M) (x : completedGroupAlgebra R Γ) (m m' : M) : hM.completedSMul x (m + m') = hM.completedSMul x m + hM.completedSMul x m'

The action of R[[Γ]] distributes over addition in M.

theorem TauCeti.IsCompactModule.add_completedSMul {R : Type u} [CommRing R] {Γ : Type v} [Group Γ] [TopologicalSpace Γ] {M : Type w} [AddCommGroup M] [Module R M] [DistribMulAction Γ M] [SMulCommClass Γ R M] [TopologicalSpace R] [CompactSpace R] [CompactSpace Γ] [SeparatelyContinuousMul Γ] [TopologicalSpace M] [ContinuousSMul Γ M] (hM : IsCompactModule R M) (x y : completedGroupAlgebra R Γ) (m : M) : hM.completedSMul (x + y) m = hM.completedSMul x m + hM.completedSMul y m

The sum of two elements of R[[Γ]] acts as the sum of their actions.

@[simp]

theorem TauCeti.IsCompactModule.zero_completedSMul {R : Type u} [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] {M : Type w} [AddCommGroup M] [Module R M] [DistribMulAction Γ M] [SMulCommClass Γ R M] [TopologicalSpace R] [CompactSpace R] [CompactSpace Γ] [SeparatelyContinuousMul Γ] [TopologicalSpace M] [ContinuousSMul Γ M] (hM : IsCompactModule R M) (m : M) : hM.completedSMul 0 m = 0

The zero element of R[[Γ]] acts as zero on M.

theorem TauCeti.IsCompactModule.smul_completedSMul {R : Type u} [CommRing R] {Γ : Type v} [Group Γ] [TopologicalSpace Γ] {M : Type w} [AddCommGroup M] [Module R M] [DistribMulAction Γ M] [SMulCommClass Γ R M] [TopologicalSpace R] [CompactSpace R] [CompactSpace Γ] [SeparatelyContinuousMul Γ] [TopologicalSpace M] [ContinuousSMul Γ M] (hM : IsCompactModule R M) (r : R) (x : completedGroupAlgebra R Γ) (m : M) : hM.completedSMul (r • x) m = r • hM.completedSMul x m

Scaling an element of R[[Γ]] by r : R scales its action on M by r.

@[instance_reducible]

noncomputable def TauCeti.IsCompactModule.completedGroupAlgebraModule {R : Type u} [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] {M : Type w} [AddCommGroup M] [Module R M] [DistribMulAction Γ M] [SMulCommClass Γ R M] [TopologicalSpace R] [CompactSpace R] [CompactSpace Γ] [SeparatelyContinuousMul Γ] [TopologicalSpace M] [ContinuousSMul Γ M] (hM : IsCompactModule R M) : Module (completedGroupAlgebra R Γ) M

A compact module with a continuous Γ-action is a module over the completed group algebra. The scalar action is TauCeti.IsCompactModule.completedSMul, so the group elements act as Γ does. The compact-module hypothesis is an argument rather than an instance; consumers introduce the structure with letI := hM.completedGroupAlgebraModule Γ.

Equations

• TauCeti.IsCompactModule.completedGroupAlgebraModule Γ hM = { smul := hM.completedSMul, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

@[simp]

theorem TauCeti.IsCompactModule.completedGroupAlgebraModule_smul {R : Type u} [CommRing R] {Γ : Type v} [Group Γ] [TopologicalSpace Γ] {M : Type w} [AddCommGroup M] [Module R M] [DistribMulAction Γ M] [SMulCommClass Γ R M] [TopologicalSpace R] [CompactSpace R] [CompactSpace Γ] [SeparatelyContinuousMul Γ] [TopologicalSpace M] [ContinuousSMul Γ M] (hM : IsCompactModule R M) (x : completedGroupAlgebra R Γ) (m : M) : x • m = hM.completedSMul x m

The scalar action of TauCeti.IsCompactModule.completedGroupAlgebraModule is TauCeti.IsCompactModule.completedSMul.

theorem TauCeti.IsCompactModule.isScalarTower_completedGroupAlgebraModule {R : Type u} [CommRing R] {Γ : Type v} [Group Γ] [TopologicalSpace Γ] {M : Type w} [AddCommGroup M] [Module R M] [DistribMulAction Γ M] [SMulCommClass Γ R M] [TopologicalSpace R] [CompactSpace R] [CompactSpace Γ] [SeparatelyContinuousMul Γ] [TopologicalSpace M] [ContinuousSMul Γ M] (hM : IsCompactModule R M) : IsScalarTower R (completedGroupAlgebra R Γ) M

The R[[Γ]]-module structure is compatible with the R-module structure.

theorem TauCeti.IsCompactModule.continuous_completedSMul {R : Type u} [CommRing R] {Γ : Type v} [Group Γ] [TopologicalSpace Γ] {M : Type w} [AddCommGroup M] [Module R M] [DistribMulAction Γ M] [SMulCommClass Γ R M] [TopologicalSpace R] [CompactSpace R] [CompactSpace Γ] [SeparatelyContinuousMul Γ] [TopologicalSpace M] [ContinuousSMul Γ M] (hM : IsCompactModule R M) : Continuous fun (p : completedGroupAlgebra R Γ × M) => hM.completedSMul p.1 p.2

Continuity of the scalar action: modulo every invariant open submodule it is the level action, which is continuous.

theorem TauCeti.IsCompactModule.continuousSMul_completedGroupAlgebraModule {R : Type u} [CommRing R] {Γ : Type v} [Group Γ] [TopologicalSpace Γ] {M : Type w} [AddCommGroup M] [Module R M] [DistribMulAction Γ M] [SMulCommClass Γ R M] [TopologicalSpace R] [CompactSpace R] [CompactSpace Γ] [SeparatelyContinuousMul Γ] [TopologicalSpace M] [ContinuousSMul Γ M] (hM : IsCompactModule R M) : ContinuousSMul (completedGroupAlgebra R Γ) M

The R[[Γ]]-module structure on a compact module is topological.

theorem TauCeti.IsCompactModule.span_completedGroupAlgebraModule_eq_top_of_dense_closure_univ_smul {R : Type u} [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] {M : Type w} [AddCommGroup M] [Module R M] [DistribMulAction Γ M] [SMulCommClass Γ R M] [TopologicalSpace R] [CompactSpace R] [CompactSpace Γ] [SeparatelyContinuousMul Γ] [TopologicalSpace M] [ContinuousSMul Γ M] (hM : IsCompactModule R M) [T2Space R] [ContinuousAdd R] {T : Set M} (hT : T.Finite) (hgen : Dense ↑(AddSubgroup.closure (Set.univ • T))) : Submodule.span (completedGroupAlgebra R Γ) T = ⊤

Finite generation over the completed group algebra. If the Γ-orbit of a finite set T generates a dense subgroup of the compact module M, then T spans M over R[[Γ]]: the span contains the orbit, because a group element acts as itself, and it is closed, because R[[Γ]] is compact.

theorem TauCeti.IsCompactModule.module_finite_completedGroupAlgebraModule_of_dense_closure_univ_smul {R : Type u} [CommRing R] (Γ : Type v) [Group Γ] [TopologicalSpace Γ] {M : Type w} [AddCommGroup M] [Module R M] [DistribMulAction Γ M] [SMulCommClass Γ R M] [TopologicalSpace R] [CompactSpace R] [CompactSpace Γ] [SeparatelyContinuousMul Γ] [TopologicalSpace M] [ContinuousSMul Γ M] (hM : IsCompactModule R M) [T2Space R] [ContinuousAdd R] {T : Set M} (hT : T.Finite) (hgen : Dense ↑(AddSubgroup.closure (Set.univ • T))) : Module.Finite (completedGroupAlgebra R Γ) M

A compact module in which the Γ-orbit of a finite set generates a dense subgroup is a finitely generated R[[Γ]]-module, spanned by that set (TauCeti.IsCompactModule.span_completedGroupAlgebraModule_eq_top_of_dense_closure_univ_smul).