Automatic continuity over compact coefficient rings

A finitely generated Hausdorff topological module over a compact ring has the module topology. Consequently every linear map from it to a topological module is continuous. In particular this applies to finitely generated compact Hausdorff topological ℤ_p-modules with continuous addition and scalar action, allowing algebraic maps between abelian pro-p groups to be used as maps of topological groups.

Implementation notes

A surjection (Fin n → R) →ₗ[R] M is a continuous map from a compact space to a Hausdorff space, hence a quotient map. The topology of M is therefore coinduced from the product topology, and since every linear map out of Fin n → R is continuous into the module topology of M, the given topology is no coarser than the module topology. It is also no finer, because the module topology is the finest topology for which addition and scalar multiplication are continuous, so IsModuleTopology.of_continuous_id identifies the two.

theorem TauCeti.isModuleTopology_of_finite_of_compactSpace {R : Type u_1} [Semiring R] [TopologicalSpace R] [CompactSpace R] {M : Type u_2} [AddCommMonoid M] [Module R M] [Module.Finite R M] [TopologicalSpace M] [T2Space M] [ContinuousAdd M] [ContinuousSMul R M] : IsModuleTopology R M

A finitely generated Hausdorff topological module over a compact semiring has the module topology.

theorem LinearMap.continuous_of_finite_of_compactSpace {R : Type u_1} [Semiring R] [TopologicalSpace R] [CompactSpace R] {M : Type u_2} [AddCommMonoid M] [Module R M] [Module.Finite R M] [TopologicalSpace M] [T2Space M] [ContinuousAdd M] [ContinuousSMul R M] {N : Type u_3} [AddCommMonoid N] [Module R N] [TopologicalSpace N] [ContinuousAdd N] [ContinuousSMul R N] (f : M →ₗ[R] N) : Continuous ⇑f

Every linear map from a finitely generated Hausdorff topological module over a compact semiring to a topological module is continuous.