mathlib3 documentation

topology.algebra.module.basic

Theory of topological modules and continuous linear maps. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We use the class has_continuous_smul for topological (semi) modules and topological vector spaces.

In this file we define continuous (semi-)linear maps, as semilinear maps between topological modules which are continuous. The set of continuous semilinear maps between the topological R₁-module M and R₂-module M₂ with respect to the ring_hom σ is denoted by M →SL[σ] M₂. Plain linear maps are denoted by M →L[R] M₂ and star-linear maps by M →L⋆[R] M₂.

The corresponding notation for equivalences is M ≃SL[σ] M₂, M ≃L[R] M₂ and M ≃L⋆[R] M₂.

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

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

Let R be a topological ring such that zero is not an isolated point (e.g., a nontrivially normed field, see normed_field.punctured_nhds_ne_bot). Let M be a nontrivial module over R such that c • x = 0 implies c = 0 ∨ x = 0. Then M has no isolated points. We formulate this using ne_bot (𝓝[≠] x).

This lemma is not an instance because Lean would need to find [has_continuous_smul ?m_1 M] with unknown ?m_1. We register this as an instance for R = ℝ in real.punctured_nhds_module_ne_bot. One can also use haveI := module.punctured_nhds_ne_bot R M in a proof.

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

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

Equations
Instances for submodule.topological_closure

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

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

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

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

Continuous linear maps between modules. We only put the type classes that are necessary for the definition, although in applications M and M₂ will be topological modules over the topological ring R.

Instances for continuous_linear_map
@[class]
structure continuous_semilinear_map_class (F : Type u_1) {R : out_param (Type u_2)} {S : out_param (Type u_3)} [semiring R] [semiring S] (σ : out_param (R →+* S)) (M : out_param (Type u_4)) [topological_space M] [add_comm_monoid M] (M₂ : out_param (Type u_5)) [topological_space M₂] [add_comm_monoid M₂] [module R M] [module S M₂] :
Type (max u_1 u_4 u_5)

continuous_semilinear_map_class F σ M M₂ asserts F is a type of bundled continuous σ-semilinear maps M → M₂. See also continuous_linear_map_class F R M M₂ for the case where σ is the identity map on R. A map f between an R-module and an S-module over a ring homomorphism σ : R →+* S is semilinear if it satisfies the two properties f (x + y) = f x + f y and f (c • x) = (σ c) • f x.

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

continuous_linear_map_class F R M M₂ asserts F is a type of bundled continuous R-linear maps M → M₂. This is an abbreviation for continuous_semilinear_map_class F (ring_hom.id R) M M₂.

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

Continuous linear equivalences between modules. We only put the type classes that are necessary for the definition, although in applications M and M₂ will be topological modules over the topological semiring R.

