Theory of topological modules

We use the class ContinuousSMul for topological (semi) modules and topological vector spaces.

theorem ContinuousSMul.of_nhds_zero {R : Type u_1} {M : Type u_2} [Ring R] [TopologicalSpace R] [TopologicalSpace M] [AddCommGroup M] [Module R M] [IsTopologicalRing R] [IsTopologicalAddGroup M] (hmul : Filter.Tendsto (fun (p : R × M) => p.1 • p.2) (nhds 0 ×ˢ nhds 0) (nhds 0)) (hmulleft : ∀ (m : M), Filter.Tendsto (fun (a : R) => a • m) (nhds 0) (nhds 0)) (hmulright : ∀ (a : R), Filter.Tendsto (fun (m : M) => a • m) (nhds 0) (nhds 0)) : ContinuousSMul R M

theorem Submodule.eq_top_of_nonempty_interior' {R : Type u_1} {M : Type u_2} [Ring R] [TopologicalSpace R] [TopologicalSpace M] [AddCommGroup M] [ContinuousAdd M] [Module R M] [ContinuousSMul R M] [(nhdsWithin 0 {x : R | IsUnit x}).NeBot] (s : Submodule R M) (hs : (interior ↑s).Nonempty) : s = ⊤

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.

theorem Module.punctured_nhds_neBot (R : Type u_1) (M : Type u_2) [Ring R] [TopologicalSpace R] [TopologicalSpace M] [AddCommGroup M] [ContinuousAdd M] [Module R M] [ContinuousSMul R M] [Nontrivial M] [(nhdsWithin 0 {0}ᶜ).NeBot] [NoZeroSMulDivisors R M] (x : M) : (nhdsWithin x {x}ᶜ).NeBot

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.

