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
- continuous_smul : continuous (λ (p : R × M), p.fst • p.snd)
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
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 f → continuous g → continuous (λ (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} :
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 (nhds c) → filter.tendsto g l (nhds x) → filter.tendsto (λ (a : α), f a • g a) l (nhds (c • x))
@[class]
structure
topological_module
(R : Type u)
(M : Type v)
[ring R]
[topological_space R]
[topological_space M]
[add_comm_group M]
[module R M] :
Prop
- to_topological_semimodule : topological_semimodule R M
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] :
Scalar multiplication by a unit is a homeomorphism from a topological module onto itself.
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]
[(nhds_within 0 {x : R | is_unit x}).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] :
Scalar multiplication by a non-zero field element is a homeomorphism from a topological vector space onto itself.
Equations
- homeomorph.smul_of_ne_zero ha = {to_equiv := (homeomorph.smul_of_unit (units.mk0 a ha)).to_equiv, continuous_to_fun := _, continuous_inv_fun := _}
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 ≠ 0 → is_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 ≠ 0 → is_closed_map (λ (x : M), a • x)
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)
- to_linear_map : M →ₗ[R] M₂
- cont : continuous c.to_linear_map.to_fun . "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)
[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)
- to_linear_equiv : M ≃ₗ[R] M₂
- continuous_to_fun : continuous c.to_linear_equiv.to_fun . "continuity'"
- continuous_inv_fun : continuous c.to_linear_equiv.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.
@[instance]
def
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₂] :
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₂] :
has_coe_to_fun (M →L[R] M₂)
Coerce continuous linear maps to functions.
@[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.coe_inj
{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₂⦄ :
@[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₂} :
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₂} :
@[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₂) :
@[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) :
@[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) :
@[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₂) :
@[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₂] :
The continuous map that is constantly zero.
Equations
- continuous_linear_map.has_zero = {zero := {to_linear_map := 0, cont := _}}
@[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₂] :
Equations
@[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) :
@[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₂] :
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₂] :
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] :
the identity map as a continuous linear map.
Equations
- continuous_linear_map.id R M = {to_linear_map := linear_map.id _inst_10, cont := _}
@[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
- continuous_linear_map.has_one = {one := continuous_linear_map.id R M _inst_10}
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) :
⇑(continuous_linear_map.id R M) x = x
@[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.coe_id'
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
[semimodule R M] :
⇑(continuous_linear_map.id R M) = id
@[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) :
@[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₂] :
@[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₂] :
@[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₂] :
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₂] :
@[instance]
def
continuous_linear_map.add_comm_monoid
{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₂] :
add_comm_monoid (M →L[R] M₂)
Equations
- continuous_linear_map.add_comm_monoid = {add := has_add.add continuous_linear_map.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, add_comm := _}
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) :
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₃] :
Composition of bounded linear maps.
Equations
- g.comp f = {to_linear_map := g.to_linear_map.comp f.to_linear_map, cont := _}
@[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₃) :
@[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₃) :
@[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₂) :
f.comp (continuous_linear_map.id R M) = f
@[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₂) :
(continuous_linear_map.id R M₂).comp f = f
@[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₂) :
@[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₂) :
@[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₂) :
@[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₂) :
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₂) :
@[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
- continuous_linear_map.has_mul = {mul := continuous_linear_map.comp _inst_10}
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) :
@[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) :
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) :
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₃] :
The cartesian product of two bounded linear maps, as a bounded linear map.
Equations
- f₁.prod f₂ = {to_linear_map := {to_fun := (f₁.to_linear_map.prod f₂.to_linear_map).to_fun, map_add' := _, map_smul' := _}, cont := _}
@[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₃) :
@[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) :
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₂] :
Kernel of a continuous linear map.
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} :
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)) :
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₂) :
is_complete ↑(f.ker)
@[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₂) :
complete_space ↥(f.ker)
Equations
- _ = _
@[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₃) :
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₂] :
Range of a continuous linear map.
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₂} :
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₂) :
Restrict codomain of a continuous linear map.
Equations
- f.cod_restrict p h = {to_linear_map := linear_map.cod_restrict p ↑f h, cont := _}
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) :
↑(f.cod_restrict p h) = linear_map.cod_restrict p ↑f h
@[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
- continuous_linear_map.subtype_val p = {to_linear_map := p.subtype, cont := _}
@[simp]
theorem
continuous_linear_map.coe_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) :
@[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) :
⇑(continuous_linear_map.subtype_val p) x = ↑x
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₂] :
prod.fst as a continuous_linear_map.
Equations
- continuous_linear_map.fst R M M₂ = {to_linear_map := linear_map.fst R M M₂ _inst_11, cont := _}
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₂] :
prod.snd as a continuous_linear_map.
Equations
- continuous_linear_map.snd R M M₂ = {to_linear_map := linear_map.snd R M M₂ _inst_11, cont := _}
@[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₂] :
↑(continuous_linear_map.fst R M M₂) = linear_map.fst R M 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₂] :
⇑(continuous_linear_map.fst R M M₂) = prod.fst
@[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₂] :
↑(continuous_linear_map.snd R M M₂) = linear_map.snd R M 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₂] :
⇑(continuous_linear_map.snd R M M₂) = prod.snd
@[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₂] :
(continuous_linear_map.fst R M M₂).prod (continuous_linear_map.snd R M M₂) = continuous_linear_map.id R (M × 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₄] :
prod.map of two continuous linear maps.
Equations
- f₁.prod_map f₂ = (f₁.comp (continuous_linear_map.fst R M M₃)).prod (f₂.comp (continuous_linear_map.snd R M M₃))
@[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₄) :
@[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₄) :
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₃] :
The continuous linear map given by (x, y) ↦ f₁ x + f₂ y.
@[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₃) :
@[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₂) :
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₂] :
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₂)
Equations
- c.smul_right f = {to_linear_map := {to_fun := (c.to_linear_map.smul_right f).to_fun, map_add' := _, map_smul' := _}, cont := _}
@[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} :
(1.smul_right x).comp (1.smul_right c) = 1.smul_right (c • x)
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)] :
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
- continuous_linear_map.pi f = {to_linear_map := linear_map.pi (λ (i : ι), ↑(f i)), cont := _}
@[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 : ι) :
⇑(continuous_linear_map.pi f) c i = ⇑(f i) c
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) :
(continuous_linear_map.pi f).comp g = 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 : ι), semimodule R (φ i)]
(i : ι) :
The projections from a family of topological modules are continuous linear maps.
Equations
- continuous_linear_map.proj i = {to_linear_map := linear_map.proj i, cont := _}
@[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) :
⇑(continuous_linear_map.proj i) b = b 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 : ι) :
(continuous_linear_map.proj i).comp (continuous_linear_map.pi f) = f 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)] :
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
- continuous_linear_map.infi_ker_proj_equiv R φ hd hu = {to_linear_equiv := linear_map.infi_ker_proj_equiv R φ hd hu, continuous_to_fun := _, continuous_inv_fun := _}
@[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) :
@[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) :
@[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) :
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₃} :
@[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₂] :
@[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₂] :
@[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₂] :
@[instance]
def
continuous_linear_map.add_comm_group
{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₂] :
add_comm_group (M →L[R] M₂)
Equations
- continuous_linear_map.add_comm_group = {add := has_add.add continuous_linear_map.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, neg := has_neg.neg continuous_linear_map.has_neg, add_left_neg := _, add_comm := _}
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) :
@[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₂] :
@[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₂] :
@[instance]
def
continuous_linear_map.ring
{R : Type u_1}
[ring R]
{M : Type u_2}
[topological_space M]
[add_comm_group M]
[semimodule R M]
[topological_add_group M] :
Equations
- continuous_linear_map.ring = {add := add_comm_group.add continuous_linear_map.add_comm_group, add_assoc := _, zero := add_comm_group.zero continuous_linear_map.add_comm_group, zero_add := _, add_zero := _, neg := add_comm_group.neg continuous_linear_map.add_comm_group, add_left_neg := _, add_comm := _, mul := has_mul.mul continuous_linear_map.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _}
theorem
continuous_linear_map.smul_right_one_pow
{R : Type u_1}
[ring R]
[topological_space R]
[topological_add_group R]
[topological_semimodule R 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}
[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) :
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
- f₁.proj_ker_of_right_inverse f₂ h = (continuous_linear_map.id R M - f₂.comp f₁).cod_restrict f₁.ker _
@[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) :
@[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)) :
⇑(f₁.proj_ker_of_right_inverse f₂ 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}
[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₃)
@[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₂) :
@[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₂] :
@[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₂] :
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₂] :
@[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₂] :
@[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₂] :
Equations
- continuous_linear_map.module = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := continuous_linear_map.has_scalar _inst_13, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
@[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₂] :
Equations
- continuous_linear_map.algebra = algebra.of_semimodule' continuous_linear_map.algebra._proof_1 continuous_linear_map.algebra._proof_2
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₂] :
A continuous linear equivalence induces a continuous linear map.
Equations
- e.to_continuous_linear_map = {to_linear_map := {to_fun := e.to_linear_equiv.to_linear_map.to_fun, map_add' := _, map_smul' := _}, cont := _}
@[instance]
def
continuous_linear_equiv.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₂] :
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₂] :
has_coe_to_fun (M ≃L[R] M₂)
Coerce continuous linear equivs to maps.
@[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) :
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₂} :
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₂] :
A continuous linear equivalence induces a homeomorphism.
Equations
- e.to_homeomorph = {to_equiv := {to_fun := e.to_linear_equiv.to_fun, inv_fun := e.to_linear_equiv.inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
@[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₂) :
@[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) :
@[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) :
@[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} :
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} :
continuous_on ⇑e s
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} :
continuous_at ⇑e x
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} :
continuous_within_at ⇑e s x
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 α) :
continuous_on (⇑e ∘ f) s ↔ continuous_on f s
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) :
continuous (⇑e ∘ f) ↔ continuous f
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} :
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] :
The identity map as a continuous linear equivalence.
Equations
- continuous_linear_equiv.refl R M = {to_linear_equiv := {to_fun := (linear_equiv.refl R M).to_fun, map_add' := _, map_smul' := _, inv_fun := (linear_equiv.refl R M).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
theorem
continuous_linear_equiv.coe_refl
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
[semimodule R M] :
@[simp]
theorem
continuous_linear_equiv.coe_refl'
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
[semimodule R M] :
⇑(continuous_linear_equiv.refl R M) = id
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₂] :
The inverse of a continuous linear equivalence as a continuous linear equivalence
Equations
- e.symm = {to_linear_equiv := {to_fun := e.to_linear_equiv.symm.to_fun, map_add' := _, map_smul' := _, inv_fun := e.to_linear_equiv.symm.inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
@[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₃] :
The composition of two continuous linear equivalences as a continuous linear equivalence.
Equations
- e₁.trans e₂ = {to_linear_equiv := {to_fun := (e₁.to_linear_equiv.trans e₂.to_linear_equiv).to_fun, map_add' := _, map_smul' := _, inv_fun := (e₁.to_linear_equiv.trans e₂.to_linear_equiv).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
@[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₃) :
(e₁.trans e₂).to_linear_equiv = e₁.to_linear_equiv.trans e₂.to_linear_equiv
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₄] :
Product of two continuous linear equivalences. The map comes from equiv.prod_congr.
Equations
- e.prod e' = {to_linear_equiv := {to_fun := (e.to_linear_equiv.prod e'.to_linear_equiv).to_fun, map_add' := _, map_smul' := _, inv_fun := (e.to_linear_equiv.prod e'.to_linear_equiv).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
@[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₃) :
@[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.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₂) :
@[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) :
@[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₂) :
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) :
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} :
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} :
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) :
function.left_inverse ⇑f₂ ⇑f₁ → function.right_inverse ⇑f₂ ⇑f₁ → (M ≃L[R] M₂)
Create a continuous_linear_equiv from two continuous_linear_maps that are
inverse of each other.
Equations
- continuous_linear_equiv.equiv_of_inverse f₁ f₂ h₁ h₂ = {to_linear_equiv := {to_fun := ⇑f₁, map_add' := _, map_smul' := _, inv_fun := ⇑f₂, left_inv := h₁, right_inv := h₂}, continuous_to_fun := _, continuous_inv_fun := _}
@[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₁) :
(continuous_linear_equiv.equiv_of_inverse f₁ f₂ h₁ h₂).symm = continuous_linear_equiv.equiv_of_inverse f₂ f₁ h₂ h₁
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₄] :
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
- e.skew_prod e' f = {to_linear_equiv := {to_fun := (e.to_linear_equiv.skew_prod e'.to_linear_equiv ↑f).to_fun, map_add' := _, map_smul' := _, inv_fun := (e.to_linear_equiv.skew_prod e'.to_linear_equiv ↑f).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
@[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₃) :
@[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₄) :
@[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) :
@[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) :
def
continuous_linear_equiv.units_equiv_aut
(R : Type u_1)
[ring R]
[topological_space R]
[topological_module R R] :
Continuous linear equivalences R ≃L[R] R are enumerated by units R.
@[simp]
theorem
continuous_linear_equiv.units_equiv_aut_apply
{R : Type u_1}
[ring R]
[topological_space R]
[topological_module R R]
(u : units R)
(x : R) :
@[simp]
theorem
continuous_linear_equiv.units_equiv_aut_apply_symm
{R : Type u_1}
[ring R]
[topological_space R]
[topological_module R R]
(u : units R)
(x : R) :
@[simp]
theorem
continuous_linear_equiv.units_equiv_aut_symm_apply
{R : Type u_1}
[ring R]
[topological_space R]
[topological_module R R]
(e : R ≃L[R] R) :
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) :
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
- continuous_linear_equiv.equiv_of_right_inverse f₁ f₂ h = continuous_linear_equiv.equiv_of_inverse (f₁.prod (f₁.proj_ker_of_right_inverse f₂ h)) (f₂.coprod (continuous_linear_map.subtype_val f₁.ker)) _ _
@[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) :
(⇑(continuous_linear_equiv.equiv_of_right_inverse f₁ f₂ h) x).fst = ⇑f₁ x
@[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
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.
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)
theorem
submodule.closed_complemented.is_closed
{R : Type u_1}
[ring R]
{M : Type u_2}
[topological_space M]
[add_comm_group M]
[module R M]
[topological_add_group M]
[t1_space M]
{p : submodule R M} :
@[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) :
function.right_inverse ⇑f₂ ⇑f₁ → f₁.ker.closed_complemented