-
Notifications
You must be signed in to change notification settings - Fork 259
/
Complemented.lean
146 lines (112 loc) · 7.28 KB
/
Complemented.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
/-
Copyright (c) 2020 Yury Kudryashov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yury Kudryashov
-/
import Mathlib.Analysis.NormedSpace.Banach
import Mathlib.Topology.Algebra.Module.FiniteDimension
#align_import analysis.normed_space.complemented from "leanprover-community/mathlib"@"3397560e65278e5f31acefcdea63138bd53d1cd4"
/-!
# 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
-/
variable {𝕜 E F G : Type*} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
[NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G]
noncomputable section
open LinearMap (ker range)
namespace ContinuousLinearMap
section
variable [CompleteSpace 𝕜]
theorem ker_closedComplemented_of_finiteDimensional_range (f : E →L[𝕜] F)
[FiniteDimensional 𝕜 (range f)] : (ker f).ClosedComplemented := by
set f' : E →L[𝕜] range f := f.codRestrict _ (LinearMap.mem_range_self (f : E →ₗ[𝕜] F))
rcases f'.exists_right_inverse_of_surjective (f : E →ₗ[𝕜] F).range_rangeRestrict with ⟨g, hg⟩
simpa only [f', ker_codRestrict] using f'.closedComplemented_ker_of_rightInverse g (ext_iff.1 hg)
#align continuous_linear_map.ker_closed_complemented_of_finite_dimensional_range ContinuousLinearMap.ker_closedComplemented_of_finiteDimensional_range
end
variable [CompleteSpace E] [CompleteSpace (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`. -/
nonrec def equivProdOfSurjectiveOfIsCompl (f : E →L[𝕜] F) (g : E →L[𝕜] G) (hf : range f = ⊤)
(hg : range g = ⊤) (hfg : IsCompl (ker f) (ker g)) : E ≃L[𝕜] F × G :=
(f.equivProdOfSurjectiveOfIsCompl (g : E →ₗ[𝕜] G) hf hg hfg).toContinuousLinearEquivOfContinuous
(f.continuous.prod_mk g.continuous)
#align continuous_linear_map.equiv_prod_of_surjective_of_is_compl ContinuousLinearMap.equivProdOfSurjectiveOfIsCompl
@[simp]
theorem coe_equivProdOfSurjectiveOfIsCompl {f : E →L[𝕜] F} {g : E →L[𝕜] G} (hf : range f = ⊤)
(hg : range g = ⊤) (hfg : IsCompl (ker f) (ker g)) :
(equivProdOfSurjectiveOfIsCompl f g hf hg hfg : E →ₗ[𝕜] F × G) = f.prod g := rfl
#align continuous_linear_map.coe_equiv_prod_of_surjective_of_is_compl ContinuousLinearMap.coe_equivProdOfSurjectiveOfIsCompl
@[simp]
theorem equivProdOfSurjectiveOfIsCompl_toLinearEquiv {f : E →L[𝕜] F} {g : E →L[𝕜] G}
(hf : range f = ⊤) (hg : range g = ⊤) (hfg : IsCompl (ker f) (ker g)) :
(equivProdOfSurjectiveOfIsCompl f g hf hg hfg).toLinearEquiv =
LinearMap.equivProdOfSurjectiveOfIsCompl f g hf hg hfg := rfl
#align continuous_linear_map.equiv_prod_of_surjective_of_is_compl_to_linear_equiv ContinuousLinearMap.equivProdOfSurjectiveOfIsCompl_toLinearEquiv
@[simp]
theorem equivProdOfSurjectiveOfIsCompl_apply {f : E →L[𝕜] F} {g : E →L[𝕜] G} (hf : range f = ⊤)
(hg : range g = ⊤) (hfg : IsCompl (ker f) (ker g)) (x : E) :
equivProdOfSurjectiveOfIsCompl f g hf hg hfg x = (f x, g x) := rfl
#align continuous_linear_map.equiv_prod_of_surjective_of_is_compl_apply ContinuousLinearMap.equivProdOfSurjectiveOfIsCompl_apply
end ContinuousLinearMap
namespace Submodule
variable [CompleteSpace E] (p q : Subspace 𝕜 E)
/-- If `q` is a closed complement of a closed subspace `p`, then `p × q` is continuously
isomorphic to `E`. -/
def prodEquivOfClosedCompl (h : IsCompl p q) (hp : IsClosed (p : Set E))
(hq : IsClosed (q : Set E)) : (p × q) ≃L[𝕜] E := by
haveI := hp.completeSpace_coe; haveI := hq.completeSpace_coe
refine (p.prodEquivOfIsCompl q h).toContinuousLinearEquivOfContinuous ?_
exact (p.subtypeL.coprod q.subtypeL).continuous
#align subspace.prod_equiv_of_closed_compl Submodule.prodEquivOfClosedCompl
/-- Projection to a closed submodule along a closed complement. -/
def linearProjOfClosedCompl (h : IsCompl p q) (hp : IsClosed (p : Set E))
(hq : IsClosed (q : Set E)) : E →L[𝕜] p :=
ContinuousLinearMap.fst 𝕜 p q ∘L ↑(prodEquivOfClosedCompl p q h hp hq).symm
#align subspace.linear_proj_of_closed_compl Submodule.linearProjOfClosedCompl
variable {p q}
@[simp]
theorem coe_prodEquivOfClosedCompl (h : IsCompl p q) (hp : IsClosed (p : Set E))
(hq : IsClosed (q : Set E)) :
⇑(p.prodEquivOfClosedCompl q h hp hq) = p.prodEquivOfIsCompl q h := rfl
#align subspace.coe_prod_equiv_of_closed_compl Submodule.coe_prodEquivOfClosedCompl
@[simp]
theorem coe_prodEquivOfClosedCompl_symm (h : IsCompl p q) (hp : IsClosed (p : Set E))
(hq : IsClosed (q : Set E)) :
⇑(p.prodEquivOfClosedCompl q h hp hq).symm = (p.prodEquivOfIsCompl q h).symm := rfl
#align subspace.coe_prod_equiv_of_closed_compl_symm Submodule.coe_prodEquivOfClosedCompl_symm
@[simp]
theorem coe_continuous_linearProjOfClosedCompl (h : IsCompl p q) (hp : IsClosed (p : Set E))
(hq : IsClosed (q : Set E)) :
(p.linearProjOfClosedCompl q h hp hq : E →ₗ[𝕜] p) = p.linearProjOfIsCompl q h := rfl
#align subspace.coe_continuous_linear_proj_of_closed_compl Submodule.coe_continuous_linearProjOfClosedCompl
@[simp]
theorem coe_continuous_linearProjOfClosedCompl' (h : IsCompl p q) (hp : IsClosed (p : Set E))
(hq : IsClosed (q : Set E)) :
⇑(p.linearProjOfClosedCompl q h hp hq) = p.linearProjOfIsCompl q h := rfl
#align subspace.coe_continuous_linear_proj_of_closed_compl' Submodule.coe_continuous_linearProjOfClosedCompl'
theorem ClosedComplemented.of_isCompl_isClosed (h : IsCompl p q) (hp : IsClosed (p : Set E))
(hq : IsClosed (q : Set E)) : p.ClosedComplemented :=
⟨p.linearProjOfClosedCompl q h hp hq, Submodule.linearProjOfIsCompl_apply_left h⟩
#align subspace.closed_complemented_of_closed_compl Submodule.ClosedComplemented.of_isCompl_isClosed
alias IsCompl.closedComplemented_of_isClosed := ClosedComplemented.of_isCompl_isClosed
theorem closedComplemented_iff_isClosed_exists_isClosed_isCompl :
p.ClosedComplemented ↔
IsClosed (p : Set E) ∧ ∃ q : Submodule 𝕜 E, IsClosed (q : Set E) ∧ IsCompl p q :=
⟨fun h => ⟨h.isClosed, h.exists_isClosed_isCompl⟩,
fun ⟨hp, ⟨_, hq, hpq⟩⟩ => .of_isCompl_isClosed hpq hp hq⟩
#align subspace.closed_complemented_iff_has_closed_compl Submodule.closedComplemented_iff_isClosed_exists_isClosed_isCompl
theorem ClosedComplemented.of_quotient_finiteDimensional [CompleteSpace 𝕜]
[FiniteDimensional 𝕜 (E ⧸ p)] (hp : IsClosed (p : Set E)) : p.ClosedComplemented := by
obtain ⟨q, hq⟩ : ∃ q, IsCompl p q := p.exists_isCompl
haveI : FiniteDimensional 𝕜 q := (p.quotientEquivOfIsCompl q hq).finiteDimensional
exact .of_isCompl_isClosed hq hp q.closed_of_finiteDimensional
#align subspace.closed_complemented_of_quotient_finite_dimensional Submodule.ClosedComplemented.of_quotient_finiteDimensional
end Submodule