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]
[TopologicalRing R]
[TopologicalAddGroup 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)
:
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]
[TopologicalSpace.SeparableSpace R]
[ContinuousAdd M]
[ContinuousSMul R M]
{s : Set M}
(hs : TopologicalSpace.IsSeparable s)
:
The span of a separable subset with respect to a separable scalar ring is again separable.
instance
Submodule.topologicalAddGroup
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
[Ring α]
[AddCommGroup β]
[Module α β]
[TopologicalAddGroup β]
(S : Submodule α β)
:
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)
:
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' := ⋯ }
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)
:
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 ⊆ ↑(Submodule.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}
:
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)
:
A maximal proper subspace of a topological module (i.e a Submodule satisfying IsCoatom)
is either closed or dense.
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))
:
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
@[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))
:
Construct a bundled linear map from a pointwise limit of linear maps
Equations
- linearMapOfTendsto f g h = linearMapOfMemClosureRangeCoe f ⋯
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)
:
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)
[TopologicalAddGroup M]
:
TopologicalAddGroup (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]
[TopologicalAddGroup 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)
[TopologicalAddGroup M]
[IsClosed ↑S]
: