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] M₃) (g : M₂ →L[R] M₃) (hd : disjoint (linear_map.range f) (linear_map.range g)) :
linear_map.ker (f.coprod g) = (linear_map.ker f).prod (linear_map.ker g)
source
@[protected, instance]
def continuous_linear_map.has_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₂} [topological_add_group M₂] :
has_neg (M →SL[σ₁₂] M₂)
Equations
source
@[simp]
theorem continuous_linear_map.neg_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₂} [topological_add_group M₂] (f : M →SL[σ₁₂] M₂) (x : M) :
(⇑-f) x = -⇑f x
source
@[simp, norm_cast]
theorem continuous_linear_map.coe_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₂} [topological_add_group M₂] (f : M →SL[σ₁₂] M₂) :
↑-f = -↑f
source
@[norm_cast]
theorem continuous_linear_map.coe_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₂} [topological_add_group M₂] (f : M →SL[σ₁₂] M₂) :
⇑-f = -⇑f
source
@[protected, instance]
def continuous_linear_map.has_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₂} [topological_add_group M₂] :
has_sub (M →SL[σ₁₂] M₂)
Equations
source
@[protected, instance]
def continuous_linear_map.add_comm_group {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₂} [topological_add_group M₂] :
add_comm_group (M →SL[σ₁₂] M₂)
Equations
source
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₂} [topological_add_group M₂] (f g : M →SL[σ₁₂] M₂) (x : M) :
⇑(f - g) x = ⇑f x - ⇑g x
source
@[simp, norm_cast]
theorem continuous_linear_map.coe_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₂} [topological_add_group M₂] (f g : M →SL[σ₁₂] M₂) :
↑(f - g) = ↑f - ↑g
source
@[simp, norm_cast]
theorem continuous_linear_map.coe_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₂} [topological_add_group M₂] (f g : M →SL[σ₁₂] M₂) :
⇑(f - g) = ⇑f - ⇑g
source
@[simp]
theorem continuous_linear_map.comp_neg {R : Type u_1} [ring R] {R₂ : Type u_2} [ring R₂] {R₃ : Type u_3} [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₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] [topological_add_group M₂] [topological_add_group M₃] (g : M₂ →SL[σ₂₃] M₃) (f : M →SL[σ₁₂] M₂) :
g.comp (-f) = -g.comp f
source
@[simp]
theorem continuous_linear_map.neg_comp {R : Type u_1} [ring R] {R₂ : Type u_2} [ring R₂] {R₃ : Type u_3} [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₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] [topological_add_group M₃] (g : M₂ →SL[σ₂₃] M₃) (f : M →SL[σ₁₂] M₂) :
(-g).comp f = -g.comp f
source
@[simp]
theorem continuous_linear_map.comp_sub {R : Type u_1} [ring R] {R₂ : Type u_2} [ring R₂] {R₃ : Type u_3} [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₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] [topological_add_group M₂] [topological_add_group 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.sub_comp {R : Type u_1} [ring R] {R₂ : Type u_2} [ring R₂] {R₃ : Type u_3} [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₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] [topological_add_group M₃] (g₁ g₂ : M₂ →SL[σ₂₃] M₃) (f : M →SL[σ₁₂] M₂) :
(g₁ - g₂).comp f = g₁.comp f - g₂.comp f
source
@[protected, instance]
def continuous_linear_map.ring {R : Type u_1} [ring R] {M : Type u_4} [topological_space M] [add_comm_group M] [module R M] [topological_add_group M] :
ring (M →L[R] M)
Equations
source
theorem continuous_linear_map.smul_right_one_pow {R : Type u_1} [ring R] [topological_space R] [topological_ring R] (c : R) (n : ℕ) :
1.smul_right c ^ n = 1.smul_right (c ^ n)
source
def continuous_linear_map.proj_ker_of_right_inverse {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₂} {σ₂₁ : R₂ →+* R} [ring_hom_inv_pair σ₁₂ σ₂₁] [topological_add_group M] (f₁ : M →SL[σ₁₂] M₂) (f₂ : M₂ →SL[σ₂₁] M) (h : function.right_inverse ⇑f₂ ⇑f₁) :
M →L[R] ↥(linear_map.ker f₁)

Given a right inverse f₂ : M₂ →L[R] M to f₁ : M →L[R] M₂, proj_ker_of_right_inverse f₁ f₂ h is the projection M →L[R] f₁.ker along f₂.range.

Equations
source
@[simp]
theorem continuous_linear_map.coe_proj_ker_of_right_inverse_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₂} {σ₂₁ : R₂ →+* R} [ring_hom_inv_pair σ₁₂ σ₂₁] [topological_add_group M] (f₁ : M →SL[σ₁₂] M₂) (f₂ : M₂ →SL[σ₂₁] M) (h : function.right_inverse ⇑f₂ ⇑f₁) (x : M) :
↑(⇑(f₁.proj_ker_of_right_inverse f₂ h) x) = x - ⇑f₂ (⇑f₁ x)
source
@[simp]
theorem continuous_linear_map.proj_ker_of_right_inverse_apply_idem {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₂} {σ₂₁ : R₂ →+* R} [ring_hom_inv_pair σ₁₂ σ₂₁] [topological_add_group M] (f₁ : M →SL[σ₁₂] M₂) (f₂ : M₂ →SL[σ₂₁] M) (h : function.right_inverse ⇑f₂ ⇑f₁) (x : ↥(linear_map.ker f₁)) :
⇑(f₁.proj_ker_of_right_inverse f₂ h) ↑x = x
source
@[simp]
theorem continuous_linear_map.proj_ker_of_right_inverse_comp_inv {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₂} {σ₂₁ : R₂ →+* R} [ring_hom_inv_pair σ₁₂ σ₂₁] [topological_add_group M] (f₁ : M →SL[σ₁₂] M₂) (f₂ : M₂ →SL[σ₂₁] M) (h : function.right_inverse ⇑f₂ ⇑f₁) (y : M₂) :
⇑(f₁.proj_ker_of_right_inverse f₂ h) (⇑f₂ y) = 0
source
@[protected]
theorem continuous_linear_map.is_open_map_of_ne_zero {R : Type u_1} {M : Type u_2} [topological_space R] [division_ring R] [has_continuous_sub R] [add_comm_group M] [topological_space M] [has_continuous_add M] [module R M] [has_continuous_smul R M] (f : M →L[R] R) (hf : f ≠ 0) :
is_open_map ⇑f

A nonzero continuous linear functional is open.

