Continuous linear maps #
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₂
.
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
.
- toFun : M → M₂
- cont : Continuous (↑self).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
.
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
.
Equations
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
.
Equations
Instances For
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₂
.
Equations
Instances For
Properties that hold for non-necessarily commutative semirings. #
Coerce continuous linear maps to linear maps.
Equations
Equations
See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.
Equations
Instances For
See Note [custom simps projection].
Equations
Instances For
Copy of a ContinuousLinearMap
with a new toFun
equal to the old one. Useful to fix
definitional equalities.
Equations
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.
Equations
Equations
The continuous map that is constantly zero.
Equations
Equations
Equations
Equations
the identity map as a continuous linear map.
Equations
Instances For
Equations
Equations
Equations
Composition of bounded linear maps.
Equations
Instances For
Composition of bounded linear maps.
Equations
Instances For
g ∘ f = id
as ContinuousLinearMap
s implies g ∘ f = id
as functions.
f ∘ g = id
as ContinuousLinearMap
s implies f ∘ g = id
as functions.
Equations
Equations
Equations
Equations
ContinuousLinearMap.toLinearMap
as a RingHom
.
Equations
Instances For
The tautological action by M₁ →L[R₁] M₁
on M
.
This generalizes Function.End.applyMulAction
.
Equations
ContinuousLinearMap.applyModule
is faithful.
Restrict codomain of a continuous linear map.
Equations
Instances For
Restrict the codomain of a continuous linear map f
to f.range
.
Equations
Instances For
Submodule.subtype
as a ContinuousLinearMap
.
Equations
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
.
Equations
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
.
Equations
Instances For
A special case of to_span_singleton_smul'
for when R
is commutative.
Equations
Equations
Equations
Equations
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₂
.
Equations
Instances For
A nonzero continuous linear functional is open.
Equations
Equations
The coercion from M →L[R] M₂
to M →ₗ[R] M₂
, as a linear map.
Equations
Instances For
The coercion from M →SL[σ] M₂
to M →ₛₗ[σ] M₂
, as a linear map.
Equations
Instances For
Given c : E →L[R] S
, c.smulRightₗ
is the linear map from F
to E →L[R] F
sending f
to fun e => c e • f
. See also ContinuousLinearMap.smulRightL
.
Equations
Instances For
Equations
If A
is an R
-algebra, then a continuous A
-linear map can be interpreted as a continuous
R
-linear map. We assume LinearMap.CompatibleSMul M₁ M₂ R A
to match assumptions of
LinearMap.map_smul_of_tower
.
Equations
Instances For
ContinuousLinearMap.restrictScalars
as a LinearMap
. See also
ContinuousLinearMap.restrictScalarsL
.
Equations
Instances For
A submodule p
is called complemented if there exists a continuous projection M →ₗ[R] p
.