Theory of topological modules and continuous linear maps. #
We use the class ContinuousSMul
for topological (semi) modules and topological vector spaces.
In this file we define continuous (semi-)linear maps, as semilinear maps between topological
modules which are continuous. The set of continuous semilinear maps between the topological
R₁
-module M
and R₂
-module M₂
with respect to the RingHom
σ
is denoted by M →SL[σ] M₂
.
Plain linear maps are denoted by M →L[R] M₂
and star-linear maps by M →L⋆[R] M₂
.
The corresponding notation for equivalences is M ≃SL[σ] M₂
, M ≃L[R] M₂
and M ≃L⋆[R] M₂
.
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.
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.
- toFun : M → M₂
- map_add' : ∀ (x y : M), AddHom.toFun s.toAddHom (x + y) = AddHom.toFun s.toAddHom x + AddHom.toFun s.toAddHom y
- map_smul' : ∀ (r : R) (x : M), AddHom.toFun s.toAddHom (r • x) = ↑σ r • AddHom.toFun s.toAddHom x
- cont : Continuous s.toFun
Continuous linear maps between modules. We only put the type classes that are necessary for the definition, although in applications
M
andM₂
will be topological modules over the topological ringR
.
Continuous linear maps between modules. We only put the type classes that are necessary for the
definition, although in applications M
and M₂
will be topological modules over the topological
ring R
.
Instances For
Continuous linear maps between modules. We only put the type classes that are necessary for the
definition, although in applications M
and M₂
will be topological modules over the topological
ring R
.
Instances For
Continuous linear maps between modules. We only put the type classes that are necessary for the
definition, although in applications M
and M₂
will be topological modules over the topological
ring R
.
Instances For
Continuous linear maps between modules. We only put the type classes that are necessary for the
definition, although in applications M
and M₂
will be topological modules over the topological
ring R
.
Instances For
- coe : F → M → M₂
- coe_injective' : Function.Injective FunLike.coe
- map_continuous : ∀ (f : F), Continuous ↑f
Continuity
ContinuousSemilinearMapClass F σ M M₂
asserts F
is a type of bundled continuous
σ
-semilinear maps M → M₂
. See also ContinuousLinearMapClass F R M M₂
for the case where
σ
is the identity map on R
. A map f
between an R
-module and an S
-module over a ring
homomorphism σ : R →+* S
is semilinear if it satisfies the two properties f (x + y) = f x + f y
and f (c • x) = (σ c) • f x
.
Instances
ContinuousLinearMapClass F R M M₂
asserts F
is a type of bundled continuous
R
-linear maps M → M₂
. This is an abbreviation for
ContinuousSemilinearMapClass F (RingHom.id R) M M₂
.
Instances For
- toFun : M → M₂
- map_add' : ∀ (x y : M), AddHom.toFun s.toAddHom (x + y) = AddHom.toFun s.toAddHom x + AddHom.toFun s.toAddHom y
- map_smul' : ∀ (r : R) (x : M), AddHom.toFun s.toAddHom (r • x) = ↑σ r • AddHom.toFun s.toAddHom x
- invFun : M₂ → M
- left_inv : Function.LeftInverse s.invFun s.toFun
- right_inv : Function.RightInverse s.invFun s.toFun
- continuous_toFun : Continuous s.toFun
Continuous linear equivalences between modules. We only put the type classes that are necessary for the definition, although in applications
M
andM₂
will be topological modules over the topological semiringR
. - continuous_invFun : Continuous s.invFun
Continuous linear equivalences between modules. We only put the type classes that are necessary for the definition, although in applications
M
andM₂
will be topological modules over the topological semiringR
.
Continuous linear equivalences between modules. We only put the type classes that are necessary
for the definition, although in applications M
and M₂
will be topological modules over the
topological semiring R
.
Instances For
Continuous linear equivalences between modules. We only put the type classes that are necessary
for the definition, although in applications M
and M₂
will be topological modules over the
topological semiring R
.
Instances For
Continuous linear equivalences between modules. We only put the type classes that are necessary
for the definition, although in applications M
and M₂
will be topological modules over the
topological semiring R
.
Instances For
Continuous linear equivalences between modules. We only put the type classes that are necessary
for the definition, although in applications M
and M₂
will be topological modules over the
topological semiring R
.
Instances For
- coe : F → M → M₂
- inv : F → M₂ → M
- left_inv : ∀ (e : F), Function.LeftInverse (EquivLike.inv e) (EquivLike.coe e)
- right_inv : ∀ (e : F), Function.RightInverse (EquivLike.inv e) (EquivLike.coe e)
- coe_injective' : ∀ (e g : F), EquivLike.coe e = EquivLike.coe g → EquivLike.inv e = EquivLike.inv g → e = g
- map_continuous : ∀ (f : F), Continuous ↑f
ContinuousSemilinearEquivClass F σ M M₂
assertsF
is a type of bundled continuousσ
-semilinear equivsM → M₂
. See alsoContinuousLinearEquivClass F R M M₂
for the case whereσ
is the identity map onR
. A mapf
between anR
-module and anS
-module over a ring homomorphismσ : R →+* S
is semilinear if it satisfies the two propertiesf (x + y) = f x + f y
andf (c • x) = (σ c) • f x
. - inv_continuous : ∀ (f : F), Continuous (EquivLike.inv f)
ContinuousSemilinearEquivClass F σ M M₂
assertsF
is a type of bundled continuousσ
-semilinear equivsM → M₂
. See alsoContinuousLinearEquivClass F R M M₂
for the case whereσ
is the identity map onR
. A mapf
between anR
-module and anS
-module over a ring homomorphismσ : R →+* S
is semilinear if it satisfies the two propertiesf (x + y) = f x + f y
andf (c • x) = (σ c) • f x
.
ContinuousSemilinearEquivClass F σ M M₂
asserts F
is a type of bundled continuous
σ
-semilinear equivs M → M₂
. See also ContinuousLinearEquivClass F R M M₂
for the case
where σ
is the identity map on R
. A map f
between an R
-module and an S
-module over a ring
homomorphism σ : R →+* S
is semilinear if it satisfies the two properties f (x + y) = f x + f y
and f (c • x) = (σ c) • f x
.
Instances
ContinuousLinearEquivClass F σ M M₂
asserts F
is a type of bundled continuous
R
-linear equivs M → M₂
. This is an abbreviation for
ContinuousSemilinearEquivClass F (RingHom.id R) M M₂
.
Instances For
Constructs a bundled linear map from a function and a proof that this function belongs to the closure of the set of linear maps.
Instances For
Construct a bundled linear map from a pointwise limit of linear maps
Instances For
Properties that hold for non-necessarily commutative semirings. #
Coerce continuous linear maps to linear maps.
Coerce continuous linear maps to functions.
See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.
Instances For
See Note [custom simps projection].
Instances For
Copy of a ContinuousLinearMap
with a new toFun
equal to the old one. Useful to fix
definitional equalities.
Instances For
If two continuous linear maps are equal on a set s
, then they are equal on the closure
of the Submodule.span
of this set.
If the submodule generated by a set s
is dense in the ambient module, then two continuous
linear maps equal on s
are equal.
Under a continuous linear map, the image of the TopologicalClosure
of a submodule is
contained in the TopologicalClosure
of its image.
Under a dense continuous linear map, a submodule whose TopologicalClosure
is ⊤
is sent to
another such submodule. That is, the image of a dense set under a map with dense range is dense.
The continuous map that is constantly zero.
the identity map as a continuous linear map.
Instances For
Composition of bounded linear maps.
Instances For
Composition of bounded linear maps.
Instances For
ContinuousLinearMap.toLinearMap
as a RingHom
.
Instances For
The tautological action by M₁ →L[R₁] M₁
on M
.
This generalizes Function.End.applyMulAction
.
ContinuousLinearMap.applyModule
is faithful.
The cartesian product of two bounded linear maps, as a bounded linear map.
Instances For
The left injection into a product is a continuous linear map.
Instances For
The right injection into a product is a continuous linear map.
Instances For
Restrict codomain of a continuous linear map.
Instances For
Submodule.subtype
as a ContinuousLinearMap
.
Instances For
Prod.fst
as a ContinuousLinearMap
.
Instances For
Prod.snd
as a ContinuousLinearMap
.
Instances For
Prod.map
of two continuous linear maps.
Instances For
The continuous linear map given by (x, y) ↦ f₁ x + f₂ y
.
Instances For
The linear map fun x => c x • f
. Associates to a scalar-valued linear map and an element of
M₂
the M₂
-valued linear map obtained by multiplying the two (a.k.a. tensoring by M₂
).
See also ContinuousLinearMap.smulRightₗ
and ContinuousLinearMap.smulRightL
.
Instances For
Given an element x
of a topological space M
over a semiring R
, the natural continuous
linear map from R
to M
by taking multiples of x
.
Instances For
A special case of to_span_singleton_smul'
for when R
is commutative.
pi
construction for continuous linear functions. From a family of continuous linear functions
it produces a continuous linear function into a family of topological modules.
Instances For
The projections from a family of topological modules are continuous linear maps.
Instances For
If I
and J
are complementary index sets, the product of the kernels of the J
th projections
of φ
is linearly equivalent to the product over I
.
Instances For
Given a right inverse f₂ : M₂ →L[R] M
to f₁ : M →L[R] M₂
,
projKerOfRightInverse f₁ f₂ h
is the projection M →L[R] LinearMap.ker f₁
along
LinearMap.range f₂
.
Instances For
A nonzero continuous linear functional is open.
ContinuousLinearMap.prod
as an Equiv
.