Documentation

theorem ContinuousNeg.of_continuousConstSMul (R : Type u_1) (M : Type u_2) [Ring R] [TopologicalSpace M] [AddCommGroup M] [Module R M] [ContinuousConstSMul R M] :

ContinuousNeg M

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.

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] [IsDomain R] [Nontrivial M] [(nhdsWithin 0 {0}ᶜ).NeBot] [IsTorsionFree 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} {S : Type u_2} {M₁ : Type u_3} {M₂' : Type u_5} {φ : R → S} [SMul R M₁] [SMul S M₂'] [u : TopologicalSpace R] [u' : TopologicalSpace S] {t' : TopologicalSpace M₂'} [ContinuousSMul S M₂'] {F' : Type u_7} [FunLike F' M₁ M₂'] [MulActionSemiHomClass F' φ M₁ M₂'] (f' : F') (hφ : Continuous φ) :

ContinuousSMul R M₁

theorem continuousSMul_induced {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [SMul R M₁] [SMul R M₂] [u : TopologicalSpace R] {t : TopologicalSpace M₂} [ContinuousSMul R M₂] {F : Type u_6} [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

Instances For

@[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.

instance instCompleteSpaceSubtypeMemSubmoduleOfIsClosedCoe {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [UniformSpace M] [Module R M] [CompleteSpace M] (K : Submodule R M) [c : IsClosed ↑K] :

CompleteSpace ↥K

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

Instances For

@[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

Instances For

@[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

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)