# mathlib3documentation

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] [ 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)) :
theorem submodule.eq_top_of_nonempty_interior' {R : Type u_1} {M : Type u_2} [ring R] [ M] [ M] [ {x : R | is_unit x}).ne_bot] (s : M) (hs : (interior s).nonempty) :
s =

If `M` is a topological module over `R` and `0` is a limit of invertible elements of `R`, then `⊤` is the only submodule of `M` with a nonempty interior. This is the case, e.g., if `R` is a nontrivially normed field.

theorem module.punctured_nhds_ne_bot (R : Type u_1) (M : Type u_2) [ring R] [ M] [ M] [nontrivial M] [ {0}).ne_bot] (x : M) :
{x}).ne_bot

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₂] [ M₁] [ M₂] [u : topological_space R] {t : topological_space M₂} [ M₂] (f : M₁ →ₗ[R] M₂) :
@[protected, instance]
def submodule.has_continuous_smul {α : Type u_1} {β : Type u_2} [semiring α] [ β] [ β] (S : β) :
@[protected, instance]
def submodule.topological_add_group {α : Type u_1} {β : Type u_2} [ring α] [ β] (S : β) :
theorem submodule.closure_smul_self_subset {R : Type u} {M : Type v} [semiring R] [ M] [ M] (s : M) :
(λ (p : R × M), p.fst p.snd) ''
theorem submodule.closure_smul_self_eq {R : Type u} {M : Type v} [semiring R] [ M] [ M] (s : M) :
(λ (p : R × M), p.fst p.snd) '' =
def submodule.topological_closure {R : Type u} {M : Type v} [semiring R] [ M] [ M] (s : M) :
M

The (topological-space) closure of a submodule of a topological `R`-module `M` is itself a submodule.

Equations
Instances for `↥submodule.topological_closure`
@[simp]
theorem submodule.topological_closure_coe {R : Type u} {M : Type v} [semiring R] [ M] [ M] (s : M) :
theorem submodule.le_topological_closure {R : Type u} {M : Type v} [semiring R] [ M] [ M] (s : M) :
theorem submodule.is_closed_topological_closure {R : Type u} {M : Type v} [semiring R] [ M] [ M] (s : M) :
theorem submodule.topological_closure_minimal {R : Type u} {M : Type v} [semiring R] [ M] [ M] (s : M) {t : M} (h : s t) (ht : is_closed t) :
theorem submodule.topological_closure_mono {R : Type u} {M : Type v} [semiring R] [ M] [ M] {s t : M} (h : s t) :
theorem is_closed.submodule_topological_closure_eq {R : Type u} {M : Type v} [semiring R] [ M] [ M] {s : M} (hs : is_closed s) :

The topological closure of a closed submodule `s` is equal to `s`.

theorem submodule.dense_iff_topological_closure_eq_top {R : Type u} {M : Type v} [semiring R] [ M] [ M] {s : M} :

A subspace is dense iff its topological closure is the entire space.