theorem continuousSMul_induced {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [SMul R M₁] [SMul R M₂] [u : TopologicalSpace R] {t : TopologicalSpace M₂} [ContinuousSMul R M₂] {F : Type u_4} [FunLike F M₁ M₂] [MulActionHomClass F R M₁ M₂] (f : F) : ContinuousSMul R M₁

theorem TopologicalSpace.IsSeparable.span {R : Type u_1} {M : Type u_2} [AddCommMonoid M] [Semiring R] [Module R M] [TopologicalSpace M] [TopologicalSpace R] [SeparableSpace R] [ContinuousAdd M] [ContinuousSMul R M] {s : Set M} (hs : IsSeparable s) : IsSeparable ↑(Submodule.span R s)

The span of a separable subset with respect to a separable scalar ring is again separable.

instance Submodule.topologicalAddGroup {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [IsTopologicalAddGroup M] (S : Submodule R M) : IsTopologicalAddGroup ↥S

theorem Submodule.mapsTo_smul_closure {R : Type u} {M : Type v} [Semiring R] [TopologicalSpace M] [AddCommMonoid M] [Module R M] [ContinuousConstSMul R M] (s : Submodule R M) (c : R) : Set.MapsTo (fun (x : M) => c • x) (closure ↑s) (closure ↑s)

theorem Submodule.smul_closure_subset {R : Type u} {M : Type v} [Semiring R] [TopologicalSpace M] [AddCommMonoid M] [Module R M] [ContinuousConstSMul R M] (s : Submodule R M) (c : R) : c • closure ↑s ⊆ closure ↑s

def Submodule.topologicalClosure {R : Type u} {M : Type v} [Semiring R] [TopologicalSpace M] [AddCommMonoid M] [Module R M] [ContinuousConstSMul R M] [ContinuousAdd M] (s : Submodule R M) : Submodule R M

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' := ⋯ }

@[simp]

theorem Submodule.topologicalClosure_coe {R : Type u} {M : Type v} [Semiring R] [TopologicalSpace M] [AddCommMonoid M] [Module R M] [ContinuousConstSMul R M] [ContinuousAdd M] (s : Submodule R M) : ↑s.topologicalClosure = closure ↑s

theorem Submodule.le_topologicalClosure {R : Type u} {M : Type v} [Semiring R] [TopologicalSpace M] [AddCommMonoid M] [Module R M] [ContinuousConstSMul R M] [ContinuousAdd M] (s : Submodule R M) : s ≤ s.topologicalClosure

theorem Submodule.closure_subset_topologicalClosure_span {R : Type u} {M : Type v} [Semiring R] [TopologicalSpace M] [AddCommMonoid M] [Module R M] [ContinuousConstSMul R M] [ContinuousAdd M] (s : Set M) : closure s ⊆ ↑(span R s).topologicalClosure

theorem Submodule.isClosed_topologicalClosure {R : Type u} {M : Type v} [Semiring R] [TopologicalSpace M] [AddCommMonoid M] [Module R M] [ContinuousConstSMul R M] [ContinuousAdd M] (s : Submodule R M) : IsClosed ↑s.topologicalClosure

theorem Submodule.topologicalClosure_minimal {R : Type u} {M : Type v} [Semiring R] [TopologicalSpace M] [AddCommMonoid M] [Module R M] [ContinuousConstSMul R M] [ContinuousAdd M] (s : Submodule R M) {t : Submodule R M} (h : s ≤ t) (ht : IsClosed ↑t) : s.topologicalClosure ≤ t

theorem Submodule.topologicalClosure_mono {R : Type u} {M : Type v} [Semiring R] [TopologicalSpace M] [AddCommMonoid M] [Module R M] [ContinuousConstSMul R M] [ContinuousAdd M] {s t : Submodule R M} (h : s ≤ t) : s.topologicalClosure ≤ t.topologicalClosure

theorem IsClosed.submodule_topologicalClosure_eq {R : Type u} {M : Type v} [Semiring R] [TopologicalSpace M] [AddCommMonoid M] [Module R M] [ContinuousConstSMul R M] [ContinuousAdd M] {s : Submodule R M} (hs : IsClosed ↑s) : s.topologicalClosure = s

The topological closure of a closed submodule s is equal to s.

theorem Submodule.dense_iff_topologicalClosure_eq_top {R : Type u} {M : Type v} [Semiring R] [TopologicalSpace M] [AddCommMonoid M] [Module R M] [ContinuousConstSMul R M] [ContinuousAdd M] {s : Submodule R M} : Dense ↑s ↔ s.topologicalClosure = ⊤

A subspace is dense iff its topological closure is the entire space.

instance Submodule.topologicalClosure.completeSpace {R : Type u} [Semiring R] {M' : Type u_1} [AddCommMonoid M'] [Module R M'] [UniformSpace M'] [ContinuousAdd M'] [ContinuousConstSMul R M'] [CompleteSpace M'] (U : Submodule R M') : CompleteSpace ↥U.topologicalClosure

theorem Submodule.isClosed_or_dense_of_isCoatom {R : Type u} {M : Type v} [Semiring R] [TopologicalSpace M] [AddCommMonoid M] [Module R M] [ContinuousConstSMul R M] [ContinuousAdd M] (s : Submodule R M) (hs : IsCoatom s) : IsClosed ↑s ∨ Dense ↑s

A maximal proper subspace of a topological module (i.e a Submodule satisfying IsCoatom) is either closed or dense.

theorem Submodule.closure_coe_iSup_map_single {ι : Type u_1} {R : Type u_2} {M : ι → Type u_3} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [(i : ι) → TopologicalSpace (M i)] [DecidableEq ι] (s : (i : ι) → Submodule R (M i)) : closure ↑(⨆ (i : ι), map (LinearMap.single R M i) (s i)) = Set.univ.pi fun (i : ι) => closure ↑(s i)

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.

theorem Submodule.topologicalClosure_iSup_map_single {ι : Type u_1} {R : Type u_2} {M : ι → Type u_3} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [(i : ι) → TopologicalSpace (M i)] [DecidableEq ι] [∀ (i : ι), ContinuousAdd (M i)] [∀ (i : ι), ContinuousConstSMul R (M i)] (s : (i : ι) → Submodule R (M i)) : (⨆ (i : ι), map (LinearMap.single R M i) (s i)).topologicalClosure = pi Set.univ fun (i : ι) => (s i).topologicalClosure

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.

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

def linearMapOfMemClosureRangeCoe {M₁ : Type u_1} {M₂ : Type u_2} {R : Type u_4} {S : Type u_5} [TopologicalSpace M₂] [T2Space M₂] [Semiring R] [Semiring S] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module S M₂] [ContinuousConstSMul S M₂] [ContinuousAdd M₂] {σ : R →+* S} (f : M₁ → M₂) (hf : f ∈ closure (Set.range DFunLike.coe)) : M₁ →ₛₗ[σ] M₂

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' := ⋯ }

@[simp]

theorem linearMapOfMemClosureRangeCoe_apply {M₁ : Type u_1} {M₂ : Type u_2} {R : Type u_4} {S : Type u_5} [TopologicalSpace M₂] [T2Space M₂] [Semiring R] [Semiring S] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module S M₂] [ContinuousConstSMul S M₂] [ContinuousAdd M₂] {σ : R →+* S} (f : M₁ → M₂) (hf : f ∈ closure (Set.range DFunLike.coe)) : ⇑(linearMapOfMemClosureRangeCoe f hf) = (↑(addMonoidHomOfMemClosureRangeCoe f hf)).toFun

