Compact modules underlying abelian pro-p groups

The canonical ℤ_[p]-module structure on an abelian pro-p group is a compact module in the sense of TauCeti.IsCompactModule. It has the same finite generation theory as the underlying topological group. A finite topological generating set spans the module because its ℤ_[p]-span is closed. Conversely, an algebraic module generating set generates a dense subgroup: multiplication by an arbitrary p-adic scalar is approximated by natural-number multiples, using the density of ℕ in ℤ_[p].

Thus a topologically finitely generated abelian pro-p group is a finitely generated ℤ_[p]-module, the input needed for the structure theorem for compact abelian pro-p groups.

Main results

• TauCeti.IsProP.isCompactModule: an abelian pro-p group is a compact ℤ_[p]-module.
• TauCeti.IsProP.topologicalClosure_closure_eq_top_iff_span_eq_top: a finite subset topologically generates an abelian pro-p group exactly when it spans its canonical ℤ_[p]-module.
• TauCeti.IsProP.isTopologicallyFinitelyGenerated_iff_module_finite: topological finite generation of an abelian pro-p group is equivalent to finite generation of its canonical ℤ_[p]-module.
• TauCeti.IsProP.exists_finite_subset_le_topologicalClosure_closure, TauCeti.IsProP.isTopologicallyFinitelyGenerated_of_isClosed: a closed subgroup of a topologically finitely generated abelian pro-p group is topologically finitely generated, by finitely many of its own elements.

References

• L. Ribes and P. Zalesskii, Profinite Groups, Section 4.3.

theorem TauCeti.IsProP.isCompactModule {p : ℕ} [Fact (Nat.Prime p)] {A : Type u_1} [CommGroup A] [TopologicalSpace A] [IsTopologicalGroup A] [CompactSpace A] [TotallyDisconnectedSpace A] (hA : IsProP p A) : IsCompactModule ℤ_[p] (Additive A)

An abelian pro-p group is a compact ℤ_p-module, for the module structure TauCeti.IsProP.module.

theorem TauCeti.IsProP.span_le_topologicalClosure_closure {p : ℕ} [Fact (Nat.Prime p)] {A : Type u_1} [CommGroup A] [TopologicalSpace A] [IsTopologicalGroup A] [CompactSpace A] [TotallyDisconnectedSpace A] (hA : IsProP p A) (s : Set (Additive A)) : ↑(Submodule.span ℤ_[p] s) ⊆ ↑(AddSubgroup.closure s).topologicalClosure

An element of the ℤ_[p]-span of s lies in the topological closure of the additive subgroup generated by s.

theorem TauCeti.IsProP.topologicalClosure_closure_eq_top_iff_span_eq_top {p : ℕ} [Fact (Nat.Prime p)] {A : Type u_1} [CommGroup A] [TopologicalSpace A] [IsTopologicalGroup A] [CompactSpace A] [TotallyDisconnectedSpace A] (hA : IsProP p A) {s : Set A} (hs : s.Finite) : (Subgroup.closure s).topologicalClosure = ⊤ ↔ Submodule.span ℤ_[p] (⇑Additive.toMul ⁻¹' s) = ⊤

A finite subset topologically generates an abelian pro-p group exactly when it spans the canonical ℤ_[p]-module TauCeti.IsProP.module.

theorem TauCeti.IsProP.isTopologicallyFinitelyGenerated_iff_module_finite {p : ℕ} [Fact (Nat.Prime p)] {A : Type u_1} [CommGroup A] [TopologicalSpace A] [IsTopologicalGroup A] [CompactSpace A] [TotallyDisconnectedSpace A] (hA : IsProP p A) : IsTopologicallyFinitelyGenerated A ↔ Module.Finite ℤ_[p] (Additive A)

Compact abelian pro-p groups have the same algebraic and topological notion of finite generation. The module structure in the right-hand side is TauCeti.IsProP.module.

theorem TauCeti.IsProP.exists_finite_subset_le_topologicalClosure_closure {p : ℕ} [Fact (Nat.Prime p)] {A : Type u_1} [CommGroup A] [TopologicalSpace A] [IsTopologicalGroup A] [CompactSpace A] [TotallyDisconnectedSpace A] (hA : IsProP p A) (hfg : IsTopologicallyFinitelyGenerated A) {K : Subgroup A} (hK : IsClosed ↑K) : ∃ (t : Set A), t.Finite ∧ t ⊆ ↑K ∧ K ≤ (Subgroup.closure t).topologicalClosure

Closed subgroups of topologically finitely generated abelian pro-p groups are topologically finitely generated, by finitely many of their own elements: a closed subgroup is a ℤ_p-submodule of the canonical module TauCeti.IsProP.module, which is a finitely generated module over the Noetherian ring ℤ_p.

theorem TauCeti.IsProP.isTopologicallyFinitelyGenerated_of_isClosed {p : ℕ} [Fact (Nat.Prime p)] {A : Type u_1} [CommGroup A] [TopologicalSpace A] [IsTopologicalGroup A] [CompactSpace A] [TotallyDisconnectedSpace A] (hA : IsProP p A) (hfg : IsTopologicallyFinitelyGenerated A) {K : Subgroup A} (hK : IsClosed ↑K) : IsTopologicallyFinitelyGenerated ↥K

A closed subgroup of a topologically finitely generated abelian pro-p group is topologically finitely generated.