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)) : 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 ⋯

@[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 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

• Submodule.prodEquivOfClosedCompl p q h hp hq = (Submodule.prodEquivOfIsCompl p q h).toContinuousLinearEquivOfContinuous ⋯

def Submodule.linearProjOfClosedCompl {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] (p 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

• Submodule.linearProjOfClosedCompl p q h hp hq = (ContinuousLinearMap.fst 𝕜 ↥p ↥q).comp ↑(Submodule.prodEquivOfClosedCompl p q h hp hq).symm

@[simp]

theorem Submodule.coe_prodEquivOfClosedCompl {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {p q : Subspace 𝕜 E} (h : IsCompl p q) (hp : IsClosed ↑p) (hq : IsClosed ↑q) : ⇑(prodEquivOfClosedCompl p q h hp hq) = ⇑(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 q : Subspace 𝕜 E} (h : IsCompl p q) (hp : IsClosed ↑p) (hq : IsClosed ↑q) : ⇑(prodEquivOfClosedCompl p q h hp hq).symm = ⇑(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 q : Subspace 𝕜 E} (h : IsCompl p q) (hp : IsClosed ↑p) (hq : IsClosed ↑q) : ↑(linearProjOfClosedCompl p q h hp hq) = 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 q : Subspace 𝕜 E} (h : IsCompl p q) (hp : IsClosed ↑p) (hq : IsClosed ↑q) : ⇑(linearProjOfClosedCompl p q h hp hq) = ⇑(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 q : Subspace 𝕜 E} (h : IsCompl p q) (hp : IsClosed ↑p) (hq : IsClosed ↑q) : ClosedComplemented p

theorem Submodule.IsCompl.closedComplemented_of_isClosed {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {p q : Subspace 𝕜 E} (h : IsCompl p q) (hp : IsClosed ↑p) (hq : IsClosed ↑q) : ClosedComplemented p

Alias of Submodule.ClosedComplemented.of_isCompl_isClosed.

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} : ClosedComplemented p ↔ IsClosed ↑p ∧ ∃ (q : Submodule 𝕜 E), IsClosed ↑q ∧ IsCompl p q

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) : ClosedComplemented p