source
@[simp]
theorem continuous_linear_map.smul_comp {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {S₃ : Type u_5} [semiring R] [semiring R₂] [semiring R₃] [monoid S₃] {M : Type u_6} [topological_space M] [add_comm_monoid M] [module R M] {M₂ : Type u_7} [topological_space M₂] [add_comm_monoid M₂] [module R₂ M₂] {M₃ : Type u_8} [topological_space M₃] [add_comm_monoid M₃] [module R₃ M₃] [distrib_mul_action S₃ M₃] [smul_comm_class R₃ S₃ M₃] [has_continuous_const_smul S₃ M₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] (c : S₃) (h : M₂ →SL[σ₂₃] M₃) (f : M →SL[σ₁₂] M₂) :
(c • h).comp f = c • h.comp f
source
@[simp]
theorem continuous_linear_map.comp_smul {R : Type u_1} {S : Type u_4} [semiring R] [monoid S] {M : Type u_6} [topological_space M] [add_comm_monoid M] [module R M] {N₂ : Type u_9} [topological_space N₂] [add_comm_monoid N₂] [module R N₂] {N₃ : Type u_10} [topological_space N₃] [add_comm_monoid N₃] [module R N₃] [distrib_mul_action S N₃] [smul_comm_class R S N₃] [has_continuous_const_smul S N₃] [distrib_mul_action S N₂] [has_continuous_const_smul S N₂] [smul_comm_class R S N₂] [linear_map.compatible_smul N₂ N₃ S R] (hₗ : N₂ →L[R] N₃) (c : S) (fₗ : M →L[R] N₂) :
hₗ.comp (c • fₗ) = c • hₗ.comp fₗ
source
@[simp]
theorem continuous_linear_map.comp_smulₛₗ {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [semiring R] [semiring R₂] [semiring R₃] {M : Type u_6} [topological_space M] [add_comm_monoid M] [module R M] {M₂ : Type u_7} [topological_space M₂] [add_comm_monoid M₂] [module R₂ M₂] {M₃ : Type u_8} [topological_space M₃] [add_comm_monoid M₃] [module R₃ M₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] [smul_comm_class R₂ R₂ M₂] [smul_comm_class R₃ R₃ M₃] [has_continuous_const_smul R₂ M₂] [has_continuous_const_smul R₃ M₃] (h : M₂ →SL[σ₂₃] M₃) (c : R₂) (f : M →SL[σ₁₂] M₂) :
h.comp (c • f) = ⇑σ₂₃ c • h.comp f
source
@[protected, instance]
def continuous_linear_map.distrib_mul_action {R : Type u_1} {R₂ : Type u_2} {S₃ : Type u_5} [semiring R] [semiring R₂] [monoid S₃] {M : Type u_6} [topological_space M] [add_comm_monoid M] [module R M] {M₂ : Type u_7} [topological_space M₂] [add_comm_monoid M₂] [module R₂ M₂] {σ₁₂ : R →+* R₂} [distrib_mul_action S₃ M₂] [has_continuous_const_smul S₃ M₂] [smul_comm_class R₂ S₃ M₂] [has_continuous_add M₂] :
distrib_mul_action S₃ (M →SL[σ₁₂] M₂)
Equations
source
def continuous_linear_map.prod_equiv {R : Type u_1} [semiring R] {M : Type u_6} [topological_space M] [add_comm_monoid M] [module R M] {N₂ : Type u_9} [topological_space N₂] [add_comm_monoid N₂] [module R N₂] {N₃ : Type u_10} [topological_space N₃] [add_comm_monoid N₃] [module R N₃] :
(M →L[R] N₂) × (M →L[R] N₃) ≃ (M →L[R] N₂ × N₃)

continuous_linear_map.prod as an equiv.

Equations
source
@[simp]
theorem continuous_linear_map.prod_equiv_apply {R : Type u_1} [semiring R] {M : Type u_6} [topological_space M] [add_comm_monoid M] [module R M] {N₂ : Type u_9} [topological_space N₂] [add_comm_monoid N₂] [module R N₂] {N₃ : Type u_10} [topological_space N₃] [add_comm_monoid N₃] [module R N₃] (f : (M →L[R] N₂) × (M →L[R] N₃)) :
⇑continuous_linear_map.prod_equiv f = f.fst.prod f.snd
source
theorem continuous_linear_map.prod_ext_iff {R : Type u_1} [semiring R] {M : Type u_6} [topological_space M] [add_comm_monoid M] [module R M] {N₂ : Type u_9} [topological_space N₂] [add_comm_monoid N₂] [module R N₂] {N₃ : Type u_10} [topological_space N₃] [add_comm_monoid N₃] [module R N₃] {f g : M × N₂ →L[R] N₃} :
f = g ↔ f.comp (continuous_linear_map.inl R M N₂) = g.comp (continuous_linear_map.inl R M N₂) ∧ f.comp (continuous_linear_map.inr R M N₂) = g.comp (continuous_linear_map.inr R M N₂)
source
@[ext]
theorem continuous_linear_map.prod_ext {R : Type u_1} [semiring R] {M : Type u_6} [topological_space M] [add_comm_monoid M] [module R M] {N₂ : Type u_9} [topological_space N₂] [add_comm_monoid N₂] [module R N₂] {N₃ : Type u_10} [topological_space N₃] [add_comm_monoid N₃] [module R N₃] {f g : M × N₂ →L[R] N₃} (hl : f.comp (continuous_linear_map.inl R M N₂) = g.comp (continuous_linear_map.inl R M N₂)) (hr : f.comp (continuous_linear_map.inr R M N₂) = g.comp (continuous_linear_map.inr R M N₂)) :
f = g
source
@[protected, instance]
def continuous_linear_map.module {R : Type u_1} {R₃ : Type u_3} {S₃ : Type u_5} [semiring R] [semiring R₃] [semiring S₃] {M : Type u_6} [topological_space M] [add_comm_monoid M] [module R M] {M₃ : Type u_8} [topological_space M₃] [add_comm_monoid M₃] [module R₃ M₃] [module S₃ M₃] [smul_comm_class R₃ S₃ M₃] [has_continuous_const_smul S₃ M₃] {σ₁₃ : R →+* R₃} [has_continuous_add M₃] :
module S₃ (M →SL[σ₁₃] M₃)
Equations
source
@[protected, instance]
def continuous_linear_map.is_central_scalar {R : Type u_1} {R₃ : Type u_3} {S₃ : Type u_5} [semiring R] [semiring R₃] [semiring S₃] {M : Type u_6} [topological_space M] [add_comm_monoid M] [module R M] {M₃ : Type u_8} [topological_space M₃] [add_comm_monoid M₃] [module R₃ M₃] [module S₃ M₃] [smul_comm_class R₃ S₃ M₃] [has_continuous_const_smul S₃ M₃] {σ₁₃ : R →+* R₃} [has_continuous_add M₃] [module S₃ᵐᵒᵖ M₃] [is_central_scalar S₃ M₃] :
is_central_scalar S₃ (M →SL[σ₁₃] M₃)
source
@[simp]
theorem continuous_linear_map.prodₗ_apply {R : Type u_1} (S : Type u_4) [semiring R] [semiring S] {M : Type u_6} [topological_space M] [add_comm_monoid M] [module R M] {N₂ : Type u_9} [topological_space N₂] [add_comm_monoid N₂] [module R N₂] {N₃ : Type u_10} [topological_space N₃] [add_comm_monoid N₃] [module R N₃] [module S N₂] [has_continuous_const_smul S N₂] [smul_comm_class R S N₂] [module S N₃] [smul_comm_class R S N₃] [has_continuous_const_smul S N₃] [has_continuous_add N₂] [has_continuous_add N₃] (ᾰ : (M →L[R] N₂) × (M →L[R] N₃)) :
⇑(continuous_linear_map.prodₗ S) ᾰ = continuous_linear_map.prod_equiv.to_fun ᾰ
source
def continuous_linear_map.prodₗ {R : Type u_1} (S : Type u_4) [semiring R] [semiring S] {M : Type u_6} [topological_space M] [add_comm_monoid M] [module R M] {N₂ : Type u_9} [topological_space N₂] [add_comm_monoid N₂] [module R N₂] {N₃ : Type u_10} [topological_space N₃] [add_comm_monoid N₃] [module R N₃] [module S N₂] [has_continuous_const_smul S N₂] [smul_comm_class R S N₂] [module S N₃] [smul_comm_class R S N₃] [has_continuous_const_smul S N₃] [has_continuous_add N₂] [has_continuous_add N₃] :
((M →L[R] N₂) × (M →L[R] N₃)) ≃ₗ[S] M →L[R] N₂ × N₃

continuous_linear_map.prod as a linear_equiv.

Equations
source
def continuous_linear_map.coe_lm {R : Type u_1} (S : Type u_4) [semiring R] [semiring S] {M : Type u_6} [topological_space M] [add_comm_monoid M] [module R M] {N₃ : Type u_10} [topological_space N₃] [add_comm_monoid N₃] [module R N₃] [module S N₃] [smul_comm_class R S N₃] [has_continuous_const_smul S N₃] [has_continuous_add N₃] :
(M →L[R] N₃) →ₗ[S] M →ₗ[R] N₃

The coercion from M →L[R] M₂ to M →ₗ[R] M₂, as a linear map.

Equations
source
@[simp]
theorem continuous_linear_map.coe_lm_apply {R : Type u_1} (S : Type u_4) [semiring R] [semiring S] {M : Type u_6} [topological_space M] [add_comm_monoid M] [module R M] {N₃ : Type u_10} [topological_space N₃] [add_comm_monoid N₃] [module R N₃] [module S N₃] [smul_comm_class R S N₃] [has_continuous_const_smul S N₃] [has_continuous_add N₃] (ᾰ : M →L[R] N₃) :
⇑(continuous_linear_map.coe_lm S) ᾰ = ↑ᾰ
source
@[simp]
theorem continuous_linear_map.coe_lmₛₗ_apply {R : Type u_1} {R₃ : Type u_3} {S₃ : Type u_5} [semiring R] [semiring R₃] [semiring S₃] {M : Type u_6} [topological_space M] [add_comm_monoid M] [module R M] {M₃ : Type u_8} [topological_space M₃] [add_comm_monoid M₃] [module R₃ M₃] [module S₃ M₃] [smul_comm_class R₃ S₃ M₃] [has_continuous_const_smul S₃ M₃] (σ₁₃ : R →+* R₃) [has_continuous_add M₃] (ᾰ : M →SL[σ₁₃] M₃) :
⇑(continuous_linear_map.coe_lmₛₗ σ₁₃) ᾰ = ↑ᾰ
source
def continuous_linear_map.coe_lmₛₗ {R : Type u_1} {R₃ : Type u_3} {S₃ : Type u_5} [semiring R] [semiring R₃] [semiring S₃] {M : Type u_6} [topological_space M] [add_comm_monoid M] [module R M] {M₃ : Type u_8} [topological_space M₃] [add_comm_monoid M₃] [module R₃ M₃] [module S₃ M₃] [smul_comm_class R₃ S₃ M₃] [has_continuous_const_smul S₃ M₃] (σ₁₃ : R →+* R₃) [has_continuous_add M₃] :
(M →SL[σ₁₃] M₃) →ₗ[S₃] M →ₛₗ[σ₁₃] M₃

The coercion from M →SL[σ] M₂ to M →ₛₗ[σ] M₂, as a linear map.

Equations
source
def continuous_linear_map.smul_rightₗ {R : Type u_1} {S : Type u_2} {T : Type u_3} {M : Type u_4} {M₂ : Type u_5} [semiring R] [semiring S] [semiring T] [module R S] [add_comm_monoid M₂] [module R M₂] [module S M₂] [is_scalar_tower R S M₂] [topological_space S] [topological_space M₂] [has_continuous_smul S M₂] [topological_space M] [add_comm_monoid M] [module R M] [has_continuous_add M₂] [module T M₂] [has_continuous_const_smul T M₂] [smul_comm_class R T M₂] [smul_comm_class S T M₂] (c : M →L[R] S) :
M₂ →ₗ[T] M →L[R] M₂

Given c : E →L[𝕜] 𝕜, c.smul_rightₗ is the linear map from F to E →L[𝕜] F sending f to λ e, c e • f. See also continuous_linear_map.smul_rightL.

Equations
source
@[simp]
theorem continuous_linear_map.coe_smul_rightₗ {R : Type u_1} {S : Type u_2} {T : Type u_3} {M : Type u_4} {M₂ : Type u_5} [semiring R] [semiring S] [semiring T] [module R S] [add_comm_monoid M₂] [module R M₂] [module S M₂] [is_scalar_tower R S M₂] [topological_space S] [topological_space M₂] [has_continuous_smul S M₂] [topological_space M] [add_comm_monoid M] [module R M] [has_continuous_add M₂] [module T M₂] [has_continuous_const_smul T M₂] [smul_comm_class R T M₂] [smul_comm_class S T M₂] (c : M →L[R] S) :
⇑(c.smul_rightₗ) = c.smul_right
source
@[protected, instance]
def continuous_linear_map.algebra {R : Type u_1} [comm_ring R] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [module R M₂] [topological_add_group M₂] [has_continuous_const_smul R M₂] :
algebra R (M₂ →L[R] M₂)
Equations
source
def continuous_linear_map.restrict_scalars {A : Type u_1} {M : Type u_2} {M₂ : Type u_3} [ring A] [add_comm_group M] [add_comm_group M₂] [module A M] [module A M₂] [topological_space M] [topological_space M₂] (R : Type u_4) [ring R] [module R M] [module R M₂] [linear_map.compatible_smul M M₂ R A] (f : M →L[A] M₂) :
M →L[R] M₂

If A is an R-algebra, then a continuous A-linear map can be interpreted as a continuous R-linear map. We assume linear_map.compatible_smul M M₂ R A to match assumptions of linear_map.map_smul_of_tower.

Equations
source
@[simp, norm_cast]
theorem continuous_linear_map.coe_restrict_scalars {A : Type u_1} {M : Type u_2} {M₂ : Type u_3} [ring A] [add_comm_group M] [add_comm_group M₂] [module A M] [module A M₂] [topological_space M] [topological_space M₂] {R : Type u_4} [ring R] [module R M] [module R M₂] [linear_map.compatible_smul M M₂ R A] (f : M →L[A] M₂) :
↑(continuous_linear_map.restrict_scalars R f) = linear_map.restrict_scalars R ↑f
source
@[simp]
theorem continuous_linear_map.coe_restrict_scalars' {A : Type u_1} {M : Type u_2} {M₂ : Type u_3} [ring A] [add_comm_group M] [add_comm_group M₂] [module A M] [module A M₂] [topological_space M] [topological_space M₂] {R : Type u_4} [ring R] [module R M] [module R M₂] [linear_map.compatible_smul M M₂ R A] (f : M →L[A] M₂) :
⇑(continuous_linear_map.restrict_scalars R f) = ⇑f
source
@[simp]
theorem continuous_linear_map.restrict_scalars_zero {A : Type u_1} {M : Type u_2} {M₂ : Type u_3} [ring A] [add_comm_group M] [add_comm_group M₂] [module A M] [module A M₂] [topological_space M] [topological_space M₂] {R : Type u_4} [ring R] [module R M] [module R M₂] [linear_map.compatible_smul M M₂ R A] :
continuous_linear_map.restrict_scalars R 0 = 0
source
@[simp]
theorem continuous_linear_map.restrict_scalars_add {A : Type u_1} {M : Type u_2} {M₂ : Type u_3} [ring A] [add_comm_group M] [add_comm_group M₂] [module A M] [module A M₂] [topological_space M] [topological_space M₂] {R : Type u_4} [ring R] [module R M] [module R M₂] [linear_map.compatible_smul M M₂ R A] [topological_add_group M₂] (f g : M →L[A] M₂) :
continuous_linear_map.restrict_scalars R (f + g) = continuous_linear_map.restrict_scalars R f + continuous_linear_map.restrict_scalars R g
source
@[simp]
theorem continuous_linear_map.restrict_scalars_neg {A : Type u_1} {M : Type u_2} {M₂ : Type u_3} [ring A] [add_comm_group M] [add_comm_group M₂] [module A M] [module A M₂] [topological_space M] [topological_space M₂] {R : Type u_4} [ring R] [module R M] [module R M₂] [linear_map.compatible_smul M M₂ R A] [topological_add_group M₂] (f : M →L[A] M₂) :
continuous_linear_map.restrict_scalars R (-f) = -continuous_linear_map.restrict_scalars R f
source
@[simp]
theorem continuous_linear_map.restrict_scalars_smul {A : Type u_1} {M : Type u_2} {M₂ : Type u_3} [ring A] [add_comm_group M] [add_comm_group M₂] [module A M] [module A M₂] [topological_space M] [topological_space M₂] {R : Type u_4} [ring R] [module R M] [module R M₂] [linear_map.compatible_smul M M₂ R A] {S : Type u_5} [ring S] [module S M₂] [has_continuous_const_smul S M₂] [smul_comm_class A S M₂] [smul_comm_class R S M₂] (c : S) (f : M →L[A] M₂) :
continuous_linear_map.restrict_scalars R (c • f) = c • continuous_linear_map.restrict_scalars R f
source
def continuous_linear_map.restrict_scalarsₗ (A : Type u_1) (M : Type u_2) (M₂ : Type u_3) [ring A] [add_comm_group M] [add_comm_group M₂] [module A M] [module A M₂] [topological_space M] [topological_space M₂] (R : Type u_4) [ring R] [module R M] [module R M₂] [linear_map.compatible_smul M M₂ R A] (S : Type u_5) [ring S] [module S M₂] [has_continuous_const_smul S M₂] [smul_comm_class A S M₂] [smul_comm_class R S M₂] [topological_add_group M₂] :
(M →L[A] M₂) →ₗ[S] M →L[R] M₂

continuous_linear_map.restrict_scalars as a linear_map. See also continuous_linear_map.restrict_scalarsL.

Equations
source
@[simp]
theorem continuous_linear_map.coe_restrict_scalarsₗ {A : Type u_1} {M : Type u_2} {M₂ : Type u_3} [ring A] [add_comm_group M] [add_comm_group M₂] [module A M] [module A M₂] [topological_space M] [topological_space M₂] {R : Type u_4} [ring R] [module R M] [module R M₂] [linear_map.compatible_smul M M₂ R A] {S : Type u_5} [ring S] [module S M₂] [has_continuous_const_smul S M₂] [smul_comm_class A S M₂] [smul_comm_class R S M₂] [topological_add_group M₂] :
⇑(continuous_linear_map.restrict_scalarsₗ A M M₂ R S) = continuous_linear_map.restrict_scalars R
source
def continuous_linear_equiv.to_continuous_linear_map {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂] (e : M₁ ≃SL[σ₁₂] M₂) :
M₁ →SL[σ₁₂] M₂

A continuous linear equivalence induces a continuous linear map.

Equations
source
@[protected, instance]
def continuous_linear_equiv.continuous_linear_map.has_coe {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₁ →SL[σ₁₂] M₂)

Coerce continuous linear equivs to continuous linear maps.

Equations
source
@[protected, instance]
def continuous_linear_equiv.continuous_semilinear_equiv_class {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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_equiv_class (M₁ ≃SL[σ₁₂] M₂) σ₁₂ M₁ M₂
Equations
source
@[protected, instance]
def continuous_linear_equiv.has_coe_to_fun {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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 equivs to maps.

Equations
source
@[simp]
theorem continuous_linear_equiv.coe_def_rev {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂] (e : M₁ ≃SL[σ₁₂] M₂) :
e.to_continuous_linear_map = ↑e
source
theorem continuous_linear_equiv.coe_apply {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂] (e : M₁ ≃SL[σ₁₂] M₂) (b : M₁) :
⇑↑e b = ⇑e b
source
@[simp]
theorem continuous_linear_equiv.coe_to_linear_equiv {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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_equiv) = ⇑f
source
@[simp, norm_cast]
theorem continuous_linear_equiv.coe_coe {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂] (e : M₁ ≃SL[σ₁₂] M₂) :
⇑↑e = ⇑e
source
theorem continuous_linear_equiv.to_linear_equiv_injective {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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 continuous_linear_equiv.to_linear_equiv
source
@[ext]
theorem continuous_linear_equiv.ext {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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 : ⇑f = ⇑g) :
f = g
source
theorem continuous_linear_equiv.coe_injective {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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
@[simp, norm_cast]
theorem continuous_linear_equiv.coe_inj {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂] {e e' : M₁ ≃SL[σ₁₂] M₂} :
↑e = ↑e' ↔ e = e'
source
def continuous_linear_equiv.to_homeomorph {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂] (e : M₁ ≃SL[σ₁₂] M₂) :
M₁ ≃ₜ M₂

A continuous linear equivalence induces a homeomorphism.

Equations
source
@[simp]
theorem continuous_linear_equiv.coe_to_homeomorph {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂] (e : M₁ ≃SL[σ₁₂] M₂) :
⇑(e.to_homeomorph) = ⇑e
source
theorem continuous_linear_equiv.image_closure {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂] (e : M₁ ≃SL[σ₁₂] M₂) (s : set M₁) :
⇑e '' closure s = closure (⇑e '' s)
source
theorem continuous_linear_equiv.preimage_closure {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂] (e : M₁ ≃SL[σ₁₂] M₂) (s : set M₂) :
⇑e ⁻¹' closure s = closure (⇑e ⁻¹' s)
source
@[simp]
theorem continuous_linear_equiv.is_closed_image {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂] (e : M₁ ≃SL[σ₁₂] M₂) {s : set M₁} :
is_closed (⇑e '' s) ↔ is_closed s
source
theorem continuous_linear_equiv.map_nhds_eq {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂] (e : M₁ ≃SL[σ₁₂] M₂) (x : M₁) :
filter.map ⇑e (nhds x) = nhds (⇑e x)
source
@[simp]
theorem continuous_linear_equiv.map_zero {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂] (e : M₁ ≃SL[σ₁₂] M₂) :
⇑e 0 = 0
source
@[simp]
theorem continuous_linear_equiv.map_add {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂] (e : M₁ ≃SL[σ₁₂] M₂) (x y : M₁) :
⇑e (x + y) = ⇑e x + ⇑e y
source
@[simp]
theorem continuous_linear_equiv.map_smulₛₗ {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂] (e : M₁ ≃SL[σ₁₂] M₂) (c : R₁) (x : M₁) :
⇑e (c • x) = ⇑σ₁₂ c • ⇑e x
source
@[simp]
theorem continuous_linear_equiv.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₂] (e : M₁ ≃L[R₁] M₂) (c : R₁) (x : M₁) :
⇑e (c • x) = c • ⇑e x
source
@[simp]
theorem continuous_linear_equiv.map_eq_zero_iff {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂] (e : M₁ ≃SL[σ₁₂] M₂) {x : M₁} :
⇑e x = 0 ↔ x = 0
source
@[protected, continuity]
theorem continuous_linear_equiv.continuous {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂] (e : M₁ ≃SL[σ₁₂] M₂) :
continuous ⇑e
source
@[protected]
theorem continuous_linear_equiv.continuous_on {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂] (e : M₁ ≃SL[σ₁₂] M₂) {s : set M₁} :
continuous_on ⇑e s
source
@[protected]
theorem continuous_linear_equiv.continuous_at {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂] (e : M₁ ≃SL[σ₁₂] M₂) {x : M₁} :
continuous_at ⇑e x
source
@[protected]
theorem continuous_linear_equiv.continuous_within_at {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂] (e : M₁ ≃SL[σ₁₂] M₂) {s : set M₁} {x : M₁} :
continuous_within_at ⇑e s x
source
theorem continuous_linear_equiv.comp_continuous_on_iff {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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} [topological_space α] (e : M₁ ≃SL[σ₁₂] M₂) {f : α → M₁} {s : set α} :
continuous_on (⇑e ∘ f) s ↔ continuous_on f s
source
theorem continuous_linear_equiv.comp_continuous_iff {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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} [topological_space α] (e : M₁ ≃SL[σ₁₂] M₂) {f : α → M₁} :
continuous (⇑e ∘ f) ↔ continuous f
source
theorem continuous_linear_equiv.ext₁ {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

An extensionality lemma for R ≃L[R] M.

source
@[protected, refl]
def continuous_linear_equiv.refl (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 equivalence.

Equations
source
@[simp, norm_cast]
theorem continuous_linear_equiv.coe_refl {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] [module R₁ M₁] :
↑(continuous_linear_equiv.refl R₁ M₁) = continuous_linear_map.id R₁ M₁
source
@[simp, norm_cast]
theorem continuous_linear_equiv.coe_refl' {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] [module R₁ M₁] :
⇑(continuous_linear_equiv.refl R₁ M₁) = id
source
@[protected, symm]
def continuous_linear_equiv.symm {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂] (e : M₁ ≃SL[σ₁₂] M₂) :
M₂ ≃SL[σ₂₁] M₁

The inverse of a continuous linear equivalence as a continuous linear equivalence

Equations
source
@[simp]
theorem continuous_linear_equiv.symm_to_linear_equiv {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂] (e : M₁ ≃SL[σ₁₂] M₂) :
e.symm.to_linear_equiv = e.to_linear_equiv.symm
source
@[simp]
theorem continuous_linear_equiv.symm_to_homeomorph {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂] (e : M₁ ≃SL[σ₁₂] M₂) :
e.to_homeomorph.symm = e.symm.to_homeomorph
source
def continuous_linear_equiv.simps.apply {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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_equiv.simps.symm_apply {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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
theorem continuous_linear_equiv.symm_map_nhds_eq {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂] (e : M₁ ≃SL[σ₁₂] M₂) (x : M₁) :
filter.map ⇑(e.symm) (nhds (⇑e x)) = nhds x
source
@[protected, trans]
def continuous_linear_equiv.trans {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [semiring R₁] [semiring R₂] [semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} [ring_hom_inv_pair σ₂₃ σ₃₂] [ring_hom_inv_pair σ₃₂ σ₂₃] {σ₁₃ : R₁ →+* R₃} {σ₃₁ : R₃ →+* R₁} [ring_hom_inv_pair σ₁₃ σ₃₁] [ring_hom_inv_pair σ₃₁ σ₁₃] [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] [ring_hom_comp_triple σ₃₂ σ₂₁ σ₃₁] {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₃] (e₁ : M₁ ≃SL[σ₁₂] M₂) (e₂ : M₂ ≃SL[σ₂₃] M₃) :
M₁ ≃SL[σ₁₃] M₃

The composition of two continuous linear equivalences as a continuous linear equivalence.

Equations
source
@[simp]
theorem continuous_linear_equiv.trans_to_linear_equiv {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [semiring R₁] [semiring R₂] [semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} [ring_hom_inv_pair σ₂₃ σ₃₂] [ring_hom_inv_pair σ₃₂ σ₂₃] {σ₁₃ : R₁ →+* R₃} {σ₃₁ : R₃ →+* R₁} [ring_hom_inv_pair σ₁₃ σ₃₁] [ring_hom_inv_pair σ₃₁ σ₁₃] [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] [ring_hom_comp_triple σ₃₂ σ₂₁ σ₃₁] {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₃] (e₁ : M₁ ≃SL[σ₁₂] M₂) (e₂ : M₂ ≃SL[σ₂₃] M₃) :
(e₁.trans e₂).to_linear_equiv = e₁.to_linear_equiv.trans e₂.to_linear_equiv
source
def continuous_linear_equiv.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₃] {M₄ : Type u_8} [topological_space M₄] [add_comm_monoid M₄] [module R₁ M₁] [module R₁ M₂] [module R₁ M₃] [module R₁ M₄] (e : M₁ ≃L[R₁] M₂) (e' : M₃ ≃L[R₁] M₄) :
(M₁ × M₃) ≃L[R₁] M₂ × M₄

Product of two continuous linear equivalences. The map comes from equiv.prod_congr.

Equations
source
@[simp, norm_cast]
theorem continuous_linear_equiv.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₃] {M₄ : Type u_8} [topological_space M₄] [add_comm_monoid M₄] [module R₁ M₁] [module R₁ M₂] [module R₁ M₃] [module R₁ M₄] (e : M₁ ≃L[R₁] M₂) (e' : M₃ ≃L[R₁] M₄) (x : M₁ × M₃) :
⇑(e.prod e') x = (⇑e x.fst, ⇑e' x.snd)
source
@[simp, norm_cast]
theorem continuous_linear_equiv.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₃] {M₄ : Type u_8} [topological_space M₄] [add_comm_monoid M₄] [module R₁ M₁] [module R₁ M₂] [module R₁ M₃] [module R₁ M₄] (e : M₁ ≃L[R₁] M₂) (e' : M₃ ≃L[R₁] M₄) :
↑(e.prod e') = ↑e.prod_map ↑e'
source
theorem continuous_linear_equiv.prod_symm {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₄] (e : M₁ ≃L[R₁] M₂) (e' : M₃ ≃L[R₁] M₄) :
(e.prod e').symm = e.symm.prod e'.symm
source
@[protected]
theorem continuous_linear_equiv.bijective {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂] (e : M₁ ≃SL[σ₁₂] M₂) :
function.bijective ⇑e
source
@[protected]
theorem continuous_linear_equiv.injective {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂] (e : M₁ ≃SL[σ₁₂] M₂) :
function.injective ⇑e
source
@[protected]
theorem continuous_linear_equiv.surjective {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂] (e : M₁ ≃SL[σ₁₂] M₂) :
function.surjective ⇑e
source
@[simp]
theorem continuous_linear_equiv.trans_apply {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [semiring R₁] [semiring R₂] [semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} [ring_hom_inv_pair σ₂₃ σ₃₂] [ring_hom_inv_pair σ₃₂ σ₂₃] {σ₁₃ : R₁ →+* R₃} {σ₃₁ : R₃ →+* R₁} [ring_hom_inv_pair σ₁₃ σ₃₁] [ring_hom_inv_pair σ₃₁ σ₁₃] [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] [ring_hom_comp_triple σ₃₂ σ₂₁ σ₃₁] {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₃] (e₁ : M₁ ≃SL[σ₁₂] M₂) (e₂ : M₂ ≃SL[σ₂₃] M₃) (c : M₁) :
⇑(e₁.trans e₂) c = ⇑e₂ (⇑e₁ c)
source
@[simp]
theorem continuous_linear_equiv.apply_symm_apply {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂] (e : M₁ ≃SL[σ₁₂] M₂) (c : M₂) :
⇑e (⇑(e.symm) c) = c
source
@[simp]
theorem continuous_linear_equiv.symm_apply_apply {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂] (e : M₁ ≃SL[σ₁₂] M₂) (b : M₁) :
⇑(e.symm) (⇑e b) = b
source
@[simp]
theorem continuous_linear_equiv.symm_trans_apply {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [semiring R₁] [semiring R₂] [semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} [ring_hom_inv_pair σ₂₃ σ₃₂] [ring_hom_inv_pair σ₃₂ σ₂₃] {σ₁₃ : R₁ →+* R₃} {σ₃₁ : R₃ →+* R₁} [ring_hom_inv_pair σ₁₃ σ₃₁] [ring_hom_inv_pair σ₃₁ σ₁₃] [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] [ring_hom_comp_triple σ₃₂ σ₂₁ σ₃₁] {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₃] (e₁ : M₂ ≃SL[σ₂₁] M₁) (e₂ : M₃ ≃SL[σ₃₂] M₂) (c : M₁) :
⇑((e₂.trans e₁).symm) c = ⇑(e₂.symm) (⇑(e₁.symm) c)
source
@[simp]
theorem continuous_linear_equiv.symm_image_image {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂] (e : M₁ ≃SL[σ₁₂] M₂) (s : set M₁) :
⇑(e.symm) '' (⇑e '' s) = s
source
@[simp]
theorem continuous_linear_equiv.image_symm_image {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂] (e : M₁ ≃SL[σ₁₂] M₂) (s : set M₂) :
⇑e '' (⇑(e.symm) '' s) = s
source
@[simp, norm_cast]
theorem continuous_linear_equiv.comp_coe {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [semiring R₁] [semiring R₂] [semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} [ring_hom_inv_pair σ₂₃ σ₃₂] [ring_hom_inv_pair σ₃₂ σ₂₃] {σ₁₃ : R₁ →+* R₃} {σ₃₁ : R₃ →+* R₁} [ring_hom_inv_pair σ₁₃ σ₃₁] [ring_hom_inv_pair σ₃₁ σ₁₃] [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] [ring_hom_comp_triple σ₃₂ σ₂₁ σ₃₁] {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₁ ≃SL[σ₁₂] M₂) (f' : M₂ ≃SL[σ₂₃] M₃) :
↑f'.comp ↑f = ↑(f.trans f')
source
@[simp]
theorem continuous_linear_equiv.coe_comp_coe_symm {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂] (e : M₁ ≃SL[σ₁₂] M₂) :
↑e.comp ↑(e.symm) = continuous_linear_map.id R₂ M₂
source
@[simp]
theorem continuous_linear_equiv.coe_symm_comp_coe {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂] (e : M₁ ≃SL[σ₁₂] M₂) :
↑(e.symm).comp ↑e = continuous_linear_map.id R₁ M₁
source
@[simp]
theorem continuous_linear_equiv.symm_comp_self {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂] (e : M₁ ≃SL[σ₁₂] M₂) :
⇑(e.symm) ∘ ⇑e = id
source
@[simp]
theorem continuous_linear_equiv.self_comp_symm {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂] (e : M₁ ≃SL[σ₁₂] M₂) :
⇑e ∘ ⇑(e.symm) = id
source
@[simp]
theorem continuous_linear_equiv.symm_symm {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂] (e : M₁ ≃SL[σ₁₂] M₂) :
e.symm.symm = e
source
@[simp]
theorem continuous_linear_equiv.refl_symm {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] [module R₁ M₁] :
(continuous_linear_equiv.refl R₁ M₁).symm = continuous_linear_equiv.refl R₁ M₁
source
theorem continuous_linear_equiv.symm_symm_apply {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂] (e : M₁ ≃SL[σ₁₂] M₂) (x : M₁) :
⇑(e.symm.symm) x = ⇑e x
source
theorem continuous_linear_equiv.symm_apply_eq {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂] (e : M₁ ≃SL[σ₁₂] M₂) {x : M₂} {y : M₁} :
⇑(e.symm) x = y ↔ x = ⇑e y
source
theorem continuous_linear_equiv.eq_symm_apply {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂] (e : M₁ ≃SL[σ₁₂] M₂) {x : M₂} {y : M₁} :
y = ⇑(e.symm) x ↔ ⇑e y = x
source
@[protected]
theorem continuous_linear_equiv.image_eq_preimage {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂] (e : M₁ ≃SL[σ₁₂] M₂) (s : set M₁) :
⇑e '' s = ⇑(e.symm) ⁻¹' s
source
@[protected]
theorem continuous_linear_equiv.image_symm_eq_preimage {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂] (e : M₁ ≃SL[σ₁₂] M₂) (s : set M₂) :
⇑(e.symm) '' s = ⇑e ⁻¹' s
source
@[protected, simp]
theorem continuous_linear_equiv.symm_preimage_preimage {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂] (e : M₁ ≃SL[σ₁₂] M₂) (s : set M₂) :
⇑(e.symm) ⁻¹' (⇑e ⁻¹' s) = s
source
@[protected, simp]
theorem continuous_linear_equiv.preimage_symm_preimage {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂] (e : M₁ ≃SL[σ₁₂] M₂) (s : set M₁) :
⇑e ⁻¹' (⇑(e.symm) ⁻¹' s) = s
source
@[protected]
theorem continuous_linear_equiv.uniform_embedding {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂] (e : E₁ ≃SL[σ₁₂] E₂) :
uniform_embedding ⇑e
source
@[protected]
theorem linear_equiv.uniform_embedding {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂] (e : E₁ ≃ₛₗ[σ₁₂] E₂) (h₁ : continuous ⇑e) (h₂ : continuous ⇑(e.symm)) :
uniform_embedding ⇑e
source
def continuous_linear_equiv.equiv_of_inverse {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂ →SL[σ₂₁] M₁) (h₁ : function.left_inverse ⇑f₂ ⇑f₁) (h₂ : function.right_inverse ⇑f₂ ⇑f₁) :
M₁ ≃SL[σ₁₂] M₂

Create a continuous_linear_equiv from two continuous_linear_maps that are inverse of each other.

Equations
source
@[simp]
theorem continuous_linear_equiv.equiv_of_inverse_apply {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂ →SL[σ₂₁] M₁) (h₁ : function.left_inverse ⇑f₂ ⇑f₁) (h₂ : function.right_inverse ⇑f₂ ⇑f₁) (x : M₁) :
⇑(continuous_linear_equiv.equiv_of_inverse f₁ f₂ h₁ h₂) x = ⇑f₁ x
source
@[simp]
theorem continuous_linear_equiv.symm_equiv_of_inverse {R₁ : Type u_1} {R₂ : Type u_2} [semiring R₁] [semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {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₂ →SL[σ₂₁] M₁) (h₁ : function.left_inverse ⇑f₂ ⇑f₁) (h₂ : function.right_inverse ⇑f₂ ⇑f₁) :
(continuous_linear_equiv.equiv_of_inverse f₁ f₂ h₁ h₂).symm = continuous_linear_equiv.equiv_of_inverse f₂ f₁ h₂ h₁
source
@[protected, instance]
def continuous_linear_equiv.automorphism_group {R₁ : Type u_1} [semiring R₁] (M₁ : Type u_4) [topological_space M₁] [add_comm_monoid M₁] [module R₁ M₁] :
group (M₁ ≃L[R₁] M₁)

The continuous linear equivalences from M to itself form a group under composition.

Equations
source
def continuous_linear_equiv.ulift {R₁ : Type u_1} [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] [module R₁ M₁] :
ulift M₁ ≃L[R₁] M₁

The continuous linear equivalence between ulift M₁ and M₁.

Equations
source
@[simp]
theorem continuous_linear_equiv.arrow_congr_equiv_symm_apply {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [semiring R₁] [semiring R₂] [semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] {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₃] {R₄ : Type u_9} [semiring R₄] [module R₄ M₄] {σ₃₄ : R₃ →+* R₄} {σ₄₃ : R₄ →+* R₃} [ring_hom_inv_pair σ₃₄ σ₄₃] [ring_hom_inv_pair σ₄₃ σ₃₄] {σ₂₄ : R₂ →+* R₄} {σ₁₄ : R₁ →+* R₄} [ring_hom_comp_triple σ₂₁ σ₁₄ σ₂₄] [ring_hom_comp_triple σ₂₄ σ₄₃ σ₂₃] [ring_hom_comp_triple σ₁₃ σ₃₄ σ₁₄] (e₁₂ : M₁ ≃SL[σ₁₂] M₂) (e₄₃ : M₄ ≃SL[σ₄₃] M₃) (f : M₂ →SL[σ₂₃] M₃) :
⇑((e₁₂.arrow_congr_equiv e₄₃).symm) f = ↑(e₄₃.symm).comp (f.comp ↑e₁₂)
source
def continuous_linear_equiv.arrow_congr_equiv {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [semiring R₁] [semiring R₂] [semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] {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₃] {R₄ : Type u_9} [semiring R₄] [module R₄ M₄] {σ₃₄ : R₃ →+* R₄} {σ₄₃ : R₄ →+* R₃} [ring_hom_inv_pair σ₃₄ σ₄₃] [ring_hom_inv_pair σ₄₃ σ₃₄] {σ₂₄ : R₂ →+* R₄} {σ₁₄ : R₁ →+* R₄} [ring_hom_comp_triple σ₂₁ σ₁₄ σ₂₄] [ring_hom_comp_triple σ₂₄ σ₄₃ σ₂₃] [ring_hom_comp_triple σ₁₃ σ₃₄ σ₁₄] (e₁₂ : M₁ ≃SL[σ₁₂] M₂) (e₄₃ : M₄ ≃SL[σ₄₃] M₃) :
(M₁ →SL[σ₁₄] M₄) ≃ (M₂ →SL[σ₂₃] M₃)

A pair of continuous (semi)linear equivalences generates an equivalence between the spaces of continuous linear maps. See also continuous_linear_equiv.arrow_congr.

Equations
source
@[simp]
theorem continuous_linear_equiv.arrow_congr_equiv_apply {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [semiring R₁] [semiring R₂] [semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] {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₃] {R₄ : Type u_9} [semiring R₄] [module R₄ M₄] {σ₃₄ : R₃ →+* R₄} {σ₄₃ : R₄ →+* R₃} [ring_hom_inv_pair σ₃₄ σ₄₃] [ring_hom_inv_pair σ₄₃ σ₃₄] {σ₂₄ : R₂ →+* R₄} {σ₁₄ : R₁ →+* R₄} [ring_hom_comp_triple σ₂₁ σ₁₄ σ₂₄] [ring_hom_comp_triple σ₂₄ σ₄₃ σ₂₃] [ring_hom_comp_triple σ₁₃ σ₃₄ σ₁₄] (e₁₂ : M₁ ≃SL[σ₁₂] M₂) (e₄₃ : M₄ ≃SL[σ₄₃] M₃) (f : M₁ →SL[σ₁₄] M₄) :
⇑(e₁₂.arrow_congr_equiv e₄₃) f = ↑e₄₃.comp (f.comp ↑(e₁₂.symm))
source
def continuous_linear_equiv.skew_prod {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_group M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] {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₂] [module R M₃] [module R M₄] [topological_add_group M₄] (e : M ≃L[R] M₂) (e' : M₃ ≃L[R] M₄) (f : M →L[R] M₄) :
(M × M₃) ≃L[R] M₂ × M₄

Equivalence given by a block lower diagonal matrix. e and e' are diagonal square blocks, and f is a rectangular block below the diagonal.

Equations
source
@[simp]
theorem continuous_linear_equiv.skew_prod_apply {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_group M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] {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₂] [module R M₃] [module R M₄] [topological_add_group M₄] (e : M ≃L[R] M₂) (e' : M₃ ≃L[R] M₄) (f : M →L[R] M₄) (x : M × M₃) :
⇑(e.skew_prod e' f) x = (⇑e x.fst, ⇑e' x.snd + ⇑f x.fst)
source
@[simp]
theorem continuous_linear_equiv.skew_prod_symm_apply {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_group M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] {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₂] [module R M₃] [module R M₄] [topological_add_group M₄] (e : M ≃L[R] M₂) (e' : M₃ ≃L[R] M₄) (f : M →L[R] M₄) (x : M₂ × M₄) :
⇑((e.skew_prod e' f).symm) x = (⇑(e.symm) x.fst, ⇑(e'.symm) (x.snd - ⇑f (⇑(e.symm) x.fst)))
source
@[simp]
theorem continuous_linear_equiv.map_sub {R : Type u_1} [ring R] {R₂ : Type u_2} [ring R₂] {M : Type u_3} [topological_space M] [add_comm_group M] [module R M] {M₂ : Type u_4} [topological_space M₂] [add_comm_group M₂] [module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] (e : M ≃SL[σ₁₂] M₂) (x y : M) :
⇑e (x - y) = ⇑e x - ⇑e y
source
@[simp]
theorem continuous_linear_equiv.map_neg {R : Type u_1} [ring R] {R₂ : Type u_2} [ring R₂] {M : Type u_3} [topological_space M] [add_comm_group M] [module R M] {M₂ : Type u_4} [topological_space M₂] [add_comm_group M₂] [module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] (e : M ≃SL[σ₁₂] M₂) (x : M) :
⇑e (-x) = -⇑e x

The next theorems cover the identification between M ≃L[𝕜] Mand the group of units of the ring M →L[R] M.

source
def continuous_linear_equiv.of_unit {R : Type u_1} [ring R] {M : Type u_3} [topological_space M] [add_comm_group M] [module R M] [topological_add_group M] (f : (M →L[R] M)ˣ) :
M ≃L[R] M

An invertible continuous linear map f determines a continuous equivalence from M to itself.

Equations
source
def continuous_linear_equiv.to_unit {R : Type u_1} [ring R] {M : Type u_3} [topological_space M] [add_comm_group M] [module R M] [topological_add_group M] (f : M ≃L[R] M) :
(M →L[R] M)ˣ

A continuous equivalence from M to itself determines an invertible continuous linear map.

Equations
source
def continuous_linear_equiv.units_equiv (R : Type u_1) [ring R] (M : Type u_3) [topological_space M] [add_comm_group M] [module R M] [topological_add_group M] :
(M →L[R] M)ˣ ≃* M ≃L[R] M

The units of the algebra of continuous R-linear endomorphisms of M is multiplicatively equivalent to the type of continuous linear equivalences between M and itself.

Equations
source
@[simp]
theorem continuous_linear_equiv.units_equiv_apply (R : Type u_1) [ring R] (M : Type u_3) [topological_space M] [add_comm_group M] [module R M] [topological_add_group M] (f : (M →L[R] M)ˣ) (x : M) :
⇑(⇑(continuous_linear_equiv.units_equiv R M) f) x = ⇑f x
source
def continuous_linear_equiv.units_equiv_aut (R : Type u_1) [ring R] [topological_space R] [has_continuous_mul R] :
Rˣ ≃ R ≃L[R] R

Continuous linear equivalences R ≃L[R] R are enumerated by Rˣ.

Equations
source
@[simp]
theorem continuous_linear_equiv.units_equiv_aut_apply {R : Type u_1} [ring R] [topological_space R] [has_continuous_mul R] (u : Rˣ) (x : R) :
⇑(⇑(continuous_linear_equiv.units_equiv_aut R) u) x = x * ↑u
source
@[simp]
theorem continuous_linear_equiv.units_equiv_aut_apply_symm {R : Type u_1} [ring R] [topological_space R] [has_continuous_mul R] (u : Rˣ) (x : R) :
⇑((⇑(continuous_linear_equiv.units_equiv_aut R) u).symm) x = x * ↑u⁻¹
source
@[simp]
theorem continuous_linear_equiv.units_equiv_aut_symm_apply {R : Type u_1} [ring R] [topological_space R] [has_continuous_mul R] (e : R ≃L[R] R) :
↑(⇑((continuous_linear_equiv.units_equiv_aut R).symm) e) = ⇑e 1
source
def continuous_linear_equiv.equiv_of_right_inverse {R : Type u_1} [ring R] {M : Type u_3} [topological_space M] [add_comm_group M] [module R M] {M₂ : Type u_4} [topological_space M₂] [add_comm_group M₂] [module R M₂] [topological_add_group M] (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) (h : function.right_inverse ⇑f₂ ⇑f₁) :
M ≃L[R] M₂ × ↥(linear_map.ker f₁)

A pair of continuous linear maps such that f₁ ∘ f₂ = id generates a continuous linear equivalence e between M and M₂ × f₁.ker such that (e x).2 = x for x ∈ f₁.ker, (e x).1 = f₁ x, and (e (f₂ y)).2 = 0. The map is given by e x = (f₁ x, x - f₂ (f₁ x)).

Equations
source
@[simp]
theorem continuous_linear_equiv.fst_equiv_of_right_inverse {R : Type u_1} [ring R] {M : Type u_3} [topological_space M] [add_comm_group M] [module R M] {M₂ : Type u_4} [topological_space M₂] [add_comm_group M₂] [module R M₂] [topological_add_group M] (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) (h : function.right_inverse ⇑f₂ ⇑f₁) (x : M) :
(⇑(continuous_linear_equiv.equiv_of_right_inverse f₁ f₂ h) x).fst = ⇑f₁ x
source
@[simp]
theorem continuous_linear_equiv.snd_equiv_of_right_inverse {R : Type u_1} [ring R] {M : Type u_3} [topological_space M] [add_comm_group M] [module R M] {M₂ : Type u_4} [topological_space M₂] [add_comm_group M₂] [module R M₂] [topological_add_group M] (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) (h : function.right_inverse ⇑f₂ ⇑f₁) (x : M) :
↑((⇑(continuous_linear_equiv.equiv_of_right_inverse f₁ f₂ h) x).snd) = x - ⇑f₂ (⇑f₁ x)
source
@[simp]
theorem continuous_linear_equiv.equiv_of_right_inverse_symm_apply {R : Type u_1} [ring R] {M : Type u_3} [topological_space M] [add_comm_group M] [module R M] {M₂ : Type u_4} [topological_space M₂] [add_comm_group M₂] [module R M₂] [topological_add_group M] (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) (h : function.right_inverse ⇑f₂ ⇑f₁) (y : M₂ × ↥(linear_map.ker f₁)) :
⇑((continuous_linear_equiv.equiv_of_right_inverse f₁ f₂ h).symm) y = ⇑f₂ y.fst + ↑(y.snd)
source
def continuous_linear_equiv.fun_unique (ι : Type u_1) (R : Type u_2) (M : Type u_3) [unique ι] [semiring R] [add_comm_monoid M] [module R M] [topological_space M] :
(ι → M) ≃L[R] M

If ι has a unique element, then ι → M is continuously linear equivalent to M.

Equations
source
@[simp]
theorem continuous_linear_equiv.coe_fun_unique {ι : Type u_1} {R : Type u_2} {M : Type u_3} [unique ι] [semiring R] [add_comm_monoid M] [module R M] [topological_space M] :
⇑(continuous_linear_equiv.fun_unique ι R M) = function.eval inhabited.default
source
@[simp]
theorem continuous_linear_equiv.coe_fun_unique_symm {ι : Type u_1} {R : Type u_2} {M : Type u_3} [unique ι] [semiring R] [add_comm_monoid M] [module R M] [topological_space M] :
⇑((continuous_linear_equiv.fun_unique ι R M).symm) = function.const ι
source
@[simp]
theorem continuous_linear_equiv.pi_fin_two_apply (R : Type u_2) [semiring R] (M : fin 2 → Type u_1) [Π (i : fin 2), add_comm_monoid (M i)] [Π (i : fin 2), module R (M i)] [Π (i : fin 2), topological_space (M i)] :
⇑(continuous_linear_equiv.pi_fin_two R M) = λ (f : Π (i : fin 2), M i), (f 0, f 1)
source
@[simp]
theorem continuous_linear_equiv.pi_fin_two_to_linear_equiv (R : Type u_2) [semiring R] (M : fin 2 → Type u_1) [Π (i : fin 2), add_comm_monoid (M i)] [Π (i : fin 2), module R (M i)] [Π (i : fin 2), topological_space (M i)] :
(continuous_linear_equiv.pi_fin_two R M).to_linear_equiv = linear_equiv.pi_fin_two R M
source
@[simp]
theorem continuous_linear_equiv.pi_fin_two_symm_apply (R : Type u_2) [semiring R] (M : fin 2 → Type u_1) [Π (i : fin 2), add_comm_monoid (M i)] [Π (i : fin 2), module R (M i)] [Π (i : fin 2), topological_space (M i)] :
⇑((continuous_linear_equiv.pi_fin_two R M).symm) = λ (p : M 0 × M 1), fin.cons p.fst (fin.cons p.snd fin_zero_elim)
source
def continuous_linear_equiv.pi_fin_two (R : Type u_2) [semiring R] (M : fin 2 → Type u_1) [Π (i : fin 2), add_comm_monoid (M i)] [Π (i : fin 2), module R (M i)] [Π (i : fin 2), topological_space (M i)] :
(Π (i : fin 2), M i) ≃L[R] M 0 × M 1

Continuous linear equivalence between dependent functions Π i : fin 2, M i and M 0 × M 1.

Equations
source
@[simp]
theorem continuous_linear_equiv.fin_two_arrow_to_linear_equiv (R : Type u_2) (M : Type u_3) [semiring R] [add_comm_monoid M] [module R M] [topological_space M] :
(continuous_linear_equiv.fin_two_arrow R M).to_linear_equiv = linear_equiv.fin_two_arrow R M
source
@[simp]
theorem continuous_linear_equiv.fin_two_arrow_apply (R : Type u_2) (M : Type u_3) [semiring R] [add_comm_monoid M] [module R M] [topological_space M] :
⇑(continuous_linear_equiv.fin_two_arrow R M) = λ (f : fin 2 → M), (f 0, f 1)
source
@[simp]
theorem continuous_linear_equiv.fin_two_arrow_symm_apply (R : Type u_2) (M : Type u_3) [semiring R] [add_comm_monoid M] [module R M] [topological_space M] :
⇑((continuous_linear_equiv.fin_two_arrow R M).symm) = λ (x : M × M), ![x.fst, x.snd]
source
def continuous_linear_equiv.fin_two_arrow (R : Type u_2) (M : Type u_3) [semiring R] [add_comm_monoid M] [module R M] [topological_space M] :
(fin 2 → M) ≃L[R] M × M

Continuous linear equivalence between vectors in M² = fin 2 → M and M × M.

Equations
source
noncomputable def continuous_linear_map.inverse {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [topological_space M] [topological_space M₂] [semiring R] [add_comm_monoid M₂] [module R M₂] [add_comm_monoid M] [module R M] :
(M →L[R] M₂) → (M₂ →L[R] M)

Introduce a function inverse from M →L[R] M₂ to M₂ →L[R] M, which sends f to f.symm if f is a continuous linear equivalence and to 0 otherwise. This definition is somewhat ad hoc, but one needs a fully (rather than partially) defined inverse function for some purposes, including for calculus.

Equations
source
@[simp]
theorem continuous_linear_map.inverse_equiv {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [topological_space M] [topological_space M₂] [semiring R] [add_comm_monoid M₂] [module R M₂] [add_comm_monoid M] [module R M] (e : M ≃L[R] M₂) :
↑e.inverse = ↑(e.symm)

By definition, if f is invertible then inverse f = f.symm.

source
@[simp]
theorem continuous_linear_map.inverse_non_equiv {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [topological_space M] [topological_space M₂] [semiring R] [add_comm_monoid M₂] [module R M₂] [add_comm_monoid M] [module R M] (f : M →L[R] M₂) (h : ¬∃ (e' : M ≃L[R] M₂), ↑e' = f) :
f.inverse = 0

By definition, if f is not invertible then inverse f = 0.

source
@[simp]
theorem continuous_linear_map.ring_inverse_equiv {R : Type u_1} {M : Type u_2} [topological_space M] [ring R] [add_comm_group M] [topological_add_group M] [module R M] (e : M ≃L[R] M) :
ring.inverse ↑e = ↑e.inverse
source
theorem continuous_linear_map.to_ring_inverse {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [topological_space M] [topological_space M₂] [ring R] [add_comm_group M] [topological_add_group M] [module R M] [add_comm_group M₂] [module R M₂] (e : M ≃L[R] M₂) (f : M →L[R] M₂) :
f.inverse = (ring.inverse (↑(e.symm).comp f)).comp ↑(e.symm)

The function continuous_linear_equiv.inverse can be written in terms of ring.inverse for the ring of self-maps of the domain.

source
theorem continuous_linear_map.ring_inverse_eq_map_inverse {R : Type u_1} {M : Type u_2} [topological_space M] [ring R] [add_comm_group M] [topological_add_group M] [module R M] :
ring.inverse = continuous_linear_map.inverse
source
def submodule.closed_complemented {R : Type u_1} [ring R] {M : Type u_2} [topological_space M] [add_comm_group M] [module R M] (p : submodule R M) :
Prop

A submodule p is called complemented if there exists a continuous projection M →ₗ[R] p.

Equations
source
theorem submodule.closed_complemented.has_closed_complement {R : Type u_1} [ring R] {M : Type u_2} [topological_space M] [add_comm_group M] [module R M] {p : submodule R M} [t1_space ↥p] (h : p.closed_complemented) :
∃ (q : submodule R M) (hq : is_closed ↑q), is_compl p q
source
@[protected]
theorem submodule.closed_complemented.is_closed {R : Type u_1} [ring R] {M : Type u_2} [topological_space M] [add_comm_group M] [module R M] [topological_add_group M] [t1_space M] {p : submodule R M} (h : p.closed_complemented) :
is_closed ↑p
source
@[simp]
theorem submodule.closed_complemented_bot {R : Type u_1} [ring R] {M : Type u_2} [topological_space M] [add_comm_group M] [module R M] :
⊥.closed_complemented
source
@[simp]
theorem submodule.closed_complemented_top {R : Type u_1} [ring R] {M : Type u_2} [topological_space M] [add_comm_group M] [module R M] :
⊤.closed_complemented
source
theorem continuous_linear_map.closed_complemented_ker_of_right_inverse {R : Type u_1} [ring R] {M : Type u_2} [topological_space M] [add_comm_group M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [module R M] [module R M₂] [topological_add_group M] (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) (h : function.right_inverse ⇑f₂ ⇑f₁) :
(linear_map.ker f₁).closed_complemented
source
theorem submodule.is_open_map_mkq {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] [topological_space M] (S : submodule R M) [topological_add_group M] :
is_open_map ⇑(S.mkq)
source
@[protected, instance]
def submodule.topological_add_group_quotient {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] [topological_space M] (S : submodule R M) [topological_add_group M] :
topological_add_group (M ⧸ S)
source
@[protected, instance]
def submodule.has_continuous_smul_quotient {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] [topological_space M] (S : submodule R M) [topological_space R] [topological_add_group M] [has_continuous_smul R M] :
has_continuous_smul R (M ⧸ S)
source
@[protected, instance]
def submodule.t3_quotient_of_is_closed {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] [topological_space M] (S : submodule R M) [topological_add_group M] [is_closed ↑S] :
t3_space (M ⧸ S)