mathlib3 documentation

topology.algebra.module.basic

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₂.

theorem has_continuous_smul.of_nhds_zero {R : Type u_1} {M : Type u_2} [ring R] [topological_space R] [topological_space M] [add_comm_group M] [module R M] [topological_ring R] [topological_add_group M] (hmul : filter.tendsto (λ (p : R × M), p.fst p.snd) ((nhds 0).prod (nhds 0)) (nhds 0)) (hmulleft : (m : M), filter.tendsto (λ (a : R), a m) (nhds 0) (nhds 0)) (hmulright : (a : R), filter.tendsto (λ (m : M), a m) (nhds 0) (nhds 0)) :

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.

theorem has_continuous_smul_induced {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [semiring R] [add_comm_monoid M₁] [add_comm_monoid M₂] [module R M₁] [module R M₂] [u : topological_space R] {t : topological_space M₂} [has_continuous_smul R M₂] (f : M₁ →ₗ[R] M₂) :
@[protected, instance]
@[protected, instance]

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.

structure continuous_linear_map {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (σ : R →+* S) (M : Type u_3) [topological_space M] [add_comm_monoid M] (M₂ : Type u_4) [topological_space M₂] [add_comm_monoid M₂] [module R M] [module S M₂] :
Type (max u_3 u_4)

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
@[class]
structure continuous_semilinear_map_class (F : Type u_1) {R : out_param (Type u_2)} {S : out_param (Type u_3)} [semiring R] [semiring S] (σ : out_param (R →+* S)) (M : out_param (Type u_4)) [topological_space M] [add_comm_monoid M] (M₂ : out_param (Type u_5)) [topological_space M₂] [add_comm_monoid M₂] [module R M] [module S M₂] :
Type (max u_1 u_4 u_5)

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
Instances of other typeclasses for continuous_semilinear_map_class
  • continuous_semilinear_map_class.has_sizeof_inst
@[instance]
def continuous_semilinear_map_class.to_semilinear_map_class (F : Type u_1) {R : out_param (Type u_2)} {S : out_param (Type u_3)} [semiring R] [semiring S] (σ : out_param (R →+* S)) (M : out_param (Type u_4)) [topological_space M] [add_comm_monoid M] (M₂ : out_param (Type u_5)) [topological_space M₂] [add_comm_monoid M₂] [module R M] [module S M₂] [self : continuous_semilinear_map_class F σ M M₂] :
@[nolint, instance]
def continuous_semilinear_map_class.to_continuous_map_class (F : Type u_1) {R : out_param (Type u_2)} {S : out_param (Type u_3)} [semiring R] [semiring S] (σ : out_param (R →+* S)) (M : out_param (Type u_4)) [topological_space M] [add_comm_monoid M] (M₂ : out_param (Type u_5)) [topological_space M₂] [add_comm_monoid M₂] [module R M] [module S M₂] [self : continuous_semilinear_map_class F σ M M₂] :
@[reducible]
def continuous_linear_map_class (F : Type u_1) (R : out_param (Type u_2)) [semiring R] (M : out_param (Type u_3)) [topological_space M] [add_comm_monoid M] (M₂ : out_param (Type u_4)) [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] :
Type (max u_1 u_3 u_4)

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₂.

@[nolint]
structure continuous_linear_equiv {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (σ : R →+* S) {σ' : S →+* R} [ring_hom_inv_pair σ σ'] [ring_hom_inv_pair σ' σ] (M : Type u_3) [topological_space M] [add_comm_monoid M] (M₂ : Type u_4) [topological_space M₂] [add_comm_monoid M₂] [module R M] [module S M₂] :
Type (max u_3 u_4)

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
@[class]
structure continuous_semilinear_equiv_class (F : Type u_1) {R : out_param (Type u_2)} {S : out_param (Type u_3)} [semiring R] [semiring S] (σ : out_param (R →+* S)) {σ' : out_param (S →+* R)} [ring_hom_inv_pair σ σ'] [ring_hom_inv_pair σ' σ] (M : out_param (Type u_4)) [topological_space M] [add_comm_monoid M] (M₂ : out_param (Type u_5)) [topological_space M₂] [add_comm_monoid M₂] [module R M] [module S M₂] :
Type (max u_1 u_4 u_5)

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
@[instance]
def continuous_semilinear_equiv_class.to_semilinear_equiv_class (F : Type u_1) {R : out_param (Type u_2)} {S : out_param (Type u_3)} [semiring R] [semiring S] (σ : out_param (R →+* S)) {σ' : out_param (S →+* R)} [ring_hom_inv_pair σ σ'] [ring_hom_inv_pair σ' σ] (M : out_param (Type u_4)) [topological_space M] [add_comm_monoid M] (M₂ : out_param (Type u_5)) [topological_space M₂] [add_comm_monoid M₂] [module R M] [module S M₂] [self : continuous_semilinear_equiv_class F σ M M₂] :
@[reducible]
def continuous_linear_equiv_class (F : Type u_1) (R : out_param (Type u_2)) [semiring R] (M : out_param (Type u_3)) [topological_space M] [add_comm_monoid M] (M₂ : out_param (Type u_4)) [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] :
Type (max u_1 u_3 u_4)

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₂.

theorem is_closed_set_of_map_smul (M₁ : Type u_1) (M₂ : Type u_2) {R : Type u_4} {S : Type u_5} [topological_space M₂] [t2_space M₂] [semiring R] [semiring S] [add_comm_monoid M₁] [add_comm_monoid M₂] [module R M₁] [module S M₂] [has_continuous_const_smul S M₂] (σ : R →+* S) :
is_closed {f : M₁ M₂ | (c : R) (x : M₁), f (c x) = σ c f x}
@[simp]
theorem linear_map_of_mem_closure_range_coe_apply {M₁ : Type u_1} {M₂ : Type u_2} {R : Type u_4} {S : Type u_5} [topological_space M₂] [t2_space M₂] [semiring R] [semiring S] [add_comm_monoid M₁] [add_comm_monoid M₂] [module R M₁] [module S M₂] [has_continuous_const_smul S M₂] [has_continuous_add M₂] {σ : R →+* S} (f : M₁ M₂) (hf : f closure (set.range coe_fn)) :
def linear_map_of_mem_closure_range_coe {M₁ : Type u_1} {M₂ : Type u_2} {R : Type u_4} {S : Type u_5} [topological_space M₂] [t2_space M₂] [semiring R] [semiring S] [add_comm_monoid M₁] [add_comm_monoid M₂] [module R M₁] [module S M₂] [has_continuous_const_smul S M₂] [has_continuous_add M₂] {σ : R →+* S} (f : M₁ M₂) (hf : f closure (set.range coe_fn)) :
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
def linear_map_of_tendsto {M₁ : Type u_1} {M₂ : Type u_2} {α : Type u_3} {R : Type u_4} {S : Type u_5} [topological_space M₂] [t2_space M₂] [semiring R] [semiring S] [add_comm_monoid M₁] [add_comm_monoid M₂] [module R M₁] [module S M₂] [has_continuous_const_smul S M₂] [has_continuous_add M₂] {σ : R →+* S} {l : filter α} (f : M₁ M₂) (g : α (M₁ →ₛₗ[σ] M₂)) [l.ne_bot] (h : filter.tendsto (λ (a : α) (x : M₁), (g a) x) l (nhds f)) :
M₁ →ₛₗ[σ] M₂

Construct a bundled linear map from a pointwise limit of linear maps

Equations
@[simp]
theorem linear_map_of_tendsto_apply {M₁ : Type u_1} {M₂ : Type u_2} {α : Type u_3} {R : Type u_4} {S : Type u_5} [topological_space M₂] [t2_space M₂] [semiring R] [semiring S] [add_comm_monoid M₁] [add_comm_monoid M₂] [module R M₁] [module S M₂] [has_continuous_const_smul S M₂] [has_continuous_add M₂] {σ : R →+* S} {l : filter α} (f : M₁ M₂) (g : α (M₁ →ₛₗ[σ] M₂)) [l.ne_bot] (h : filter.tendsto (λ (a : α) (x : M₁), (g a) x) l (nhds f)) :
theorem linear_map.is_closed_range_coe (M₁ : Type u_1) (M₂ : Type u_2) {R : Type u_4} {S : Type u_5} [topological_space M₂] [t2_space M₂] [semiring R] [semiring S] [add_comm_monoid M₁] [add_comm_monoid M₂] [module R M₁] [module S M₂] [has_continuous_const_smul S M₂] [has_continuous_add M₂] (σ : R →+* S) :

Properties that hold for non-necessarily commutative semirings. #

@[protected, instance]
def continuous_linear_map.linear_map.has_coe {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] :
has_coe (M₁ →SL[σ₁₂] M₂) (M₁ →ₛₗ[σ₁₂] M₂)

Coerce continuous linear maps to linear maps.

Equations
@[simp]
theorem continuous_linear_map.to_linear_map_eq_coe {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) :
theorem continuous_linear_map.coe_injective {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] :
@[protected, instance]
def continuous_linear_map.continuous_semilinear_map_class {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] :
continuous_semilinear_map_class (M₁ →SL[σ₁₂] M₂) σ₁₂ M₁ M₂
Equations
@[protected, instance]
def continuous_linear_map.to_fun {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] :
has_coe_to_fun (M₁ →SL[σ₁₂] M₂) (λ (_x : M₁ →SL[σ₁₂] M₂), M₁ M₂)

Coerce continuous linear maps to functions.

Equations
@[simp]
theorem continuous_linear_map.coe_mk {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] (f : M₁ →ₛₗ[σ₁₂] M₂) (h : continuous f.to_fun . "continuity'") :
{to_linear_map := f, cont := h} = f
@[simp]
theorem continuous_linear_map.coe_mk' {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] (f : M₁ →ₛₗ[σ₁₂] M₂) (h : continuous f.to_fun . "continuity'") :
@[protected, continuity]
theorem continuous_linear_map.continuous {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) :
@[protected]
theorem continuous_linear_map.uniform_continuous {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {E₁ : Type u_3} {E₂ : Type u_4} [uniform_space E₁] [uniform_space E₂] [add_comm_group E₁] [add_comm_group E₂] [module R₁ E₁] [module R₂ E₂] [uniform_add_group E₁] [uniform_add_group E₂] (f : E₁ →SL[σ₁₂] E₂) :
@[simp, norm_cast]
theorem continuous_linear_map.coe_inj {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] {f g : M₁ →SL[σ₁₂] M₂} :
f = g f = g
theorem continuous_linear_map.coe_fn_injective {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] :
def continuous_linear_map.simps.apply {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] (h : M₁ →SL[σ₁₂] M₂) :
M₁ M₂

See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.

Equations
def continuous_linear_map.simps.coe {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] (h : M₁ →SL[σ₁₂] M₂) :
M₁ →ₛₗ[σ₁₂] M₂

See Note [custom simps projection].

Equations
@[ext]
theorem continuous_linear_map.ext {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] {f g : M₁ →SL[σ₁₂] M₂} (h : (x : M₁), f x = g x) :
f = g
theorem continuous_linear_map.ext_iff {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] {f g : M₁ →SL[σ₁₂] M₂} :
f = g (x : M₁), f x = g x
@[protected]
def continuous_linear_map.copy {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) (f' : M₁ M₂) (h : f' = f) :
M₁ →SL[σ₁₂] M₂

Copy of a continuous_linear_map with a new to_fun equal to the old one. Useful to fix definitional equalities.

Equations
@[simp]
theorem continuous_linear_map.coe_copy {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) (f' : M₁ M₂) (h : f' = f) :
(f.copy f' h) = f'
theorem continuous_linear_map.copy_eq {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) (f' : M₁ M₂) (h : f' = f) :
f.copy f' h = f
@[protected]
theorem continuous_linear_map.map_zero {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) :
f 0 = 0
@[protected]
theorem continuous_linear_map.map_add {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) (x y : M₁) :
f (x + y) = f x + f y
@[protected, simp]
theorem continuous_linear_map.map_smulₛₗ {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) (c : R₁) (x : M₁) :
f (c x) = σ₁₂ c f x
@[protected, simp]
theorem continuous_linear_map.map_smul {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₁ M₂] (f : M₁ →L[R₁] M₂) (c : R₁) (x : M₁) :
f (c x) = c f x
@[simp]
theorem continuous_linear_map.map_smul_of_tower {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] {R : Type u_1} {S : Type u_2} [semiring S] [has_smul R M₁] [module S M₁] [has_smul R M₂] [module S M₂] [linear_map.compatible_smul M₁ M₂ R S] (f : M₁ →L[S] M₂) (c : R) (x : M₁) :
f (c x) = c f x
@[protected]
theorem continuous_linear_map.map_sum {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] {ι : Type u_3} (f : M₁ →SL[σ₁₂] M₂) (s : finset ι) (g : ι M₁) :
f (s.sum (λ (i : ι), g i)) = s.sum (λ (i : ι), f (g i))
@[simp, norm_cast]
theorem continuous_linear_map.coe_coe {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) :
@[ext]
theorem continuous_linear_map.ext_ring {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] [module R₁ M₁] [topological_space R₁] {f g : R₁ →L[R₁] M₁} (h : f 1 = g 1) :
f = g
theorem continuous_linear_map.ext_ring_iff {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] [module R₁ M₁] [topological_space R₁] {f g : R₁ →L[R₁] M₁} :
f = g f 1 = g 1
theorem continuous_linear_map.eq_on_closure_span {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] [t2_space M₂] {s : set M₁} {f g : M₁ →SL[σ₁₂] M₂} (h : set.eq_on f g s) :

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.

theorem continuous_linear_map.ext_on {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] [t2_space M₂] {s : set M₁} (hs : dense (submodule.span R₁ s)) {f g : M₁ →SL[σ₁₂] M₂} (h : set.eq_on f g s) :
f = g

If the submodule generated by a set s is dense in the ambient module, then two continuous linear maps equal on s are equal.

theorem submodule.topological_closure_map {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] [ring_hom_surjective σ₁₂] [topological_space R₁] [topological_space R₂] [has_continuous_smul R₁ M₁] [has_continuous_add M₁] [has_continuous_smul R₂ M₂] [has_continuous_add M₂] (f : M₁ →SL[σ₁₂] M₂) (s : submodule R₁ M₁) :

Under a continuous linear map, the image of the topological_closure of a submodule is contained in the topological_closure of its image.

theorem dense_range.topological_closure_map_submodule {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] [ring_hom_surjective σ₁₂] [topological_space R₁] [topological_space R₂] [has_continuous_smul R₁ M₁] [has_continuous_add M₁] [has_continuous_smul R₂ M₂] [has_continuous_add M₂] {f : M₁ →SL[σ₁₂] M₂} (hf' : dense_range f) {s : submodule R₁ M₁} (hs : s.topological_closure = ) :

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.

@[protected, instance]
def continuous_linear_map.mul_action {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] {S₂ : Type u_9} [monoid S₂] [distrib_mul_action S₂ M₂] [smul_comm_class R₂ S₂ M₂] [has_continuous_const_smul S₂ M₂] :
mul_action S₂ (M₁ →SL[σ₁₂] M₂)
Equations
theorem continuous_linear_map.smul_apply {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] {S₂ : Type u_9} [monoid S₂] [distrib_mul_action S₂ M₂] [smul_comm_class R₂ S₂ M₂] [has_continuous_const_smul S₂ M₂] (c : S₂) (f : M₁ →SL[σ₁₂] M₂) (x : M₁) :
(c f) x = c f x
@[simp, norm_cast]
theorem continuous_linear_map.coe_smul {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] {S₂ : Type u_9} [monoid S₂] [distrib_mul_action S₂ M₂] [smul_comm_class R₂ S₂ M₂] [has_continuous_const_smul S₂ M₂] (c : S₂) (f : M₁ →SL[σ₁₂] M₂) :
(c f) = c f
@[simp, norm_cast]
theorem continuous_linear_map.coe_smul' {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] {S₂ : Type u_9} [monoid S₂] [distrib_mul_action S₂ M₂] [smul_comm_class R₂ S₂ M₂] [has_continuous_const_smul S₂ M₂] (c : S₂) (f : M₁ →SL[σ₁₂] M₂) :
(c f) = c f
@[protected, instance]
def continuous_linear_map.is_scalar_tower {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] {S₂ : Type u_9} {T₂ : Type u_10} [monoid S₂] [monoid T₂] [distrib_mul_action S₂ M₂] [smul_comm_class R₂ S₂ M₂] [has_continuous_const_smul S₂ M₂] [distrib_mul_action T₂ M₂] [smul_comm_class R₂ T₂ M₂] [has_continuous_const_smul T₂ M₂] [has_smul S₂ T₂] [is_scalar_tower S₂ T₂ M₂] :
is_scalar_tower S₂ T₂ (M₁ →SL[σ₁₂] M₂)
@[protected, instance]
def continuous_linear_map.smul_comm_class {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] {S₂ : Type u_9} {T₂ : Type u_10} [monoid S₂] [monoid T₂] [distrib_mul_action S₂ M₂] [smul_comm_class R₂ S₂ M₂] [has_continuous_const_smul S₂ M₂] [distrib_mul_action T₂ M₂] [smul_comm_class R₂ T₂ M₂] [has_continuous_const_smul T₂ M₂] [smul_comm_class S₂ T₂ M₂] :
smul_comm_class S₂ T₂ (M₁ →SL[σ₁₂] M₂)
@[protected, instance]
def continuous_linear_map.has_zero {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] :
has_zero (M₁ →SL[σ₁₂] M₂)

The continuous map that is constantly zero.

Equations
@[protected, instance]
def continuous_linear_map.inhabited {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] :
inhabited (M₁ →SL[σ₁₂] M₂)
Equations
@[simp]
theorem continuous_linear_map.default_def {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] :
@[simp]
theorem continuous_linear_map.zero_apply {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] (x : M₁) :
0 x = 0
@[simp, norm_cast]
theorem continuous_linear_map.coe_zero {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] :
0 = 0
@[norm_cast]
theorem continuous_linear_map.coe_zero' {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] :
0 = 0
@[protected, instance]
def continuous_linear_map.unique_of_left {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] [subsingleton M₁] :
unique (M₁ →SL[σ₁₂] M₂)
Equations
@[protected, instance]
def continuous_linear_map.unique_of_right {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] [subsingleton M₂] :
unique (M₁ →SL[σ₁₂] M₂)
Equations
theorem continuous_linear_map.exists_ne_zero {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] {f : M₁ →SL[σ₁₂] M₂} (hf : f 0) :
(x : M₁), f x 0
def continuous_linear_map.id (R₁ : Type u_1) [semiring R₁] (M₁ : Type u_4) [topological_space M₁] [add_comm_monoid M₁] [module R₁ M₁] :
M₁ →L[R₁] M₁

the identity map as a continuous linear map.

Equations
@[protected, instance]
def continuous_linear_map.has_one {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] [module R₁ M₁] :
has_one (M₁ →L[R₁] M₁)
Equations
theorem continuous_linear_map.one_def {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] [module R₁ M₁] :
theorem continuous_linear_map.id_apply {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] [module R₁ M₁] (x : M₁) :
@[simp, norm_cast]
theorem continuous_linear_map.coe_id {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] [module R₁ M₁] :
@[simp, norm_cast]
theorem continuous_linear_map.coe_id' {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] [module R₁ M₁] :
@[simp, norm_cast]
theorem continuous_linear_map.coe_eq_id {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] [module R₁ M₁] {f : M₁ →L[R₁] M₁} :
@[simp]
theorem continuous_linear_map.one_apply {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] [module R₁ M₁] (x : M₁) :
1 x = x
@[protected, instance]
def continuous_linear_map.has_add {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] [has_continuous_add M₂] :
has_add (M₁ →SL[σ₁₂] M₂)
Equations
@[simp]
theorem continuous_linear_map.add_apply {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] [has_continuous_add M₂] (f g : M₁ →SL[σ₁₂] M₂) (x : M₁) :
(f + g) x = f x + g x
@[simp, norm_cast]
theorem continuous_linear_map.coe_add {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] [has_continuous_add M₂] (f g : M₁ →SL[σ₁₂] M₂) :
(f + g) = f + g
@[norm_cast]
theorem continuous_linear_map.coe_add' {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] [has_continuous_add M₂] (f g : M₁ →SL[σ₁₂] M₂) :
(f + g) = f + g
@[protected, instance]
def continuous_linear_map.add_comm_monoid {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] [has_continuous_add M₂] :
add_comm_monoid (M₁ →SL[σ₁₂] M₂)
Equations
@[simp, norm_cast]
theorem continuous_linear_map.coe_sum {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] [has_continuous_add M₂] {ι : Type u_3} (t : finset ι) (f : ι (M₁ →SL[σ₁₂] M₂)) :
(t.sum (λ (d : ι), f d)) = t.sum (λ (d : ι), (f d))
@[simp, norm_cast]
theorem continuous_linear_map.coe_sum' {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] [has_continuous_add M₂] {ι : Type u_3} (t : finset ι) (f : ι (M₁ →SL[σ₁₂] M₂)) :
(t.sum (λ (d : ι), f d)) = t.sum (λ (d : ι), (f d))
theorem continuous_linear_map.sum_apply {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] [has_continuous_add M₂] {ι : Type u_3} (t : finset ι) (f : ι (M₁ →SL[σ₁₂] M₂)) (b : M₁) :
(t.sum (λ (d : ι), f d)) b = t.sum (λ (d : ι), (f d) b)
def continuous_linear_map.comp {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [semiring R₁] [semiring R₂] [semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_7} [topological_space M₃] [add_comm_monoid M₃] [module R₁ M₁] [module R₂ M₂] [module R₃ M₃] [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] (g : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) :
M₁ →SL[σ₁₃] M₃

Composition of bounded linear maps.

Equations
@[simp, norm_cast]
theorem continuous_linear_map.coe_comp {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [semiring R₁] [semiring R₂] [semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_7} [topological_space M₃] [add_comm_monoid M₃] [module R₁ M₁] [module R₂ M₂] [module R₃ M₃] [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] (h : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) :
(h.comp f) = h.comp f
@[simp, norm_cast]
theorem continuous_linear_map.coe_comp' {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [semiring R₁] [semiring R₂] [semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_7} [topological_space M₃] [add_comm_monoid M₃] [module R₁ M₁] [module R₂ M₂] [module R₃ M₃] [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] (h : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) :
(h.comp f) = h f
theorem continuous_linear_map.comp_apply {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [semiring R₁] [semiring R₂] [semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_7} [topological_space M₃] [add_comm_monoid M₃] [module R₁ M₁] [module R₂ M₂] [module R₃ M₃] [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] (g : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) (x : M₁) :
(g.comp f) x = g (f x)
@[simp]
theorem continuous_linear_map.comp_id {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) :
@[simp]
theorem continuous_linear_map.id_comp {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) :
@[simp]
theorem continuous_linear_map.comp_zero {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [semiring R₁] [semiring R₂] [semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_7} [topological_space M₃] [add_comm_monoid M₃] [module R₁ M₁] [module R₂ M₂] [module R₃ M₃] [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] (g : M₂ →SL[σ₂₃] M₃) :
g.comp 0 = 0
@[simp]
theorem continuous_linear_map.zero_comp {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [semiring R₁] [semiring R₂] [semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_7} [topological_space M₃] [add_comm_monoid M₃] [module R₁ M₁] [module R₂ M₂] [module R₃ M₃] [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] (f : M₁ →SL[σ₁₂] M₂) :
0.comp f = 0
@[simp]
theorem continuous_linear_map.comp_add {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [semiring R₁] [semiring R₂] [semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_7} [topological_space M₃] [add_comm_monoid M₃] [module R₁ M₁] [module R₂ M₂] [module R₃ M₃] [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] [has_continuous_add M₂] [has_continuous_add M₃] (g : M₂ →SL[σ₂₃] M₃) (f₁ f₂ : M₁ →SL[σ₁₂] M₂) :
g.comp (f₁ + f₂) = g.comp f₁ + g.comp f₂
@[simp]
theorem continuous_linear_map.add_comp {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [semiring R₁] [semiring R₂] [semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_7} [topological_space M₃] [add_comm_monoid M₃] [module R₁ M₁] [module R₂ M₂] [module R₃ M₃] [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] [has_continuous_add M₃] (g₁ g₂ : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) :
(g₁ + g₂).comp f = g₁.comp f + g₂.comp f
theorem continuous_linear_map.comp_assoc {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [semiring R₁] [semiring R₂] [semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_7} [topological_space M₃] [add_comm_monoid M₃] {M₄ : Type u_8} [topological_space M₄] [add_comm_monoid M₄] [module R₁ M₁] [module R₂ M₂] [module R₃ M₃] [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] {R₄ : Type u_5} [semiring R₄] [module R₄ M₄] {σ₁₄ : R₁ →+* R₄} {σ₂₄ : R₂ →+* R₄} {σ₃₄ : R₃ →+* R₄} [ring_hom_comp_triple σ₁₃ σ₃₄ σ₁₄] [ring_hom_comp_triple σ₂₃ σ₃₄ σ₂₄] [ring_hom_comp_triple σ₁₂ σ₂₄ σ₁₄] (h : M₃ →SL[σ₃₄] M₄) (g : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) :
(h.comp g).comp f = h.comp (g.comp f)
@[protected, instance]
def continuous_linear_map.has_mul {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] [module R₁ M₁] :
has_mul (M₁ →L[R₁] M₁)
Equations
theorem continuous_linear_map.mul_def {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] [module R₁ M₁] (f g : M₁ →L[R₁] M₁) :
f * g = f.comp g
@[simp]
theorem continuous_linear_map.coe_mul {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] [module R₁ M₁] (f g : M₁ →L[R₁] M₁) :
(f * g) = f g
theorem continuous_linear_map.mul_apply {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] [module R₁ M₁] (f g : M₁ →L[R₁] M₁) (x : M₁) :
(f * g) x = f (g x)
@[protected, instance]
def continuous_linear_map.monoid_with_zero {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] [module R₁ M₁] :
monoid_with_zero (M₁ →L[R₁] M₁)
Equations
@[protected, instance]
def continuous_linear_map.semiring {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] [module R₁ M₁] [has_continuous_add M₁] :
semiring (M₁ →L[R₁] M₁)
Equations
@[simp]
@[protected, instance]
def continuous_linear_map.apply_module {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] [module R₁ M₁] [has_continuous_add M₁] :
module (M₁ →L[R₁] M₁) M₁

The tautological action by M₁ →L[R₁] M₁ on M.

This generalizes function.End.apply_mul_action.

Equations
@[protected, simp]
theorem continuous_linear_map.smul_def {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] [module R₁ M₁] [has_continuous_add M₁] (f : M₁ →L[R₁] M₁) (a : M₁) :
f a = f a
@[protected, instance]
def continuous_linear_map.apply_has_faithful_smul {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] [module R₁ M₁] [has_continuous_add M₁] :
has_faithful_smul (M₁ →L[R₁] M₁) M₁

continuous_linear_map.apply_module is faithful.

@[protected, instance]
def continuous_linear_map.apply_smul_comm_class {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] [module R₁ M₁] [has_continuous_add M₁] :
smul_comm_class R₁ (M₁ →L[R₁] M₁) M₁
@[protected, instance]
def continuous_linear_map.apply_smul_comm_class' {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] [module R₁ M₁] [has_continuous_add M₁] :
smul_comm_class (M₁ →L[R₁] M₁) R₁ M₁
@[protected, instance]
def continuous_linear_map.has_continuous_const_smul {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] [module R₁ M₁] [has_continuous_add M₁] :
has_continuous_const_smul (M₁ →L[R₁] M₁) M₁
@[protected]
def continuous_linear_map.prod {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_7} [topological_space M₃] [add_comm_monoid M₃] [module R₁ M₁] [module R₁ M₂] [module R₁ M₃] (f₁ : M₁ →L[R₁] M₂) (f₂ : M₁ →L[R₁] M₃) :
M₁ →L[R₁] M₂ × M₃

The cartesian product of two bounded linear maps, as a bounded linear map.

Equations
@[simp, norm_cast]
theorem continuous_linear_map.coe_prod {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_7} [topological_space M₃] [add_comm_monoid M₃] [module R₁ M₁] [module R₁ M₂] [module R₁ M₃] (f₁ : M₁ →L[R₁] M₂) (f₂ : M₁ →L[R₁] M₃) :
(f₁.prod f₂) = f₁.prod f₂
@[simp, norm_cast]
theorem continuous_linear_map.prod_apply {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_7} [topological_space M₃] [add_comm_monoid M₃] [module R₁ M₁] [module R₁ M₂] [module R₁ M₃] (f₁ : M₁ →L[R₁] M₂) (f₂ : M₁ →L[R₁] M₃) (x : M₁) :
(f₁.prod f₂) x = (f₁ x, f₂ x)
def continuous_linear_map.inl (R₁ : Type u_1) [semiring R₁] (M₁ : Type u_4) [topological_space M₁] [add_comm_monoid M₁] (M₂ : Type u_6) [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₁ M₂] :
M₁ →L[R₁] M₁ × M₂

The left injection into a product is a continuous linear map.

Equations
def continuous_linear_map.inr (R₁ : Type u_1) [semiring R₁] (M₁ : Type u_4) [topological_space M₁] [add_comm_monoid M₁] (M₂ : Type u_6) [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₁ M₂] :
M₂ →L[R₁] M₁ × M₂

The right injection into a product is a continuous linear map.

Equations
@[simp]
theorem continuous_linear_map.inl_apply {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₁ M₂] (x : M₁) :
(continuous_linear_map.inl R₁ M₁ M₂) x = (x, 0)
@[simp]
theorem continuous_linear_map.inr_apply {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₁ M₂] (x : M₂) :
(continuous_linear_map.inr R₁ M₁ M₂) x = (0, x)
@[simp, norm_cast]
theorem continuous_linear_map.coe_inl {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₁ M₂] :
(continuous_linear_map.inl R₁ M₁ M₂) = linear_map.inl R₁ M₁ M₂
@[simp, norm_cast]
theorem continuous_linear_map.coe_inr {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₁ M₂] :
(continuous_linear_map.inr R₁ M₁ M₂) = linear_map.inr R₁ M₁ M₂
theorem continuous_linear_map.is_closed_ker {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] {F : Type u_9} [t1_space M₂] [continuous_semilinear_map_class F σ₁₂ M₁ M₂] (f : F) :
theorem continuous_linear_map.is_complete_ker {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₂ M₂] {F : Type u_9} {M' : Type u_3} [uniform_space M'] [complete_space M'] [add_comm_monoid M'] [module R₁ M'] [t1_space M₂] [continuous_semilinear_map_class F σ₁₂ M' M₂] (f : F) :
@[protected, instance]
def continuous_linear_map.complete_space_ker {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₂ M₂] {F : Type u_9} {M' : Type u_3} [uniform_space M'] [complete_space M'] [add_comm_monoid M'] [module R₁ M'] [t1_space M₂] [continuous_semilinear_map_class F σ₁₂ M' M₂] (f : F) :
@[simp]
theorem continuous_linear_map.ker_prod {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_7} [topological_space M₃] [add_comm_monoid M₃] [module R₁ M₁] [module R₁ M₂] [module R₁ M₃] (f : M₁ →L[R₁] M₂) (g : M₁ →L[R₁] M₃) :
def continuous_linear_map.cod_restrict {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) (p : submodule R₂ M₂) (h : (x : M₁), f x p) :
M₁ →SL[σ₁₂] p

Restrict codomain of a continuous linear map.

Equations
@[norm_cast]
theorem continuous_linear_map.coe_cod_restrict {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) (p : submodule R₂ M₂) (h : (x : M₁), f x p) :
@[simp]
theorem continuous_linear_map.coe_cod_restrict_apply {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) (p : submodule R₂ M₂) (h : (x : M₁), f x p) (x : M₁) :
((f.cod_restrict p h) x) = f x
@[simp]
theorem continuous_linear_map.ker_cod_restrict {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) (p : submodule R₂ M₂) (h : (x : M₁), f x p) :
def submodule.subtypeL {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] [module R₁ M₁] (p : submodule R₁ M₁) :
p →L[R₁] M₁

submodule.subtype as a continuous_linear_map.

Equations
@[simp, norm_cast]
theorem submodule.coe_subtypeL {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] [module R₁ M₁] (p : submodule R₁ M₁) :
@[simp]
theorem submodule.coe_subtypeL' {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] [module R₁ M₁] (p : submodule R₁ M₁) :
@[simp, norm_cast]
theorem submodule.subtypeL_apply {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] [module R₁ M₁] (p : submodule R₁ M₁) (x : p) :
@[simp]
theorem submodule.range_subtypeL {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] [module R₁ M₁] (p : submodule R₁ M₁) :
@[simp]
theorem submodule.ker_subtypeL {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] [module R₁ M₁] (p : submodule R₁ M₁) :
def continuous_linear_map.fst (R₁ : Type u_1) [semiring R₁] (M₁ : Type u_4) [topological_space M₁] [add_comm_monoid M₁] (M₂ : Type u_6) [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₁ M₂] :
M₁ × M₂ →L[R₁] M₁

prod.fst as a continuous_linear_map.

Equations
def continuous_linear_map.snd (R₁ : Type u_1) [semiring R₁] (M₁ : Type u_4) [topological_space M₁] [add_comm_monoid M₁] (M₂ : Type u_6) [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₁ M₂] :
M₁ × M₂ →L[R₁] M₂

prod.snd as a continuous_linear_map.

Equations
@[simp, norm_cast]
theorem continuous_linear_map.coe_fst {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₁ M₂] :
(continuous_linear_map.fst R₁ M₁ M₂) = linear_map.fst R₁ M₁ M₂
@[simp, norm_cast]
theorem continuous_linear_map.coe_fst' {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₁ M₂] :
@[simp, norm_cast]
theorem continuous_linear_map.coe_snd {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₁ M₂] :
(continuous_linear_map.snd R₁ M₁ M₂) = linear_map.snd R₁ M₁ M₂
@[simp, norm_cast]
theorem continuous_linear_map.coe_snd' {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₁ M₂] :
@[simp]
theorem continuous_linear_map.fst_prod_snd {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₁] [module R₁ M₂] :
(continuous_linear_map.fst R₁ M₁ M₂).prod (continuous_linear_map.snd R₁ M₁ M₂) = continuous_linear_map.id R₁ (M₁ × M₂)
@[simp]
theorem continuous_linear_map.fst_comp_prod {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_7} [topological_space M₃] [add_comm_monoid M₃] [module R₁ M₁] [module R₁ M₂] [module R₁ M₃] (f : M₁ →L[R₁] M₂) (g : M₁ →L[R₁] M₃) :
(continuous_linear_map.fst R₁ M₂ M₃).comp (f.prod g) = f
@[simp]
theorem continuous_linear_map.snd_comp_prod {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_7} [topological_space M₃] [add_comm_monoid M₃] [module R₁ M₁] [module R₁ M₂] [module R₁ M₃] (f : M₁ →L[R₁] M₂) (g : M₁ →L[R₁] M₃) :
(continuous_linear_map.snd R₁ M₂ M₃).comp (f.prod g) = g
def continuous_linear_map.prod_map {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_7} [topological_space M₃] [add_comm_monoid M₃] {M₄ : Type u_8} [topological_space M₄] [add_comm_monoid M₄] [module R₁ M₁] [module R₁ M₂] [module R₁ M₃] [module R₁ M₄] (f₁ : M₁ →L[R₁] M₂) (f₂ : M₃ →L[R₁] M₄) :
M₁ × M₃ →L[R₁] M₂ × M₄

prod.map of two continuous linear maps.

Equations
@[simp, norm_cast]
theorem continuous_linear_map.coe_prod_map {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_7} [topological_space M₃] [add_comm_monoid M₃] {M₄ : Type u_8} [topological_space M₄] [add_comm_monoid M₄] [module R₁ M₁] [module R₁ M₂] [module R₁ M₃] [module R₁ M₄] (f₁ : M₁ →L[R₁] M₂) (f₂ : M₃ →L[R₁] M₄) :
(f₁.prod_map f₂) = f₁.prod_map f₂
@[simp, norm_cast]
theorem continuous_linear_map.coe_prod_map' {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_7} [topological_space M₃] [add_comm_monoid M₃] {M₄ : Type u_8} [topological_space M₄] [add_comm_monoid M₄] [module R₁ M₁] [module R₁ M₂] [module R₁ M₃] [module R₁ M₄] (f₁ : M₁ →L[R₁] M₂) (f₂ : M₃ →L[R₁] M₄) :
(f₁.prod_map f₂) = prod.map f₁ f₂
def continuous_linear_map.coprod {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_7} [topological_space M₃] [add_comm_monoid M₃] [module R₁ M₁] [module R₁ M₂] [module R₁ M₃] [has_continuous_add M₃] (f₁ : M₁ →L[R₁] M₃) (f₂ : M₂ →L[R₁] M₃) :
M₁ × M₂ →L[R₁] M₃

The continuous linear map given by (x, y) ↦ f₁ x + f₂ y.

Equations
@[simp, norm_cast]
theorem continuous_linear_map.coe_coprod {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_7} [topological_space M₃] [add_comm_monoid M₃] [module R₁ M₁] [module R₁ M₂] [module R₁ M₃] [has_continuous_add M₃] (f₁ : M₁ →L[R₁] M₃) (f₂ : M₂ →L[R₁] M₃) :
(f₁.coprod f₂) = f₁.coprod f₂
@[simp]
theorem continuous_linear_map.coprod_apply {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_7} [topological_space M₃] [add_comm_monoid M₃] [module R₁ M₁] [module R₁ M₂] [module R₁ M₃] [has_continuous_add M₃] (f₁ : M₁ →L[R₁] M₃) (f₂ : M₂ →L[R₁] M₃) (x : M₁ × M₂) :
(f₁.coprod f₂) x = f₁ x.fst + f₂ x.snd
theorem continuous_linear_map.range_coprod {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_7} [topological_space M₃] [add_comm_monoid M₃] [module R₁ M₁] [module R₁ M₂] [module R₁ M₃] [has_continuous_add M₃] (f₁ : M₁ →L[R₁] M₃) (f₂ : M₂ →L[R₁] M₃) :
theorem continuous_linear_map.comp_fst_add_comp_snd {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_7} [topological_space M₃] [add_comm_monoid M₃] [module R₁ M₁] [module R₁ M₂] [module R₁ M₃] [has_continuous_add M₃] (f : M₁ →L[R₁] M₃) (g : M₂ →L[R₁] M₃) :
f.comp (continuous_linear_map.fst R₁ M₁ M₂) + g.comp (continuous_linear_map.snd R₁ M₁ M₂) = f.coprod g
theorem continuous_linear_map.coprod_inl_inr {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M'₁ : Type u_5} [topological_space M'₁] [add_comm_monoid M'₁] [module R₁ M₁] [module R₁ M'₁] [has_continuous_add M₁] [has_continuous_add M'₁] :
(continuous_linear_map.inl R₁ M₁ M'₁).coprod (continuous_linear_map.inr R₁ M₁ M'₁) = continuous_linear_map.id R₁ (M₁ × M'₁)
def continuous_linear_map.smul_right {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] {R : Type u_10} {S : Type u_11} [semiring R] [semiring S] [module R M₁] [module R M₂] [module R S] [module S M₂] [is_scalar_tower R S M₂] [topological_space S] [has_continuous_smul S M₂] (c : M₁ →L[R] S) (f : M₂) :
M₁ →L[R] M₂

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
@[simp]
theorem continuous_linear_map.smul_right_apply {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] {R : Type u_10} {S : Type u_11} [semiring R] [semiring S] [module R M₁] [module R M₂] [module R S] [module S M₂] [is_scalar_tower R S M₂] [topological_space S] [has_continuous_smul S M₂] {c : M₁ →L[R] S} {f : M₂} {x : M₁} :
(c.smul_right f) x = c x f
@[simp]
theorem continuous_linear_map.smul_right_one_one {R₁ : Type u_1} [semiring R₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₂] [topological_space R₁] [has_continuous_smul R₁ M₂] (c : R₁ →L[R₁] M₂) :
1.smul_right (c 1) = c
@[simp]
theorem continuous_linear_map.smul_right_one_eq_iff {R₁ : Type u_1} [semiring R₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₂] [topological_space R₁] [has_continuous_smul R₁ M₂] {f f' : M₂} :
1.smul_right f = 1.smul_right f' f = f'
theorem continuous_linear_map.smul_right_comp {R₁ : Type u_1} [semiring R₁] {M₂ : Type u_6} [topological_space M₂] [add_comm_monoid M₂] [module R₁ M₂] [topological_space R₁] [has_continuous_smul R₁ M₂] [has_continuous_mul R₁] {x : M₂} {c : R₁} :
def continuous_linear_map.to_span_singleton (R₁ : Type u_1) [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] [module R₁ M₁] [topological_space R₁] [has_continuous_smul R₁ M₁] (x : M₁) :
R₁ →L[R₁] M₁

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
theorem continuous_linear_map.to_span_singleton_apply (R₁ : Type u_1) [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] [module R₁ M₁] [topological_space R₁] [has_continuous_smul R₁ M₁] (x : M₁) (r : R₁) :
theorem continuous_linear_map.to_span_singleton_smul' (R₁ : Type u_1) [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] [module R₁ M₁] [topological_space R₁] [has_continuous_smul R₁ M₁] {α : Type u_2} [monoid α] [distrib_mul_action α M₁] [has_continuous_const_smul α M₁] [smul_comm_class R₁ α M₁] (c : α) (x : M₁) :

A special case of to_span_singleton_smul' for when R is commutative.

def continuous_linear_map.pi {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] [module R M] {ι : Type u_4} {φ : ι Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), module R (φ i)] (f : Π (i : ι), M →L[R] φ i) :
M →L[R] Π (i : ι), φ i

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
@[simp]
theorem continuous_linear_map.coe_pi' {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] [module R M] {ι : Type u_4} {φ : ι Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), module R (φ i)] (f : Π (i : ι), M →L[R] φ i) :
(continuous_linear_map.pi f) = λ (c : M) (i : ι), (f i) c
@[simp]
theorem continuous_linear_map.coe_pi {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] [module R M] {ι : Type u_4} {φ : ι Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), module R (φ i)] (f : Π (i : ι), M →L[R] φ i) :
theorem continuous_linear_map.pi_apply {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] [module R M] {ι : Type u_4} {φ : ι Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), module R (φ i)] (f : Π (i : ι), M →L[R] φ i) (c : M) (i : ι) :
theorem continuous_linear_map.pi_eq_zero {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] [module R M] {ι : Type u_4} {φ : ι Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), module R (φ i)] (f : Π (i : ι), M →L[R] φ i) :
continuous_linear_map.pi f = 0 (i : ι), f i = 0
theorem continuous_linear_map.pi_zero {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] [module R M] {ι : Type u_4} {φ : ι Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), module R (φ i)] :
continuous_linear_map.pi (λ (i : ι), 0) = 0
theorem continuous_linear_map.pi_comp {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] [module R M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M₂] {ι : Type u_4} {φ : ι Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), module R (φ i)] (f : Π (i : ι), M →L[R] φ i) (g : M₂ →L[R] M) :
def continuous_linear_map.proj {R : Type u_1} [semiring R] {ι : Type u_4} {φ : ι Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), module R (φ i)] (i : ι) :
(Π (i : ι), φ i) →L[R] φ i

The projections from a family of topological modules are continuous linear maps.

Equations
@[simp]
theorem continuous_linear_map.proj_apply {R : Type u_1} [semiring R] {ι : Type u_4} {φ : ι Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), module R (φ i)] (i : ι) (b : Π (i : ι), φ i) :
theorem continuous_linear_map.proj_pi {R : Type u_1} [semiring R] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [module R M₂] {ι : Type u_4} {φ : ι Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), module R (φ i)] (f : Π (i : ι), M₂ →L[R] φ i) (i : ι) :
theorem continuous_linear_map.infi_ker_proj {R : Type u_1} [semiring R] {ι : Type u_4} {φ : ι Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), module R (φ i)] :
def continuous_linear_map.infi_ker_proj_equiv (R : Type u_1) [semiring R] {ι : Type u_4} (φ : ι Type u_5) [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), module R (φ i)] {I J : set ι} [decidable_pred (λ (i : ι), i I)] (hd : disjoint I J) (hu : set.univ I J) :
( (i : ι) (H : i J), linear_map.ker (continuous_linear_map.proj i)) ≃L[R] Π (i : I), φ i

If I and J are complementary index sets, the product of the kernels of the Jth projections of φ is linearly equivalent to the product over I.

Equations
@[protected]
theorem continuous_linear_map.map_neg {R : Type u_1} [ring R] {R₂ : Type u_2} [ring R₂] {M : Type u_4} [topological_space M] [add_comm_group M] {M₂ : Type u_5} [topological_space M₂] [add_comm_group M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} (f : M →SL[σ₁₂] M₂) (x : M) :
f (-x) = -f x
@[protected]
theorem continuous_linear_map.map_sub {R : Type u_1} [ring R] {R₂ : Type u_2} [ring R₂] {M : Type u_4} [topological_space M] [add_comm_group M] {M₂ : Type u_5} [topological_space M₂] [add_comm_group M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} (f : M →SL[σ₁₂] M₂) (x y : M) :
f (x - y) = f x - f y
@[simp]
theorem continuous_linear_map.sub_apply' {R : Type u_1} [ring R] {R₂ : Type u_2} [ring R₂] {M : Type u_4} [topological_space M] [add_comm_group M] {M₂ : Type u_5} [topological_space M₂] [add_comm_group M₂] [module R M] [module R₂ M₂] {σ₁₂ : R →+* R₂} (f g : M →SL[σ₁₂] M₂) (x : M) :
(f - g) x = f x - g x
theorem continuous_linear_map.range_prod_eq {R : Type u_1} [ring R] {M : Type u_4} [topological_space M] [add_comm_group M] {M₂ : Type u_5} [topological_space M₂] [add_comm_group M₂] {M₃ : Type u_6} [topological_space M₃] [add_comm_group M₃] [module R M] [module R M₂] [module R M₃] {f : M →L[R] M₂} {g : M →L[R] M₃} (h : linear_map.ker f linear_map.ker g = ) :
theorem continuous_linear_map.ker_prod_ker_le_ker_coprod {R : Type u_1} [ring R] {M : Type u_4} [topological_space M] [add_comm_group M] {M₂ : Type u_5} [topological_space M₂] [add_comm_group M₂] {M₃ : Type u_6} [topological_space M₃] [add_comm_group M₃] [module R M] [module R M₂] [module R M₃] [has_continuous_add M₃] (f : M →L[R] M₃) (g : M₂ →L[R] M₃) :
theorem continuous_linear_map.ker_coprod_of_disjoint_range {R : Type u_1} [ring R] {M : Type u_4} [topological_space M] [add_comm_group M] {M₂ : Type u_5} [topological_space M₂] [add_comm_group M₂] {M₃ : Type u_6} [topological_space M₃] [add_comm_group M₃] [module R M] [module R M₂] [module R M₃] [has_continuous_add M₃] (f : M →L[R