Theory of topological modules and continuous linear maps. #
We use the class has_continuous_smul for topological (semi) modules and topological vector spaces.
In this file we define continuous (semi-)linear maps, as semilinear maps between topological
modules which are continuous. The set of continuous semilinear maps between the topological
R₁-module M and R₂-module M₂ with respect to the ring_hom σ is denoted by M →SL[σ] M₂.
Plain linear maps are denoted by M →L[R] M₂ and star-linear maps by M →L⋆[R] M₂.
The corresponding notation for equivalences is M ≃SL[σ] M₂, M ≃L[R] M₂ and M ≃L⋆[R] M₂.
theorem
has_continuous_smul.of_nhds_zero
{R : Type u_1}
{M : Type u_2}
[ring R]
[topological_space R]
[topological_space M]
[add_comm_group M]
[module R M]
[topological_ring R]
[topological_add_group M]
(hmul : filter.tendsto (λ (p : R × M), p.fst • p.snd) (𝓝 0 ×ᶠ 𝓝 0) (𝓝 0))
(hmulleft : ∀ (m : M), filter.tendsto (λ (a : R), a • m) (𝓝 0) (𝓝 0))
(hmulright : ∀ (a : R), filter.tendsto (λ (m : M), a • m) (𝓝 0) (𝓝 0)) :
theorem
submodule.eq_top_of_nonempty_interior'
{R : Type u_1}
{M : Type u_2}
[ring R]
[topological_space R]
[topological_space M]
[add_comm_group M]
[has_continuous_add M]
[module R M]
[has_continuous_smul R M]
[(𝓝[{x : R | is_unit x}] 0).ne_bot]
(s : submodule R M)
(hs : (interior ↑s).nonempty) :
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.
theorem
module.punctured_nhds_ne_bot
(R : Type u_1)
(M : Type u_2)
[ring R]
[topological_space R]
[topological_space M]
[add_comm_group M]
[has_continuous_add M]
[module R M]
[has_continuous_smul R M]
[nontrivial M]
[(𝓝[{0}ᶜ] 0).ne_bot]
[no_zero_smul_divisors R M]
(x : M) :
Let R be a topological ring such that zero is not an isolated point (e.g., a nondiscrete
normed field, see normed_field.punctured_nhds_ne_bot). Let M be a nontrivial module over R
such that c • x = 0 implies c = 0 ∨ x = 0. Then M has no isolated points. We formulate this
using ne_bot (𝓝[≠] x).
This lemma is not an instance because Lean would need to find [has_continuous_smul ?m_1 M] with
unknown ?m_1. We register this as an instance for R = ℝ in real.punctured_nhds_module_ne_bot.
One can also use haveI := module.punctured_nhds_ne_bot R M in a proof.
theorem
has_continuous_smul_induced
{R : Type u_2}
{M₁ : Type u_3}
{M₂ : Type u_4}
[semiring R]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[module R M₁]
[module R M₂]
[u : topological_space R]
{t : topological_space M₂}
[has_continuous_smul R M₂]
(f : M₁ →ₗ[R] M₂) :
has_continuous_smul R M₁
@[protected, instance]
def
submodule.has_continuous_smul
{α : Type u_1}
{β : Type u_2}
[topological_space β]
[topological_space α]
[semiring α]
[add_comm_monoid β]
[module α β]
[has_continuous_smul α β]
(S : submodule α β) :
@[protected, instance]
def
submodule.topological_add_group
{α : Type u_1}
{β : Type u_2}
[topological_space β]
[ring α]
[add_comm_group β]
[module α β]
[topological_add_group β]
(S : submodule α β) :
theorem
submodule.closure_smul_self_subset
{R : Type u}
{M : Type v}
[semiring R]
[topological_space R]
[topological_space M]
[add_comm_monoid M]
[module R M]
[has_continuous_smul R M]
(s : submodule R M) :
theorem
submodule.closure_smul_self_eq
{R : Type u}
{M : Type v}
[semiring R]
[topological_space R]
[topological_space M]
[add_comm_monoid M]
[module R M]
[has_continuous_smul R M]
(s : submodule R M) :
def
submodule.topological_closure
{R : Type u}
{M : Type v}
[semiring R]
[topological_space R]
[topological_space M]
[add_comm_monoid M]
[module R M]
[has_continuous_smul R M]
[has_continuous_add M]
(s : submodule R M) :
submodule R M
The (topological-space) closure of a submodule of a topological R-module M is itself
a submodule.
@[simp]
theorem
submodule.topological_closure_coe
{R : Type u}
{M : Type v}
[semiring R]
[topological_space R]
[topological_space M]
[add_comm_monoid M]
[module R M]
[has_continuous_smul R M]
[has_continuous_add M]
(s : submodule R M) :
↑(s.topological_closure) = closure ↑s
@[protected, instance]
def
submodule.topological_closure_has_continuous_smul
{R : Type u}
{M : Type v}
[semiring R]
[topological_space R]
[topological_space M]
[add_comm_monoid M]
[module R M]
[has_continuous_smul R M]
[has_continuous_add M]
(s : submodule R M) :
theorem
submodule.submodule_topological_closure
{R : Type u}
{M : Type v}
[semiring R]
[topological_space R]
[topological_space M]
[add_comm_monoid M]
[module R M]
[has_continuous_smul R M]
[has_continuous_add M]
(s : submodule R M) :
s ≤ s.topological_closure
theorem
submodule.is_closed_topological_closure
{R : Type u}
{M : Type v}
[semiring R]
[topological_space R]
[topological_space M]
[add_comm_monoid M]
[module R M]
[has_continuous_smul R M]
[has_continuous_add M]
(s : submodule R M) :
theorem
submodule.topological_closure_minimal
{R : Type u}
{M : Type v}
[semiring R]
[topological_space R]
[topological_space M]
[add_comm_monoid M]
[module R M]
[has_continuous_smul R M]
[has_continuous_add M]
(s : submodule R M)
{t : submodule R M}
(h : s ≤ t)
(ht : is_closed ↑t) :
s.topological_closure ≤ t
theorem
submodule.topological_closure_mono
{R : Type u}
{M : Type v}
[semiring R]
[topological_space R]
[topological_space M]
[add_comm_monoid M]
[module R M]
[has_continuous_smul R M]
[has_continuous_add M]
{s t : submodule R M}
(h : s ≤ t) :
structure
continuous_linear_map
{R : Type u_1}
{S : Type u_2}
[semiring R]
[semiring S]
(σ : R →+* S)
(M : Type u_3)
[topological_space M]
[add_comm_monoid M]
(M₂ : Type u_4)
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module S M₂] :
Type (max u_3 u_4)
- to_linear_map : M →ₛₗ[σ] M₂
- cont : continuous self.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}
{S : Type u_2}
[semiring R]
[semiring S]
(σ : R →+* S)
{σ' : S →+* R}
[ring_hom_inv_pair σ σ']
[ring_hom_inv_pair σ' σ]
(M : Type u_3)
[topological_space M]
[add_comm_monoid M]
(M₂ : Type u_4)
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module S M₂] :
Type (max u_3 u_4)
- to_linear_equiv : M ≃ₛₗ[σ] M₂
- continuous_to_fun : continuous self.to_linear_equiv.to_fun . "continuity'"
- continuous_inv_fun : continuous self.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 semiring R.
theorem
is_closed_set_of_map_smul
(M₁ : Type u_1)
(M₂ : Type u_2)
{R : Type u_4}
{S : Type u_5}
[topological_space M₂]
[t2_space M₂]
[semiring R]
[semiring S]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[module R M₁]
[module S M₂]
[has_continuous_const_smul S M₂]
(σ : R →+* S) :
@[simp]
theorem
linear_map_of_mem_closure_range_coe_apply
{M₁ : Type u_1}
{M₂ : Type u_2}
{R : Type u_4}
{S : Type u_5}
[topological_space M₂]
[t2_space M₂]
[semiring R]
[semiring S]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[module R M₁]
[module S M₂]
[has_continuous_const_smul S M₂]
[has_continuous_add M₂]
{σ : R →+* S}
(f : M₁ → M₂)
(hf : f ∈ closure (set.range coe_fn)) :
⇑(linear_map_of_mem_closure_range_coe f hf) = f
def
linear_map_of_mem_closure_range_coe
{M₁ : Type u_1}
{M₂ : Type u_2}
{R : Type u_4}
{S : Type u_5}
[topological_space M₂]
[t2_space M₂]
[semiring R]
[semiring S]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[module R M₁]
[module S M₂]
[has_continuous_const_smul S M₂]
[has_continuous_add M₂]
{σ : R →+* S}
(f : M₁ → M₂)
(hf : f ∈ closure (set.range coe_fn)) :
Constructs a bundled linear map from a function and a proof that this function belongs to the closure of the set of linear maps.
def
linear_map_of_tendsto
{M₁ : Type u_1}
{M₂ : Type u_2}
{α : Type u_3}
{R : Type u_4}
{S : Type u_5}
[topological_space M₂]
[t2_space M₂]
[semiring R]
[semiring S]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[module R M₁]
[module S M₂]
[has_continuous_const_smul S M₂]
[has_continuous_add M₂]
{σ : R →+* S}
{l : filter α}
(f : M₁ → M₂)
(g : α → (M₁ →ₛₗ[σ] M₂))
[l.ne_bot]
(h : filter.tendsto (λ (a : α) (x : M₁), ⇑(g a) x) l (𝓝 f)) :
Construct a bundled linear map from a pointwise limit of linear maps
Equations
@[simp]
theorem
linear_map_of_tendsto_apply
{M₁ : Type u_1}
{M₂ : Type u_2}
{α : Type u_3}
{R : Type u_4}
{S : Type u_5}
[topological_space M₂]
[t2_space M₂]
[semiring R]
[semiring S]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[module R M₁]
[module S M₂]
[has_continuous_const_smul S M₂]
[has_continuous_add M₂]
{σ : R →+* S}
{l : filter α}
(f : M₁ → M₂)
(g : α → (M₁ →ₛₗ[σ] M₂))
[l.ne_bot]
(h : filter.tendsto (λ (a : α) (x : M₁), ⇑(g a) x) l (𝓝 f)) :
⇑(linear_map_of_tendsto f g h) = f
theorem
linear_map.is_closed_range_coe
(M₁ : Type u_1)
(M₂ : Type u_2)
{R : Type u_4}
{S : Type u_5}
[topological_space M₂]
[t2_space M₂]
[semiring R]
[semiring S]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[module R M₁]
[module S M₂]
[has_continuous_const_smul S M₂]
[has_continuous_add M₂]
(σ : R →+* S) :
Properties that hold for non-necessarily commutative semirings. #
@[protected, instance]
def
continuous_linear_map.linear_map.has_coe
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂] :
Coerce continuous linear maps to linear maps.
Equations
@[simp]
theorem
continuous_linear_map.to_linear_map_eq_coe
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(f : M₁ →SL[σ₁₂] M₂) :
f.to_linear_map = ↑f
theorem
continuous_linear_map.coe_injective
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂] :
@[protected, instance]
def
continuous_linear_map.add_monoid_hom_class
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂] :
add_monoid_hom_class (M₁ →SL[σ₁₂] M₂) M₁ M₂
Equations
- continuous_linear_map.add_monoid_hom_class = {coe := λ (f : M₁ →SL[σ₁₂] M₂), f.to_linear_map.to_fun, coe_injective' := _, map_add := _, map_zero := _}
@[protected, instance]
def
continuous_linear_map.to_fun
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂] :
has_coe_to_fun (M₁ →SL[σ₁₂] M₂) (λ (_x : M₁ →SL[σ₁₂] M₂), M₁ → M₂)
Coerce continuous linear maps to functions.
Equations
- continuous_linear_map.to_fun = {coe := λ (f : M₁ →SL[σ₁₂] M₂), f.to_linear_map.to_fun}
@[simp]
theorem
continuous_linear_map.coe_mk
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(f : M₁ →ₛₗ[σ₁₂] M₂)
(h : continuous f.to_fun . "continuity'") :
↑{to_linear_map := f, cont := h} = f
@[simp]
theorem
continuous_linear_map.coe_mk'
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(f : M₁ →ₛₗ[σ₁₂] M₂)
(h : continuous f.to_fun . "continuity'") :
@[protected, continuity]
theorem
continuous_linear_map.continuous
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(f : M₁ →SL[σ₁₂] M₂) :
@[simp, norm_cast]
theorem
continuous_linear_map.coe_inj
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
{f g : M₁ →SL[σ₁₂] M₂} :
theorem
continuous_linear_map.coe_fn_injective
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂] :
def
continuous_linear_map.simps.apply
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(h : M₁ →SL[σ₁₂] M₂) :
M₁ → M₂
See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.
Equations
def
continuous_linear_map.simps.coe
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(h : M₁ →SL[σ₁₂] M₂) :
See Note [custom simps projection].
Equations
@[ext]
theorem
continuous_linear_map.ext
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
{f g : M₁ →SL[σ₁₂] M₂}
(h : ∀ (x : M₁), ⇑f x = ⇑g x) :
f = g
theorem
continuous_linear_map.ext_iff
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
{f g : M₁ →SL[σ₁₂] M₂} :
@[protected]
def
continuous_linear_map.copy
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(f : M₁ →SL[σ₁₂] M₂)
(f' : M₁ → M₂)
(h : f' = ⇑f) :
Copy of a continuous_linear_map with a new to_fun equal to the old one. Useful to fix
definitional equalities.
Equations
- f.copy f' h = {to_linear_map := f.to_linear_map.copy f' h, cont := _}
@[protected]
theorem
continuous_linear_map.map_zero
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(f : M₁ →SL[σ₁₂] M₂) :
@[protected]
theorem
continuous_linear_map.map_add
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(f : M₁ →SL[σ₁₂] M₂)
(x y : M₁) :
@[simp]
theorem
continuous_linear_map.map_smulₛₗ
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(f : M₁ →SL[σ₁₂] M₂)
(c : R₁)
(x : M₁) :
@[simp]
theorem
continuous_linear_map.map_smul
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₁ M₂]
(f : M₁ →L[R₁] M₂)
(c : R₁)
(x : M₁) :
@[simp]
theorem
continuous_linear_map.map_smul_of_tower
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{R : Type u_1}
{S : Type u_2}
[semiring S]
[has_scalar R M₁]
[module S M₁]
[has_scalar R M₂]
[module S M₂]
[linear_map.compatible_smul M₁ M₂ R S]
(f : M₁ →L[S] M₂)
(c : R)
(x : M₁) :
@[protected]
theorem
continuous_linear_map.map_sum
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
{ι : Type u_3}
(f : M₁ →SL[σ₁₂] M₂)
(s : finset ι)
(g : ι → M₁) :
@[simp, norm_cast]
theorem
continuous_linear_map.coe_coe
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(f : M₁ →SL[σ₁₂] M₂) :
@[ext]
theorem
continuous_linear_map.ext_ring
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁]
[topological_space R₁]
{f g : R₁ →L[R₁] M₁}
(h : ⇑f 1 = ⇑g 1) :
f = g
theorem
continuous_linear_map.ext_ring_iff
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁]
[topological_space R₁]
{f g : R₁ →L[R₁] M₁} :
theorem
continuous_linear_map.eq_on_closure_span
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
[t2_space M₂]
{s : set M₁}
{f g : M₁ →SL[σ₁₂] M₂}
(h : set.eq_on ⇑f ⇑g s) :
If two continuous linear maps are equal on a set s, then they are equal on the closure
of the submodule.span of this set.
theorem
continuous_linear_map.ext_on
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
[t2_space M₂]
{s : set M₁}
(hs : dense ↑(submodule.span R₁ s))
{f g : M₁ →SL[σ₁₂] M₂}
(h : set.eq_on ⇑f ⇑g s) :
f = g
If the submodule generated by a set s is dense in the ambient module, then two continuous
linear maps equal on s are equal.
theorem
submodule.topological_closure_map
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
[ring_hom_surjective σ₁₂]
[topological_space R₁]
[topological_space R₂]
[has_continuous_smul R₁ M₁]
[has_continuous_add M₁]
[has_continuous_smul R₂ M₂]
[has_continuous_add M₂]
(f : M₁ →SL[σ₁₂] M₂)
(s : submodule R₁ M₁) :
Under a continuous linear map, the image of the topological_closure of a submodule is
contained in the topological_closure of its image.
theorem
dense_range.topological_closure_map_submodule
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
[ring_hom_surjective σ₁₂]
[topological_space R₁]
[topological_space R₂]
[has_continuous_smul R₁ M₁]
[has_continuous_add M₁]
[has_continuous_smul R₂ M₂]
[has_continuous_add M₂]
{f : M₁ →SL[σ₁₂] M₂}
(hf' : dense_range ⇑f)
{s : submodule R₁ M₁}
(hs : s.topological_closure = ⊤) :
(submodule.map ↑f s).topological_closure = ⊤
Under a dense continuous linear map, a submodule whose topological_closure is ⊤ is sent to
another such submodule. That is, the image of a dense set under a map with dense range is dense.
@[protected, instance]
def
continuous_linear_map.mul_action
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
{S₂ : Type u_9}
[monoid S₂]
[distrib_mul_action S₂ M₂]
[smul_comm_class R₂ S₂ M₂]
[has_continuous_const_smul S₂ M₂] :
mul_action S₂ (M₁ →SL[σ₁₂] M₂)
Equations
- continuous_linear_map.mul_action = {to_has_scalar := {smul := λ (c : S₂) (f : M₁ →SL[σ₁₂] M₂), {to_linear_map := c • ↑f, cont := _}}, one_smul := _, mul_smul := _}
theorem
continuous_linear_map.smul_apply
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
{S₂ : Type u_9}
[monoid S₂]
[distrib_mul_action S₂ M₂]
[smul_comm_class R₂ S₂ M₂]
[has_continuous_const_smul S₂ M₂]
(c : S₂)
(f : M₁ →SL[σ₁₂] M₂)
(x : M₁) :
@[simp, norm_cast]
theorem
continuous_linear_map.coe_smul
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
{S₂ : Type u_9}
[monoid S₂]
[distrib_mul_action S₂ M₂]
[smul_comm_class R₂ S₂ M₂]
[has_continuous_const_smul S₂ M₂]
(c : S₂)
(f : M₁ →SL[σ₁₂] M₂) :
@[simp, norm_cast]
theorem
continuous_linear_map.coe_smul'
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
{S₂ : Type u_9}
[monoid S₂]
[distrib_mul_action S₂ M₂]
[smul_comm_class R₂ S₂ M₂]
[has_continuous_const_smul S₂ M₂]
(c : S₂)
(f : M₁ →SL[σ₁₂] M₂) :
@[protected, instance]
def
continuous_linear_map.is_scalar_tower
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
{S₂ : Type u_9}
{T₂ : Type u_10}
[monoid S₂]
[monoid T₂]
[distrib_mul_action S₂ M₂]
[smul_comm_class R₂ S₂ M₂]
[has_continuous_const_smul S₂ M₂]
[distrib_mul_action T₂ M₂]
[smul_comm_class R₂ T₂ M₂]
[has_continuous_const_smul T₂ M₂]
[has_scalar S₂ T₂]
[is_scalar_tower S₂ T₂ M₂] :
is_scalar_tower S₂ T₂ (M₁ →SL[σ₁₂] M₂)
@[protected, instance]
def
continuous_linear_map.smul_comm_class
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
{S₂ : Type u_9}
{T₂ : Type u_10}
[monoid S₂]
[monoid T₂]
[distrib_mul_action S₂ M₂]
[smul_comm_class R₂ S₂ M₂]
[has_continuous_const_smul S₂ M₂]
[distrib_mul_action T₂ M₂]
[smul_comm_class R₂ T₂ M₂]
[has_continuous_const_smul T₂ M₂]
[smul_comm_class S₂ T₂ M₂] :
smul_comm_class S₂ T₂ (M₁ →SL[σ₁₂] M₂)
@[protected, instance]
def
continuous_linear_map.has_zero
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂] :
The continuous map that is constantly zero.
Equations
- continuous_linear_map.has_zero = {zero := {to_linear_map := 0, cont := _}}
@[protected, instance]
def
continuous_linear_map.inhabited
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂] :
Equations
@[simp]
theorem
continuous_linear_map.default_def
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂] :
@[simp]
theorem
continuous_linear_map.zero_apply
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(x : M₁) :
@[simp, norm_cast]
theorem
continuous_linear_map.coe_zero
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂] :
@[norm_cast]
theorem
continuous_linear_map.coe_zero'
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂] :
@[protected, instance]
def
continuous_linear_map.unique_of_left
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
[subsingleton M₁] :
@[protected, instance]
def
continuous_linear_map.unique_of_right
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
[subsingleton M₂] :
def
continuous_linear_map.id
(R₁ : Type u_1)
[semiring R₁]
(M₁ : Type u_4)
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁] :
the identity map as a continuous linear map.
Equations
- continuous_linear_map.id R₁ M₁ = {to_linear_map := linear_map.id _inst_14, cont := _}
@[protected, instance]
def
continuous_linear_map.has_one
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁] :
Equations
- continuous_linear_map.has_one = {one := continuous_linear_map.id R₁ M₁ _inst_14}
theorem
continuous_linear_map.one_def
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁] :
1 = continuous_linear_map.id R₁ M₁
theorem
continuous_linear_map.id_apply
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁]
(x : M₁) :
⇑(continuous_linear_map.id R₁ M₁) x = x
@[simp, norm_cast]
theorem
continuous_linear_map.coe_id
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁] :
↑(continuous_linear_map.id R₁ M₁) = linear_map.id
@[simp, norm_cast]
theorem
continuous_linear_map.coe_id'
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁] :
⇑(continuous_linear_map.id R₁ M₁) = id
@[simp, norm_cast]
theorem
continuous_linear_map.coe_eq_id
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁]
{f : M₁ →L[R₁] M₁} :
↑f = linear_map.id ↔ f = continuous_linear_map.id R₁ M₁
@[simp]
theorem
continuous_linear_map.one_apply
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁]
(x : M₁) :
@[protected, instance]
def
continuous_linear_map.has_add
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
[has_continuous_add M₂] :
@[simp]
theorem
continuous_linear_map.add_apply
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
[has_continuous_add M₂]
(f g : M₁ →SL[σ₁₂] M₂)
(x : M₁) :
@[simp, norm_cast]
theorem
continuous_linear_map.coe_add
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
[has_continuous_add M₂]
(f g : M₁ →SL[σ₁₂] M₂) :
@[norm_cast]
theorem
continuous_linear_map.coe_add'
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
[has_continuous_add M₂]
(f g : M₁ →SL[σ₁₂] M₂) :
@[protected, instance]
def
continuous_linear_map.add_comm_monoid
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
[has_continuous_add M₂] :
add_comm_monoid (M₁ →SL[σ₁₂] M₂)
Equations
- continuous_linear_map.add_comm_monoid = {add := has_add.add continuous_linear_map.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := has_scalar.smul mul_action.to_has_scalar, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}
@[simp, norm_cast]
theorem
continuous_linear_map.coe_sum
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
[has_continuous_add M₂]
{ι : Type u_3}
(t : finset ι)
(f : ι → (M₁ →SL[σ₁₂] M₂)) :
@[simp, norm_cast]
theorem
continuous_linear_map.coe_sum'
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
[has_continuous_add M₂]
{ι : Type u_3}
(t : finset ι)
(f : ι → (M₁ →SL[σ₁₂] M₂)) :
theorem
continuous_linear_map.sum_apply
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
[has_continuous_add M₂]
{ι : Type u_3}
(t : finset ι)
(f : ι → (M₁ →SL[σ₁₂] M₂))
(b : M₁) :
def
continuous_linear_map.comp
{R₁ : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
[semiring R₁]
[semiring R₂]
[semiring R₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R₁ →+* R₃}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₂ M₂]
[module R₃ M₃]
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
(g : M₂ →SL[σ₂₃] M₃)
(f : M₁ →SL[σ₁₂] M₂) :
Composition of bounded linear maps.
@[simp, norm_cast]
theorem
continuous_linear_map.coe_comp
{R₁ : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
[semiring R₁]
[semiring R₂]
[semiring R₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R₁ →+* R₃}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₂ M₂]
[module R₃ M₃]
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
(h : M₂ →SL[σ₂₃] M₃)
(f : M₁ →SL[σ₁₂] M₂) :
@[simp, norm_cast]
theorem
continuous_linear_map.coe_comp'
{R₁ : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
[semiring R₁]
[semiring R₂]
[semiring R₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R₁ →+* R₃}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₂ M₂]
[module R₃ M₃]
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
(h : M₂ →SL[σ₂₃] M₃)
(f : M₁ →SL[σ₁₂] M₂) :
theorem
continuous_linear_map.comp_apply
{R₁ : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
[semiring R₁]
[semiring R₂]
[semiring R₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R₁ →+* R₃}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₂ M₂]
[module R₃ M₃]
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
(g : M₂ →SL[σ₂₃] M₃)
(f : M₁ →SL[σ₁₂] M₂)
(x : M₁) :
@[simp]
theorem
continuous_linear_map.comp_id
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(f : M₁ →SL[σ₁₂] M₂) :
f.comp (continuous_linear_map.id R₁ M₁) = f
@[simp]
theorem
continuous_linear_map.id_comp
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(f : M₁ →SL[σ₁₂] M₂) :
(continuous_linear_map.id R₂ M₂).comp f = f
@[simp]
theorem
continuous_linear_map.comp_zero
{R₁ : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
[semiring R₁]
[semiring R₂]
[semiring R₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R₁ →+* R₃}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₂ M₂]
[module R₃ M₃]
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
(g : M₂ →SL[σ₂₃] M₃) :
@[simp]
theorem
continuous_linear_map.zero_comp
{R₁ : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
[semiring R₁]
[semiring R₂]
[semiring R₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R₁ →+* R₃}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₂ M₂]
[module R₃ M₃]
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
(f : M₁ →SL[σ₁₂] M₂) :
@[simp]
theorem
continuous_linear_map.comp_add
{R₁ : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
[semiring R₁]
[semiring R₂]
[semiring R₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R₁ →+* R₃}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₂ M₂]
[module R₃ M₃]
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
[has_continuous_add M₂]
[has_continuous_add M₃]
(g : M₂ →SL[σ₂₃] M₃)
(f₁ f₂ : M₁ →SL[σ₁₂] M₂) :
@[simp]
theorem
continuous_linear_map.add_comp
{R₁ : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
[semiring R₁]
[semiring R₂]
[semiring R₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R₁ →+* R₃}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₂ M₂]
[module R₃ M₃]
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
[has_continuous_add M₃]
(g₁ g₂ : M₂ →SL[σ₂₃] M₃)
(f : M₁ →SL[σ₁₂] M₂) :
theorem
continuous_linear_map.comp_assoc
{R₁ : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
[semiring R₁]
[semiring R₂]
[semiring R₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R₁ →+* R₃}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
{M₄ : Type u_8}
[topological_space M₄]
[add_comm_monoid M₄]
[module R₁ M₁]
[module R₂ M₂]
[module R₃ M₃]
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
{R₄ : Type u_5}
[semiring R₄]
[module R₄ M₄]
{σ₁₄ : R₁ →+* R₄}
{σ₂₄ : R₂ →+* R₄}
{σ₃₄ : R₃ →+* R₄}
[ring_hom_comp_triple σ₁₃ σ₃₄ σ₁₄]
[ring_hom_comp_triple σ₂₃ σ₃₄ σ₂₄]
[ring_hom_comp_triple σ₁₂ σ₂₄ σ₁₄]
(h : M₃ →SL[σ₃₄] M₄)
(g : M₂ →SL[σ₂₃] M₃)
(f : M₁ →SL[σ₁₂] M₂) :
@[protected, instance]
def
continuous_linear_map.has_mul
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁] :
Equations
- continuous_linear_map.has_mul = {mul := continuous_linear_map.comp continuous_linear_map.has_mul._proof_1}
theorem
continuous_linear_map.mul_def
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁]
(f g : M₁ →L[R₁] M₁) :
@[simp]
theorem
continuous_linear_map.coe_mul
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁]
(f g : M₁ →L[R₁] M₁) :
theorem
continuous_linear_map.mul_apply
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁]
(f g : M₁ →L[R₁] M₁)
(x : M₁) :
@[protected]
def
continuous_linear_map.prod
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₁ M₂]
[module R₁ M₃]
(f₁ : M₁ →L[R₁] M₂)
(f₂ : M₁ →L[R₁] M₃) :
The cartesian product of two bounded linear maps, as a bounded linear map.
@[simp, norm_cast]
theorem
continuous_linear_map.coe_prod
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₁ M₂]
[module R₁ M₃]
(f₁ : M₁ →L[R₁] M₂)
(f₂ : M₁ →L[R₁] M₃) :
@[simp, norm_cast]
theorem
continuous_linear_map.prod_apply
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₁ M₂]
[module R₁ M₃]
(f₁ : M₁ →L[R₁] M₂)
(f₂ : M₁ →L[R₁] M₃)
(x : M₁) :
def
continuous_linear_map.inl
(R₁ : Type u_1)
[semiring R₁]
(M₁ : Type u_4)
[topological_space M₁]
[add_comm_monoid M₁]
(M₂ : Type u_6)
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₁ M₂] :
The left injection into a product is a continuous linear map.
Equations
- continuous_linear_map.inl R₁ M₁ M₂ = (continuous_linear_map.id R₁ M₁).prod 0
def
continuous_linear_map.inr
(R₁ : Type u_1)
[semiring R₁]
(M₁ : Type u_4)
[topological_space M₁]
[add_comm_monoid M₁]
(M₂ : Type u_6)
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₁ M₂] :
The right injection into a product is a continuous linear map.
Equations
- continuous_linear_map.inr R₁ M₁ M₂ = 0.prod (continuous_linear_map.id R₁ M₂)
@[simp]
theorem
continuous_linear_map.inl_apply
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₁ M₂]
(x : M₁) :
⇑(continuous_linear_map.inl R₁ M₁ M₂) x = (x, 0)
@[simp]
theorem
continuous_linear_map.inr_apply
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₁ M₂]
(x : M₂) :
⇑(continuous_linear_map.inr R₁ M₁ M₂) x = (0, x)
@[simp, norm_cast]
theorem
continuous_linear_map.coe_inl
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₁ M₂] :
↑(continuous_linear_map.inl R₁ M₁ M₂) = linear_map.inl R₁ M₁ M₂
@[simp, norm_cast]
theorem
continuous_linear_map.coe_inr
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₁ M₂] :
↑(continuous_linear_map.inr R₁ M₁ M₂) = linear_map.inr R₁ M₁ M₂
def
continuous_linear_map.ker
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(f : M₁ →SL[σ₁₂] M₂) :
submodule R₁ M₁
Kernel of a continuous linear map.
@[norm_cast]
theorem
continuous_linear_map.ker_coe
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(f : M₁ →SL[σ₁₂] M₂) :
@[simp]
theorem
continuous_linear_map.mem_ker
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
{f : M₁ →SL[σ₁₂] M₂}
{x : M₁} :
theorem
continuous_linear_map.is_closed_ker
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
[t1_space M₂]
(f : M₁ →SL[σ₁₂] M₂) :
@[simp]
theorem
continuous_linear_map.apply_ker
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(f : M₁ →SL[σ₁₂] M₂)
(x : ↥(f.ker)) :
theorem
continuous_linear_map.is_complete_ker
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{M' : Type u_3}
[uniform_space M']
[complete_space M']
[add_comm_monoid M']
[module R₁ M']
[t1_space M₂]
(f : M' →SL[σ₁₂] M₂) :
is_complete ↑(f.ker)
@[protected, instance]
def
continuous_linear_map.complete_space_ker
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{M' : Type u_3}
[uniform_space M']
[complete_space M']
[add_comm_monoid M']
[module R₁ M']
[t1_space M₂]
(f : M' →SL[σ₁₂] M₂) :
complete_space ↥(f.ker)
@[simp]
theorem
continuous_linear_map.ker_prod
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₁ M₂]
[module R₁ M₃]
(f : M₁ →L[R₁] M₂)
(g : M₁ →L[R₁] M₃) :
def
continuous_linear_map.range
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
[ring_hom_surjective σ₁₂]
(f : M₁ →SL[σ₁₂] M₂) :
submodule R₂ M₂
Range of a continuous linear map.
theorem
continuous_linear_map.range_coe
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
[ring_hom_surjective σ₁₂]
(f : M₁ →SL[σ₁₂] M₂) :
theorem
continuous_linear_map.mem_range
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
[ring_hom_surjective σ₁₂]
{f : M₁ →SL[σ₁₂] M₂}
{y : M₂} :
theorem
continuous_linear_map.mem_range_self
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
[ring_hom_surjective σ₁₂]
(f : M₁ →SL[σ₁₂] M₂)
(x : M₁) :
theorem
continuous_linear_map.range_prod_le
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₁ M₂]
[module R₁ M₃]
(f : M₁ →L[R₁] M₂)
(g : M₁ →L[R₁] M₃) :
def
continuous_linear_map.cod_restrict
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(f : M₁ →SL[σ₁₂] M₂)
(p : submodule R₂ M₂)
(h : ∀ (x : M₁), ⇑f x ∈ p) :
Restrict codomain of a continuous linear map.
Equations
- f.cod_restrict p h = {to_linear_map := linear_map.cod_restrict p ↑f h, cont := _}
@[norm_cast]
theorem
continuous_linear_map.coe_cod_restrict
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(f : M₁ →SL[σ₁₂] M₂)
(p : submodule R₂ M₂)
(h : ∀ (x : M₁), ⇑f x ∈ p) :
↑(f.cod_restrict p h) = linear_map.cod_restrict p ↑f h
@[simp]
theorem
continuous_linear_map.coe_cod_restrict_apply
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(f : M₁ →SL[σ₁₂] M₂)
(p : submodule R₂ M₂)
(h : ∀ (x : M₁), ⇑f x ∈ p)
(x : M₁) :
↑(⇑(f.cod_restrict p h) x) = ⇑f x
@[simp]
theorem
continuous_linear_map.ker_cod_restrict
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(f : M₁ →SL[σ₁₂] M₂)
(p : submodule R₂ M₂)
(h : ∀ (x : M₁), ⇑f x ∈ p) :
(f.cod_restrict p h).ker = f.ker
def
continuous_linear_map.subtype_val
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module 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, norm_cast]
theorem
continuous_linear_map.coe_subtype_val
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁]
(p : submodule R₁ M₁) :
@[simp, norm_cast]
theorem
continuous_linear_map.subtype_val_apply
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁]
(p : submodule R₁ M₁)
(x : ↥p) :
⇑(continuous_linear_map.subtype_val p) x = ↑x
def
continuous_linear_map.fst
(R₁ : Type u_1)
[semiring R₁]
(M₁ : Type u_4)
[topological_space M₁]
[add_comm_monoid M₁]
(M₂ : Type u_6)
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₁ M₂] :
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_19, cont := _}
def
continuous_linear_map.snd
(R₁ : Type u_1)
[semiring R₁]
(M₁ : Type u_4)
[topological_space M₁]
[add_comm_monoid M₁]
(M₂ : Type u_6)
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₁ M₂] :
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_19, cont := _}
@[simp, norm_cast]
theorem
continuous_linear_map.coe_fst
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₁ M₂] :
↑(continuous_linear_map.fst R₁ M₁ M₂) = linear_map.fst R₁ M₁ M₂
@[simp, norm_cast]
theorem
continuous_linear_map.coe_fst'
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₁ M₂] :
⇑(continuous_linear_map.fst R₁ M₁ M₂) = prod.fst
@[simp, norm_cast]
theorem
continuous_linear_map.coe_snd
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₁ M₂] :
↑(continuous_linear_map.snd R₁ M₁ M₂) = linear_map.snd R₁ M₁ M₂
@[simp, norm_cast]
theorem
continuous_linear_map.coe_snd'
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₁ M₂] :
⇑(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_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₁ M₂] :
(continuous_linear_map.fst R₁ M₁ M₂).prod (continuous_linear_map.snd R₁ M₁ M₂) = continuous_linear_map.id R₁ (M₁ × M₂)
@[simp]
theorem
continuous_linear_map.fst_comp_prod
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₁ M₂]
[module R₁ M₃]
(f : M₁ →L[R₁] M₂)
(g : M₁ →L[R₁] M₃) :
(continuous_linear_map.fst R₁ M₂ M₃).comp (f.prod g) = f
@[simp]
theorem
continuous_linear_map.snd_comp_prod
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₁ M₂]
[module R₁ M₃]
(f : M₁ →L[R₁] M₂)
(g : M₁ →L[R₁] M₃) :
(continuous_linear_map.snd R₁ M₂ M₃).comp (f.prod g) = g
def
continuous_linear_map.prod_map
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
{M₄ : Type u_8}
[topological_space M₄]
[add_comm_monoid M₄]
[module R₁ M₁]
[module R₁ M₂]
[module R₁ M₃]
[module R₁ M₄]
(f₁ : M₁ →L[R₁] M₂)
(f₂ : M₃ →L[R₁] M₄) :
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, norm_cast]
theorem
continuous_linear_map.coe_prod_map
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
{M₄ : Type u_8}
[topological_space M₄]
[add_comm_monoid M₄]
[module R₁ M₁]
[module R₁ M₂]
[module R₁ M₃]
[module R₁ M₄]
(f₁ : M₁ →L[R₁] M₂)
(f₂ : M₃ →L[R₁] M₄) :
@[simp, norm_cast]
theorem
continuous_linear_map.coe_prod_map'
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
{M₄ : Type u_8}
[topological_space M₄]
[add_comm_monoid M₄]
[module R₁ M₁]
[module R₁ M₂]
[module R₁ M₃]
[module R₁ M₄]
(f₁ : M₁ →L[R₁] M₂)
(f₂ : M₃ →L[R₁] M₄) :
def
continuous_linear_map.coprod
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₁ M₂]
[module R₁ M₃]
[has_continuous_add M₃]
(f₁ : M₁ →L[R₁] M₃)
(f₂ : M₂ →L[R₁] M₃) :
The continuous linear map given by (x, y) ↦ f₁ x + f₂ y.
@[simp, norm_cast]
theorem
continuous_linear_map.coe_coprod
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₁ M₂]
[module R₁ M₃]
[has_continuous_add M₃]
(f₁ : M₁ →L[R₁] M₃)
(f₂ : M₂ →L[R₁] M₃) :
@[simp]
theorem
continuous_linear_map.coprod_apply
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₁ M₂]
[module R₁ M₃]
[has_continuous_add M₃]
(f₁ : M₁ →L[R₁] M₃)
(f₂ : M₂ →L[R₁] M₃)
(x : M₁ × M₂) :
theorem
continuous_linear_map.range_coprod
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₁ M₂]
[module R₁ M₃]
[has_continuous_add M₃]
(f₁ : M₁ →L[R₁] M₃)
(f₂ : M₂ →L[R₁] M₃) :
def
continuous_linear_map.smul_right
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{R : Type u_9}
{S : Type u_10}
[semiring R]
[semiring S]
[module R M₁]
[module R M₂]
[module R S]
[module S M₂]
[is_scalar_tower R S M₂]
[topological_space S]
[has_continuous_smul S M₂]
(c : M₁ →L[R] S)
(f : M₂) :
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
- 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
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{R : Type u_9}
{S : Type u_10}
[semiring R]
[semiring S]
[module R M₁]
[module R M₂]
[module R S]
[module S M₂]
[is_scalar_tower R S M₂]
[topological_space S]
[has_continuous_smul S M₂]
{c : M₁ →L[R] S}
{f : M₂}
{x : M₁} :
⇑(c.smul_right f) x = ⇑c x • f
@[simp]
theorem
continuous_linear_map.image_smul_setₛₗ
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(f : M₁ →SL[σ₁₂] M₂)
(c : R₁)
(s : set M₁) :
theorem
continuous_linear_map.image_smul_set
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M'₁ : Type u_5}
[topological_space M'₁]
[add_comm_monoid M'₁]
[module R₁ M₁]
[module R₁ M'₁]
(fₗ : M₁ →L[R₁] M'₁)
(c : R₁)
(s : set M₁) :
theorem
continuous_linear_map.preimage_smul_setₛₗ
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(f : M₁ →SL[σ₁₂] M₂)
{c : R₁}
(hc : is_unit c)
(s : set M₂) :
theorem
continuous_linear_map.preimage_smul_set
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M'₁ : Type u_5}
[topological_space M'₁]
[add_comm_monoid M'₁]
[module R₁ M₁]
[module R₁ M'₁]
(fₗ : M₁ →L[R₁] M'₁)
{c : R₁}
(hc : is_unit c)
(s : set M'₁) :
@[simp]
theorem
continuous_linear_map.smul_right_one_one
{R₁ : Type u_1}
[semiring R₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₂]
[topological_space R₁]
[has_continuous_smul R₁ M₂]
(c : R₁ →L[R₁] M₂) :
1.smul_right (⇑c 1) = c
@[simp]
theorem
continuous_linear_map.smul_right_one_eq_iff
{R₁ : Type u_1}
[semiring R₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₂]
[topological_space R₁]
[has_continuous_smul R₁ M₂]
{f f' : M₂} :
1.smul_right f = 1.smul_right f' ↔ f = f'
theorem
continuous_linear_map.smul_right_comp
{R₁ : Type u_1}
[semiring R₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₂]
[topological_space R₁]
[has_continuous_smul R₁ M₂]
[has_continuous_mul R₁]
{x : M₂}
{c : R₁} :
(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]
[module R M]
{ι : Type u_4}
{φ : ι → Type u_5}
[Π (i : ι), topological_space (φ i)]
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(f : Π (i : ι), M →L[R] φ i) :
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.coe_pi'
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
[module R M]
{ι : Type u_4}
{φ : ι → Type u_5}
[Π (i : ι), topological_space (φ i)]
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(f : Π (i : ι), M →L[R] φ i) :
⇑(continuous_linear_map.pi f) = λ (c : M) (i : ι), ⇑(f i) c
@[simp]
theorem
continuous_linear_map.coe_pi
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
[module R M]
{ι : Type u_4}
{φ : ι → Type u_5}
[Π (i : ι), topological_space (φ i)]
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(f : Π (i : ι), M →L[R] φ i) :
↑(continuous_linear_map.pi f) = linear_map.pi (λ (i : ι), ↑(f i))
theorem
continuous_linear_map.pi_apply
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
[module R M]
{ι : Type u_4}
{φ : ι → Type u_5}
[Π (i : ι), topological_space (φ i)]
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(f : Π (i : ι), M →L[R] φ i)
(c : M)
(i : ι) :
⇑(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]
[module R M]
{ι : Type u_4}
{φ : ι → Type u_5}
[Π (i : ι), topological_space (φ i)]
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(f : Π (i : ι), M →L[R] φ i) :
continuous_linear_map.pi f = 0 ↔ ∀ (i : ι), f i = 0
theorem
continuous_linear_map.pi_zero
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
[module R M]
{ι : Type u_4}
{φ : ι → Type u_5}
[Π (i : ι), topological_space (φ i)]
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)] :
continuous_linear_map.pi (λ (i : ι), 0) = 0
theorem
continuous_linear_map.pi_comp
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
[module R M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M₂]
{ι : Type u_4}
{φ : ι → Type u_5}
[Π (i : ι), topological_space (φ i)]
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(f : Π (i : ι), M →L[R] φ i)
(g : M₂ →L[R] M) :
(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 : ι), module 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 : ι), module 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₂]
[module R M₂]
{ι : Type u_4}
{φ : ι → Type u_5}
[Π (i : ι), topological_space (φ i)]
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(f : Π (i : ι), M₂ →L[R] φ i)
(i : ι) :
(continuous_linear_map.proj i).comp (continuous_linear_map.pi f) = f i
theorem
continuous_linear_map.infi_ker_proj
{R : Type u_1}
[semiring R]
{ι : Type u_4}
{φ : ι → Type u_5}
[Π (i : ι), topological_space (φ i)]
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)] :
(⨅ (i : ι), (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 : ι), module R (φ i)]
{I J : set ι}
[decidable_pred (λ (i : ι), i ∈ I)]
(hd : disjoint I J)
(hu : set.univ ⊆ I ∪ J) :
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 := _}
@[protected]
theorem
continuous_linear_map.map_neg
{R : Type u_1}
[ring R]
{R₂ : Type u_2}
[ring R₂]
{M : Type u_3}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_4}
[topological_space M₂]
[add_comm_group M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
(f : M →SL[σ₁₂] M₂)
(x : M) :
@[protected]
theorem
continuous_linear_map.map_sub
{R : Type u_1}
[ring R]
{R₂ : Type u_2}
[ring R₂]
{M : Type u_3}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_4}
[topological_space M₂]
[add_comm_group M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
(f : M →SL[σ₁₂] M₂)
(x y : M) :
@[simp]
theorem
continuous_linear_map.sub_apply'
{R : Type u_1}
[ring R]
{R₂ : Type u_2}
[ring R₂]
{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₂]
{σ₁₂ : R →+* R₂}
(f g : M →SL[σ₁₂] M₂)
(x : M) :
theorem
continuous_linear_map.range_prod_eq
{R : Type u_1}
[ring R]
{M : Type u_3}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_4}
[topological_space M₂]
[add_comm_group M₂]
{M₃ : Type u_5}
[topological_space M₃]
[add_comm_group M₃]
[module R M]
[module R M₂]
[module R M₃]
{f : M →L[R] M₂}
{g : M →L[R] M₃}
(h : f.ker ⊔ g.ker = ⊤) :
theorem
continuous_linear_map.ker_prod_ker_le_ker_coprod
{R : Type u_1}
[ring R]
{M : Type u_3}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_4}
[topological_space M₂]
[add_comm_group M₂]
{M₃ : Type u_5}
[topological_space M₃]
[add_comm_group M₃]
[module R M]
[module R M₂]
[module R M₃]
[has_continuous_add M₃]
(f : M →L[R] M₃)
(g : M₂ →L[R] M₃) :
theorem
continuous_linear_map.ker_coprod_of_disjoint_range
{R : Type u_1}
[ring R]
{M : Type u_3}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_4}
[topological_space M₂]
[add_comm_group M₂]
{M₃ : Type u_5}
[topological_space M₃]
[add_comm_group M₃]
[module R M]
[module R M₂]
[module R M₃]
[has_continuous_add M₃]
(f : M →L[R] M₃)
(g : M₂ →L[R] M₃)
(hd : disjoint f.range g.range) :
@[protected, instance]
def
continuous_linear_map.has_neg
{R : Type u_1}
[ring R]
{R₂ : Type u_2}
[ring R₂]
{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₂]
{σ₁₂ : R →+* R₂}
[topological_add_group M₂] :
@[simp]
theorem
continuous_linear_map.neg_apply
{R : Type u_1}
[ring R]
{R₂ : Type u_2}
[ring R₂]
{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₂]
{σ₁₂ : R →+* R₂}
[topological_add_group M₂]
(f : M →SL[σ₁₂] M₂)
(x : M) :
@[simp, norm_cast]
theorem
continuous_linear_map.coe_neg
{R : Type u_1}
[ring R]
{R₂ : Type u_2}
[ring R₂]
{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₂]
{σ₁₂ : R →+* R₂}
[topological_add_group M₂]
(f : M →SL[σ₁₂] M₂) :
@[norm_cast]
theorem
continuous_linear_map.coe_neg'
{R : Type u_1}
[ring R]
{R₂ : Type u_2}
[ring R₂]
{M : Type u_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₂]
{σ₁₂ : R →+* R₂}
[topological_add_group M₂]
(f : M →SL[σ₁₂] M₂) :
@[protected, instance]
def
continuous_linear_map.has_sub
{R : Type u_1}
[ring R]
{R₂ : Type u_2}
[ring R₂]
{M : Type u_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₂]
{σ₁₂ : R →+* R₂}
[topological_add_group M₂] :
@[protected, instance]
def
continuous_linear_map.add_comm_group
{R : Type u_1}
[ring R]
{R₂ : Type u_2}
[ring R₂]
{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₂]
{σ₁₂ : R →+* R₂}
[topological_add_group M₂] :
add_comm_group (M →SL[σ₁₂] 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 := _, nsmul := has_scalar.smul add_monoid.has_scalar_nat, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg continuous_linear_map.has_neg, sub := has_sub.sub continuous_linear_map.has_sub, sub_eq_add_neg := _, zsmul := has_scalar.smul mul_action.to_has_scalar, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}
theorem
continuous_linear_map.sub_apply
{R : Type u_1}
[ring R]
{R₂ : Type u_2}
[ring R₂]
{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₂]
{σ₁₂ : R →+* R₂}
[topological_add_group M₂]
(f g : M →SL[σ₁₂] M₂)
(x : M) :
@[simp, norm_cast]
theorem
continuous_linear_map.coe_sub
{R : Type u_1}
[ring R]
{R₂ : Type u_2}
[ring R₂]
{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₂]
{σ₁₂ : R →+* R₂}
[topological_add_group M₂]
(f g : M →SL[σ₁₂] M₂) :
@[simp, norm_cast]
theorem
continuous_linear_map.coe_sub'
{R : Type u_1}
[ring R]
{R₂ : Type u_2}
[ring R₂]
{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₂]
{σ₁₂ : R →+* R₂}
[topological_add_group M₂]
(f g : M →SL[σ₁₂] M₂) :
@[protected, instance]
def
continuous_linear_map.ring
{R : Type u_1}
[ring R]
{M : Type u_3}
[topological_space M]
[add_comm_group M]
[module 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 := _, nsmul := add_comm_group.nsmul continuous_linear_map.add_comm_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg continuous_linear_map.add_comm_group, sub := add_comm_group.sub continuous_linear_map.add_comm_group, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul continuous_linear_map.add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := has_mul.mul continuous_linear_map.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := monoid.npow._default 1 has_mul.mul continuous_linear_map.ring._proof_15 continuous_linear_map.ring._proof_16, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}
theorem
continuous_linear_map.smul_right_one_pow
{R : Type u_1}
[ring R]
[topological_space R]
[topological_ring R]
(c : R)
(n : ℕ) :
1.smul_right c ^ n = 1.smul_right (c ^ n)
def
continuous_linear_map.proj_ker_of_right_inverse
{R : Type u_1}
[ring R]
{R₂ : Type u_2}
[ring R₂]
{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₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[topological_add_group M]
(f₁ : M →SL[σ₁₂] M₂)
(f₂ : M₂ →SL[σ₂₁] M)
(h : function.right_inverse ⇑f₂ ⇑f₁) :
Given a right inverse f₂ : M₂ →L[R] M to f₁ : M →L[R] M₂,
proj_ker_of_right_inverse f₁ f₂ h is the projection M →L[R] f₁.ker along f₂.range.
Equations
- 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]
{R₂ : Type u_2}
[ring R₂]
{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₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[topological_add_group M]
(f₁ : M →SL[σ₁₂] M₂)
(f₂ : M₂ →SL[σ₂₁] M)
(h : function.right_inverse ⇑f₂ ⇑f₁)
(x : M) :
@[simp]
theorem
continuous_linear_map.proj_ker_of_right_inverse_apply_idem
{R : Type u_1}
[ring R]
{R₂ : Type u_2}
[ring R₂]
{M : Type u_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₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[topological_add_group M]
(f₁ : M →SL[σ₁₂] M₂)
(f₂ : M₂ →SL[σ₂₁] M)
(h : function.right_inverse ⇑f₂ ⇑f₁)
(x : ↥(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]
{R₂ : Type u_2}
[ring R₂]
{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₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[topological_add_group M]
(f₁ : M →SL[σ₁₂] M₂)
(f₂ : M₂ →SL[σ₂₁] M)
(h : function.right_inverse ⇑f₂ ⇑f₁)
(y : M₂) :
⇑(f₁.proj_ker_of_right_inverse f₂ h) (⇑f₂ y) = 0
@[simp]
theorem
continuous_linear_map.smul_comp
{R : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
{S₃ : Type u_5}
[semiring R]
[semiring R₂]
[semiring R₃]
[monoid S₃]
{M : Type u_6}
[topological_space M]
[add_comm_monoid M]
[module R M]
{M₂ : Type u_7}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{M₃ : Type u_8}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₃ M₃]
[distrib_mul_action S₃ M₃]
[smul_comm_class R₃ S₃ M₃]
[has_continuous_const_smul S₃ M₃]
{σ₁₂ : R →+* R₂}
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R →+* R₃}
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
(c : S₃)
(h : M₂ →SL[σ₂₃] M₃)
(f : M →SL[σ₁₂] M₂) :
@[simp]
theorem
continuous_linear_map.comp_smul
{R : Type u_1}
{S : Type u_4}
[semiring R]
[monoid S]
{M : Type u_6}
[topological_space M]
[add_comm_monoid M]
[module R M]
{N₂ : Type u_9}
[topological_space N₂]
[add_comm_monoid N₂]
[module R N₂]
{N₃ : Type u_10}
[topological_space N₃]
[add_comm_monoid N₃]
[module R N₃]
[distrib_mul_action S N₃]
[smul_comm_class R S N₃]
[has_continuous_const_smul S N₃]
[distrib_mul_action S N₂]
[has_continuous_const_smul S N₂]
[smul_comm_class R S N₂]
[linear_map.compatible_smul N₂ N₃ S R]
(hₗ : N₂ →L[R] N₃)
(c : S)
(fₗ : M →L[R] N₂) :
@[simp]
theorem
continuous_linear_map.comp_smulₛₗ
{R : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
[semiring R]
[semiring R₂]
[semiring R₃]
{M : Type u_6}
[topological_space M]
[add_comm_monoid M]
[module R M]
{M₂ : Type u_7}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{M₃ : Type u_8}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₃ M₃]
{σ₁₂ : R →+* R₂}
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R →+* R₃}
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
[smul_comm_class R₂ R₂ M₂]
[smul_comm_class R₃ R₃ M₃]
[has_continuous_const_smul R₂ M₂]
[has_continuous_const_smul R₃ M₃]
(h : M₂ →SL[σ₂₃] M₃)
(c : R₂)
(f : M →SL[σ₁₂] M₂) :
@[protected, instance]
def
continuous_linear_map.distrib_mul_action
{R : Type u_1}
{R₂ : Type u_2}
{S₃ : Type u_5}
[semiring R]
[semiring R₂]
[monoid S₃]
{M : Type u_6}
[topological_space M]
[add_comm_monoid M]
[module R M]
{M₂ : Type u_7}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
[distrib_mul_action S₃ M₂]
[has_continuous_const_smul S₃ M₂]
[smul_comm_class R₂ S₃ M₂]
[has_continuous_add M₂] :
distrib_mul_action S₃ (M →SL[σ₁₂] M₂)
Equations
- continuous_linear_map.distrib_mul_action = {to_mul_action := continuous_linear_map.mul_action _inst_29, smul_add := _, smul_zero := _}
def
continuous_linear_map.prod_equiv
{R : Type u_1}
[semiring R]
{M : Type u_6}
[topological_space M]
[add_comm_monoid M]
[module R M]
{N₂ : Type u_9}
[topological_space N₂]
[add_comm_monoid N₂]
[module R N₂]
{N₃ : Type u_10}
[topological_space N₃]
[add_comm_monoid N₃]
[module R N₃] :
continuous_linear_map.prod as an equiv.
@[simp]
theorem
continuous_linear_map.prod_equiv_apply
{R : Type u_1}
[semiring R]
{M : Type u_6}
[topological_space M]
[add_comm_monoid M]
[module R M]
{N₂ : Type u_9}
[topological_space N₂]
[add_comm_monoid N₂]
[module R N₂]
{N₃ : Type u_10}
[topological_space N₃]
[add_comm_monoid N₃]
[module R N₃]
(f : (M →L[R] N₂) × (M →L[R] N₃)) :
theorem
continuous_linear_map.prod_ext_iff
{R : Type u_1}
[semiring R]
{M : Type u_6}
[topological_space M]
[add_comm_monoid M]
[module R M]
{N₂ : Type u_9}
[topological_space N₂]
[add_comm_monoid N₂]
[module R N₂]
{N₃ : Type u_10}
[topological_space N₃]
[add_comm_monoid N₃]
[module R N₃]
{f g : M × N₂ →L[R] N₃} :
f = g ↔ f.comp (continuous_linear_map.inl R M N₂) = g.comp (continuous_linear_map.inl R M N₂) ∧ f.comp (continuous_linear_map.inr R M N₂) = g.comp (continuous_linear_map.inr R M N₂)
@[ext]
theorem
continuous_linear_map.prod_ext
{R : Type u_1}
[semiring R]
{M : Type u_6}
[topological_space M]
[add_comm_monoid M]
[module R M]
{N₂ : Type u_9}
[topological_space N₂]
[add_comm_monoid N₂]
[module R N₂]
{N₃ : Type u_10}
[topological_space N₃]
[add_comm_monoid N₃]
[module R N₃]
{f g : M × N₂ →L[R] N₃}
(hl : f.comp (continuous_linear_map.inl R M N₂) = g.comp (continuous_linear_map.inl R M N₂))
(hr : f.comp (continuous_linear_map.inr R M N₂) = g.comp (continuous_linear_map.inr R M N₂)) :
f = g
@[protected, instance]
def
continuous_linear_map.module
{R : Type u_1}
{R₃ : Type u_3}
{S₃ : Type u_5}
[semiring R]
[semiring R₃]
[semiring S₃]
{M : Type u_6}
[topological_space M]
[add_comm_monoid M]
[module R M]
{M₃ : Type u_8}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₃ M₃]
[module S₃ M₃]
[smul_comm_class R₃ S₃ M₃]
[has_continuous_const_smul S₃ M₃]
{σ₁₃ : R →+* R₃}
[has_continuous_add M₃] :
Equations
- continuous_linear_map.module = {to_distrib_mul_action := continuous_linear_map.distrib_mul_action _inst_32, add_smul := _, zero_smul := _}
@[protected, instance]
def
continuous_linear_map.is_central_scalar
{R : Type u_1}
{R₃ : Type u_3}
{S₃ : Type u_5}
[semiring R]
[semiring R₃]
[semiring S₃]
{M : Type u_6}
[topological_space M]
[add_comm_monoid M]
[module R M]
{M₃ : Type u_8}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₃ M₃]
[module S₃ M₃]
[smul_comm_class R₃ S₃ M₃]
[has_continuous_const_smul S₃ M₃]
{σ₁₃ : R →+* R₃}
[has_continuous_add M₃]
[module S₃ᵐᵒᵖ M₃]
[is_central_scalar S₃ M₃] :
is_central_scalar S₃ (M →SL[σ₁₃] M₃)
@[simp]
theorem
continuous_linear_map.prodₗ_apply
{R : Type u_1}
(S : Type u_4)
[semiring R]
[semiring S]
{M : Type u_6}
[topological_space M]
[add_comm_monoid M]
[module R M]
{N₂ : Type u_9}
[topological_space N₂]
[add_comm_monoid N₂]
[module R N₂]
{N₃ : Type u_10}
[topological_space N₃]
[add_comm_monoid N₃]
[module R N₃]
[module S N₂]
[has_continuous_const_smul S N₂]
[smul_comm_class R S N₂]
[module S N₃]
[smul_comm_class R S N₃]
[has_continuous_const_smul S N₃]
[has_continuous_add N₂]
[has_continuous_add N₃]
(ᾰ : (M →L[R] N₂) × (M →L[R] N₃)) :
def
continuous_linear_map.prodₗ
{R : Type u_1}
(S : Type u_4)
[semiring R]
[semiring S]
{M : Type u_6}
[topological_space M]
[add_comm_monoid M]
[module R M]
{N₂ : Type u_9}
[topological_space N₂]
[add_comm_monoid N₂]
[module R N₂]
{N₃ : Type u_10}
[topological_space N₃]
[add_comm_monoid N₃]
[module R N₃]
[module S N₂]
[has_continuous_const_smul S N₂]
[smul_comm_class R S N₂]
[module S N₃]
[smul_comm_class R S N₃]
[has_continuous_const_smul S N₃]
[has_continuous_add N₂]
[has_continuous_add N₃] :
continuous_linear_map.prod as a linear_equiv.
Equations
- continuous_linear_map.prodₗ S = {to_fun := continuous_linear_map.prod_equiv.to_fun, map_add' := _, map_smul' := _, inv_fun := continuous_linear_map.prod_equiv.inv_fun, left_inv := _, right_inv := _}
def
continuous_linear_map.coe_lm
{R : Type u_1}
(S : Type u_4)
[semiring R]
[semiring S]
{M : Type u_6}
[topological_space M]
[add_comm_monoid M]
[module R M]
{N₃ : Type u_10}
[topological_space N₃]
[add_comm_monoid N₃]
[module R N₃]
[module S N₃]
[smul_comm_class R S N₃]
[has_continuous_const_smul S N₃]
[has_continuous_add N₃] :
The coercion from M →L[R] M₂ to M →ₗ[R] M₂, as a linear map.
Equations
- continuous_linear_map.coe_lm S = {to_fun := coe coe_to_lift, map_add' := _, map_smul' := _}
@[simp]
theorem
continuous_linear_map.coe_lm_apply
{R : Type u_1}
(S : Type u_4)
[semiring R]
[semiring S]
{M : Type u_6}
[topological_space M]
[add_comm_monoid M]
[module R M]
{N₃ : Type u_10}
[topological_space N₃]
[add_comm_monoid N₃]
[module R N₃]
[module S N₃]
[smul_comm_class R S N₃]
[has_continuous_const_smul S N₃]
[has_continuous_add N₃]
(ᾰ : M →L[R] N₃) :
⇑(continuous_linear_map.coe_lm S) ᾰ = ↑ᾰ
@[simp]
theorem
continuous_linear_map.coe_lmₛₗ_apply
{R : Type u_1}
{R₃ : Type u_3}
{S₃ : Type u_5}
[semiring R]
[semiring R₃]
[semiring S₃]
{M : Type u_6}
[topological_space M]
[add_comm_monoid M]
[module R M]
{M₃ : Type u_8}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₃ M₃]
[module S₃ M₃]
[smul_comm_class R₃ S₃ M₃]
[has_continuous_const_smul S₃ M₃]
(σ₁₃ : R →+* R₃)
[has_continuous_add M₃]
(ᾰ : M →SL[σ₁₃] M₃) :
⇑(continuous_linear_map.coe_lmₛₗ σ₁₃) ᾰ = ↑ᾰ
def
continuous_linear_map.coe_lmₛₗ
{R : Type u_1}
{R₃ : Type u_3}
{S₃ : Type u_5}
[semiring R]
[semiring R₃]
[semiring S₃]
{M : Type u_6}
[topological_space M]
[add_comm_monoid M]
[module R M]
{M₃ : Type u_8}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₃ M₃]
[module S₃ M₃]
[smul_comm_class R₃ S₃ M₃]
[has_continuous_const_smul S₃ M₃]
(σ₁₃ : R →+* R₃)
[has_continuous_add M₃] :
The coercion from M →SL[σ] M₂ to M →ₛₗ[σ] M₂, as a linear map.
Equations
- continuous_linear_map.coe_lmₛₗ σ₁₃ = {to_fun := coe coe_to_lift, map_add' := _, map_smul' := _}
def
continuous_linear_map.smul_rightₗ
{R : Type u_1}
{S : Type u_2}
{T : Type u_3}
{M : Type u_4}
{M₂ : Type u_5}
[ring R]
[ring S]
[ring T]
[module R S]
[add_comm_group M₂]
[module R M₂]
[module S M₂]
[is_scalar_tower R S M₂]
[topological_space S]
[topological_space M₂]
[has_continuous_smul S M₂]
[topological_space M]
[add_comm_group M]
[module R M]
[topological_add_group M₂]
[module T M₂]
[has_continuous_const_smul T M₂]
[smul_comm_class R T M₂]
[smul_comm_class S T M₂]
(c : M →L[R] S) :
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
- c.smul_rightₗ = {to_fun := c.smul_right, map_add' := _, map_smul' := _}
@[simp]
theorem
continuous_linear_map.coe_smul_rightₗ
{R : Type u_1}
{S : Type u_2}
{T : Type u_3}
{M : Type u_4}
{M₂ : Type u_5}
[ring R]
[ring S]
[ring T]
[module R S]
[add_comm_group M₂]
[module R M₂]
[module S M₂]
[is_scalar_tower R S M₂]
[topological_space S]
[topological_space M₂]
[has_continuous_smul S M₂]
[topological_space M]
[add_comm_group M]
[module R M]
[topological_add_group M₂]
[module T M₂]
[has_continuous_const_smul T M₂]
[smul_comm_class R T M₂]
[smul_comm_class S T M₂]
(c : M →L[R] S) :
⇑(c.smul_rightₗ) = c.smul_right
noncomputable
def
continuous_linear_map.det
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[topological_space M]
[add_comm_group M]
[module R M]
(A : M →L[R] M) :
R
The determinant of a continuous linear map, mainly as a convenience device to be able to
write A.det instead of (A : M →ₗ[R] M).det.
Equations
- A.det = ⇑linear_map.det ↑A
@[protected, instance]
def
continuous_linear_map.algebra
{R : Type u_1}
[comm_ring R]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_group M₂]
[module R M₂]
[topological_add_group M₂]
[has_continuous_const_smul R M₂] :
Equations
- continuous_linear_map.algebra = algebra.of_module continuous_linear_map.algebra._proof_3 continuous_linear_map.algebra._proof_4
def
continuous_linear_map.restrict_scalars
{A : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[ring A]
[add_comm_group M]
[add_comm_group M₂]
[module A M]
[module A M₂]
[topological_space M]
[topological_space M₂]
(R : Type u_4)
[ring R]
[module R M]
[module R M₂]
[linear_map.compatible_smul M M₂ R A]
(f : M →L[A] M₂) :
If A is an R-algebra, then a continuous A-linear map can be interpreted as a continuous
R-linear map. We assume linear_map.compatible_smul M M₂ R A to match assumptions of
linear_map.map_smul_of_tower.
Equations
- continuous_linear_map.restrict_scalars R f = {to_linear_map := linear_map.restrict_scalars R ↑f, cont := _}
@[simp, norm_cast]
theorem
continuous_linear_map.coe_restrict_scalars
{A : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[ring A]
[add_comm_group M]
[add_comm_group M₂]
[module A M]
[module A M₂]
[topological_space M]
[topological_space M₂]
{R : Type u_4}
[ring R]
[module R M]
[module R M₂]
[linear_map.compatible_smul M M₂ R A]
(f : M →L[A] M₂) :
@[simp]
theorem
continuous_linear_map.coe_restrict_scalars'
{A : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[ring A]
[add_comm_group M]
[add_comm_group M₂]
[module A M]
[module A M₂]
[topological_space M]
[topological_space M₂]
{R : Type u_4}
[ring R]
[module R M]
[module R M₂]
[linear_map.compatible_smul M M₂ R A]
(f : M →L[A] M₂) :
@[simp]
theorem
continuous_linear_map.restrict_scalars_zero
{A : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[ring A]
[add_comm_group M]
[add_comm_group M₂]
[module A M]
[module A M₂]
[topological_space M]
[topological_space M₂]
{R : Type u_4}
[ring R]
[module R M]
[module R M₂]
[linear_map.compatible_smul M M₂ R A] :
@[simp]
theorem
continuous_linear_map.restrict_scalars_add
{A : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[ring A]
[add_comm_group M]
[add_comm_group M₂]
[module A M]
[module A M₂]
[topological_space M]
[topological_space M₂]
{R : Type u_4}
[ring R]
[module R M]
[module R M₂]
[linear_map.compatible_smul M M₂ R A]
[topological_add_group M₂]
(f g : M →L[A] M₂) :
@[simp]
theorem
continuous_linear_map.restrict_scalars_neg
{A : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[ring A]
[add_comm_group M]
[add_comm_group M₂]
[module A M]
[module A M₂]
[topological_space M]
[topological_space M₂]
{R : Type u_4}
[ring R]
[module R M]
[module R M₂]
[linear_map.compatible_smul M M₂ R A]
[topological_add_group M₂]
(f : M →L[A] M₂) :
@[simp]
theorem
continuous_linear_map.restrict_scalars_smul
{A : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[ring A]
[add_comm_group M]
[add_comm_group M₂]
[module A M]
[module A M₂]
[topological_space M]
[topological_space M₂]
{R : Type u_4}
[ring R]
[module R M]
[module R M₂]
[linear_map.compatible_smul M M₂ R A]
{S : Type u_5}
[ring S]
[module S M₂]
[has_continuous_const_smul S M₂]
[smul_comm_class A S M₂]
[smul_comm_class R S M₂]
(c : S)
(f : M →L[A] M₂) :
def
continuous_linear_map.restrict_scalarsₗ
(A : Type u_1)
(M : Type u_2)
(M₂ : Type u_3)
[ring A]
[add_comm_group M]
[add_comm_group M₂]
[module A M]
[module A M₂]
[topological_space M]
[topological_space M₂]
(R : Type u_4)
[ring R]
[module R M]
[module R M₂]
[linear_map.compatible_smul M M₂ R A]
(S : Type u_5)
[ring S]
[module S M₂]
[has_continuous_const_smul S M₂]
[smul_comm_class A S M₂]
[smul_comm_class R S M₂]
[topological_add_group M₂] :
continuous_linear_map.restrict_scalars as a linear_map. See also
continuous_linear_map.restrict_scalarsL.
Equations
- continuous_linear_map.restrict_scalarsₗ A M M₂ R S = {to_fun := continuous_linear_map.restrict_scalars R _inst_11, map_add' := _, map_smul' := _}
@[simp]
theorem
continuous_linear_map.coe_restrict_scalarsₗ
{A : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[ring A]
[add_comm_group M]
[add_comm_group M₂]
[module A M]
[module A M₂]
[topological_space M]
[topological_space M₂]
{R : Type u_4}
[ring R]
[module R M]
[module R M₂]
[linear_map.compatible_smul M M₂ R A]
{S : Type u_5}
[ring S]
[module S M₂]
[has_continuous_const_smul S M₂]
[smul_comm_class A S M₂]
[smul_comm_class R S M₂]
[topological_add_group M₂] :
def
continuous_linear_equiv.to_continuous_linear_map
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂) :
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 := _}
@[protected, instance]
def
continuous_linear_equiv.continuous_linear_map.has_coe
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂] :
Coerce continuous linear equivs to continuous linear maps.
@[protected, instance]
def
continuous_linear_equiv.has_coe_to_fun
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂] :
has_coe_to_fun (M₁ ≃SL[σ₁₂] M₂) (λ (_x : M₁ ≃SL[σ₁₂] M₂), M₁ → M₂)
Coerce continuous linear equivs to maps.
@[simp]
theorem
continuous_linear_equiv.coe_def_rev
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂) :
theorem
continuous_linear_equiv.coe_apply
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(b : M₁) :
@[simp]
theorem
continuous_linear_equiv.coe_to_linear_equiv
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(f : M₁ ≃SL[σ₁₂] M₂) :
⇑(f.to_linear_equiv) = ⇑f
@[simp, norm_cast]
theorem
continuous_linear_equiv.coe_coe
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂) :
theorem
continuous_linear_equiv.to_linear_equiv_injective
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂] :
@[ext]
theorem
continuous_linear_equiv.ext
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
{f g : M₁ ≃SL[σ₁₂] M₂}
(h : ⇑f = ⇑g) :
f = g
theorem
continuous_linear_equiv.coe_injective
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂] :
@[simp, norm_cast]
theorem
continuous_linear_equiv.coe_inj
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
{e e' : M₁ ≃SL[σ₁₂] M₂} :
def
continuous_linear_equiv.to_homeomorph
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂) :
M₁ ≃ₜ M₂
A continuous linear equivalence induces a homeomorphism.
Equations
- e.to_homeomorph = {to_equiv := e.to_linear_equiv.to_equiv, continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
theorem
continuous_linear_equiv.coe_to_homeomorph
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂) :
⇑(e.to_homeomorph) = ⇑e
theorem
continuous_linear_equiv.image_closure
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(s : set M₁) :
theorem
continuous_linear_equiv.preimage_closure
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(s : set M₂) :
@[simp]
theorem
continuous_linear_equiv.is_closed_image
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
{s : set M₁} :
theorem
continuous_linear_equiv.map_nhds_eq
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(x : M₁) :
@[simp]
theorem
continuous_linear_equiv.map_zero
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂) :
@[simp]
theorem
continuous_linear_equiv.map_add
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(x y : M₁) :
@[simp]
theorem
continuous_linear_equiv.map_smulₛₗ
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(c : R₁)
(x : M₁) :
@[simp]
theorem
continuous_linear_equiv.map_smul
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₁ M₂]
(e : M₁ ≃L[R₁] M₂)
(c : R₁)
(x : M₁) :
@[simp]
theorem
continuous_linear_equiv.map_eq_zero_iff
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
{x : M₁} :
@[protected, continuity]
theorem
continuous_linear_equiv.continuous
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂) :
@[protected]
theorem
continuous_linear_equiv.continuous_on
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
{s : set M₁} :
continuous_on ⇑e s
@[protected]
theorem
continuous_linear_equiv.continuous_at
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
{x : M₁} :
continuous_at ⇑e x
@[protected]
theorem
continuous_linear_equiv.continuous_within_at
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
{s : set M₁}
{x : M₁} :
continuous_within_at ⇑e s x
theorem
continuous_linear_equiv.comp_continuous_on_iff
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
{α : Type u_3}
[topological_space α]
(e : M₁ ≃SL[σ₁₂] M₂)
{f : α → M₁}
{s : set α} :
continuous_on (⇑e ∘ f) s ↔ continuous_on f s
theorem
continuous_linear_equiv.comp_continuous_iff
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
{α : Type u_3}
[topological_space α]
(e : M₁ ≃SL[σ₁₂] M₂)
{f : α → M₁} :
continuous (⇑e ∘ f) ↔ continuous f
theorem
continuous_linear_equiv.ext₁
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁]
[topological_space R₁]
{f g : R₁ ≃L[R₁] M₁}
(h : ⇑f 1 = ⇑g 1) :
f = g
An extensionality lemma for R ≃L[R] M.
@[protected]
def
continuous_linear_equiv.refl
(R₁ : Type u_1)
[semiring R₁]
(M₁ : Type u_4)
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁] :
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, norm_cast]
theorem
continuous_linear_equiv.coe_refl
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁] :
↑(continuous_linear_equiv.refl R₁ M₁) = continuous_linear_map.id R₁ M₁
@[simp, norm_cast]
theorem
continuous_linear_equiv.coe_refl'
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁] :
⇑(continuous_linear_equiv.refl R₁ M₁) = id
@[protected]
def
continuous_linear_equiv.symm
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂) :
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}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂) :
@[simp]
theorem
continuous_linear_equiv.symm_to_homeomorph
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂) :
def
continuous_linear_equiv.simps.apply
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(h : M₁ ≃SL[σ₁₂] M₂) :
M₁ → M₂
See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.
Equations
def
continuous_linear_equiv.simps.symm_apply
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(h : M₁ ≃SL[σ₁₂] M₂) :
M₂ → M₁
See Note [custom simps projection]
Equations
theorem
continuous_linear_equiv.symm_map_nhds_eq
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(x : M₁) :
@[protected]
def
continuous_linear_equiv.trans
{R₁ : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
[semiring R₁]
[semiring R₂]
[semiring R₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{σ₂₃ : R₂ →+* R₃}
{σ₃₂ : R₃ →+* R₂}
[ring_hom_inv_pair σ₂₃ σ₃₂]
[ring_hom_inv_pair σ₃₂ σ₂₃]
{σ₁₃ : R₁ →+* R₃}
{σ₃₁ : R₃ →+* R₁}
[ring_hom_inv_pair σ₁₃ σ₃₁]
[ring_hom_inv_pair σ₃₁ σ₁₃]
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
[ring_hom_comp_triple σ₃₂ σ₂₁ σ₃₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₂ M₂]
[module R₃ M₃]
(e₁ : M₁ ≃SL[σ₁₂] M₂)
(e₂ : M₂ ≃SL[σ₂₃] M₃) :
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}
{R₂ : Type u_2}
{R₃ : Type u_3}
[semiring R₁]
[semiring R₂]
[semiring R₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{σ₂₃ : R₂ →+* R₃}
{σ₃₂ : R₃ →+* R₂}
[ring_hom_inv_pair σ₂₃ σ₃₂]
[ring_hom_inv_pair σ₃₂ σ₂₃]
{σ₁₃ : R₁ →+* R₃}
{σ₃₁ : R₃ →+* R₁}
[ring_hom_inv_pair σ₁₃ σ₃₁]
[ring_hom_inv_pair σ₃₁ σ₁₃]
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
[ring_hom_comp_triple σ₃₂ σ₂₁ σ₃₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₂ M₂]
[module R₃ M₃]
(e₁ : M₁ ≃SL[σ₁₂] M₂)
(e₂ : M₂ ≃SL[σ₂₃] M₃) :
(e₁.trans e₂).to_linear_equiv = e₁.to_linear_equiv.trans e₂.to_linear_equiv
def
continuous_linear_equiv.prod
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
{M₄ : Type u_8}
[topological_space M₄]
[add_comm_monoid M₄]
[module R₁ M₁]
[module R₁ M₂]
[module R₁ M₃]
[module R₁ M₄]
(e : M₁ ≃L[R₁] M₂)
(e' : M₃ ≃L[R₁] M₄) :
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, norm_cast]
theorem
continuous_linear_equiv.prod_apply
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
{M₄ : Type u_8}
[topological_space M₄]
[add_comm_monoid M₄]
[module R₁ M₁]
[module R₁ M₂]
[module R₁ M₃]
[module R₁ M₄]
(e : M₁ ≃L[R₁] M₂)
(e' : M₃ ≃L[R₁] M₄)
(x : M₁ × M₃) :
@[simp, norm_cast]
theorem
continuous_linear_equiv.coe_prod
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
{M₄ : Type u_8}
[topological_space M₄]
[add_comm_monoid M₄]
[module R₁ M₁]
[module R₁ M₂]
[module R₁ M₃]
[module R₁ M₄]
(e : M₁ ≃L[R₁] M₂)
(e' : M₃ ≃L[R₁] M₄) :
theorem
continuous_linear_equiv.bijective
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂) :
theorem
continuous_linear_equiv.injective
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂) :
theorem
continuous_linear_equiv.surjective
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂) :
@[simp]
theorem
continuous_linear_equiv.trans_apply
{R₁ : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
[semiring R₁]
[semiring R₂]
[semiring R₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{σ₂₃ : R₂ →+* R₃}
{σ₃₂ : R₃ →+* R₂}
[ring_hom_inv_pair σ₂₃ σ₃₂]
[ring_hom_inv_pair σ₃₂ σ₂₃]
{σ₁₃ : R₁ →+* R₃}
{σ₃₁ : R₃ →+* R₁}
[ring_hom_inv_pair σ₁₃ σ₃₁]
[ring_hom_inv_pair σ₃₁ σ₁₃]
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
[ring_hom_comp_triple σ₃₂ σ₂₁ σ₃₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₂ M₂]
[module R₃ M₃]
(e₁ : M₁ ≃SL[σ₁₂] M₂)
(e₂ : M₂ ≃SL[σ₂₃] M₃)
(c : M₁) :
@[simp]
theorem
continuous_linear_equiv.apply_symm_apply
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(c : M₂) :
@[simp]
theorem
continuous_linear_equiv.symm_apply_apply
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(b : M₁) :
@[simp]
theorem
continuous_linear_equiv.symm_trans_apply
{R₁ : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
[semiring R₁]
[semiring R₂]
[semiring R₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{σ₂₃ : R₂ →+* R₃}
{σ₃₂ : R₃ →+* R₂}
[ring_hom_inv_pair σ₂₃ σ₃₂]
[ring_hom_inv_pair σ₃₂ σ₂₃]
{σ₁₃ : R₁ →+* R₃}
{σ₃₁ : R₃ →+* R₁}
[ring_hom_inv_pair σ₁₃ σ₃₁]
[ring_hom_inv_pair σ₃₁ σ₁₃]
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
[ring_hom_comp_triple σ₃₂ σ₂₁ σ₃₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₂ M₂]
[module R₃ M₃]
(e₁ : M₂ ≃SL[σ₂₁] M₁)
(e₂ : M₃ ≃SL[σ₃₂] M₂)
(c : M₁) :
@[simp]
theorem
continuous_linear_equiv.symm_image_image
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(s : set M₁) :
@[simp]
theorem
continuous_linear_equiv.image_symm_image
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(s : set M₂) :
@[simp, norm_cast]
theorem
continuous_linear_equiv.comp_coe
{R₁ : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
[semiring R₁]
[semiring R₂]
[semiring R₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{σ₂₃ : R₂ →+* R₃}
{σ₃₂ : R₃ →+* R₂}
[ring_hom_inv_pair σ₂₃ σ₃₂]
[ring_hom_inv_pair σ₃₂ σ₂₃]
{σ₁₃ : R₁ →+* R₃}
{σ₃₁ : R₃ →+* R₁}
[ring_hom_inv_pair σ₁₃ σ₃₁]
[ring_hom_inv_pair σ₃₁ σ₁₃]
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
[ring_hom_comp_triple σ₃₂ σ₂₁ σ₃₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₂ M₂]
[module R₃ M₃]
(f : M₁ ≃SL[σ₁₂] M₂)
(f' : M₂ ≃SL[σ₂₃] M₃) :
@[simp]
theorem
continuous_linear_equiv.coe_comp_coe_symm
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂) :
@[simp]
theorem
continuous_linear_equiv.coe_symm_comp_coe
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂) :
@[simp]
theorem
continuous_linear_equiv.symm_comp_self
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂) :
@[simp]
theorem
continuous_linear_equiv.self_comp_symm
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂) :
@[simp]
theorem
continuous_linear_equiv.symm_symm
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂) :
@[simp]
theorem
continuous_linear_equiv.refl_symm
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁] :
(continuous_linear_equiv.refl R₁ M₁).symm = continuous_linear_equiv.refl R₁ M₁
theorem
continuous_linear_equiv.symm_symm_apply
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(x : M₁) :
theorem
continuous_linear_equiv.symm_apply_eq
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
{x : M₂}
{y : M₁} :
theorem
continuous_linear_equiv.eq_symm_apply
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
{x : M₂}
{y : M₁} :
@[protected]
theorem
continuous_linear_equiv.image_eq_preimage
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(s : set M₁) :
@[protected]
theorem
continuous_linear_equiv.image_symm_eq_preimage
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(s : set M₂) :
@[protected, simp]
theorem
continuous_linear_equiv.symm_preimage_preimage
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(s : set M₂) :
@[protected, simp]
theorem
continuous_linear_equiv.preimage_symm_preimage
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(s : set M₁) :
def
continuous_linear_equiv.equiv_of_inverse
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(f₁ : M₁ →SL[σ₁₂] M₂)
(f₂ : M₂ →SL[σ₂₁] M₁)
(h₁ : function.left_inverse ⇑f₂ ⇑f₁)
(h₂ : function.right_inverse ⇑f₂ ⇑f₁) :
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}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(f₁ : M₁ →SL[σ₁₂] M₂)
(f₂ : M₂ →SL[σ₂₁] M₁)
(h₁ : function.left_inverse ⇑f₂ ⇑f₁)
(h₂ : function.right_inverse ⇑f₂ ⇑f₁)
(x : M₁) :
⇑(continuous_linear_equiv.equiv_of_inverse f₁ f₂ h₁ h₂) x = ⇑f₁ x
@[simp]
theorem
continuous_linear_equiv.symm_equiv_of_inverse
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(f₁ : M₁ →SL[σ₁₂] M₂)
(f₂ : M₂ →SL[σ₂₁] M₁)
(h₁ : function.left_inverse ⇑f₂ ⇑f₁)
(h₂ : function.right_inverse ⇑f₂ ⇑f₁) :
(continuous_linear_equiv.equiv_of_inverse f₁ f₂ h₁ h₂).symm = continuous_linear_equiv.equiv_of_inverse f₂ f₁ h₂ h₁
@[simp]
theorem
continuous_linear_equiv.image_smul_setₛₗ
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(c : R₁)
(s : set M₁) :
@[simp]
theorem
continuous_linear_equiv.preimage_smul_setₛₗ
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(c : R₂)
(s : set M₂) :
@[simp]
theorem
continuous_linear_equiv.image_smul_set
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M'₁ : Type u_5}
[topological_space M'₁]
[add_comm_monoid M'₁]
[module R₁ M₁]
[module R₁ M'₁]
(e : M₁ ≃L[R₁] M'₁)
(c : R₁)
(s : set M₁) :
@[simp]
theorem
continuous_linear_equiv.preimage_smul_set
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M'₁ : Type u_5}
[topological_space M'₁]
[add_comm_monoid M'₁]
[module R₁ M₁]
[module R₁ M'₁]
(e : M₁ ≃L[R₁] M'₁)
(c : R₁)
(s : set M'₁) :
@[protected, instance]
def
continuous_linear_equiv.automorphism_group
{R₁ : Type u_1}
[semiring R₁]
(M₁ : Type u_4)
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁] :
The continuous linear equivalences from M to itself form a group under composition.
Equations
- continuous_linear_equiv.automorphism_group M₁ = {mul := λ (f g : M₁ ≃L[R₁] M₁), g.trans f, mul_assoc := _, one := continuous_linear_equiv.refl R₁ M₁ _inst_22, one_mul := _, mul_one := _, npow := div_inv_monoid.npow._default (continuous_linear_equiv.refl R₁ M₁) (λ (f g : M₁ ≃L[R₁] M₁), g.trans f) _ _, npow_zero' := _, npow_succ' := _, inv := λ (f : M₁ ≃L[R₁] M₁), f.symm, div := div_inv_monoid.div._default (λ (f g : M₁ ≃L[R₁] M₁), g.trans f) _ (continuous_linear_equiv.refl R₁ M₁) _ _ (div_inv_monoid.npow._default (continuous_linear_equiv.refl R₁ M₁) (λ (f g : M₁ ≃L[R₁] M₁), g.trans f) _ _) _ _ (λ (f : M₁ ≃L[R₁] M₁), f.symm), div_eq_mul_inv := _, zpow := div_inv_monoid.zpow._default (λ (f g : M₁ ≃L[R₁] M₁), g.trans f) _ (continuous_linear_equiv.refl R₁ M₁) _ _ (div_inv_monoid.npow._default (continuous_linear_equiv.refl R₁ M₁) (λ (f g : M₁ ≃L[R₁] M₁), g.trans f) _ _) _ _ (λ (f : M₁ ≃L[R₁] M₁), f.symm), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _}
@[simp]
theorem
continuous_linear_equiv.arrow_congr_equiv_symm_apply
{R₁ : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
[semiring R₁]
[semiring R₂]
[semiring R₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R₁ →+* R₃}
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
{M₄ : Type u_8}
[topological_space M₄]
[add_comm_monoid M₄]
[module R₁ M₁]
[module R₂ M₂]
[module R₃ M₃]
{R₄ : Type u_9}
[semiring R₄]
[module R₄ M₄]
{σ₃₄ : R₃ →+* R₄}
{σ₄₃ : R₄ →+* R₃}
[ring_hom_inv_pair σ₃₄ σ₄₃]
[ring_hom_inv_pair σ₄₃ σ₃₄]
{σ₂₄ : R₂ →+* R₄}
{σ₁₄ : R₁ →+* R₄}
[ring_hom_comp_triple σ₂₁ σ₁₄ σ₂₄]
[ring_hom_comp_triple σ₂₄ σ₄₃ σ₂₃]
[ring_hom_comp_triple σ₁₃ σ₃₄ σ₁₄]
(e₁₂ : M₁ ≃SL[σ₁₂] M₂)
(e₄₃ : M₄ ≃SL[σ₄₃] M₃)
(f : M₂ →SL[σ₂₃] M₃) :
def
continuous_linear_equiv.arrow_congr_equiv
{R₁ : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
[semiring R₁]
[semiring R₂]
[semiring R₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R₁ →+* R₃}
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
{M₄ : Type u_8}
[topological_space M₄]
[add_comm_monoid M₄]
[module R₁ M₁]
[module R₂ M₂]
[module R₃ M₃]
{R₄ : Type u_9}
[semiring R₄]
[module R₄ M₄]
{σ₃₄ : R₃ →+* R₄}
{σ₄₃ : R₄ →+* R₃}
[ring_hom_inv_pair σ₃₄ σ₄₃]
[ring_hom_inv_pair σ₄₃ σ₃₄]
{σ₂₄ : R₂ →+* R₄}
{σ₁₄ : R₁ →+* R₄}
[ring_hom_comp_triple σ₂₁ σ₁₄ σ₂₄]
[ring_hom_comp_triple σ₂₄ σ₄₃ σ₂₃]
[ring_hom_comp_triple σ₁₃ σ₃₄ σ₁₄]
(e₁₂ : M₁ ≃SL[σ₁₂] M₂)
(e₄₃ : M₄ ≃SL[σ₄₃] M₃) :
A pair of continuous (semi)linear equivalences generates an equivalence between the spaces of continuous linear maps.
@[simp]
theorem
continuous_linear_equiv.arrow_congr_equiv_apply
{R₁ : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
[semiring R₁]
[semiring R₂]
[semiring R₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R₁ →+* R₃}
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
{M₄ : Type u_8}
[topological_space M₄]
[add_comm_monoid M₄]
[module R₁ M₁]
[module R₂ M₂]
[module R₃ M₃]
{R₄ : Type u_9}
[semiring R₄]
[module R₄ M₄]
{σ₃₄ : R₃ →+* R₄}
{σ₄₃ : R₄ →+* R₃}
[ring_hom_inv_pair σ₃₄ σ₄₃]
[ring_hom_inv_pair σ₄₃ σ₃₄]
{σ₂₄ : R₂ →+* R₄}
{σ₁₄ : R₁ →+* R₄}
[ring_hom_comp_triple σ₂₁ σ₁₄ σ₂₄]
[ring_hom_comp_triple σ₂₄ σ₄₃ σ₂₃]
[ring_hom_comp_triple σ₁₃ σ₃₄ σ₁₄]
(e₁₂ : M₁ ≃SL[σ₁₂] M₂)
(e₄₃ : M₄ ≃SL[σ₄₃] M₃)
(f : M₁ →SL[σ₁₄] M₄) :
def
continuous_linear_equiv.skew_prod
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_group M₂]
{M₃ : Type u_4}
[topological_space M₃]
[add_comm_group M₃]
{M₄ : Type u_5}
[topological_space M₄]
[add_comm_group M₄]
[module R M]
[module R M₂]
[module R M₃]
[module R M₄]
[topological_add_group M₄]
(e : M ≃L[R] M₂)
(e' : M₃ ≃L[R] M₄)
(f : M →L[R] M₄) :
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₄]
[module R M]
[module R M₂]
[module R M₃]
[module R M₄]
[topological_add_group M₄]
(e : M ≃L[R] M₂)
(e' : M₃ ≃L[R] M₄)
(f : M →L[R] M₄)
(x : M × M₃) :
@[simp]
theorem
continuous_linear_equiv.skew_prod_symm_apply
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_group M₂]
{M₃ : Type u_4}
[topological_space M₃]
[add_comm_group M₃]
{M₄ : Type u_5}
[topological_space M₄]
[add_comm_group M₄]
[module R M]
[module R M₂]
[module R M₃]
[module R M₄]
[topological_add_group M₄]
(e : M ≃L[R] M₂)
(e' : M₃ ≃L[R] M₄)
(f : M →L[R] M₄)
(x : M₂ × M₄) :
@[simp]
theorem
continuous_linear_equiv.map_sub
{R : Type u_1}
[ring R]
{R₂ : Type u_2}
[ring R₂]
{M : Type u_3}
[topological_space M]
[add_comm_group M]
[module R M]
{M₂ : Type u_4}
[topological_space M₂]
[add_comm_group M₂]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
(e : M ≃SL[σ₁₂] M₂)
(x y : M) :
@[simp]
theorem
continuous_linear_equiv.map_neg
{R : Type u_1}
[ring R]
{R₂ : Type u_2}
[ring R₂]
{M : Type u_3}
[topological_space M]
[add_comm_group M]
[module R M]
{M₂ : Type u_4}
[topological_space M₂]
[add_comm_group M₂]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
(e : M ≃SL[σ₁₂] M₂)
(x : M) :
The next theorems cover the identification between M ≃L[𝕜] Mand the group of units of the ring
M →L[R] M.
def
continuous_linear_equiv.of_unit
{R : Type u_1}
[ring R]
{M : Type u_3}
[topological_space M]
[add_comm_group M]
[module R M]
[topological_add_group M]
(f : (M →L[R] M)ˣ) :
An invertible continuous linear map f determines a continuous equivalence from M to itself.
Equations
- continuous_linear_equiv.of_unit f = {to_linear_equiv := {to_fun := ⇑(f.val), map_add' := _, map_smul' := _, inv_fun := ⇑(f.inv), left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
def
continuous_linear_equiv.to_unit
{R : Type u_1}
[ring R]
{M : Type u_3}
[topological_space M]
[add_comm_group M]
[module R M]
[topological_add_group M]
(f : M ≃L[R] M) :
A continuous equivalence from M to itself determines an invertible continuous linear map.
def
continuous_linear_equiv.units_equiv
(R : Type u_1)
[ring R]
(M : Type u_3)
[topological_space M]
[add_comm_group M]
[module R M]
[topological_add_group M] :
The units of the algebra of continuous R-linear endomorphisms of M is multiplicatively
equivalent to the type of continuous linear equivalences between M and itself.
Equations
- continuous_linear_equiv.units_equiv R M = {to_fun := continuous_linear_equiv.of_unit _inst_11, inv_fun := continuous_linear_equiv.to_unit _inst_11, left_inv := _, right_inv := _, map_mul' := _}
@[simp]
theorem
continuous_linear_equiv.units_equiv_apply
(R : Type u_1)
[ring R]
(M : Type u_3)
[topological_space M]
[add_comm_group M]
[module R M]
[topological_add_group M]
(f : (M →L[R] M)ˣ)
(x : M) :
⇑(⇑(continuous_linear_equiv.units_equiv R M) f) x = ⇑f x
def
continuous_linear_equiv.units_equiv_aut
(R : Type u_1)
[ring R]
[topological_space R]
[has_continuous_mul R] :
Continuous linear equivalences R ≃L[R] R are enumerated by Rˣ.
@[simp]
theorem
continuous_linear_equiv.units_equiv_aut_apply
{R : Type u_1}
[ring R]
[topological_space R]
[has_continuous_mul R]
(u : Rˣ)
(x : R) :
@[simp]
theorem
continuous_linear_equiv.units_equiv_aut_apply_symm
{R : Type u_1}
[ring R]
[topological_space R]
[has_continuous_mul R]
(u : Rˣ)
(x : R) :
@[simp]
theorem
continuous_linear_equiv.units_equiv_aut_symm_apply
{R : Type u_1}
[ring R]
[topological_space R]
[has_continuous_mul R]
(e : R ≃L[R] R) :
def
continuous_linear_equiv.equiv_of_right_inverse
{R : Type u_1}
[ring R]
{M : Type u_3}
[topological_space M]
[add_comm_group M]
[module R M]
{M₂ : Type u_4}
[topological_space M₂]
[add_comm_group M₂]
[module R M₂]
[topological_add_group M]
(f₁ : M →L[R] M₂)
(f₂ : M₂ →L[R] M)
(h : function.right_inverse ⇑f₂ ⇑f₁) :
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_3}
[topological_space M]
[add_comm_group M]
[module R M]
{M₂ : Type u_4}
[topological_space M₂]
[add_comm_group M₂]
[module R M₂]
[topological_add_group M]
(f₁ : M →L[R] M₂)
(f₂ : M₂ →L[R] M)
(h : function.right_inverse ⇑f₂ ⇑f₁)
(x : M) :
(⇑(continuous_linear_equiv.equiv_of_right_inverse f₁ f₂ h) x).fst = ⇑f₁ x
@[simp]
theorem
continuous_linear_equiv.snd_equiv_of_right_inverse
{R : Type u_1}
[ring R]
{M : Type u_3}
[topological_space M]
[add_comm_group M]
[module R M]
{M₂ : Type u_4}
[topological_space M₂]
[add_comm_group M₂]
[module R M₂]
[topological_add_group M]
(f₁ : M →L[R] M₂)
(f₂ : M₂ →L[R] M)
(h : function.right_inverse ⇑f₂ ⇑f₁)
(x : M) :
@[simp]
theorem
continuous_linear_equiv.equiv_of_right_inverse_symm_apply
{R : Type u_1}
[ring R]
{M : Type u_3}
[topological_space M]
[add_comm_group M]
[module R M]
{M₂ : Type u_4}
[topological_space M₂]
[add_comm_group M₂]
[module R M₂]
[topological_add_group M]
(f₁ : M →L[R] M₂)
(f₂ : M₂ →L[R] M)
(h : function.right_inverse ⇑f₂ ⇑f₁)
(y : M₂ × ↥(f₁.ker)) :
def
continuous_linear_equiv.fun_unique
(ι : Type u_1)
(R : Type u_2)
(M : Type u_3)
[unique ι]
[semiring R]
[add_comm_monoid M]
[module R M]
[topological_space M] :
If ι has a unique element, then ι → M is continuously linear equivalent to M.
Equations
- continuous_linear_equiv.fun_unique ι R M = {to_linear_equiv := linear_equiv.fun_unique ι R M _inst_4, continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
theorem
continuous_linear_equiv.coe_fun_unique
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
[unique ι]
[semiring R]
[add_comm_monoid M]
[module R M]
[topological_space M] :
@[simp]
theorem
continuous_linear_equiv.coe_fun_unique_symm
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
[unique ι]
[semiring R]
[add_comm_monoid M]
[module R M]
[topological_space M] :
⇑((continuous_linear_equiv.fun_unique ι R M).symm) = function.const ι
@[simp]
theorem
continuous_linear_equiv.pi_fin_two_apply
(R : Type u_2)
[semiring R]
(M : fin 2 → Type u_1)
[Π (i : fin 2), add_comm_monoid (M i)]
[Π (i : fin 2), module R (M i)]
[Π (i : fin 2), topological_space (M i)] :
⇑(continuous_linear_equiv.pi_fin_two R M) = λ (f : Π (i : fin 2), M i), (f 0, f 1)
@[simp]
theorem
continuous_linear_equiv.pi_fin_two_to_linear_equiv
(R : Type u_2)
[semiring R]
(M : fin 2 → Type u_1)
[Π (i : fin 2), add_comm_monoid (M i)]
[Π (i : fin 2), module R (M i)]
[Π (i : fin 2), topological_space (M i)] :
@[simp]
theorem
continuous_linear_equiv.pi_fin_two_symm_apply
(R : Type u_2)
[semiring R]
(M : fin 2 → Type u_1)
[Π (i : fin 2), add_comm_monoid (M i)]
[Π (i : fin 2), module R (M i)]
[Π (i : fin 2), topological_space (M i)] :
⇑((continuous_linear_equiv.pi_fin_two R M).symm) = λ (p : M 0 × M 1), fin.cons p.fst (fin.cons p.snd fin_zero_elim)
def
continuous_linear_equiv.pi_fin_two
(R : Type u_2)
[semiring R]
(M : fin 2 → Type u_1)
[Π (i : fin 2), add_comm_monoid (M i)]
[Π (i : fin 2), module R (M i)]
[Π (i : fin 2), topological_space (M i)] :
Continuous linear equivalence between dependent functions Π i : fin 2, M i and M 0 × M 1.
Equations
- continuous_linear_equiv.pi_fin_two R M = {to_linear_equiv := linear_equiv.pi_fin_two R M (λ (i : fin 2), _inst_7 i), continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
theorem
continuous_linear_equiv.fin_two_arrow_to_linear_equiv
(R : Type u_2)
(M : Type u_3)
[semiring R]
[add_comm_monoid M]
[module R M]
[topological_space M] :
@[simp]
theorem
continuous_linear_equiv.fin_two_arrow_apply
(R : Type u_2)
(M : Type u_3)
[semiring R]
[add_comm_monoid M]
[module R M]
[topological_space M] :
⇑(continuous_linear_equiv.fin_two_arrow R M) = λ (f : fin 2 → M), (f 0, f 1)
@[simp]
theorem
continuous_linear_equiv.fin_two_arrow_symm_apply
(R : Type u_2)
(M : Type u_3)
[semiring R]
[add_comm_monoid M]
[module R M]
[topological_space M] :
def
continuous_linear_equiv.fin_two_arrow
(R : Type u_2)
(M : Type u_3)
[semiring R]
[add_comm_monoid M]
[module R M]
[topological_space M] :
Continuous linear equivalence between vectors in M² = fin 2 → M and M × M.
Equations
- continuous_linear_equiv.fin_two_arrow R M = {to_linear_equiv := linear_equiv.fin_two_arrow R M _inst_4, continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
theorem
continuous_linear_equiv.det_coe_symm
{R : Type u_1}
[field R]
{M : Type u_2}
[topological_space M]
[add_comm_group M]
[module R M]
(A : M ≃L[R] M) :
noncomputable
def
continuous_linear_map.inverse
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[topological_space M]
[topological_space M₂]
[semiring R]
[add_comm_monoid M₂]
[module R M₂]
[add_comm_monoid M]
[module R M] :
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.
@[simp]
theorem
continuous_linear_map.inverse_equiv
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[topological_space M]
[topological_space M₂]
[semiring R]
[add_comm_monoid M₂]
[module R M₂]
[add_comm_monoid M]
[module R M]
(e : M ≃L[R] M₂) :
By definition, if f is invertible then inverse f = f.symm.
@[simp]
theorem
continuous_linear_map.inverse_non_equiv
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[topological_space M]
[topological_space M₂]
[semiring R]
[add_comm_monoid M₂]
[module R M₂]
[add_comm_monoid M]
[module R M]
(f : M →L[R] M₂)
(h : ¬∃ (e' : M ≃L[R] M₂), ↑e' = f) :
By definition, if f is not invertible then inverse f = 0.
@[simp]
theorem
continuous_linear_map.ring_inverse_equiv
{R : Type u_1}
{M : Type u_2}
[topological_space M]
[ring R]
[add_comm_group M]
[topological_add_group M]
[module R M]
(e : M ≃L[R] M) :
ring.inverse ↑e = ↑e.inverse
theorem
continuous_linear_map.to_ring_inverse
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[topological_space M]
[topological_space M₂]
[ring R]
[add_comm_group M]
[topological_add_group M]
[module R M]
[add_comm_group M₂]
[module R M₂]
(e : M ≃L[R] M₂)
(f : M →L[R] M₂) :
The function continuous_linear_equiv.inverse can be written in terms of ring.inverse for the
ring of self-maps of the domain.
theorem
continuous_linear_map.ring_inverse_eq_map_inverse
{R : Type u_1}
{M : Type u_2}
[topological_space M]
[ring R]
[add_comm_group M]
[topological_add_group M]
[module R M] :
def
submodule.closed_complemented
{R : Type u_1}
[ring R]
{M : Type u_2}
[topological_space M]
[add_comm_group M]
[module R M]
(p : submodule R M) :
Prop
A submodule p is called complemented if there exists a continuous projection M →ₗ[R] p.
theorem
submodule.closed_complemented.has_closed_complement
{R : Type u_1}
[ring R]
{M : Type u_2}
[topological_space M]
[add_comm_group M]
[module R M]
{p : submodule R M}
[t1_space ↥p]
(h : p.closed_complemented) :
@[protected]
theorem
submodule.closed_complemented.is_closed
{R : Type u_1}
[ring R]
{M : Type u_2}
[topological_space M]
[add_comm_group M]
[module R M]
[topological_add_group M]
[t1_space M]
{p : submodule R M}
(h : p.closed_complemented) :
@[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)
(h : function.right_inverse ⇑f₂ ⇑f₁) :