Documentation

TauCeti.Topology.Algebra.Nonarchimedean.LinearTopology

A linear topology is nonarchimedean and compatible with multiplication #

If the neighbourhoods of zero of a topological module M over R have a basis of open submodules (IsLinearTopology R M), then every neighbourhood of zero contains an open additive subgroup, namely the underlying subgroup of an open submodule. So M is a nonarchimedean additive group, and a linearly topologized ring is a nonarchimedean ring. A ring that is linearly topologized on both sides, with topological additive group, is a topological ring, because open ideals absorb multiplication.

These are theorems rather than instances: Tau Ceti has the converse instance TauCeti.NonarchimedeanAddGroup.isLinearTopology over a compact ring, and the two together would form an instance loop.

Main results #

source
theorem IsLinearTopology.isTopologicalRing {R : Type u_1} [Ring R] [TopologicalSpace R] [IsTopologicalAddGroup R] [IsLinearTopology R R] [IsLinearTopology Rᵐᵒᵖ R] :
IsTopologicalRing R

A two-sided linearly topologised ring is a topological ring, as soon as its additive group is topological. For a commutative ring the Rᵐᵒᵖ hypothesis is supplied automatically.

source
theorem IsLinearTopology.nonarchimedeanAddGroup (R : Type u_1) {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [IsTopologicalAddGroup M] [IsLinearTopology R M] :
NonarchimedeanAddGroup M

A linearly topologized module is a nonarchimedean additive group: each open submodule inside a neighbourhood of zero is an open additive subgroup.

source
theorem IsLinearTopology.nonarchimedeanRing (R : Type u_1) [Ring R] [TopologicalSpace R] [IsTopologicalRing R] [IsLinearTopology R R] :
NonarchimedeanRing R

A linearly topologized ring is a nonarchimedean ring: each open ideal inside a neighbourhood of zero is an open additive subgroup.