# mathlibdocumentation

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] [ 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] [ M]  :
continuous (λ (p : R × M), p.fst p.snd)

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

theorem tendsto_smul {R : Type u} {M : Type v} [semiring 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] [ M] {α : Type u_1} {l : filter α} {f : α → R} {g : α → M} {c : R} {x : M} :
(𝓝 c) (𝓝 x)filter.tendsto (λ (a : α), f a g a) l (𝓝 (c x))

@[instance]
def topological_semiring.to_semimodule {R : Type u_1} [semiring R]  :

def topological_module (R : Type u) (M : Type v) [ring 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] [ 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] [ M] [ M] :
M ≃ₜ 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] [ M] [ 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] [ M] [ 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] [ M] [ M] [(𝓝[{x : R | is_unit x}] 0).ne_bot] (s : 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] [ 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] [ 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] [ 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) (M₂ : Type u_3) [add_comm_monoid M₂] [ M] [ M₂] :
Type (max u_2 u_3)
• to_linear_map : M →ₗ[R] M₂
• cont : . "continuity'"

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

@[nolint]
structure continuous_linear_equiv (R : Type u_1) [semiring R] (M : Type u_2) (M₂ : Type u_3) [add_comm_monoid M₂] [ M] [ M₂] :
Type (max u_2 u_3)
• to_linear_equiv : M ≃ₗ[R] M₂
• continuous_to_fun : . "continuity'"
• continuous_inv_fun : . "continuity'"

Continuous linear equivalences between modules. We only put the type classes that are necessary for the definition, although in applications `M` and `M₂` will be topological modules over the topological 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (f : M →ₗ[R] M₂) (h : . "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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (f : M →ₗ[R] M₂) (h : . "continuity'") :

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

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

theorem continuous_linear_map.injective_coe_fn {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (f : M →L[R] M₂) :

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

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

theorem continuous_linear_map.ext_on {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] [t2_space M₂] {s : set M} (hs : dense s)) {f g : M →L[R] M₂} :
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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] :
inhabited (M →L[R] M₂)

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

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

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

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

@[instance]
def continuous_linear_map.unique_of_left {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] [subsingleton M] :
unique (M →L[R] M₂)

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

Equations
def continuous_linear_map.id (R : Type u_1) [semiring R] (M : Type u_2) [ 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} [ M] :

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

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

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

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

@[instance]
def continuous_linear_map.has_add {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂]  :

Equations
@[simp]
theorem continuous_linear_map.add_apply {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (f g : M →L[R] M₂) (x : 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (f g : M →L[R] M₂)  :
(f + g) = f + g

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

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

Equations
theorem continuous_linear_map.sum_apply {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] [ M] [ M₂] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] [ M] [ M₂] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] [ M] [ M₂] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (f : M →L[R] M₂) :
f.comp = f

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

@[simp]
theorem continuous_linear_map.comp_zero {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] [ M] [ M₂] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] [ M] [ M₂] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] [ M] [ M₂] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] [ M] [ M₂] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] {M₄ : Type u_5} [add_comm_monoid M₄] [ M] [ M₂] [ M₃] [ 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} [ M] :

Equations
theorem continuous_linear_map.mul_def {R : Type u_1} [semiring R] {M : Type u_2} [ 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} [ 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} [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] [ M] [ M₂] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] [ M] [ M₂] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] [ M] [ M₂] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] :
(M →L[R] M₂) M

Kernel of a continuous linear map.

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

@[simp]
theorem continuous_linear_map.mem_ker {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} [add_comm_monoid M₂] [ M₂] {M' : Type u_2} [uniform_space M'] [complete_space M'] [add_comm_monoid M'] [ 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} [add_comm_monoid M₂] [ M₂] {M' : Type u_2} [uniform_space M'] [complete_space M'] [add_comm_monoid M'] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] [ M] [ M₂] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] :
(M →L[R] M₂) M₂

Range of a continuous linear map.

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

