Theorems · Inductive type · commutative algebra

IsLinearTopology

(R : Type u_1) →
  (M : Type u_3) → [inst : Ring R] → [inst_1 : AddCommGroup M] → [Module R M] → [TopologicalSpace M] → Prop

Consider a (left-)module M over a ring R. A topology on M is `R`-linear if the open sub-R-modules of M form a basis of neighborhoods of zero. Typically one would also that the topology is invariant by translation (ContinuousConstVAdd M M), or equivalently that M is a topological group, but we do not assume it for the definition. In particular, we say that a topology on the ring R is linear if it is both R-linear and Rᵐᵒᵖ-linear for the obvious module structures. To spell this in Lean, simply use [IsLinearTopology R R] [IsLinearTopology Rᵐᵒᵖ R].

Defined in

Mathlib.Topology.Algebra.LinearTopology

Cited by

83 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

RingAddCommGroupModuleTopologicalSpace