def linearMapOfTendsto {M₁ : Type u_1} {M₂ : Type u_2} {α : Type u_3} {R : Type u_4} {S : Type u_5} [TopologicalSpace M₂] [T2Space M₂] [Semiring R] [Semiring S] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module S M₂] [ContinuousConstSMul S M₂] [ContinuousAdd M₂] {σ : R →+* S} {l : Filter α} (f : M₁ → M₂) (g : α → M₁ →ₛₗ[σ] M₂) [l.NeBot] (h : Filter.Tendsto (fun (a : α) (x : M₁) => (g a) x) l (nhds f)) : M₁ →ₛₗ[σ] M₂

Construct a bundled linear map from a pointwise limit of linear maps

Equations

• linearMapOfTendsto f g h = linearMapOfMemClosureRangeCoe f ⋯

@[simp]

theorem linearMapOfTendsto_apply {M₁ : Type u_1} {M₂ : Type u_2} {α : Type u_3} {R : Type u_4} {S : Type u_5} [TopologicalSpace M₂] [T2Space M₂] [Semiring R] [Semiring S] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module S M₂] [ContinuousConstSMul S M₂] [ContinuousAdd M₂] {σ : R →+* S} {l : Filter α} (f : M₁ → M₂) (g : α → M₁ →ₛₗ[σ] M₂) [l.NeBot] (h : Filter.Tendsto (fun (a : α) (x : M₁) => (g a) x) l (nhds f)) : ⇑(linearMapOfTendsto f g h) = f

theorem LinearMap.isClosed_range_coe (M₁ : Type u_1) (M₂ : Type u_2) {R : Type u_4} {S : Type u_5} [TopologicalSpace M₂] [T2Space M₂] [Semiring R] [Semiring S] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module S M₂] [ContinuousConstSMul S M₂] [ContinuousAdd M₂] (σ : R →+* S) : IsClosed (Set.range DFunLike.coe)

instance QuotientModule.Quotient.topologicalSpace {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] (S : Submodule R M) : TopologicalSpace (M ⧸ S)

Equations

• QuotientModule.Quotient.topologicalSpace S = inferInstanceAs (TopologicalSpace (Quotient S.quotientRel))

theorem Submodule.isOpenMap_mkQ {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] (S : Submodule R M) [ContinuousAdd M] : IsOpenMap ⇑S.mkQ

theorem Submodule.isOpenQuotientMap_mkQ {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] (S : Submodule R M) [ContinuousAdd M] : IsOpenQuotientMap ⇑S.mkQ

instance Submodule.topologicalAddGroup_quotient {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] (S : Submodule R M) [IsTopologicalAddGroup M] : IsTopologicalAddGroup (M ⧸ S)

instance Submodule.continuousSMul_quotient {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] (S : Submodule R M) [TopologicalSpace R] [IsTopologicalAddGroup M] [ContinuousSMul R M] : ContinuousSMul R (M ⧸ S)

instance Submodule.t3_quotient_of_isClosed {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] (S : Submodule R M) [IsTopologicalAddGroup M] [IsClosed ↑S] : T3Space (M ⧸ S)