Complemented subspaces of normed vector spaces #
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
ContinuousLinearMap.ker_closedComplemented_of_finiteDimensional_range
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[CompleteSpace 𝕜]
(f : E →L[𝕜] F)
[FiniteDimensional 𝕜 ↥(LinearMap.range f)]
:
(LinearMap.ker f).ClosedComplemented
def
ContinuousLinearMap.equivProdOfSurjectiveOfIsCompl
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[CompleteSpace E]
[CompleteSpace (F × G)]
(f : E →L[𝕜] F)
(g : E →L[𝕜] G)
(hf : LinearMap.range f = ⊤)
(hg : LinearMap.range g = ⊤)
(hfg : IsCompl (LinearMap.ker f) (LinearMap.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.equivProdOfSurjectiveOfIsCompl g hf hg hfg = ((↑f).equivProdOfSurjectiveOfIsCompl (↑g) hf hg hfg).toContinuousLinearEquivOfContinuous ⋯
Instances For
@[simp]
theorem
ContinuousLinearMap.coe_equivProdOfSurjectiveOfIsCompl
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[CompleteSpace E]
[CompleteSpace (F × G)]
{f : E →L[𝕜] F}
{g : E →L[𝕜] G}
(hf : LinearMap.range f = ⊤)
(hg : LinearMap.range g = ⊤)
(hfg : IsCompl (LinearMap.ker f) (LinearMap.ker g))
:
↑↑(f.equivProdOfSurjectiveOfIsCompl g hf hg hfg) = ↑(f.prod g)
@[simp]
theorem
ContinuousLinearMap.equivProdOfSurjectiveOfIsCompl_toLinearEquiv
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[CompleteSpace E]
[CompleteSpace (F × G)]
{f : E →L[𝕜] F}
{g : E →L[𝕜] G}
(hf : LinearMap.range f = ⊤)
(hg : LinearMap.range g = ⊤)
(hfg : IsCompl (LinearMap.ker f) (LinearMap.ker g))
:
(f.equivProdOfSurjectiveOfIsCompl g hf hg hfg).toLinearEquiv = (↑f).equivProdOfSurjectiveOfIsCompl (↑g) hf hg hfg
@[simp]
theorem
ContinuousLinearMap.equivProdOfSurjectiveOfIsCompl_apply
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[CompleteSpace E]
[CompleteSpace (F × G)]
{f : E →L[𝕜] F}
{g : E →L[𝕜] G}
(hf : LinearMap.range f = ⊤)
(hg : LinearMap.range g = ⊤)
(hfg : IsCompl (LinearMap.ker f) (LinearMap.ker g))
(x : E)
:
(f.equivProdOfSurjectiveOfIsCompl g hf hg hfg) x = (f x, g x)
def
Submodule.prodEquivOfClosedCompl
{𝕜 : Type u_1}
{E : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[CompleteSpace E]
(p : Subspace 𝕜 E)
(q : Subspace 𝕜 E)
(h : IsCompl p q)
(hp : IsClosed ↑p)
(hq : IsClosed ↑q)
:
If q is a closed complement of a closed subspace p, then p × q is continuously
isomorphic to E.
Equations
- Submodule.prodEquivOfClosedCompl p q h hp hq = (Submodule.prodEquivOfIsCompl p q h).toContinuousLinearEquivOfContinuous ⋯
Instances For
def
Submodule.linearProjOfClosedCompl
{𝕜 : Type u_1}
{E : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[CompleteSpace E]
(p : Subspace 𝕜 E)
(q : Subspace 𝕜 E)
(h : IsCompl p q)
(hp : IsClosed ↑p)
(hq : IsClosed ↑q)
:
Projection to a closed submodule along a closed complement.
Equations
- Submodule.linearProjOfClosedCompl p q h hp hq = (ContinuousLinearMap.fst 𝕜 ↥p ↥q).comp ↑(Submodule.prodEquivOfClosedCompl p q h hp hq).symm
Instances For
@[simp]
theorem
Submodule.coe_prodEquivOfClosedCompl
{𝕜 : Type u_1}
{E : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[CompleteSpace E]
{p : Subspace 𝕜 E}
{q : Subspace 𝕜 E}
(h : IsCompl p q)
(hp : IsClosed ↑p)
(hq : IsClosed ↑q)
:
⇑(Submodule.prodEquivOfClosedCompl p q h hp hq) = ⇑(Submodule.prodEquivOfIsCompl p q h)
@[simp]
theorem
Submodule.coe_prodEquivOfClosedCompl_symm
{𝕜 : Type u_1}
{E : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[CompleteSpace E]
{p : Subspace 𝕜 E}
{q : Subspace 𝕜 E}
(h : IsCompl p q)
(hp : IsClosed ↑p)
(hq : IsClosed ↑q)
:
⇑(Submodule.prodEquivOfClosedCompl p q h hp hq).symm = ⇑(Submodule.prodEquivOfIsCompl p q h).symm
@[simp]
theorem
Submodule.coe_continuous_linearProjOfClosedCompl
{𝕜 : Type u_1}
{E : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[CompleteSpace E]
{p : Subspace 𝕜 E}
{q : Subspace 𝕜 E}
(h : IsCompl p q)
(hp : IsClosed ↑p)
(hq : IsClosed ↑q)
:
↑(Submodule.linearProjOfClosedCompl p q h hp hq) = Submodule.linearProjOfIsCompl p q h
@[simp]
theorem
Submodule.coe_continuous_linearProjOfClosedCompl'
{𝕜 : Type u_1}
{E : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[CompleteSpace E]
{p : Subspace 𝕜 E}
{q : Subspace 𝕜 E}
(h : IsCompl p q)
(hp : IsClosed ↑p)
(hq : IsClosed ↑q)
:
⇑(Submodule.linearProjOfClosedCompl p q h hp hq) = ⇑(Submodule.linearProjOfIsCompl p q h)
theorem
Submodule.ClosedComplemented.of_isCompl_isClosed
{𝕜 : Type u_1}
{E : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[CompleteSpace E]
{p : Subspace 𝕜 E}
{q : Subspace 𝕜 E}
(h : IsCompl p q)
(hp : IsClosed ↑p)
(hq : IsClosed ↑q)
:
theorem
Submodule.IsCompl.closedComplemented_of_isClosed
{𝕜 : Type u_1}
{E : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[CompleteSpace E]
{p : Subspace 𝕜 E}
{q : Subspace 𝕜 E}
(h : IsCompl p q)
(hp : IsClosed ↑p)
(hq : IsClosed ↑q)
:
theorem
Submodule.closedComplemented_iff_isClosed_exists_isClosed_isCompl
{𝕜 : Type u_1}
{E : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[CompleteSpace E]
{p : Subspace 𝕜 E}
:
theorem
Submodule.ClosedComplemented.of_quotient_finiteDimensional
{𝕜 : Type u_1}
{E : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[CompleteSpace E]
{p : Subspace 𝕜 E}
[CompleteSpace 𝕜]
[FiniteDimensional 𝕜 (E ⧸ p)]
(hp : IsClosed ↑p)
: