mathlib documentation

topology.algebra.module

Theory of topological modules and continuous linear maps.

We define classes topological_semimodule, topological_module and topological_vector_spaces, as extensions of the corresponding algebraic classes where the algebraic operations are continuous.

We also define continuous linear maps, as linear maps between topological modules which are continuous. The set of continuous linear maps between the topological R-modules M and M₂ is denoted by M →L[R] M₂.

Continuous linear equivalences are denoted by M ≃L[R] M₂.

Implementation notes

Topological vector spaces are defined as an abbreviation for topological modules, if the base ring is a field. This has as advantage that topological vector spaces are completely transparent for type class inference, which means that all instances for topological modules are immediately picked up for vector spaces as well. A cosmetic disadvantage is that one can not extend topological vector spaces. The solution is to extend topological_module instead.

@[class]
structure topological_semimodule (R : Type u) (M : Type v) [semiring R] [topological_space R] [topological_space M] [add_comm_monoid M] [semimodule R M] :
Prop

A topological semimodule, over a semiring which is also a topological space, is a semimodule in which scalar multiplication is continuous. In applications, R will be a topological semiring and M a topological additive semigroup, but this is not needed for the definition

Instances
theorem continuous_smul {R : Type u} {M : Type v} [semiring R] [topological_space R] [topological_space M] [add_comm_monoid M] [semimodule R M] [topological_semimodule R M] :
continuous (λ (p : R × M), p.fst p.snd)

theorem continuous.smul {R : Type u} {M : Type v} [semiring R] [topological_space R] [topological_space M] [add_comm_monoid M] [semimodule R M] [topological_semimodule R M] {α : Type u_1} [topological_space α] {f : α → R} {g : α → M} :
continuous fcontinuous gcontinuous (λ (p : α), f p g p)

theorem tendsto_smul {R : Type u} {M : Type v} [semiring R] [topological_space R] [topological_space M] [add_comm_monoid M] [semimodule R M] [topological_semimodule R M] {c : R} {x : M} :
filter.tendsto (λ (p : R × M), p.fst p.snd) (𝓝 (c, x)) (𝓝 (c x))

theorem filter.tendsto.smul {R : Type u} {M : Type v} [semiring R] [topological_space R] [topological_space M] [add_comm_monoid M] [semimodule R M] [topological_semimodule R M] {α : Type u_1} {l : filter α} {f : α → R} {g : α → M} {c : R} {x : M} :
filter.tendsto f l (𝓝 c)filter.tendsto g l (𝓝 x)filter.tendsto (λ (a : α), f a g a) l (𝓝 (c x))

def topological_module (R : Type u) (M : Type v) [ring R] [topological_space R] [topological_space M] [add_comm_group M] [module R M] :
Prop

A topological module, over a ring which is also a topological space, is a module in which scalar multiplication is continuous. In applications, R will be a topological ring and M a topological additive group, but this is not needed for the definition

Instances
def topological_vector_space (R : Type u) (M : Type v) [field R] [topological_space R] [topological_space M] [add_comm_group M] [module R M] :
Prop

A topological vector space is a topological module over a field.

Instances
def homeomorph.smul_of_unit {R : Type u_1} {M : Type u_2} [ring R] [topological_space R] [topological_space M] [add_comm_group M] [module R M] [topological_module R M] :
units RM ≃ₜ M

Scalar multiplication by a unit is a homeomorphism from a topological module onto itself.

Equations
theorem is_open_map_smul_of_unit {R : Type u_1} {M : Type u_2} [ring R] [topological_space R] [topological_space M] [add_comm_group M] [module R M] [topological_module R M] (a : units R) :
is_open_map (λ (x : M), a x)

theorem is_closed_map_smul_of_unit {R : Type u_1} {M : Type u_2} [ring R] [topological_space R] [topological_space M] [add_comm_group M] [module R M] [topological_module R M] (a : units R) :
is_closed_map (λ (x : M), a x)

theorem submodule.eq_top_of_nonempty_interior' {R : Type u_1} {M : Type u_2} [ring R] [topological_space R] [topological_space M] [add_comm_group M] [module R M] [topological_module R M] [has_continuous_add M] [(𝓝[{x : R | is_unit x}] 0).ne_bot] (s : submodule R M) :

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 nondiscrete normed field.

def homeomorph.smul_of_ne_zero {R : Type u_1} {M : Type u_2} {a : R} [field R] [topological_space R] [topological_space M] [add_comm_group M] [vector_space R M] [topological_vector_space R M] :
a 0M ≃ₜ M

Scalar multiplication by a non-zero field element is a homeomorphism from a topological vector space onto itself.

Equations
theorem is_open_map_smul_of_ne_zero {R : Type u_1} {M : Type u_2} {a : R} [field R] [topological_space R] [topological_space M] [add_comm_group M] [vector_space R M] [topological_vector_space R M] :
a 0is_open_map (λ (x : M), a x)

theorem is_closed_map_smul_of_ne_zero {R : Type u_1} {M : Type u_2} {a : R} [field R] [topological_space R] [topological_space M] [add_comm_group M] [vector_space R M] [topological_vector_space R M] :
a 0is_closed_map (λ (x : M), a x)

smul is a closed map in the second argument.

The lemma that smul is a closed map in the first argument (for a normed space over a complete normed field) is is_closed_map_smul_left in analysis.normed_space.finite_dimension.

structure continuous_linear_map (R : Type u_1) [semiring R] (M : Type u_2) [topological_space M] [add_comm_monoid M] (M₂ : Type u_3) [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :
Type (max u_2 u_3)

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.

@[nolint]
structure continuous_linear_equiv (R : Type u_1) [semiring R] (M : Type u_2) [topological_space M] [add_comm_monoid M] (M₂ : Type u_3) [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :
Type (max u_2 u_3)

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 ring R.

Properties that hold for non-necessarily commutative semirings.

@[instance]
def continuous_linear_map.linear_map.has_coe {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :
has_coe (M →L[R] M₂) (M →ₗ[R] M₂)

Coerce continuous linear maps to linear maps.

Equations
@[instance]
def continuous_linear_map.to_fun {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :

Coerce continuous linear maps to functions.

Equations
@[simp]
theorem continuous_linear_map.coe_mk {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M →ₗ[R] 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} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M →ₗ[R] M₂) (h : continuous f.to_fun . "continuity'") :

theorem continuous_linear_map.continuous {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M →L[R] M₂) :

theorem continuous_linear_map.coe_injective {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :

theorem continuous_linear_map.injective_coe_fn {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :
function.injective (λ (f : M →L[R] M₂), show M → M₂, from f)

@[ext]
theorem continuous_linear_map.ext {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {f g : M →L[R] M₂} :
(∀ (x : M), f x = g x)f = g

theorem continuous_linear_map.ext_iff {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {f g : M →L[R] M₂} :
f = g ∀ (x : M), f x = g x

@[simp]
theorem continuous_linear_map.map_zero {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M →L[R] M₂) :
f 0 = 0

@[simp]
theorem continuous_linear_map.map_add {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M →L[R] M₂) (x y : M) :
f (x + y) = f x + f y

@[simp]
theorem continuous_linear_map.map_smul {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (c : R) (f : M →L[R] M₂) (x : M) :
f (c x) = c f x

theorem continuous_linear_map.map_sum {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M →L[R] M₂) {ι : Type u_4} (s : finset ι) (g : ι → M) :
f (∑ (i : ι) in s, g i) = ∑ (i : ι) in s, f (g i)

@[simp]
theorem continuous_linear_map.coe_coe {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M →L[R] M₂) :

theorem continuous_linear_map.eq_on_closure_span {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] [t2_space M₂] {s : set M} {f g : M →L[R] M₂} :

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} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] [t2_space M₂] {s : set M} (hs : dense (submodule.span R s)) {f g : M →L[R] M₂} :
set.eq_on f g sf = g

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

@[instance]
def continuous_linear_map.has_zero {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :
has_zero (M →L[R] M₂)

The continuous map that is constantly zero.

Equations
@[instance]
def continuous_linear_map.inhabited {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :
inhabited (M →L[R] M₂)

Equations
@[simp]
theorem continuous_linear_map.default_def {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :
default (M →L[R] M₂) = 0

@[simp]
theorem continuous_linear_map.zero_apply {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (x : M) :
0 x = 0

@[simp]
theorem continuous_linear_map.coe_zero {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :
0 = 0

theorem continuous_linear_map.coe_zero' {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :
0 = 0

def continuous_linear_map.id (R : Type u_1) [semiring R] (M : Type u_2) [topological_space M] [add_comm_monoid M] [semimodule R M] :
M →L[R] M

the identity map as a continuous linear map.

Equations
@[instance]
def continuous_linear_map.has_one {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] [semimodule R M] :

Equations
theorem continuous_linear_map.id_apply {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] [semimodule R M] (x : M) :

@[simp]
theorem continuous_linear_map.coe_id' {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] [semimodule R M] :

@[simp]
theorem continuous_linear_map.one_apply {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] [semimodule R M] (x : M) :
1 x = x

@[instance]
def continuous_linear_map.has_add {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] [has_continuous_add M₂] :
has_add (M →L[R] M₂)

Equations
@[simp]
theorem continuous_linear_map.add_apply {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f g : M →L[R] M₂) (x : M) [has_continuous_add M₂] :
(f + g) x = f x + g x

@[simp]
theorem continuous_linear_map.coe_add {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f g : M →L[R] M₂) [has_continuous_add M₂] :
(f + g) = f + g

theorem continuous_linear_map.coe_add' {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f g : M →L[R] M₂) [has_continuous_add M₂] :
(f + g) = f + g

theorem continuous_linear_map.sum_apply {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] [has_continuous_add M₂] {ι : Type u_4} (t : finset ι) (f : ι → (M →L[R] M₂)) (b : M) :
(∑ (d : ι) in t, f d) b = ∑ (d : ι) in t, (f d) b

def continuous_linear_map.comp {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] :
(M₂ →L[R] M₃)(M →L[R] M₂)(M →L[R] M₃)

Composition of bounded linear maps.

Equations
@[simp]
theorem continuous_linear_map.coe_comp {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] (f : M →L[R] M₂) (h : M₂ →L[R] M₃) :
(h.comp f) = h.comp f

@[simp]
theorem continuous_linear_map.coe_comp' {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] (f : M →L[R] M₂) (h : M₂ →L[R] M₃) :
(h.comp f) = h f

@[simp]
theorem continuous_linear_map.comp_id {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M →L[R] M₂) :

@[simp]
theorem continuous_linear_map.id_comp {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M →L[R] M₂) :

@[simp]
theorem continuous_linear_map.comp_zero {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] (f : M →L[R] M₂) :
f.comp 0 = 0

@[simp]
theorem continuous_linear_map.zero_comp {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] (f : M →L[R] M₂) :
0.comp f = 0

@[simp]
theorem continuous_linear_map.comp_add {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] [has_continuous_add M₂] [has_continuous_add M₃] (g : M₂ →L[R] M₃) (f₁ f₂ : M →L[R] M₂) :
g.comp (f₁ + f₂) = g.comp f₁ + g.comp f₂

@[simp]
theorem continuous_linear_map.add_comp {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] [has_continuous_add M₃] (g₁ g₂ : M₂ →L[R] M₃) (f : M →L[R] M₂) :
(g₁ + g₂).comp f = g₁.comp f + g₂.comp f

theorem continuous_linear_map.comp_assoc {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] {M₄ : Type u_5} [topological_space M₄] [add_comm_monoid M₄] [semimodule R M] [semimodule R M₂] [semimodule R M₃] [semimodule R M₄] (h : M₃ →L[R] M₄) (g : M₂ →L[R] M₃) (f : M →L[R] M₂) :
(h.comp g).comp f = h.comp (g.comp f)

@[instance]
def continuous_linear_map.has_mul {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] [semimodule R M] :

Equations
theorem continuous_linear_map.mul_def {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] [semimodule 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_2} [topological_space M] [add_comm_monoid M] [semimodule 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_2} [topological_space M] [add_comm_monoid M] [semimodule R M] (f g : M →L[R] M) (x : M) :
(f * g) x = f (g x)

def continuous_linear_map.prod {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] :
(M →L[R] M₂)(M →L[R] M₃)(M →L[R] M₂ × M₃)

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

Equations
@[simp]
theorem continuous_linear_map.coe_prod {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] (f₁ : M →L[R] M₂) (f₂ : M →L[R] M₃) :
(f₁.prod f₂) = f₁.prod f₂

@[simp]
theorem continuous_linear_map.prod_apply {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule 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.ker {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :
(M →L[R] M₂)submodule R M

Kernel of a continuous linear map.

Equations
theorem continuous_linear_map.ker_coe {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M →L[R] M₂) :

@[simp]
theorem continuous_linear_map.mem_ker {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {f : M →L[R] M₂} {x : M} :
x f.ker f x = 0

theorem continuous_linear_map.is_closed_ker {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M →L[R] M₂) [t1_space M₂] :

@[simp]
theorem continuous_linear_map.apply_ker {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M →L[R] M₂) (x : (f.ker)) :
f x = 0

theorem continuous_linear_map.is_complete_ker {R : Type u_1} [semiring R] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M₂] {M' : Type u_2} [uniform_space M'] [complete_space M'] [add_comm_monoid M'] [semimodule R M'] [t1_space M₂] (f : M' →L[R] M₂) :

@[instance]
def continuous_linear_map.complete_space_ker {R : Type u_1} [semiring R] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M₂] {M' : Type u_2} [uniform_space M'] [complete_space M'] [add_comm_monoid M'] [semimodule R M'] [t1_space M₂] (f : M' →L[R] M₂) :

@[simp]
theorem continuous_linear_map.ker_prod {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] (f : M →L[R] M₂) (g : M →L[R] M₃) :
(f.prod g).ker = f.ker g.ker

def continuous_linear_map.range {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :
(M →L[R] M₂)submodule R M₂

Range of a continuous linear map.

Equations
theorem continuous_linear_map.range_coe {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M →L[R] M₂) :

theorem continuous_linear_map.mem_range {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {f : M →L[R] M₂} {y : M₂} :
y f.range ∃ (x : M), f x = y

theorem continuous_linear_map.range_prod_le {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] (f : M →L[R] M₂) (g : M →L[R] M₃) :

def continuous_linear_map.cod_restrict {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M →L[R] M₂) (p : submodule R M₂) :
(∀ (x : M), f x p)(M →L[R] p)

Restrict codomain of a continuous linear map.

Equations
theorem continuous_linear_map.coe_cod_restrict {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M →L[R] M₂) (p : submodule R M₂) (h : ∀ (x : M), f x p) :

@[simp]
theorem continuous_linear_map.coe_cod_restrict_apply {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M →L[R] 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} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M →L[R] M₂) (p : submodule R M₂) (h : ∀ (x : M), f x p) :
(f.cod_restrict p h).ker = f.ker

def continuous_linear_map.subtype_val {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] [semimodule R M] (p : submodule R M) :

Embedding of a submodule into the ambient space as a continuous linear map.

Equations
@[simp]
theorem continuous_linear_map.subtype_val_apply {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] [semimodule R M] (p : submodule R M) (x : p) :

def continuous_linear_map.fst (R : Type u_1) [semiring R] (M : Type u_2) [topological_space M] [add_comm_monoid M] (M₂ : Type u_3) [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule 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_2) [topological_space M] [add_comm_monoid M] (M₂ : Type u_3) [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :
M × M₂ →L[R] M₂

prod.snd as a continuous_linear_map.

Equations
@[simp]
theorem continuous_linear_map.coe_fst {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :

@[simp]
theorem continuous_linear_map.coe_fst' {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :

@[simp]
theorem continuous_linear_map.coe_snd {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :

@[simp]
theorem continuous_linear_map.coe_snd' {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :

@[simp]
theorem continuous_linear_map.fst_prod_snd {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :

def continuous_linear_map.prod_map {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] {M₄ : Type u_5} [topological_space M₄] [add_comm_monoid M₄] [semimodule R M] [semimodule R M₂] [semimodule R M₃] [semimodule R M₄] :
(M →L[R] M₂)(M₃ →L[R] M₄)(M × M₃ →L[R] M₂ × M₄)

prod.map of two continuous linear maps.

Equations
@[simp]
theorem continuous_linear_map.coe_prod_map {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] {M₄ : Type u_5} [topological_space M₄] [add_comm_monoid M₄] [semimodule R M] [semimodule R M₂] [semimodule R M₃] [semimodule R M₄] (f₁ : M →L[R] M₂) (f₂ : M₃ →L[R] M₄) :
(f₁.prod_map f₂) = f₁.prod_map f₂

@[simp]
theorem continuous_linear_map.coe_prod_map' {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] {M₄ : Type u_5} [topological_space M₄] [add_comm_monoid M₄] [semimodule R M] [semimodule R M₂] [semimodule R M₃] [semimodule 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_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] [has_continuous_add M₃] :
(M →L[R] M₃)(M₂ →L[R] M₃)(M × M₂ →L[R] M₃)

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

Equations
@[simp]
theorem continuous_linear_map.coe_coprod {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule 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_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule 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

def continuous_linear_map.smul_right {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] [topological_space R] [topological_semimodule R M₂] :
(M →L[R] R)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 {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] [topological_space R] [topological_semimodule R M₂] {c : M →L[R] R} {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_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M₂] [topological_space R] [topological_semimodule 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_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M₂] [topological_space R] [topological_semimodule 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_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M₂] [topological_space R] [topological_semimodule R M₂] [topological_semimodule R R] {x : M₂} {c : R} :

def continuous_linear_map.pi {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] [semimodule R M] {ι : Type u_4} {φ : ι → Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), semimodule R (φ i)] :
(Π (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.pi_apply {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] [semimodule R M] {ι : Type u_4} {φ : ι → Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), semimodule 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] [semimodule R M] {ι : Type u_4} {φ : ι → Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), semimodule 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] [semimodule R M] {ι : Type u_4} {φ : ι → Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), semimodule 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] [semimodule R M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M₂] {ι : Type u_4} {φ : ι → Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), semimodule 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 : ι), semimodule 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 : ι), semimodule 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₂] [semimodule R M₂] {ι : Type u_4} {φ : ι → Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), semimodule 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 : ι), semimodule R (φ i)] :
(⨅ (i : ι), (continuous_linear_map.proj i).ker) =

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 : ι), semimodule R (φ i)] {I J : set ι} [decidable_pred (λ (i : ι), i I)] :
disjoint I Jset.univ I J((⨅ (i : ι) (H : i J), (continuous_linear_map.proj i).ker) ≃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
@[simp]
theorem continuous_linear_map.map_neg {R : Type u_1} [ring R] {M : Type u_2} [topological_space M] [add_comm_group M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [semimodule R M] [semimodule R M₂] (f : M →L[R] M₂) (x : M) :
f (-x) = -f x

@[simp]
theorem continuous_linear_map.map_sub {R : Type u_1} [ring R] {M : Type u_2} [topological_space M] [add_comm_group M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [semimodule R M] [semimodule R M₂] (f : M →L[R] M₂) (x y : M) :
f (x - y) = f x - f y

@[simp]
theorem continuous_linear_map.sub_apply' {R : Type u_1} [ring R] {M : Type u_2} [topological_space M] [add_comm_group M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [semimodule R M] [semimodule R M₂] (f g : M →L[R] 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_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₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] {f : M →L[R] M₂} {g : M →L[R] M₃} :
f.ker g.ker = (f.prod g).range = f.range.prod g.range

@[instance]
def continuous_linear_map.has_neg {R : Type u_1} [ring R] {M : Type u_2} [topological_space M] [add_comm_group M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [semimodule R M] [semimodule R M₂] [topological_add_group M₂] :
has_neg (M →L[R] M₂)

Equations
@[simp]
theorem continuous_linear_map.neg_apply {R : Type u_1} [ring R] {M : Type u_2} [topological_space M] [add_comm_group M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [semimodule R M] [semimodule R M₂] (f : M →L[R] M₂) (x : M) [topological_add_group M₂] :
(-f) x = -f x

@[simp]
theorem continuous_linear_map.coe_neg {R : Type u_1} [ring R] {M : Type u_2} [topological_space M] [add_comm_group M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [semimodule R M] [semimodule R M₂] (f : M →L[R] M₂) [topological_add_group M₂] :

theorem continuous_linear_map.coe_neg' {R : Type u_1} [ring R] {M : Type u_2} [topological_space M] [add_comm_group M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [semimodule R M] [semimodule R M₂] (f : M →L[R] M₂) [topological_add_group M₂] :

theorem continuous_linear_map.sub_apply {R : Type u_1} [ring R] {M : Type u_2} [topological_space M] [add_comm_group M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [semimodule R M] [semimodule R M₂] (f g : M →L[R] M₂) [topological_add_group M₂] (x : M) :
(f - g) x = f x - g x

@[simp]
theorem continuous_linear_map.coe_sub {R : Type u_1} [ring R] {M : Type u_2} [topological_space M] [add_comm_group M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [semimodule R M] [semimodule R M₂] (f g : M →L[R] M₂) [topological_add_group M₂] :
(f - g) = f - g

@[simp]
theorem continuous_linear_map.coe_sub' {R : Type u_1} [ring R] {M : Type u_2} [topological_space M] [add_comm_group M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [semimodule R M] [semimodule R M₂] (f g : M →L[R] M₂) [topological_add_group M₂] :
(f - g) = f - g

def continuous_linear_map.proj_ker_of_right_inverse {R : Type u_1} [ring R] {M : Type u_2} [topological_space M] [add_comm_group M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [semimodule R M] [semimodule R M₂] [topological_add_group M] (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) :
function.right_inverse f₂ f₁(M →L[R] (f₁.ker))

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] {M : Type u_2} [topological_space M] [add_comm_group M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [semimodule R M] [semimodule R M₂] [topological_add_group M] (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] 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] {M : Type u_2} [topological_space M] [add_comm_group M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [semimodule R M] [semimodule R M₂] [topological_add_group M] (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) (h : function.right_inverse f₂ f₁) (x : (f₁.ker)) :

@[simp]
theorem continuous_linear_map.proj_ker_of_right_inverse_comp_inv {R : Type u_1} [ring R] {M : Type u_2} [topological_space M] [add_comm_group M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [semimodule R M] [semimodule R M₂] [topological_add_group M] (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) (h : function.right_inverse f₂ f₁) (y : M₂) :
(f₁.proj_ker_of_right_inverse f₂ h) (f₂ y) = 0

@[instance]
def continuous_linear_map.has_scalar {R : Type u_1} [comm_ring R] [topological_space R] {M : Type u_2} [topological_space M] [add_comm_group M] {M₃ : Type u_4} [topological_space M₃] [add_comm_group M₃] [module R M] [module R M₃] [topological_module R M₃] :
has_scalar R (M →L[R] M₃)

Equations
@[simp]
theorem continuous_linear_map.smul_comp {R : Type u_1} [comm_ring R] [topological_space 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₃] [module R M] [module R M₂] [module R M₃] [topological_module R M₃] (c : R) (h : M₂ →L[R] M₃) (f : M →L[R] M₂) :
(c h).comp f = c h.comp f

@[simp]
theorem continuous_linear_map.smul_apply {R : Type u_1} [comm_ring R] [topological_space R] {M : Type u_2} [topological_space M] [add_comm_group M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [module R M] [module R M₂] (c : R) (f : M →L[R] M₂) (x : M) [topological_module R M₂] :
(c f) x = c f x

@[simp]
theorem continuous_linear_map.coe_apply {R : Type u_1} [comm_ring R] [topological_space R] {M : Type u_2} [topological_space M] [add_comm_group M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [module R M] [module R M₂] (c : R) (f : M →L[R] M₂) [topological_module R M₂] :
(c f) = c f

theorem continuous_linear_map.coe_apply' {R : Type u_1} [comm_ring R] [topological_space R] {M : Type u_2} [topological_space M] [add_comm_group M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [module R M] [module R M₂] (c : R) (f : M →L[R] M₂) [topological_module R M₂] :
(c f) = c f

@[simp]
theorem continuous_linear_map.comp_smul {R : Type u_1} [comm_ring R] [topological_space 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₃] [module R M] [module R M₂] [module R M₃] [topological_module R M₃] (c : R) (h : M₂ →L[R] M₃) (f : M →L[R] M₂) [topological_module R M₂] :
h.comp (c f) = c h.comp f

@[instance]
def continuous_linear_map.module {R : Type u_1} [comm_ring R] [topological_space R] {M : Type u_2} [topological_space M] [add_comm_group M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [module R M] [module R M₂] [topological_module R M₂] [topological_add_group M₂] :
module R (M →L[R] M₂)

Equations
@[instance]
def continuous_linear_map.algebra {R : Type u_1} [comm_ring R] [topological_space R] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [module R M₂] [topological_module R M₂] [topological_add_group M₂] :
algebra R (M₂ →L[R] M₂)

Equations
def continuous_linear_map.smul_rightₗ {R : Type u_1} [comm_ring R] [topological_space R] {M : Type u_2} [topological_space M] [add_comm_group M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [module R M] [module R M₂] [topological_module R M₂] [topological_add_group M₂] :
(M →L[R] R)(M₂ →ₗ[R] 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
def continuous_linear_equiv.to_continuous_linear_map {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :
(M ≃L[R] M₂)(M →L[R] M₂)

A continuous linear equivalence induces a continuous linear map.

Equations
@[instance]
def continuous_linear_equiv.continuous_linear_map.has_coe {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :
has_coe (M ≃L[R] M₂) (M →L[R] M₂)

Coerce continuous linear equivs to continuous linear maps.

Equations
@[instance]
def continuous_linear_equiv.has_coe_to_fun {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :

Coerce continuous linear equivs to maps.

Equations
@[simp]
theorem continuous_linear_equiv.coe_def_rev {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (e : M ≃L[R] M₂) :

@[simp]
theorem continuous_linear_equiv.coe_apply {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (e : M ≃L[R] M₂) (b : M) :
e b = e b

@[simp]
theorem continuous_linear_equiv.coe_to_linear_equiv {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M ≃L[R] M₂) :

theorem continuous_linear_equiv.coe_coe {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (e : M ≃L[R] M₂) :

@[ext]
theorem continuous_linear_equiv.ext {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {f g : M ≃L[R] M₂} :
f = gf = g

def continuous_linear_equiv.to_homeomorph {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :
(M ≃L[R] M₂)M ≃ₜ M₂

A continuous linear equivalence induces a homeomorphism.

Equations
@[simp]
theorem continuous_linear_equiv.map_zero {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (e : M ≃L[R] M₂) :
e 0 = 0

@[simp]
theorem continuous_linear_equiv.map_add {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (e : M ≃L[R] M₂) (x y : M) :
e (x + y) = e x + e y

@[simp]
theorem continuous_linear_equiv.map_smul {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule 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} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (e : M ≃L[R] M₂) {x : M} :
e x = 0 x = 0

theorem continuous_linear_equiv.continuous {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (e : M ≃L[R] M₂) :

theorem continuous_linear_equiv.continuous_on {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (e : M ≃L[R] M₂) {s : set M} :

theorem continuous_linear_equiv.continuous_at {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (e : M ≃L[R] M₂) {x : M} :

theorem continuous_linear_equiv.continuous_within_at {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (e : M ≃L[R] M₂) {s : set M} {x : M} :

theorem continuous_linear_equiv.comp_continuous_on_iff {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {α : Type u_4} [topological_space α] (e : M ≃L[R] M₂) (f : α → M) (s : set α) :

theorem continuous_linear_equiv.comp_continuous_iff {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] {α : Type u_4} [topological_space α] (e : M ≃L[R] M₂) (f : α → M) :

theorem continuous_linear_equiv.ext₁ {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] [semimodule R M] [topological_space R] {f g : R ≃L[R] M} :
f 1 = g 1f = g

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

def continuous_linear_equiv.refl (R : Type u_1) [semiring R] (M : Type u_2) [topological_space M] [add_comm_monoid M] [semimodule R M] :
M ≃L[R] M

The identity map as a continuous linear equivalence.

Equations
@[simp]

def continuous_linear_equiv.symm {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :
(M ≃L[R] M₂)(M₂ ≃L[R] 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} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (e : M ≃L[R] M₂) :

def continuous_linear_equiv.trans {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] :
(M ≃L[R] M₂)(M₂ ≃L[R] M₃)(M ≃L[R] 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} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] (e₁ : M ≃L[R] M₂) (e₂ : M₂ ≃L[R] M₃) :

def continuous_linear_equiv.prod {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] {M₄ : Type u_5} [topological_space M₄] [add_comm_monoid M₄] [semimodule R M] [semimodule R M₂] [semimodule R M₃] [semimodule R M₄] :
(M ≃L[R] M₂)(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]
theorem continuous_linear_equiv.prod_apply {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] {M₄ : Type u_5} [topological_space M₄] [add_comm_monoid M₄] [semimodule R M] [semimodule R M₂] [semimodule R M₃] [semimodule 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]
theorem continuous_linear_equiv.coe_prod {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] {M₄ : Type u_5} [topological_space M₄] [add_comm_monoid M₄] [semimodule R M] [semimodule R M₂] [semimodule R M₃] [semimodule R M₄] (e : M ≃L[R] M₂) (e' : M₃ ≃L[R] M₄) :

theorem continuous_linear_equiv.bijective {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (e : M ≃L[R] M₂) :

theorem continuous_linear_equiv.injective {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (e : M ≃L[R] M₂) :

theorem continuous_linear_equiv.surjective {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (e : M ≃L[R] M₂) :

@[simp]
theorem continuous_linear_equiv.trans_apply {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] (e₁ : M ≃L[R] M₂) (e₂ : M₂ ≃L[R] M₃) (c : M) :
(e₁.trans e₂) c = e₂ (e₁ c)

@[simp]
theorem continuous_linear_equiv.apply_symm_apply {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (e : M ≃L[R] M₂) (c : M₂) :
e ((e.symm) c) = c

@[simp]
theorem continuous_linear_equiv.symm_apply_apply {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (e : M ≃L[R] M₂) (b : M) :
(e.symm) (e b) = b

@[simp]
theorem continuous_linear_equiv.symm_trans_apply {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] (e₁ : M₂ ≃L[R] M) (e₂ : M₃ ≃L[R] M₂) (c : M) :
((e₂.trans e₁).symm) c = (e₂.symm) ((e₁.symm) c)

@[simp]
theorem continuous_linear_equiv.comp_coe {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] {M₃ : Type u_4} [topological_space M₃] [add_comm_monoid M₃] [semimodule R M] [semimodule R M₂] [semimodule R M₃] (f : M ≃L[R] M₂) (f' : M₂ ≃L[R] M₃) :
f'.comp f = (f.trans f')

@[simp]
theorem continuous_linear_equiv.coe_comp_coe_symm {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (e : M ≃L[R] M₂) :

@[simp]
theorem continuous_linear_equiv.coe_symm_comp_coe {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (e : M ≃L[R] M₂) :

theorem continuous_linear_equiv.symm_comp_self {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (e : M ≃L[R] M₂) :

theorem continuous_linear_equiv.self_comp_symm {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (e : M ≃L[R] M₂) :

@[simp]
theorem continuous_linear_equiv.symm_comp_self' {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (e : M ≃L[R] M₂) :

@[simp]
theorem continuous_linear_equiv.self_comp_symm' {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (e : M ≃L[R] M₂) :

@[simp]
theorem continuous_linear_equiv.symm_symm {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (e : M ≃L[R] M₂) :
e.symm.symm = e

theorem continuous_linear_equiv.symm_symm_apply {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (e : M ≃L[R] M₂) (x : M) :
(e.symm.symm) x = e x

theorem continuous_linear_equiv.symm_apply_eq {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (e : M ≃L[R] M₂) {x : M₂} {y : M} :
(e.symm) x = y x = e y

theorem continuous_linear_equiv.eq_symm_apply {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (e : M ≃L[R] M₂) {x : M₂} {y : M} :
y = (e.symm) x e y = x

def continuous_linear_equiv.equiv_of_inverse {R : Type u_1} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] 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} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] 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} [semiring R] {M : Type u_2} [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) (h₁ : function.left_inverse f₂ f₁) (h₂ : function.right_inverse f₂ f₁) :

@[instance]
def continuous_linear_equiv.automorphism_group {R : Type u_1} [semiring R] (M : Type u_2) [topological_space M] [add_comm_monoid M] [semimodule 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.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₄] [semimodule R M] [semimodule R M₂] [semimodule R M₃] [semimodule R M₄] [topological_add_group M₄] :
(M ≃L[R] M₂)(M₃ ≃L[R] M₄)(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₄] [semimodule R M] [semimodule R M₂] [semimodule R M₃] [semimodule 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₄] [semimodule R M] [semimodule R M₂] [semimodule R M₃] [semimodule 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] {M : Type u_2} [topological_space M] [add_comm_group M] [semimodule R M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [semimodule R M₂] (e : M ≃L[R] M₂) (x y : M) :
e (x - y) = e x - e y

@[simp]
theorem continuous_linear_equiv.map_neg {R : Type u_1} [ring R] {M : Type u_2} [topological_space M] [add_comm_group M] [semimodule R M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [semimodule R M₂] (e : M ≃L[R] 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_2} [topological_space M] [add_comm_group M] [semimodule R M] [topological_add_group M] :
units (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_2} [topological_space M] [add_comm_group M] [semimodule R M] [topological_add_group M] :
(M ≃L[R] M)units (M →L[R] M)

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

Equations
def continuous_linear_equiv.units_equiv (R : Type u_1) [ring R] (M : Type u_2) [topological_space M] [add_comm_group M] [semimodule R M] [topological_add_group M] :
units (M →L[R] M) ≃* M ≃L[R] M

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

Equations
@[simp]
theorem continuous_linear_equiv.units_equiv_apply (R : Type u_1) [ring R] (M : Type u_2) [topological_space M] [add_comm_group M] [semimodule R M] [topological_add_group M] (f : units (M →L[R] M)) (x : M) :

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

Equations
def continuous_linear_equiv.equiv_of_right_inverse {R : Type u_1} [ring R] {M : Type u_2} [topological_space M] [add_comm_group M] [semimodule R M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [semimodule R M₂] [topological_add_group M] (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) :
function.right_inverse f₂ f₁(M ≃L[R] M₂ × (f₁.ker))

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_2} [topological_space M] [add_comm_group M] [semimodule R M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [semimodule 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_2} [topological_space M] [add_comm_group M] [semimodule R M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [semimodule 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_2} [topological_space M] [add_comm_group M] [semimodule R M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [semimodule R M₂] [topological_add_group M] (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) (h : function.right_inverse f₂ f₁) (y : M₂ × (f₁.ker)) :

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₂] [semimodule R M₂] [add_comm_monoid M] [semimodule 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₂] [semimodule R M₂] [add_comm_monoid M] [semimodule 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₂] [semimodule R M₂] [add_comm_monoid M] [semimodule R M] (f : M →L[R] M₂) :
(¬∃ (e' : M ≃L[R] M₂), e' = f)f.inverse = 0

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

@[simp]

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] :
submodule R M → Prop

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

Equations
theorem submodule.closed_complemented.has_closed_complement {R : Type u_1} [ring R] {M : Type u_2} [topological_space M] [add_comm_group M] [module R M] {p : submodule R M} [t1_space p] :
p.closed_complemented(∃ (q : submodule R M) (hq : is_closed q), is_compl p q)

@[simp]
theorem submodule.closed_complemented_bot {R : Type u_1} [ring R] {M : Type u_2} [topological_space M] [add_comm_group M] [module R M] :

@[simp]
theorem submodule.closed_complemented_top {R : Type u_1} [ring R] {M : Type u_2} [topological_space M] [add_comm_group M] [module R M] :

theorem continuous_linear_map.closed_complemented_ker_of_right_inverse {R : Type u_1} [ring R] {M : Type u_2} [topological_space M] [add_comm_group M] {M₂ : Type u_3} [topological_space M₂] [add_comm_group M₂] [module R M] [module R M₂] [topological_add_group M] (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) :