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

source
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)) :
has_continuous_smul R M
source
theorem submodule.eq_top_of_nonempty_interior' {R : Type u_1} {M : Type u_2} [ring R] [topological_space R] [topological_space M] [add_comm_group M] [has_continuous_add M] [module R M] [has_continuous_smul R M] [(nhds_within 0 {x : R | is_unit x}).ne_bot] (s : submodule R 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.

source
theorem module.punctured_nhds_ne_bot (R : Type u_1) (M : Type u_2) [ring R] [topological_space R] [topological_space M] [add_comm_group M] [has_continuous_add M] [module R M] [has_continuous_smul R M] [nontrivial M] [(nhds_within 0 {0}ᶜ).ne_bot] [no_zero_smul_divisors R M] (x : M) :
(nhds_within x {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.

source
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₂) :
has_continuous_smul R M₁
source
@[protected, instance]
def submodule.has_continuous_smul {α : Type u_1} {β : Type u_2} [topological_space β] [topological_space α] [semiring α] [add_comm_monoid β] [module α β] [has_continuous_smul α β] (S : submodule α β) :
has_continuous_smul α ↥S
source
@[protected, instance]
def submodule.topological_add_group {α : Type u_1} {β : Type u_2} [topological_space β] [ring α] [add_comm_group β] [module α β] [topological_add_group β] (S : submodule α β) :
topological_add_group ↥S
source
theorem submodule.closure_smul_self_subset {R : Type u} {M : Type v} [semiring R] [topological_space R] [topological_space M] [add_comm_monoid M] [module R M] [has_continuous_smul R M] (s : submodule R M) :
(λ (p : R × M), p.fst • p.snd) '' set.univ ×ˢ closure ↑s ⊆ closure ↑s
source
theorem submodule.closure_smul_self_eq {R : Type u} {M : Type v} [semiring R] [topological_space R] [topological_space M] [add_comm_monoid M] [module R M] [has_continuous_smul R M] (s : submodule R M) :
(λ (p : R × M), p.fst • p.snd) '' set.univ ×ˢ closure ↑s = closure ↑s
source
def submodule.topological_closure {R : Type u} {M : Type v} [semiring R] [topological_space R] [topological_space M] [add_comm_monoid M] [module R M] [has_continuous_smul R M] [has_continuous_add M] (s : submodule R M) :
submodule R M

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

Equations
Instances for ↥submodule.topological_closure
source
@[simp]
theorem submodule.topological_closure_coe {R : Type u} {M : Type v} [semiring R] [topological_space R] [topological_space M] [add_comm_monoid M] [module R M] [has_continuous_smul R M] [has_continuous_add M] (s : submodule R M) :
↑(s.topological_closure) = closure ↑s
source
theorem submodule.le_topological_closure {R : Type u} {M : Type v} [semiring R] [topological_space R] [topological_space M] [add_comm_monoid M] [module R M] [has_continuous_smul R M] [has_continuous_add M] (s : submodule R M) :
s ≤ s.topological_closure
source
theorem submodule.is_closed_topological_closure {R : Type u} {M : Type v} [semiring R] [topological_space R] [topological_space M] [add_comm_monoid M] [module R M] [has_continuous_smul R M] [has_continuous_add M] (s : submodule R M) :
is_closed ↑(s.topological_closure)
source
theorem submodule.topological_closure_minimal {R : Type u} {M : Type v} [semiring R] [topological_space R] [topological_space M] [add_comm_monoid M] [module R M] [has_continuous_smul R M] [has_continuous_add M] (s : submodule R M) {t : submodule R M} (h : s ≤ t) (ht : is_closed ↑t) :
s.topological_closure ≤ t
source
theorem submodule.topological_closure_mono {R : Type u} {M : Type v} [semiring R] [topological_space R] [topological_space M] [add_comm_monoid M] [module R M] [has_continuous_smul R M] [has_continuous_add M] {s t : submodule R M} (h : s ≤ t) :
s.topological_closure ≤ t.topological_closure
source
theorem is_closed.submodule_topological_closure_eq {R : Type u} {M : Type v} [semiring R] [topological_space R] [topological_space M] [add_comm_monoid M] [module R M] [has_continuous_smul R M] [has_continuous_add M] {s : submodule R M} (hs : is_closed ↑s) :
s.topological_closure = s

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

source
theorem submodule.dense_iff_topological_closure_eq_top {R : Type u} {M : Type v} [semiring R] [topological_space R] [topological_space M] [add_comm_monoid M] [module R M] [has_continuous_smul R M] [has_continuous_add M] {s : submodule R M} :
dense ↑s ↔ s.topological_closure = ⊤

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

source
@[protected, instance]
def submodule.topological_closure.complete_space {R : Type u} [semiring R] [topological_space R] {M' : Type u_1} [add_comm_monoid M'] [module R M'] [uniform_space M'] [has_continuous_add M'] [has_continuous_smul R M'] [complete_space M'] (U : submodule R M') :
complete_space ↥(U.topological_closure)
source
theorem submodule.is_closed_or_dense_of_is_coatom {R : Type u} {M : Type v} [semiring R] [topological_space R] [topological_space M] [add_comm_monoid M] [module R M] [has_continuous_smul R M] [has_continuous_add M] (s : submodule R M) (hs : is_coatom s) :
is_closed ↑s ∨ dense ↑s

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

source
theorem linear_map.continuous_on_pi {ι : Type u_1} {R : Type u_2} {M : Type u_3} [finite ι] [semiring R] [topological_space R] [add_comm_monoid M] [module R M] [topological_space M] [has_continuous_add M] [has_continuous_smul R M] (f : (ι → R) →ₗ[R] M) :
continuous ⇑f
source
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
source
@[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
source
@[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₂] :
semilinear_map_class F σ M M₂
source
@[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₂] :
continuous_map_class F M M₂
source
@[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₂.

source
@[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
source
@[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
source
@[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₂] :
semilinear_equiv_class F σ M M₂
source
@[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₂.

source
@[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} [ring_hom_inv_pair σ σ'] [ring_hom_inv_pair σ' σ] (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 S M₂] [s : continuous_semilinear_equiv_class F σ M M₂] :
continuous_semilinear_map_class F σ M M₂
Equations
source
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}
source
@[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)) :
⇑(linear_map_of_mem_closure_range_coe f hf) = f
source
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
source
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
source
@[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)) :
⇑(linear_map_of_tendsto f g h) = f
source
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) :
is_closed (set.range coe_fn)

Properties that hold for non-necessarily commutative semirings. #

source
@[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
source
@[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₂) :
f.to_linear_map = ↑f
source
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₂] :
function.injective coe
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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₂) :
continuous ⇑f
source
@[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₂) :
uniform_continuous ⇑f
source
@[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
source
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₂] :
function.injective coe_fn
source
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
source
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
source
@[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
source
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
source
@[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
source
@[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'
source
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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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))
source
@[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₂) :
⇑↑f = ⇑f
source
@[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
source
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
source
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) :
set.eq_on ⇑f ⇑g (closure ↑(submodule.span R₁ 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.

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

source
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₁) :
submodule.map ↑f s.topological_closure ≤ (submodule.map ↑f s).topological_closure

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

source
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 = ⊤) :
(submodule.map ↑f 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.

source
@[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
source
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
source
@[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
source
@[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
source
@[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₂)
source
@[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₂)
source
@[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
source
@[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
source
@[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₂] :
inhabited.default = 0
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
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
source
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
source
@[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
source
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₁] :
1 = continuous_linear_map.id R₁ M₁
source
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₁) :
⇑(continuous_linear_map.id R₁ M₁) x = x
source
@[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₁] :
↑(continuous_linear_map.id R₁ M₁) = linear_map.id
source
@[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₁] :
⇑(continuous_linear_map.id R₁ M₁) = id
source
@[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₁} :
↑f = linear_map.id ↔ f = continuous_linear_map.id R₁ M₁
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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))
source
@[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))
source
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)
source
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
source
@[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
source
@[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
source
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)
source
@[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₂) :
f.comp (continuous_linear_map.id R₁ M₁) = f
source
@[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₂) :
(continuous_linear_map.id R₂ M₂).comp f = f
source
@[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
source
@[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
source
@[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₂
source
@[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
source
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)
source
@[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
source
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
source
@[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
source
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)
source
@[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
source
@[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
source
def continuous_linear_map.to_linear_map_ring_hom {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] [module R₁ M₁] [has_continuous_add M₁] :
(M₁ →L[R₁] M₁) →+* M₁ →ₗ[R₁] M₁

continuous_linear_map.to_linear_map as a ring_hom.

Equations
source
@[simp]
theorem continuous_linear_map.to_linear_map_ring_hom_apply {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] [module R₁ M₁] [has_continuous_add M₁] (self : M₁ →L[R₁] M₁) :
⇑continuous_linear_map.to_linear_map_ring_hom self = self.to_linear_map
source
@[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
source
@[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
source
@[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.

source
@[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₁
source
@[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₁
source
@[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₁
source
@[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
source
@[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₂
source
@[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)
source
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
source
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
source
@[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)
source
@[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)
source
@[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₂
source
@[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₂
source
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) :
is_closed ↑(linear_map.ker f)
source
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) :
is_complete ↑(linear_map.ker f)
source
@[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) :
complete_space ↥(linear_map.ker f)
source
@[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₃) :
linear_map.ker (f.prod g) = linear_map.ker f ⊓ linear_map.ker g
source
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
source
@[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) :
↑(f.cod_restrict p h) = linear_map.cod_restrict p ↑f h
source
@[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
source
@[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) :
linear_map.ker (f.cod_restrict p h) = linear_map.ker f
source
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
source
@[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₁) :
↑(p.subtypeL) = p.subtype
source
@[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₁) :
⇑(p.subtypeL) = ⇑(p.subtype)
source
@[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) :
⇑(p.subtypeL) x = ↑x
source
@[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₁) :
linear_map.range p.subtypeL = p
source
@[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₁) :
linear_map.ker p.subtypeL = ⊥
source
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
source
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
source
@[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₂
source
@[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₂) = prod.fst
source
@[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₂
source
@[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₂) = prod.snd
source
@[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₂)
source
@[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
source
@[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
source
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
source
@[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₂
source
@[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₂
source
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
source
@[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₂
source
@[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
source
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₃) :
linear_map.range (f₁.coprod f₂) = linear_map.range f₁ ⊔ linear_map.range f₂
source
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
source
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'₁)
source
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
source
@[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
source
@[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
source
@[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'
source
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₁} :
(1.smul_right x).comp (1.smul_right c) = 1.smul_right (c • x)
source
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
source
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₁) :
⇑(continuous_linear_map.to_span_singleton R₁ x) r = r • x
source
theorem continuous_linear_map.to_span_singleton_add (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₁] [has_continuous_add M₁] (x y : M₁) :
continuous_linear_map.to_span_singleton R₁ (x + y) = continuous_linear_map.to_span_singleton R₁ x + continuous_linear_map.to_span_singleton R₁ y
source
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₁) :
continuous_linear_map.to_span_singleton R₁ (c • x) = c • continuous_linear_map.to_span_singleton R₁ x
source
theorem continuous_linear_map.to_span_singleton_smul (R : Type u_1) {M₁ : Type u_2} [comm_semiring R] [add_comm_monoid M₁] [module R M₁] [topological_space R] [topological_space M₁] [has_continuous_smul R M₁] (c : R) (x : M₁) :
continuous_linear_map.to_span_singleton R (c • x) = c • continuous_linear_map.to_span_singleton R x

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

source
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
source
@[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
source
@[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) = linear_map.pi (λ (i : ι), ↑(f i))
source
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 : ι) :
⇑(continuous_linear_map.pi f) c i = ⇑(f i) c
source
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
source
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
source
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) :
(continuous_linear_map.pi f).comp g = continuous_linear_map.pi (λ (i : ι), (f i).comp g)
source
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
source
@[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) :
⇑(continuous_linear_map.proj i) b = b i
source
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 : ι) :
(continuous_linear_map.proj i).comp (continuous_linear_map.pi f) = f i
source
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)] :
(⨅ (i : ι), linear_map.ker (continuous_linear_map.proj i)) = ⊥
source
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
source
@[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
source
@[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
source
@[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
source
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 = ⊤) :
linear_map.range (f.prod g) = (linear_map.range f).prod (linear_map.range g)
source
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₃) :
(linear_map.ker f).prod (linear_map.ker g) ≤ linear_map.ker (f.coprod g)
source
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