Theory of topological modules and continuous linear maps. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We use the class has_continuous_smul
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 ring_hom
σ
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 normed_field.punctured_nhds_ne_bot
). 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 ne_bot (𝓝[≠] x)
.
This lemma is not an instance because Lean would need to find [has_continuous_smul ?m_1 M]
with
unknown ?m_1
. We register this as an instance for R = ℝ
in real.punctured_nhds_module_ne_bot
.
One can also use haveI := module.punctured_nhds_ne_bot R M
in a proof.
The (topological-space) closure of a submodule of a topological R
-module M
is itself
a submodule.
Equations
Instances for ↥submodule.topological_closure
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 is_coatom
)
is either closed or dense.
- to_linear_map : M →ₛₗ[σ] M₂
- cont : continuous self.to_linear_map.to_fun . "continuity'"
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_map
- continuous_linear_map.has_sizeof_inst
- continuous_linear_map.linear_map.has_coe
- continuous_linear_map.continuous_semilinear_map_class
- continuous_linear_map.to_fun
- continuous_linear_map.mul_action
- continuous_linear_map.is_scalar_tower
- continuous_linear_map.smul_comm_class
- continuous_linear_map.has_zero
- continuous_linear_map.inhabited
- continuous_linear_map.unique_of_left
- continuous_linear_map.unique_of_right
- continuous_linear_map.has_one
- continuous_linear_map.has_add
- continuous_linear_map.add_comm_monoid
- continuous_linear_map.has_mul
- continuous_linear_map.monoid_with_zero
- continuous_linear_map.semiring
- continuous_linear_map.apply_module
- continuous_linear_map.apply_has_faithful_smul
- continuous_linear_map.apply_smul_comm_class
- continuous_linear_map.apply_smul_comm_class'
- continuous_linear_map.has_continuous_const_smul
- continuous_linear_map.has_neg
- continuous_linear_map.has_sub
- continuous_linear_map.add_comm_group
- continuous_linear_map.ring
- continuous_linear_map.distrib_mul_action
- continuous_linear_map.module
- continuous_linear_map.is_central_scalar
- continuous_linear_map.algebra
- continuous_linear_equiv.continuous_linear_map.has_coe
- linear_isometry_equiv.continuous_linear_map.has_coe_t
- continuous_linear_map.topological_space
- continuous_linear_map.topological_add_group
- continuous_linear_map.has_continuous_smul
- continuous_linear_map.uniform_space
- continuous_linear_map.uniform_add_group
- continuous_linear_map.t2_space
- continuous_linear_map.has_op_norm
- continuous_linear_map.to_pseudo_metric_space
- continuous_linear_map.to_seminormed_add_comm_group
- continuous_linear_map.to_normed_space
- continuous_linear_map.to_semi_normed_ring
- continuous_linear_map.to_normed_algebra
- continuous_linear_map.norm_one_class
- continuous_linear_map.to_normed_add_comm_group
- continuous_linear_map.to_normed_ring
- continuous_linear_map.complete_space
- continuous_linear_map.finite_dimensional
- linear_map.can_lift_continuous_linear_map
- continuous_linear_map.topological_space.second_countable_topology
- continuous_linear_map.measurable_space
- continuous_linear_map.borel_space
- continuous_linear_map.locally_convex_space
- continuous_linear_map.has_coe_to_cont_mdiff_map
- continuous_linear_map.has_star
- continuous_linear_map.has_involutive_star
- continuous_linear_map.star_semigroup
- continuous_linear_map.star_ring
- continuous_linear_map.star_module
- continuous_linear_map.cstar_ring
- von_neumann_algebra.continuous_linear_map.set_like
- von_neumann_algebra.continuous_linear_map.star_mem_class
- von_neumann_algebra.continuous_linear_map.subring_class
- bundle.continuous_linear_map.module
- bundle.continuous_linear_map.fiber_bundle
- bundle.continuous_linear_map.vector_bundle
- smooth_vector_bundle.continuous_linear_map
- coe : F → Π (a : M), (λ (_x : M), M₂) a
- coe_injective' : function.injective continuous_semilinear_map_class.coe
- map_add : ∀ (f : F) (x y : M), ⇑f (x + y) = ⇑f x + ⇑f y
- map_smulₛₗ : ∀ (f : F) (r : R) (x : M), ⇑f (r • x) = ⇑σ r • ⇑f x
- map_continuous : ∀ (f : F), continuous ⇑f
continuous_semilinear_map_class F σ M M₂
asserts F
is a type of bundled continuous
σ
-semilinear maps M → M₂
. See also continuous_linear_map_class 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 of this typeclass
- continuous_semilinear_equiv_class.continuous_semilinear_map_class
- semilinear_isometry_class.continuous_semilinear_map_class
- alg_hom.continuous_linear_map_class
- star_alg_hom.continuous_linear_map_class
- continuous_linear_map.continuous_semilinear_map_class
- linear_map.continuous_linear_map_class_of_finite_dimensional
- weak_dual.weak_dual.continuous_linear_map_class
- normed_space.continuous_linear_map_class
- weak_dual.character_space.continuous_linear_map_class
Instances of other typeclasses for continuous_semilinear_map_class
- continuous_semilinear_map_class.has_sizeof_inst
continuous_linear_map_class F R M M₂
asserts F
is a type of bundled continuous
R
-linear maps M → M₂
. This is an abbreviation for
continuous_semilinear_map_class F (ring_hom.id R) M M₂
.
- to_linear_equiv : M ≃ₛₗ[σ] M₂
- continuous_to_fun : continuous self.to_linear_equiv.to_fun . "continuity'"
- continuous_inv_fun : continuous self.to_linear_equiv.inv_fun . "continuity'"
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_equiv
- continuous_linear_equiv.has_sizeof_inst
- continuous_linear_equiv.continuous_linear_map.has_coe
- continuous_linear_equiv.continuous_semilinear_equiv_class
- continuous_linear_equiv.has_coe_to_fun
- continuous_linear_equiv.automorphism_group
- linear_isometry_equiv.continuous_linear_equiv.has_coe_t
- linear_equiv.can_lift_continuous_linear_equiv
- coe : F → M → M₂
- inv : F → M₂ → M
- left_inv : ∀ (e : F), function.left_inverse (continuous_semilinear_equiv_class.inv e) (continuous_semilinear_equiv_class.coe e)
- right_inv : ∀ (e : F), function.right_inverse (continuous_semilinear_equiv_class.inv e) (continuous_semilinear_equiv_class.coe e)
- coe_injective' : ∀ (e g : F), continuous_semilinear_equiv_class.coe e = continuous_semilinear_equiv_class.coe g → continuous_semilinear_equiv_class.inv e = continuous_semilinear_equiv_class.inv g → e = g
- map_add : ∀ (f : F) (a b : M), ⇑f (a + b) = ⇑f a + ⇑f b
- map_smulₛₗ : ∀ (f : F) (r : R) (x : M), ⇑f (r • x) = ⇑σ r • ⇑f x
- map_continuous : (∀ (f : F), continuous ⇑f) . "continuity'"
- inv_continuous : (∀ (f : F), continuous (continuous_semilinear_equiv_class.inv f)) . "continuity'"
continuous_semilinear_equiv_class F σ M M₂
asserts F
is a type of bundled continuous
σ
-semilinear equivs M → M₂
. See also continuous_linear_equiv_class 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 of this typeclass
Instances of other typeclasses for continuous_semilinear_equiv_class
- continuous_semilinear_equiv_class.has_sizeof_inst
continuous_linear_equiv_class F σ M M₂
asserts F
is a type of bundled continuous
R
-linear equivs M → M₂
. This is an abbreviation for
continuous_semilinear_equiv_class F (ring_hom.id) M M₂
.
Equations
- continuous_semilinear_equiv_class.continuous_semilinear_map_class F σ M M₂ = {coe := continuous_semilinear_equiv_class.coe s, coe_injective' := _, map_add := _, map_smulₛₗ := _, map_continuous := _}
Constructs a bundled linear map from a function and a proof that this function belongs to the closure of the set of linear maps.
Construct a bundled linear map from a pointwise limit of linear maps
Equations
Properties that hold for non-necessarily commutative semirings. #
Coerce continuous linear maps to linear maps.
Equations
Equations
- continuous_linear_map.continuous_semilinear_map_class = {coe := λ (f : M₁ →SL[σ₁₂] M₂), f.to_linear_map.to_fun, coe_injective' := _, map_add := _, map_smulₛₗ := _, map_continuous := _}
Coerce continuous linear maps to functions.
Equations
- continuous_linear_map.to_fun = {coe := λ (f : M₁ →SL[σ₁₂] M₂), f.to_linear_map.to_fun}
See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.
Equations
See Note [custom simps projection].
Equations
Copy of a continuous_linear_map
with a new to_fun
equal to the old one. Useful to fix
definitional equalities.
Equations
- f.copy f' h = {to_linear_map := f.to_linear_map.copy f' h, cont := _}
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 topological_closure
of a submodule is
contained in the topological_closure
of its image.
Under a dense continuous linear map, a submodule whose topological_closure
is ⊤
is sent to
another such submodule. That is, the image of a dense set under a map with dense range is dense.
Equations
- continuous_linear_map.mul_action = {to_has_smul := {smul := λ (c : S₂) (f : M₁ →SL[σ₁₂] M₂), {to_linear_map := c • ↑f, cont := _}}, one_smul := _, mul_smul := _}
The continuous map that is constantly zero.
Equations
- continuous_linear_map.has_zero = {zero := {to_linear_map := 0, cont := _}}
Equations
the identity map as a continuous linear map.
Equations
- continuous_linear_map.id R₁ M₁ = {to_linear_map := linear_map.id _inst_14, cont := _}
Equations
- continuous_linear_map.has_one = {one := continuous_linear_map.id R₁ M₁ _inst_14}
Equations
- continuous_linear_map.add_comm_monoid = {add := has_add.add continuous_linear_map.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := has_smul.smul mul_action.to_has_smul, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}
Composition of bounded linear maps.
Equations
- continuous_linear_map.has_mul = {mul := continuous_linear_map.comp continuous_linear_map.has_mul._proof_1}
Equations
- continuous_linear_map.monoid_with_zero = {mul := has_mul.mul continuous_linear_map.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := monoid.npow._default 1 has_mul.mul continuous_linear_map.monoid_with_zero._proof_4 continuous_linear_map.monoid_with_zero._proof_5, npow_zero' := _, npow_succ' := _, zero := 0, zero_mul := _, mul_zero := _}
Equations
- continuous_linear_map.semiring = {add := add_comm_monoid.add continuous_linear_map.add_comm_monoid, add_assoc := _, zero := monoid_with_zero.zero continuous_linear_map.monoid_with_zero, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul continuous_linear_map.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := has_mul.mul continuous_linear_map.has_mul, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := 1, one_mul := _, mul_one := _, nat_cast := non_assoc_semiring.nat_cast._default 1 add_comm_monoid.add continuous_linear_map.semiring._proof_14 monoid_with_zero.zero continuous_linear_map.semiring._proof_15 continuous_linear_map.semiring._proof_16 add_comm_monoid.nsmul continuous_linear_map.semiring._proof_17 continuous_linear_map.semiring._proof_18, nat_cast_zero := _, nat_cast_succ := _, npow := monoid_with_zero.npow continuous_linear_map.monoid_with_zero, npow_zero' := _, npow_succ' := _}
continuous_linear_map.to_linear_map
as a ring_hom
.
Equations
- continuous_linear_map.to_linear_map_ring_hom = {to_fun := continuous_linear_map.to_linear_map _inst_14, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
The tautological action by M₁ →L[R₁] M₁
on M
.
This generalizes function.End.apply_mul_action
.
continuous_linear_map.apply_module
is faithful.
The cartesian product of two bounded linear maps, as a bounded linear map.
The left injection into a product is a continuous linear map.
Equations
- continuous_linear_map.inl R₁ M₁ M₂ = (continuous_linear_map.id R₁ M₁).prod 0
The right injection into a product is a continuous linear map.
Equations
- continuous_linear_map.inr R₁ M₁ M₂ = 0.prod (continuous_linear_map.id R₁ M₂)
Restrict codomain of a continuous linear map.
Equations
- f.cod_restrict p h = {to_linear_map := linear_map.cod_restrict p ↑f h, cont := _}
prod.fst
as a continuous_linear_map
.
Equations
- continuous_linear_map.fst R₁ M₁ M₂ = {to_linear_map := linear_map.fst R₁ M₁ M₂ _inst_19, cont := _}
prod.snd
as a continuous_linear_map
.
Equations
- continuous_linear_map.snd R₁ M₁ M₂ = {to_linear_map := linear_map.snd R₁ M₁ M₂ _inst_19, cont := _}
prod.map
of two continuous linear maps.
Equations
- f₁.prod_map f₂ = (f₁.comp (continuous_linear_map.fst R₁ M₁ M₃)).prod (f₂.comp (continuous_linear_map.snd R₁ M₁ M₃))
The continuous linear map given by (x, y) ↦ f₁ x + f₂ y
.
The linear map λ 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 continuous_linear_map.smul_rightₗ
and continuous_linear_map.smul_rightL
.
Equations
- c.smul_right f = {to_linear_map := {to_fun := (c.to_linear_map.smul_right f).to_fun, map_add' := _, map_smul' := _}, cont := _}
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
- continuous_linear_map.to_span_singleton R₁ x = {to_linear_map := linear_map.to_span_singleton R₁ M₁ x, cont := _}
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.
Equations
- continuous_linear_map.pi f = {to_linear_map := linear_map.pi (λ (i : ι), ↑(f i)), cont := _}
The projections from a family of topological modules are continuous linear maps.
Equations
- continuous_linear_map.proj i = {to_linear_map := linear_map.proj i, cont := _}
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
.
Equations
- continuous_linear_map.infi_ker_proj_equiv R φ hd hu = {to_linear_equiv := linear_map.infi_ker_proj_equiv R φ hd hu, continuous_to_fun := _, continuous_inv_fun := _}