Complemented subspaces of normed vector spaces #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
A submodule p of a topological module E over R is called complemented if there exists
a continuous linear projection f : E →ₗ[R] p, ∀ x : p, f x = x. We prove that for
a closed subspace of a normed space this condition is equivalent to existence of a closed
subspace q such that p ⊓ q = ⊥, p ⊔ q = ⊤. We also prove that a subspace of finite codimension
is always a complemented subspace.
Tags #
complemented subspace, normed vector space
theorem
continuous_linear_map.ker_closed_complemented_of_finite_dimensional_range
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[nontrivially_normed_field 𝕜]
[normed_add_comm_group E]
[normed_space 𝕜 E]
[normed_add_comm_group F]
[normed_space 𝕜 F]
[complete_space 𝕜]
(f : E →L[𝕜] F)
[finite_dimensional 𝕜 ↥(linear_map.range f)] :
noncomputable
def
continuous_linear_map.equiv_prod_of_surjective_of_is_compl
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[nontrivially_normed_field 𝕜]
[normed_add_comm_group E]
[normed_space 𝕜 E]
[normed_add_comm_group F]
[normed_space 𝕜 F]
[normed_add_comm_group G]
[normed_space 𝕜 G]
[complete_space E]
[complete_space (F × G)]
(f : E →L[𝕜] F)
(g : E →L[𝕜] G)
(hf : linear_map.range f = ⊤)
(hg : linear_map.range g = ⊤)
(hfg : is_compl (linear_map.ker f) (linear_map.ker g)) :
If f : E →L[R] F and g : E →L[R] G are two surjective linear maps and
their kernels are complement of each other, then x ↦ (f x, g x) defines
a linear equivalence E ≃L[R] F × G.
Equations
- f.equiv_prod_of_surjective_of_is_compl g hf hg hfg = (↑f.equiv_prod_of_surjective_of_is_compl ↑g hf hg hfg).to_continuous_linear_equiv_of_continuous _
@[simp]
theorem
continuous_linear_map.coe_equiv_prod_of_surjective_of_is_compl
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[nontrivially_normed_field 𝕜]
[normed_add_comm_group E]
[normed_space 𝕜 E]
[normed_add_comm_group F]
[normed_space 𝕜 F]
[normed_add_comm_group G]
[normed_space 𝕜 G]
[complete_space E]
[complete_space (F × G)]
{f : E →L[𝕜] F}
{g : E →L[𝕜] G}
(hf : linear_map.range f = ⊤)
(hg : linear_map.range g = ⊤)
(hfg : is_compl (linear_map.ker f) (linear_map.ker g)) :
↑(f.equiv_prod_of_surjective_of_is_compl g hf hg hfg) = ↑(f.prod g)
@[simp]
theorem
continuous_linear_map.equiv_prod_of_surjective_of_is_compl_to_linear_equiv
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[nontrivially_normed_field 𝕜]
[normed_add_comm_group E]
[normed_space 𝕜 E]
[normed_add_comm_group F]
[normed_space 𝕜 F]
[normed_add_comm_group G]
[normed_space 𝕜 G]
[complete_space E]
[complete_space (F × G)]
{f : E →L[𝕜] F}
{g : E →L[𝕜] G}
(hf : linear_map.range f = ⊤)
(hg : linear_map.range g = ⊤)
(hfg : is_compl (linear_map.ker f) (linear_map.ker g)) :
(f.equiv_prod_of_surjective_of_is_compl g hf hg hfg).to_linear_equiv = ↑f.equiv_prod_of_surjective_of_is_compl ↑g hf hg hfg
@[simp]
theorem
continuous_linear_map.equiv_prod_of_surjective_of_is_compl_apply
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[nontrivially_normed_field 𝕜]
[normed_add_comm_group E]
[normed_space 𝕜 E]
[normed_add_comm_group F]
[normed_space 𝕜 F]
[normed_add_comm_group G]
[normed_space 𝕜 G]
[complete_space E]
[complete_space (F × G)]
{f : E →L[𝕜] F}
{g : E →L[𝕜] G}
(hf : linear_map.range f = ⊤)
(hg : linear_map.range g = ⊤)
(hfg : is_compl (linear_map.ker f) (linear_map.ker g))
(x : E) :
⇑(f.equiv_prod_of_surjective_of_is_compl g hf hg hfg) x = (⇑f x, ⇑g x)
noncomputable
def
subspace.prod_equiv_of_closed_compl
{𝕜 : Type u_1}
{E : Type u_2}
[nontrivially_normed_field 𝕜]
[normed_add_comm_group E]
[normed_space 𝕜 E]
[complete_space E]
(p q : subspace 𝕜 E)
(h : is_compl p q)
(hp : is_closed ↑p)
(hq : is_closed ↑q) :
If q is a closed complement of a closed subspace p, then p × q is continuously
isomorphic to E.
Equations
- p.prod_equiv_of_closed_compl q h hp hq = (submodule.prod_equiv_of_is_compl p q h).to_continuous_linear_equiv_of_continuous _
noncomputable
def
subspace.linear_proj_of_closed_compl
{𝕜 : Type u_1}
{E : Type u_2}
[nontrivially_normed_field 𝕜]
[normed_add_comm_group E]
[normed_space 𝕜 E]
[complete_space E]
(p q : subspace 𝕜 E)
(h : is_compl p q)
(hp : is_closed ↑p)
(hq : is_closed ↑q) :
Projection to a closed submodule along a closed complement.
Equations
- p.linear_proj_of_closed_compl q h hp hq = (continuous_linear_map.fst 𝕜 ↥p ↥q).comp ↑((p.prod_equiv_of_closed_compl q h hp hq).symm)
@[simp]
theorem
subspace.coe_prod_equiv_of_closed_compl
{𝕜 : Type u_1}
{E : Type u_2}
[nontrivially_normed_field 𝕜]
[normed_add_comm_group E]
[normed_space 𝕜 E]
[complete_space E]
{p q : subspace 𝕜 E}
(h : is_compl p q)
(hp : is_closed ↑p)
(hq : is_closed ↑q) :
⇑(p.prod_equiv_of_closed_compl q h hp hq) = ⇑(submodule.prod_equiv_of_is_compl p q h)
@[simp]
theorem
subspace.coe_prod_equiv_of_closed_compl_symm
{𝕜 : Type u_1}
{E : Type u_2}
[nontrivially_normed_field 𝕜]
[normed_add_comm_group E]
[normed_space 𝕜 E]
[complete_space E]
{p q : subspace 𝕜 E}
(h : is_compl p q)
(hp : is_closed ↑p)
(hq : is_closed ↑q) :
⇑((p.prod_equiv_of_closed_compl q h hp hq).symm) = ⇑((submodule.prod_equiv_of_is_compl p q h).symm)
@[simp]
theorem
subspace.coe_continuous_linear_proj_of_closed_compl
{𝕜 : Type u_1}
{E : Type u_2}
[nontrivially_normed_field 𝕜]
[normed_add_comm_group E]
[normed_space 𝕜 E]
[complete_space E]
{p q : subspace 𝕜 E}
(h : is_compl p q)
(hp : is_closed ↑p)
(hq : is_closed ↑q) :
↑(p.linear_proj_of_closed_compl q h hp hq) = submodule.linear_proj_of_is_compl p q h
@[simp]
theorem
subspace.coe_continuous_linear_proj_of_closed_compl'
{𝕜 : Type u_1}
{E : Type u_2}
[nontrivially_normed_field 𝕜]
[normed_add_comm_group E]
[normed_space 𝕜 E]
[complete_space E]
{p q : subspace 𝕜 E}
(h : is_compl p q)
(hp : is_closed ↑p)
(hq : is_closed ↑q) :
⇑(p.linear_proj_of_closed_compl q h hp hq) = ⇑(submodule.linear_proj_of_is_compl p q h)
theorem
subspace.closed_complemented_of_closed_compl
{𝕜 : Type u_1}
{E : Type u_2}
[nontrivially_normed_field 𝕜]
[normed_add_comm_group E]
[normed_space 𝕜 E]
[complete_space E]
{p q : subspace 𝕜 E}
(h : is_compl p q)
(hp : is_closed ↑p)
(hq : is_closed ↑q) :
theorem
subspace.closed_complemented_iff_has_closed_compl
{𝕜 : Type u_1}
{E : Type u_2}
[nontrivially_normed_field 𝕜]
[normed_add_comm_group E]
[normed_space 𝕜 E]
[complete_space E]
{p : subspace 𝕜 E} :
theorem
subspace.closed_complemented_of_quotient_finite_dimensional
{𝕜 : Type u_1}
{E : Type u_2}
[nontrivially_normed_field 𝕜]
[normed_add_comm_group E]
[normed_space 𝕜 E]
[complete_space E]
{p : subspace 𝕜 E}
[complete_space 𝕜]
[finite_dimensional 𝕜 (E ⧸ p)]
(hp : is_closed ↑p) :