Instances for continuous_linear_equiv
@[class]
structure continuous_semilinear_equiv_class (F : Type u_1) {R : out_param (Type u_2)} {S : out_param (Type u_3)} [semiring R] [semiring S] (σ : out_param (R →+* S)) {σ' : out_param (S →+* R)} [ring_hom_inv_pair σ σ'] [ring_hom_inv_pair σ' σ] (M : out_param (Type u_4)) [topological_space M] [add_comm_monoid M] (M₂ : out_param (Type u_5)) [topological_space M₂] [add_comm_monoid M₂] [module R M] [module S M₂] :
Type (max u_1 u_4 u_5)

continuous_semilinear_equiv_class F σ M M₂ asserts F is a type of bundled continuous σ-semilinear equivs M → M₂. See also continuous_linear_equiv_class F R M M₂ for the case where σ is the identity map on R. A map f between an R-module and an S-module over a ring homomorphism σ : R →+* S is semilinear if it satisfies the two properties f (x + y) = f x + f y and f (c • x) = (σ c) • f x.

Instances of this typeclass
Instances of other typeclasses for continuous_semilinear_equiv_class
  • continuous_semilinear_equiv_class.has_sizeof_inst
@[instance]
def continuous_semilinear_equiv_class.to_semilinear_equiv_class (F : Type u_1) {R : out_param (Type u_2)} {S : out_param (Type u_3)} [semiring R] [semiring S] (σ : out_param (R →+* S)) {σ' : out_param (S →+* R)} [ring_hom_inv_pair σ σ'] [ring_hom_inv_pair σ' σ] (M : out_param (Type u_4)) [topological_space M] [add_comm_monoid M] (M₂ : out_param (Type u_5)) [topological_space M₂] [add_comm_monoid M₂] [module R M] [module S M₂] [self : continuous_semilinear_equiv_class F σ M M₂] :
@[reducible]
def continuous_linear_equiv_class (F : Type u_1) (R : out_param (Type u_2)) [semiring R] (M : out_param (Type u_3)) [topological_space M] [add_comm_monoid M] (M₂ : out_param (Type u_4)) [topological_space M₂] [add_comm_monoid M₂] [module R M] [module R M₂] :
Type (max u_1 u_3 u_4)

continuous_linear_equiv_class F σ M M₂ asserts F is a type of bundled continuous R-linear equivs M → M₂. This is an abbreviation for continuous_semilinear_equiv_class F (ring_hom.id) M M₂.

theorem is_closed_set_of_map_smul (M₁ : Type u_1) (M₂ : Type u_2) {R : Type u_4} {S : Type u_5} [topological_space M₂] [t2_space M₂] [semiring R] [semiring S] [add_comm_monoid M₁] [add_comm_monoid M₂] [module R M₁] [module S M₂] [has_continuous_const_smul S M₂] (σ : R →+* S) :
is_closed {f : M₁ M₂ | (c : R) (x : M₁), f (c x) = σ c f x}
@[simp]
theorem linear_map_of_mem_closure_range_coe_apply {M₁ : Type u_1} {M₂ : Type u_2} {R : Type u_4} {S : Type u_5} [topological_space M₂] [t2_space M₂] [semiring R] [semiring S] [add_comm_monoid M₁] [add_comm_monoid M₂] [module R M₁] [module S M₂] [has_continuous_const_smul S M₂] [has_continuous_add M₂] {σ : R →+* S} (f : M₁ M₂) (hf : f closure (set.range coe_fn)) :
def linear_map_of_mem_closure_range_coe {M₁ : Type u_1} {M₂ : Type u_2} {R : Type u_4} {S : Type u_5} [topological_space M₂] [t2_space M₂] [semiring R] [semiring S] [add_comm_monoid M₁] [add_comm_monoid M₂] [module R M₁] [module S M₂] [has_continuous_const_smul S M₂] [has_continuous_add M₂] {σ : R →+* S} (f : M₁ M₂) (hf : f closure (set.range coe_fn)) :
M₁ →ₛₗ[σ] M₂

Constructs a bundled linear map from a function and a proof that this function belongs to the closure of the set of linear maps.

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

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

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

Properties that hold for non-necessarily commutative semirings. #

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

Coerce continuous linear maps to linear maps.

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

Coerce continuous linear maps to functions.

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

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

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

See Note [custom simps projection].

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

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

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

If two continuous linear maps are equal on a set s, then they are equal on the closure of the submodule.span of this set.

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

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

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

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

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

Under a dense continuous linear map, a submodule whose topological_closure is is sent to another such submodule. That is, the image of a dense set under a map with dense range is dense.

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

The continuous map that is constantly zero.

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

the identity map as a continuous linear map.

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

Composition of bounded linear maps.

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

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

This generalizes function.End.apply_mul_action.

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

continuous_linear_map.apply_module is faithful.

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

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

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

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

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

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

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

Restrict codomain of a continuous linear map.

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

submodule.subtype as a continuous_linear_map.

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

prod.fst as a continuous_linear_map.

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

prod.snd as a continuous_linear_map.

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

prod.map of two continuous linear maps.

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

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

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

The linear map λ x, c x • f. Associates to a scalar-valued linear map and an element of M₂ the M₂-valued linear map obtained by multiplying the two (a.k.a. tensoring by M₂). See also continuous_linear_map.smul_rightₗ and continuous_linear_map.smul_rightL.

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

Given an element x of a topological space M over a semiring R, the natural continuous linear map from R to M by taking multiples of x.

Equations
theorem continuous_linear_map.to_span_singleton_apply (R₁ : Type u_1) [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] [module R₁ M₁] [topological_space R₁] [has_continuous_smul R₁ M₁] (x : M₁) (r : R₁) :
theorem continuous_linear_map.to_span_singleton_smul' (R₁ : Type u_1) [semiring R₁] {M₁ : Type u_4} [topological_space M₁] [add_comm_monoid M₁] [module R₁ M₁] [topological_space R₁] [has_continuous_smul R₁ M₁] {α : Type u_2} [monoid α] [distrib_mul_action α M₁] [has_continuous_const_smul α M₁] [smul_comm_class R₁ α M₁] (c : α) (x : M₁) :

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

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

pi construction for continuous linear functions. From a family of continuous linear functions it produces a continuous linear function into a family of topological modules.

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

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

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

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

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

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
@[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)
@[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₁)) :
@[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
@[protected]

A nonzero continuous linear functional is open.

@[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
@[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ₗ
@[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
@[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
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
@[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₃)) :
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₃} :
@[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
@[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
@[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₃)
@[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₃)) :
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
@[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₃) :
@[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₃) :
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
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
@[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) :
@[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
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
@[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₂) :
@[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₂) :
@[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] :
@[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₂) :
@[simp]
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
@[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
@[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
@[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
@[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₂) :
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
@[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₂) :
@[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₂) :
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₂] :
@[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
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₂] :
@[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'
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
@[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₂) :
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₁) :
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₂) :
@[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₁} :
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₁) :
@[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
@[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
@[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
@[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
@[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
@[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₂) :
@[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₁} :
@[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₁} :
@[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₁} :
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 α} :
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₁} :
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.

@[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
@[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₁] :
@[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₁] :
@[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
@[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₂) :
@[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₂) :
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
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
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₁) :
@[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
@[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₃) :
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
@[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)
@[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₄) :
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
@[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₂) :
@[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₂) :
@[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₂) :
@[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)
@[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
@[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
@[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)
@[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
@[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
@[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')
@[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₂) :
@[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₂) :
@[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₂) :
@[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₂) :
@[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
@[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₁] :
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
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
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
@[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
@[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
@[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₂) :
@[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₁) :
@[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₂) :
@[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)) :
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
@[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
@[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₁) :
@[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
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
@[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₁₂)
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
@[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))
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
@[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)
@[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)))
@[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
@[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.

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

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

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

Equations
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
@[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) :
@[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) :
@[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₁)) :
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
@[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)
@[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)] :
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
@[simp]

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

Equations
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
@[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₂) :

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

@[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) :

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

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₂) :

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

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
@[protected, instance]
@[protected, instance]