Complemented subspaces of Banach spaces

A submodule p of a topological module E over R is called complemented (Submodule.ClosedComplemented) if there exists a continuous linear projection f : E →ₗ[R] p, ∀ x : p, f x = x.

All results in this file rely on the open mapping theorem, hence the Banach space assumption.

Main results

• Submodule.isTopCompl_iff_isCompl_isClosed: in a Banach space, two submodules are topological complements (Submodule.IsTopCompl) if and only if they are algebraic complements (IsCompl)
• Submodule.closedComplemented_iff_isClosed_exists_isClosed_isCompl: in a Banach space. a submodule is complemented if and only if it is closed and admits a closed algebraic complement.

TODO

Generalize these results to metrizable complete topological vector spaces, once the open mapping theorem is available in that setting.

Tags

complemented subspace, Banach space

noncomputable 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 : (↑f).range = ⊤) (hg : (↑g).range = ⊤) (hfg : IsCompl (↑f).ker (↑g).ker) : 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 : (↑f).range = ⊤) (hg : (↑g).range = ⊤) (hfg : IsCompl (↑f).ker (↑g).ker) : ↑↑(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 : (↑f).range = ⊤) (hg : (↑g).range = ⊤) (hfg : IsCompl (↑f).ker (↑g).ker) : ↑(f.equivProdOfSurjectiveOfIsCompl g hf hg hfg) = (↑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 : (↑f).range = ⊤) (hg : (↑g).range = ⊤) (hfg : IsCompl (↑f).ker (↑g).ker) (x : E) : (f.equivProdOfSurjectiveOfIsCompl g hf hg hfg) x = (f x, g x)

theorem Submodule.IsCompl.isTopCompl_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) : IsTopCompl p q

theorem Submodule.isTopCompl_iff_isCompl_isClosed {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {p q : Subspace 𝕜 E} : IsTopCompl p q ↔ IsCompl p q ∧ IsClosed ↑p ∧ IsClosed ↑q

@[deprecated Submodule.prodEquivOfIsTopCompl (since := "2026-06-07")]

noncomputable 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 ⋯

@[deprecated Submodule.projectionOntoL (since := "2026-06-07")]

noncomputable 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 ∘SL ↑(Submodule.prodEquivOfClosedCompl p q h hp hq).symm

@[deprecated "Use `coe_prodEquivOfIsTopCompl` instead" (since := "2026-06-07")]

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)

@[deprecated "Use `coe_symm_prodEquivOfIsTopCompl` instead" (since := "2026-06-07")]

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

@[deprecated "Use `toLinearMap_projectionOntoL` instead" (since := "2026-06-07")]

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) = projectionOnto p q h

@[deprecated "Use `coe_projectionOntoL` instead" (since := "2026-06-07")]

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) = ⇑(projectionOnto 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