Documentation

Mathlib.Analysis.Normed.Module.Complemented

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

source
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
source
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 ⋯
Instances For
    source
    @[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)
    source
    @[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
    source
    @[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)
    source
    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
    Instances For
      source
      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
      Instances For
        source
        @[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) :
        ⇑(Submodule.prodEquivOfClosedCompl p q h hp hq) = ⇑(Submodule.prodEquivOfIsCompl p q h)
        source
        @[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) :
        ⇑(Submodule.prodEquivOfClosedCompl p q h hp hq).symm = ⇑(Submodule.prodEquivOfIsCompl p q h).symm
        source
        @[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) :
        ↑(Submodule.linearProjOfClosedCompl p q h hp hq) = Submodule.linearProjOfIsCompl p q h
        source
        @[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) :
        ⇑(Submodule.linearProjOfClosedCompl p q h hp hq) = ⇑(Submodule.linearProjOfIsCompl p q h)
        source
        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) :
        Submodule.ClosedComplemented p
        source
        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) :
        Submodule.ClosedComplemented p

        Alias of Submodule.ClosedComplemented.of_isCompl_isClosed.

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