# 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} [] [] [] (f : E →L[𝕜] F) [] :
().ClosedComplemented
def ContinuousLinearMap.equivProdOfSurjectiveOfIsCompl {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [] [] [] [] [CompleteSpace (F × G)] (f : E →L[𝕜] F) (g : E →L[𝕜] G) (hf : ) (hg : ) (hfg : ) :
E ≃L[𝕜] F × 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} [] [] [] [] [CompleteSpace (F × G)] {f : E →L[𝕜] F} {g : E →L[𝕜] G} (hf : ) (hg : ) (hfg : ) :
(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} [] [] [] [] [CompleteSpace (F × G)] {f : E →L[𝕜] F} {g : E →L[𝕜] G} (hf : ) (hg : ) (hfg : ) :
(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} [] [] [] [] [CompleteSpace (F × G)] {f : E →L[𝕜] F} {g : E →L[𝕜] G} (hf : ) (hg : ) (hfg : ) (x : E) :
(f.equivProdOfSurjectiveOfIsCompl g hf hg hfg) x = (f x, g x)
def Submodule.prodEquivOfClosedCompl {𝕜 : Type u_1} {E : Type u_2} [] [] (p : Subspace 𝕜 E) (q : Subspace 𝕜 E) (h : IsCompl p q) (hp : IsClosed p) (hq : IsClosed q) :
(p × q) ≃L[𝕜] E

If q is a closed complement of a closed subspace p, then p × q is continuously isomorphic to E.

Equations
• = ().toContinuousLinearEquivOfContinuous
Instances For
def Submodule.linearProjOfClosedCompl {𝕜 : Type u_1} {E : Type u_2} [] [] (p : Subspace 𝕜 E) (q : Subspace 𝕜 E) (h : IsCompl p q) (hp : IsClosed p) (hq : IsClosed q) :
E →L[𝕜] p

Projection to a closed submodule along a closed complement.

Equations
• = ().comp ().symm
Instances For
@[simp]
theorem Submodule.coe_prodEquivOfClosedCompl {𝕜 : Type u_1} {E : Type u_2} [] [] {p : Subspace 𝕜 E} {q : Subspace 𝕜 E} (h : IsCompl p q) (hp : IsClosed p) (hq : IsClosed q) :
() = ()
@[simp]
theorem Submodule.coe_prodEquivOfClosedCompl_symm {𝕜 : Type u_1} {E : Type u_2} [] [] {p : Subspace 𝕜 E} {q : Subspace 𝕜 E} (h : IsCompl p q) (hp : IsClosed p) (hq : IsClosed q) :
().symm = ().symm
@[simp]
theorem Submodule.coe_continuous_linearProjOfClosedCompl {𝕜 : Type u_1} {E : Type u_2} [] [] {p : Subspace 𝕜 E} {q : Subspace 𝕜 E} (h : IsCompl p q) (hp : IsClosed p) (hq : IsClosed q) :
() =
@[simp]
theorem Submodule.coe_continuous_linearProjOfClosedCompl' {𝕜 : Type u_1} {E : Type u_2} [] [] {p : Subspace 𝕜 E} {q : Subspace 𝕜 E} (h : IsCompl p q) (hp : IsClosed p) (hq : IsClosed q) :
() = ()
theorem Submodule.ClosedComplemented.of_isCompl_isClosed {𝕜 : Type u_1} {E : Type u_2} [] [] {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} [] [] {p : Subspace 𝕜 E} {q : Subspace 𝕜 E} (h : IsCompl p q) (hp : IsClosed p) (hq : IsClosed q) :

Alias of Submodule.ClosedComplemented.of_isCompl_isClosed.

theorem Submodule.closedComplemented_iff_isClosed_exists_isClosed_isCompl {𝕜 : Type u_1} {E : Type u_2} [] [] {p : Subspace 𝕜 E} :
IsClosed p ∃ (q : ), IsClosed q IsCompl p q
theorem Submodule.ClosedComplemented.of_quotient_finiteDimensional {𝕜 : Type u_1} {E : Type u_2} [] [] {p : Subspace 𝕜 E} [] [FiniteDimensional 𝕜 (E p)] (hp : IsClosed p) :