Theory of topological modules #
We use the class ContinuousSMul for topological (semi) modules and topological vector spaces.
A topological module over a ring has continuous negation.
This cannot be an instance, because it would cause search for [Module ?R M] with unknown R.
If M is a topological module over R and 0 is a limit of invertible elements of R, then
⊤ is the only submodule of M with a nonempty interior.
This is the case, e.g., if R is a nontrivially normed field.
Let R be a topological ring such that zero is not an isolated point (e.g., a nontrivially
normed field, see NormedField.punctured_nhds_neBot). Let M be a nontrivial module over R
such that c • x = 0 implies c = 0 ∨ x = 0. Then M has no isolated points. We formulate this
using NeBot (𝓝[≠] x).
This lemma is not an instance because Lean would need to find [ContinuousSMul ?m_1 M] with
unknown ?m_1. We register this as an instance for R = ℝ in Real.punctured_nhds_module_neBot.
One can also use haveI := Module.punctured_nhds_neBot R M in a proof.
The span of a separable subset with respect to a separable scalar ring is again separable.
The (topological-space) closure of a submodule of a topological R-module M is itself
a submodule.
Equations
- s.topologicalClosure = { toAddSubmonoid := s.topologicalClosure, smul_mem' := ⋯ }
Instances For
The topological closure of a closed submodule s is equal to s.
A subspace is dense iff its topological closure is the entire space.
A maximal proper subspace of a topological module (i.e a Submodule satisfying IsCoatom)
is either closed or dense.
If s i is a family of submodules, each is in its module,
then the closure of their span in the indexed product of the modules
is the product of their closures.
In case of a finite index type, this statement immediately follows from Submodule.iSup_map_single.
However, the statement is true for an infinite index type as well.
If s i is a family of submodules, each is in its module,
then the closure of their span in the indexed product of the modules
is the product of their closures.
In case of a finite index type, this statement immediately follows from Submodule.iSup_map_single.
However, the statement is true for an infinite index type as well.
This version is stated in terms of Submodule.topologicalClosure,
thus assumes that M is are topological modules over R.
However, the statement is true without assuming continuity of the operations,
see Submodule.closure_coe_iSup_map_single above.
Constructs a bundled linear map from a function and a proof that this function belongs to the closure of the set of linear maps.
Equations
- linearMapOfMemClosureRangeCoe f hf = { toFun := (↑(addMonoidHomOfMemClosureRangeCoe f hf)).toFun, map_add' := ⋯, map_smul' := ⋯ }
Instances For
Construct a bundled linear map from a pointwise limit of linear maps
Equations
- linearMapOfTendsto f g h = linearMapOfMemClosureRangeCoe f ⋯