theorem continuous_linear_map.mem_range {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] [ M] [ M₂] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (f : M →L[R] M₂) (p : 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (f : M →L[R] M₂) (p : 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (f : M →L[R] M₂) (p : M₂) (h : ∀ (x : M), f x p) (x : M) :
((f.cod_restrict p h) x) = f x

@[simp]
theorem continuous_linear_map.ker_cod_restrict {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (f : M →L[R] M₂) (p : 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} [ M] (p : M) :

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

Equations
@[simp]
theorem continuous_linear_map.coe_subtype_val {R : Type u_1} [semiring R] {M : Type u_2} [ M] (p : M) :

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

def continuous_linear_map.fst (R : Type u_1) [semiring R] (M : Type u_2) (M₂ : Type u_3) [add_comm_monoid M₂] [ M] [ 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) (M₂ : Type u_3) [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] :
M₂) = M₂

@[simp]
theorem continuous_linear_map.coe_fst' {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] :
M₂) = prod.fst

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

@[simp]
theorem continuous_linear_map.coe_snd' {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] :
M₂) = prod.snd

@[simp]
theorem continuous_linear_map.fst_prod_snd {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] :
M₂).prod M₂) = (M × M₂)

def continuous_linear_map.prod_map {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] {M₄ : Type u_5} [add_comm_monoid M₄] [ M] [ M₂] [ M₃] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] {M₄ : Type u_5} [add_comm_monoid M₄] [ M] [ M₂] [ M₃] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] {M₄ : Type u_5} [add_comm_monoid M₄] [ M] [ M₂] [ M₃] [ M₄] (f₁ : M →L[R] M₂) (f₂ : M₃ →L[R] M₄) :
(f₁.prod_map f₂) = f₂

def continuous_linear_map.coprod {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] [ M] [ M₂] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] [ M] [ M₂] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] [ M] [ M₂] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] [ 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} [add_comm_monoid M₂] [ M₂] [ M₂] (c : R →L[R] M₂) :
1.smul_right (c 1) = c

@[simp]
theorem continuous_linear_map.smul_right_one_eq_iff {R : Type u_1} [semiring R] {M₂ : Type u_3} [add_comm_monoid M₂] [ M₂] [ M₂] {f f' : M₂} :
1.smul_right f = 1.smul_right f' f = f'

theorem continuous_linear_map.smul_right_comp {R : Type u_1} [semiring R] {M₂ : Type u_3} [add_comm_monoid M₂] [ M₂] [ M₂] {x : M₂} {c : R} :

def continuous_linear_map.pi {R : Type u_1} [semiring R] {M : Type u_2} [ M] {ι : Type u_4} {φ : ι → Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), (φ i)] :
(Π (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} [ M] {ι : Type u_4} {φ : ι → Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), (φ i)] (f : Π (i : ι), M →L[R] φ i) (c : M) (i : ι) :
i = (f i) c

theorem continuous_linear_map.pi_eq_zero {R : Type u_1} [semiring R] {M : Type u_2} [ M] {ι : Type u_4} {φ : ι → Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), (φ i)] (f : Π (i : ι), M →L[R] φ i) :
∀ (i : ι), f i = 0

theorem continuous_linear_map.pi_zero {R : Type u_1} [semiring R] {M : Type u_2} [ M] {ι : Type u_4} {φ : ι → Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), (φ i)] :
continuous_linear_map.pi (λ (i : ι), 0) = 0

theorem continuous_linear_map.pi_comp {R : Type u_1} [semiring R] {M : Type u_2} [ M] {M₂ : Type u_3} [add_comm_monoid M₂] [ M₂] {ι : Type u_4} {φ : ι → Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), (φ i)] (f : Π (i : ι), M →L[R] φ i) (g : M₂ →L[R] M) :
= continuous_linear_map.pi (λ (i : ι), (f i).comp g)

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

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

Equations
@[simp]
theorem continuous_linear_map.proj_apply {R : Type u_1} [semiring R] {ι : Type u_4} {φ : ι → Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), (φ i)] (i : ι) (b : Π (i : ι), φ i) :
= b i

theorem continuous_linear_map.proj_pi {R : Type u_1} [semiring R] {M₂ : Type u_3} [add_comm_monoid M₂] [ M₂] {ι : Type u_4} {φ : ι → Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), (φ i)] (f : Π (i : ι), M₂ →L[R] φ i) (i : ι) :

theorem continuous_linear_map.infi_ker_proj {R : Type u_1} [semiring R] {ι : Type u_4} {φ : ι → Type u_5} [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), (φ i)] :
(⨅ (i : ι), =

def continuous_linear_map.infi_ker_proj_equiv (R : Type u_1) [semiring R] {ι : Type u_4} (φ : ι → Type u_5) [Π (i : ι), topological_space (φ i)] [Π (i : ι), add_comm_monoid (φ i)] [Π (i : ι), (φ i)] {I J : set ι} [decidable_pred (λ (i : ι), i I)] :
Jset.univ I J((⨅ (i : ι) (H : i J), ≃L[R] Π (i : I), φ i)

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

Equations
@[simp]
theorem continuous_linear_map.map_neg {R : Type u_1} [ring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_group M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_group M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_group M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_group M₂] {M₃ : Type u_4} [add_comm_group M₃] [ M] [ M₂] [ 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} {M₂ : Type u_3} [add_comm_group M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_group M₂] [ M] [ M₂] (f : M →L[R] M₂) (x : M)  :
(-f) x = -f x

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

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

@[instance]
def continuous_linear_map.add_comm_group {R : Type u_1} [ring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_group M₂] [ M] [ M₂]  :

Equations
theorem continuous_linear_map.sub_apply {R : Type u_1} [ring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_group M₂] [ M] [ M₂] (f g : M →L[R] 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} {M₂ : Type u_3} [add_comm_group M₂] [ M] [ M₂] (f g : M →L[R] M₂)  :
(f - g) = f - g

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

@[instance]
def continuous_linear_map.ring {R : Type u_1} [ring R] {M : Type u_2} [ M]  :
ring (M →L[R] M)

Equations
theorem continuous_linear_map.smul_right_one_pow {R : Type u_1} [ring R] (c : R) (n : ) :
1.smul_right c ^ n = 1.smul_right (c ^ n)

def continuous_linear_map.proj_ker_of_right_inverse {R : Type u_1} [ring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_group M₂] [ M] [ M₂] (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) :
(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} {M₂ : Type u_3} [add_comm_group M₂] [ M] [ M₂] (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) (h : f₁) (x : M) :
( 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} {M₂ : Type u_3} [add_comm_group M₂] [ M] [ M₂] (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) (h : f₁) (x : (f₁.ker)) :
h) x = x

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

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

Equations
@[simp]
theorem continuous_linear_map.smul_comp {R : Type u_1} [comm_ring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_group M₂] {M₃ : Type u_4} [add_comm_group M₃] [ M] [ M₂] [ M₃] [ 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] {M : Type u_2} {M₂ : Type u_3} [add_comm_group M₂] [ M] [ M₂] (c : R) (f : M →L[R] M₂) (x : M) [ M₂] :
(c f) x = c f x

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

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

@[simp]
theorem continuous_linear_map.comp_smul {R : Type u_1} [comm_ring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_group M₂] {M₃ : Type u_4} [add_comm_group M₃] [ M] [ M₂] [ M₃] [ M₃] (c : R) (h : M₂ →L[R] M₃) (f : M →L[R] M₂) [ M₂] :
h.comp (c f) = c h.comp f

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

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

Equations
def continuous_linear_map.smul_rightₗ {R : Type u_1} [comm_ring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_group M₂] [ M] [ M₂] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (e : M ≃L[R] M₂) :

@[simp]
theorem continuous_linear_equiv.coe_apply {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (f : M ≃L[R] M₂) :

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

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

theorem continuous_linear_equiv.continuous_on {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] {α : Type u_4} (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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] {α : Type u_4} (e : M ≃L[R] M₂) (f : α → M) :

theorem continuous_linear_equiv.ext₁ {R : Type u_1} [semiring R] {M : Type u_2} [ M] {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) [ M] :
M ≃L[R] M

The identity map as a continuous linear equivalence.

Equations
@[simp]
theorem continuous_linear_equiv.coe_refl {R : Type u_1} [semiring R] {M : Type u_2} [ M] :

@[simp]
theorem continuous_linear_equiv.coe_refl' {R : Type u_1} [semiring R] {M : Type u_2} [ M] :

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

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

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

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

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

@[simp]
theorem continuous_linear_equiv.trans_apply {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] [ M] [ M₂] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] [ M] [ M₂] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] {M₃ : Type u_4} [add_comm_monoid M₃] [ M] [ M₂] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (e : M ≃L[R] M₂) :

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

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

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

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

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

@[simp]
theorem continuous_linear_equiv.refl_symm {R : Type u_1} [semiring R] {M : Type u_2} [ M] :

theorem continuous_linear_equiv.symm_symm_apply {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) :
(M ≃L[R] M₂)

Create a `continuous_linear_equiv` from two `continuous_linear_map`s 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} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) (h₁ : f₁) (h₂ : f₁) (x : M) :
h₂) x = f₁ x

@[simp]
theorem continuous_linear_equiv.symm_equiv_of_inverse {R : Type u_1} [semiring R] {M : Type u_2} {M₂ : Type u_3} [add_comm_monoid M₂] [ M] [ M₂] (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) (h₁ : f₁) (h₂ : f₁) :
h₂).symm = h₁

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

The next theorems cover the identification between `M ≃L[𝕜] M`and 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} [ 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} [ 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) [ 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) [ M] (f : units (M →L[R] M)) (x : M) :
f) x = f x

def continuous_linear_equiv.units_equiv_aut (R : Type u_1) [ring R] [ R] :
R ≃L[R] R

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

Equations
@[simp]
theorem continuous_linear_equiv.units_equiv_aut_apply {R : Type u_1} [ring R] [ R] (u : units R) (x : R) :
= x * u

@[simp]
theorem continuous_linear_equiv.units_equiv_aut_apply_symm {R : Type u_1} [ring R] [ R] (u : units R) (x : R) :
x = x * u⁻¹

@[simp]
theorem continuous_linear_equiv.units_equiv_aut_symm_apply {R : Type u_1} [ring R] [ R] (e : R ≃L[R] R) :
= e 1

def continuous_linear_equiv.equiv_of_right_inverse {R : Type u_1} [ring R] {M : Type u_2} [ M] {M₂ : Type u_3} [add_comm_group M₂] [ M₂] (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) :
(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} [ M] {M₂ : Type u_3} [add_comm_group M₂] [ M₂] (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) (h : f₁) (x : M) :
x).fst = f₁ x

@[simp]
theorem continuous_linear_equiv.snd_equiv_of_right_inverse {R : Type u_1} [ring R] {M : Type u_2} [ M] {M₂ : Type u_3} [add_comm_group M₂] [ M₂] (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) (h : f₁) (x : M) :
(( x).snd) = x - f₂ (f₁ x)

@[simp]
theorem continuous_linear_equiv.equiv_of_right_inverse_symm_apply {R : Type u_1} [ring R] {M : Type u_2} [ M] {M₂ : Type u_3} [add_comm_group M₂] [ M₂] (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) (h : f₁) (y : M₂ × (f₁.ker)) :
.symm) y = f₂ y.fst + (y.snd)

def continuous_linear_map.inverse {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [semiring R] [add_comm_monoid M₂] [ M₂] [ 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} [semiring R] [add_comm_monoid M₂] [ M₂] [ 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} [semiring R] [add_comm_monoid M₂] [ M₂] [ 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.ring_inverse_equiv {R : Type u_1} {M : Type u_2} [ring R] [ M] (e : M ≃L[R] M) :

theorem continuous_linear_map.to_ring_inverse {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [ring R] [ M] [add_comm_group M₂] [ 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.

theorem continuous_linear_map.ring_inverse_eq_map_inverse {R : Type u_1} {M : Type u_2} [ring R] [ M] :

def submodule.closed_complemented {R : Type u_1} [ring R] {M : Type u_2} [ M] :
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} [ M] {p : M} [t1_space p] :
p.closed_complemented(∃ (q : M) (hq : , q)

theorem submodule.closed_complemented.is_closed {R : Type u_1} [ring R] {M : Type u_2} [ M] [t1_space M] {p : M} :

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

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

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