@[protected, instance]
def submodule.topological_closure.complete_space {R : Type u} [semiring R] {M' : Type u_1} [add_comm_monoid M'] [ M'] [uniform_space M'] [ M'] [complete_space M'] (U : M') :
theorem submodule.is_closed_or_dense_of_is_coatom {R : Type u} {M : Type v} [semiring R] [ M] [ M] (s : M) (hs : is_coatom s) :

A maximal proper subspace of a topological module (i.e a `submodule` satisfying `is_coatom`) is either closed or dense.

theorem linear_map.continuous_on_pi {ι : Type u_1} {R : Type u_2} {M : Type u_3} [finite ι] [semiring R] [ M] [ M] (f : R) →ₗ[R] M) :
structure continuous_linear_map {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (σ : R →+* S) (M : Type u_3) (M₂ : Type u_4) [add_comm_monoid M₂] [ M] [ M₂] :
Type (max u_3 u_4)
• to_linear_map : M →ₛₗ[σ] M₂
• cont : . "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`
@[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)) (M₂ : out_param (Type u_5)) [add_comm_monoid M₂] [ M] [ M₂] :
Type (max u_1 u_4 u_5)
• coe : F Π (a : M), (λ (_x : M), M₂) a
• coe_injective' :
• 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_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)) (M₂ : out_param (Type u_5)) [add_comm_monoid M₂] [ M] [ M₂] [self : M₂] :
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)) (M₂ : out_param (Type u_5)) [add_comm_monoid M₂] [ M] [ M₂] [self : 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)) (M₂ : out_param (Type u_4)) [add_comm_monoid M₂] [ M] [ 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} [ σ'] [ σ] (M : Type u_3) (M₂ : Type u_4) [add_comm_monoid M₂] [ M] [ M₂] :
Type (max u_3 u_4)
• to_linear_equiv : M ≃ₛₗ[σ] M₂
• continuous_to_fun : . "continuity'"
• continuous_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`
@[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)} [ σ'] [ σ] (M : out_param (Type u_4)) (M₂ : out_param (Type u_5)) [add_comm_monoid M₂] [ M] [ M₂] :
Type (max u_1 u_4 u_5)
• coe : F M M₂
• inv : F M₂ M
• left_inv :
• right_inv :
• coe_injective' :
• 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), . "continuity'"
• inv_continuous : ( (f : 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
@[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)} [ σ'] [ σ] (M : out_param (Type u_4)) (M₂ : out_param (Type u_5)) [add_comm_monoid M₂] [ M] [ M₂] [self : 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)) (M₂ : out_param (Type u_4)) [add_comm_monoid M₂] [ M] [ 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₂`.

@[protected, nolint, instance]
def continuous_semilinear_equiv_class.continuous_semilinear_map_class (F : Type u_1) {R : Type u_2} {S : Type u_3} [semiring R] [semiring S] (σ : R →+* S) {σ' : S →+* R} [ σ'] [ σ] (M : Type u_4) (M₂ : Type u_5) [add_comm_monoid M₂] [ M] [ M₂] [s : M₂] :
M₂
Equations
theorem is_closed_set_of_map_smul (M₁ : Type u_1) (M₂ : Type u_2) {R : Type u_4} {S : Type u_5} [t2_space M₂] [semiring R] [semiring S] [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ 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} [t2_space M₂] [semiring R] [semiring S] [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] {σ : R →+* S} (f : M₁ M₂) (hf : f ) :
def linear_map_of_mem_closure_range_coe {M₁ : Type u_1} {M₂ : Type u_2} {R : Type u_4} {S : Type u_5} [t2_space M₂] [semiring R] [semiring S] [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] {σ : R →+* S} (f : M₁ M₂) (hf : f ) :
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} [t2_space M₂] [semiring R] [semiring S] [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ 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} [t2_space M₂] [semiring R] [semiring S] [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ 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)) :
h) = f
theorem linear_map.is_closed_range_coe (M₁ : Type u_1) (M₂ : Type u_2) {R : Type u_4} {S : Type u_5} [t2_space M₂] [semiring R] [semiring S] [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ 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} [add_comm_monoid M₁] {M₂ : Type u_6} [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} [add_comm_monoid M₁] {M₂ : Type u_6} [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} [add_comm_monoid M₁] {M₂ : Type u_6} [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} [add_comm_monoid M₁] {M₂ : Type u_6} [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} [add_comm_monoid M₁] {M₂ : Type u_6} [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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] (f : M₁ →ₛₗ[σ₁₂] M₂) (h : . "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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] (f : M₁ →ₛₗ[σ₁₂] M₂) (h : . "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} [add_comm_monoid M₁] {M₂ : Type u_6} [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₂] (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} [add_comm_monoid M₁] {M₂ : Type u_6} [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} [add_comm_monoid M₁] {M₂ : Type u_6} [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} [add_comm_monoid M₁] {M₂ : Type u_6} [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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] (h : M₁ →SL[σ₁₂] M₂) :
M₁ →ₛₗ[σ₁₂] M₂
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} [add_comm_monoid M₁] {M₂ : Type u_6} [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} [add_comm_monoid M₁] {M₂ : Type u_6} [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} [add_comm_monoid M₁] {M₂ : Type u_6} [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} [add_comm_monoid M₁] {M₂ : Type u_6} [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} [add_comm_monoid M₁] {M₂ : Type u_6} [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} [add_comm_monoid M₁] {M₂ : Type u_6} [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} [add_comm_monoid M₁] {M₂ : Type u_6} [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} [add_comm_monoid M₁] {M₂ : Type u_6} [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} [add_comm_monoid M₁] {M₂ : Type u_6} [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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] {R : Type u_1} {S : Type u_2} [semiring S] [ M₁] [ M₁] [ 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} [add_comm_monoid M₁] {M₂ : Type u_6} [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} [add_comm_monoid M₁] {M₂ : Type u_6} [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} [add_comm_monoid M₁] [module R₁ M₁] {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} [add_comm_monoid M₁] [module R₁ M₁] {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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] [t2_space M₂] {s : set M₁} {f g : M₁ →SL[σ₁₂] M₂} (h : g s) :
g (closure 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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] [t2_space M₂] {s : set M₁} (hs : dense s)) {f g : M₁ →SL[σ₁₂] M₂} (h : 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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] [ring_hom_surjective σ₁₂] [ M₁] [ M₂] (f : M₁ →SL[σ₁₂] M₂) (s : 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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] [ring_hom_surjective σ₁₂] [ M₁] [ M₂] {f : M₁ →SL[σ₁₂] M₂} (hf' : dense_range f) {s : 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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] {S₂ : Type u_9} [monoid S₂] [ M₂] [ S₂ M₂] [ M₂] :
(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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] {S₂ : Type u_9} [monoid S₂] [ M₂] [ S₂ M₂] [ 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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] {S₂ : Type u_9} [monoid S₂] [ M₂] [ S₂ M₂] [ 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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] {S₂ : Type u_9} [monoid S₂] [ M₂] [ S₂ M₂] [ 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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] {S₂ : Type u_9} {T₂ : Type u_10} [monoid S₂] [monoid T₂] [ M₂] [ S₂ M₂] [ M₂] [ M₂] [ T₂ M₂] [ M₂] [has_smul S₂ T₂] [ T₂ M₂] :
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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] {S₂ : Type u_9} {T₂ : Type u_10} [monoid S₂] [monoid T₂] [ M₂] [ S₂ M₂] [ M₂] [ M₂] [ T₂ M₂] [ M₂] [ T₂ M₂] :
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} [add_comm_monoid M₁] {M₂ : Type u_6} [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} [add_comm_monoid M₁] {M₂ : Type u_6} [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} [add_comm_monoid M₁] {M₂ : Type u_6} [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} [add_comm_monoid M₁] {M₂ : Type u_6} [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} [add_comm_monoid M₁] {M₂ : Type u_6} [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} [add_comm_monoid M₁] {M₂ : Type u_6} [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} [add_comm_monoid M₁] {M₂ : Type u_6} [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} [add_comm_monoid M₁] {M₂ : Type u_6} [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} [add_comm_monoid M₁] {M₂ : Type u_6} [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) [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} [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} [add_comm_monoid M₁] [module R₁ M₁] :
1 =
theorem continuous_linear_map.id_apply {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [add_comm_monoid M₁] [module R₁ M₁] (x : M₁) :
M₁) x = x
@[simp, norm_cast]
theorem continuous_linear_map.coe_id {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [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} [add_comm_monoid M₁] [module R₁ M₁] :
M₁) = id
@[simp, norm_cast]
theorem continuous_linear_map.coe_eq_id {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [add_comm_monoid M₁] [module R₁ M₁] {f : M₁ →L[R₁] M₁} :
f =
@[simp]
theorem continuous_linear_map.one_apply {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] [module R₁ M₁] [module R₂ 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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] [module R₁ M₁] [module R₂ 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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] [module R₁ M₁] [module R₂ 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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] [module R₁ M₁] [module R₂ 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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] [module R₁ M₁] [module R₂ 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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] [module R₁ M₁] [module R₂ 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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] [module R₁ M₁] [module R₂ 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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] [module R₁ M₁] [module R₂ 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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] {M₃ : Type u_7} [add_comm_monoid M₃] [module R₁ M₁] [module R₂ M₂] [module R₃ M₃] [ σ₂₃ σ₁₃] (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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] {M₃ : Type u_7} [add_comm_monoid M₃] [module R₁ M₁] [module R₂ M₂] [module R₃ M₃] [ σ₂₃ σ₁₃] (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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] {M₃ : Type u_7} [add_comm_monoid M₃] [module R₁ M₁] [module R₂ M₂] [module R₃ M₃] [ σ₂₃ σ₁₃] (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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] {M₃ : Type u_7} [add_comm_monoid M₃] [module R₁ M₁] [module R₂ M₂] [module R₃ M₃] [ σ₂₃ σ₁₃] (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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) :
f.comp M₁) = f
@[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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) :
M₂).comp f = f
@[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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] {M₃ : Type u_7} [add_comm_monoid M₃] [module R₁ M₁] [module R₂ M₂] [module R₃ M₃] [ σ₂₃ σ₁₃] (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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] {M₃ : Type u_7} [add_comm_monoid M₃] [module R₁ M₁] [module R₂ M₂] [module R₃ M₃] [ σ₂₃ σ₁₃] (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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] {M₃ : Type u_7} [add_comm_monoid M₃] [module R₁ M₁] [module R₂ M₂] [module R₃ 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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] {M₃ : Type u_7} [add_comm_monoid M₃] [module R₁ M₁] [module R₂ M₂] [module R₃ 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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] {M₃ : Type u_7} [add_comm_monoid M₃] {M₄ : Type u_8} [add_comm_monoid M₄] [module R₁ M₁] [module R₂ M₂] [module R₃ M₃] [ σ₂₃ σ₁₃] {R₄ : Type u_5} [semiring R₄] [module R₄ M₄] {σ₁₄ : R₁ →+* R₄} {σ₂₄ : R₂ →+* R₄} {σ₃₄ : R₃ →+* R₄} [ σ₃₄ σ₁₄] [ σ₃₄ σ₂₄] [ σ₂₄ σ₁₄] (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} [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} [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} [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} [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} [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} [add_comm_monoid M₁] [module R₁ M₁]  :
semiring (M₁ →L[R₁] M₁)
Equations
def continuous_linear_map.to_linear_map_ring_hom {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [add_comm_monoid M₁] [module R₁ M₁]  :
(M₁ →L[R₁] M₁) →+* M₁ →ₗ[R₁] M₁

`continuous_linear_map.to_linear_map` as a `ring_hom`.

Equations
@[simp]
theorem continuous_linear_map.to_linear_map_ring_hom_apply {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [add_comm_monoid M₁] [module R₁ M₁] (self : M₁ →L[R₁] M₁) :
@[protected, instance]
def continuous_linear_map.apply_module {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [add_comm_monoid M₁] [module R₁ 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} [add_comm_monoid M₁] [module R₁ 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} [add_comm_monoid M₁] [module R₁ 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} [add_comm_monoid M₁] [module R₁ M₁]  :
(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} [add_comm_monoid M₁] [module R₁ 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} [add_comm_monoid M₁] [module R₁ 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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] {M₃ : Type u_7} [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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] {M₃ : Type u_7} [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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] {M₃ : Type u_7} [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) [add_comm_monoid M₁] (M₂ : Type u_6) [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) [add_comm_monoid M₁] (M₂ : Type u_6) [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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] [module R₁ M₁] [module R₁ M₂] (x : M₁) :
M₂) x = (x, 0)
@[simp]
theorem continuous_linear_map.inr_apply {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] [module R₁ M₁] [module R₁ M₂] (x : M₂) :
M₂) x = (0, x)
@[simp, norm_cast]
theorem continuous_linear_map.coe_inl {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] [module R₁ M₁] [module R₁ M₂] :
M₂) = M₁ M₂
@[simp, norm_cast]
theorem continuous_linear_map.coe_inr {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] [module R₁ M₁] [module R₁ M₂] :
M₂) = 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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] {F : Type u_9} [t1_space M₂] [ 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} [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₂] [ 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} [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₂] [ M' M₂] (f : F) :
@[simp]
theorem continuous_linear_map.ker_prod {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] {M₃ : Type u_7} [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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) (p : 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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) (p : 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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) (p : 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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] [module R₁ M₁] [module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) (p : M₂) (h : (x : M₁), f x p) :
def submodule.subtypeL {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [add_comm_monoid M₁] [module R₁ M₁] (p : 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} [add_comm_monoid M₁] [module R₁ M₁] (p : M₁) :
@[simp]
theorem submodule.coe_subtypeL' {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [add_comm_monoid M₁] [module R₁ M₁] (p : M₁) :
@[simp, norm_cast]
theorem submodule.subtypeL_apply {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [add_comm_monoid M₁] [module R₁ M₁] (p : M₁) (x : p) :
@[simp]
theorem submodule.range_subtypeL {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [add_comm_monoid M₁] [module R₁ M₁] (p : M₁) :
@[simp]
theorem submodule.ker_subtypeL {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [add_comm_monoid M₁] [module R₁ M₁] (p : M₁) :
def continuous_linear_map.fst (R₁ : Type u_1) [semiring R₁] (M₁ : Type u_4) [add_comm_monoid M₁] (M₂ : Type u_6) [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) [add_comm_monoid M₁] (M₂ : Type u_6) [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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] [module R₁ M₁] [module R₁ M₂] :
M₂) = M₁ M₂
@[simp, norm_cast]
theorem continuous_linear_map.coe_fst' {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] [module R₁ M₁] [module R₁ M₂] :
M₂) = prod.fst
@[simp, norm_cast]
theorem continuous_linear_map.coe_snd {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] [module R₁ M₁] [module R₁ M₂] :
M₂) = M₁ M₂
@[simp, norm_cast]
theorem continuous_linear_map.coe_snd' {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] [module R₁ M₁] [module R₁ M₂] :
M₂) = prod.snd
@[simp]
theorem continuous_linear_map.fst_prod_snd {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] [module R₁ M₁] [module R₁ M₂] :
M₂).prod M₂) = (M₁ × M₂)
@[simp]
theorem continuous_linear_map.fst_comp_prod {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] {M₃ : Type u_7} [add_comm_monoid M₃] [module R₁ M₁] [module R₁ M₂] [module R₁ M₃] (f : M₁ →L[R₁] M₂) (g : M₁ →L[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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] {M₃ : Type u_7} [add_comm_monoid M₃] [module R₁ M₁] [module R₁ M₂] [module R₁ M₃] (f : M₁ →L[R₁] M₂) (g : M₁ →L[R₁] M₃) :
M₃).comp (f.prod g) = g
def continuous_linear_map.prod_map {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] {M₃ : Type u_7} [add_comm_monoid M₃] {M₄ : Type u_8} [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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] {M₃ : Type u_7} [add_comm_monoid M₃] {M₄ : Type u_8} [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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] {M₃ : Type u_7} [add_comm_monoid M₃] {M₄ : Type u_8} [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₂
def continuous_linear_map.coprod {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] {M₃ : Type u_7} [add_comm_monoid 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₃

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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] {M₃ : Type u_7} [add_comm_monoid M₃] [module R₁ M₁] [module R₁ M₂] [module R₁ 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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] {M₃ : Type u_7} [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₁ × 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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] {M₃ : Type u_7} [add_comm_monoid M₃] [module R₁ M₁] [module R₁ M₂] [module R₁ 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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] {M₃ : Type u_7} [add_comm_monoid M₃] [module R₁ M₁] [module R₁ M₂] [module R₁ M₃] (f : M₁ →L[R₁] M₃) (g : M₂ →L[R₁] M₃) :
f.comp M₂) + g.comp M₂) = f.coprod g
theorem continuous_linear_map.coprod_inl_inr {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [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'₁] :
M'₁).coprod M'₁) = (M₁ × M'₁)
def continuous_linear_map.smul_right {M₁ : Type u_4} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] {R : Type u_10} {S : Type u_11} [semiring R] [semiring S] [ M₁] [ M₂] [ S] [ M₂] [ M₂] [ 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} [add_comm_monoid M₁] {M₂ : Type u_6} [add_comm_monoid M₂] {R : Type u_10} {S : Type u_11} [semiring R] [semiring S] [ M₁] [ M₂] [ S] [ M₂] [ M₂] [ 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} [add_comm_monoid M₂] [module R₁ M₂] [ 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} [add_comm_monoid M₂] [module R₁ M₂] [ 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} [add_comm_monoid M₂] [module R₁ M₂] [ M₂] {x : M₂} {c : R₁} :
def continuous_linear_map.to_span_singleton (R₁ : Type u_1) [semiring R₁] {M₁ : Type u_4} [add_comm_monoid M₁] [module R₁ M₁] [ 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} [add_comm_monoid M₁] [module R₁ M₁] [ M₁] (x : M₁) (r : R₁) :
= r x
theorem continuous_linear_map.to_span_singleton_add (R₁ : Type u_1) [semiring R₁] {M₁ : Type u_4} [add_comm_monoid M₁] [module R₁ M₁] [ M₁] (x y : M₁) :
theorem continuous_linear_map.to_span_singleton_smul' (R₁ : Type u_1) [semiring R₁] {M₁ : Type u_4} [add_comm_monoid M₁] [module R₁ M₁] [ M₁] {α : Type u_2} [monoid α] [ M₁] [ α M₁] (c : α) (x : M₁) :
theorem continuous_linear_map.to_span_singleton_smul (R : Type u_1) {M₁ : Type u_2} [add_comm_monoid M₁] [ M₁] [ M₁] (c : R) (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} [ M] {ι : Type u_4} {φ : ι Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), (φ 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} [ M] {ι : Type u_4} {φ : ι Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), (φ i)] (f : Π (i : ι), M →L[R] φ i) :
= λ (c : M) (i : ι), (f i) c
@[simp]
theorem continuous_linear_map.coe_pi {R : Type u_1} [semiring R] {M : Type u_2} [ M] {ι : Type u_4} {φ : ι Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), (φ i)] (f : Π (i : ι), M →L[R] φ i) :
= linear_map.pi (λ (i : ι), (f i))
theorem continuous_linear_map.pi_apply {R : Type u_1} [semiring R] {M : Type u_2} [ M] {ι : Type u_4} {φ : ι Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), (φ i)] (f : Π (i : ι), M →L[R] φ i) (c : M) (i : ι) :
i = (f i) c
theorem continuous_linear_map.pi_eq_zero {R : Type u_1} [semiring R] {M : Type u_2} [ M] {ι : Type u_4} {φ : ι Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), (φ i)] (f : Π (i : ι), M →L[R] φ i) :
(i : ι), f i = 0
theorem continuous_linear_map.pi_zero {R : Type u_1} [semiring R] {M : Type u_2} [ M] {ι : Type u_4} {φ : ι Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), (φ i)] :
continuous_linear_map.pi (λ (i : ι), 0) = 0
theorem continuous_linear_map.pi_comp {R : Type u_1} [semiring R] {M : Type u_2} [ M] {M₂ : Type u_3} [add_comm_monoid M₂] [ M₂] {ι : Type u_4} {φ : ι Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), (φ i)] (f : Π (i : ι), M →L[R] φ i) (g : M₂ →L[R] M) :
= continuous_linear_map.pi (λ (i : ι), (f i).comp g)
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 : ι), (φ 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 : ι), (φ i)] (i : ι) (b : Π (i : ι), φ i) :
= b i
theorem continuous_linear_map.proj_pi {R : Type u_1} [semiring R] {M₂ : Type u_3} [add_comm_monoid M₂] [ M₂] {ι : Type u_4} {φ : ι Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), (φ 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 : ι), (φ i)] :
( (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 : ι), (φ i)] {I J : set ι} [decidable_pred (λ (i : ι), i I)] (hd : J) (hu : set.univ I J) :
( (i : ι) (H : i J), ≃L[R] Π (i : I), φ i

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
@[protected]
theorem continuous_linear_map.map_neg {R : Type u_1} [ring R] {R₂ : Type u_2} [ring R₂] {M : Type u_4} {M₂ : Type u_5} [add_comm_group M₂] [ 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} {M₂ : Type u_5} [add_comm_group M₂] [ 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} {M₂ : Type u_5} [add_comm_group M₂] [ 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} {M₂ : Type u_5} [add_comm_group M₂] {M₃ : Type u_6} [add_comm_group M₃] [ M] [ M₂] [ M₃] {f : M →L[R] M₂} {g : M →L[R] M₃} (h : = ) :
theorem continuous_linear_map.ker_prod_ker_le_ker_coprod {R : Type u_1} [ring R] {M : Type u_4} {M₂ : Type u_5} [add_comm_group M₂] {M₃ : Type u_6} [add_comm_group M₃] [ M] [ M₂] [ 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} {M₂ : Type u_5} [add_comm_group M₂] {M₃ : Type u_6} [add_comm_group M₃] [ M] [ M₂] [ M₃] (f : M →L[R