-
Notifications
You must be signed in to change notification settings - Fork 251
/
LinearPMap.lean
237 lines (190 loc) · 9.94 KB
/
LinearPMap.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
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
/-
Copyright (c) 2022 Moritz Doll. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Moritz Doll
-/
import Mathlib.LinearAlgebra.LinearPMap
import Mathlib.Topology.Algebra.Module.Basic
#align_import topology.algebra.module.linear_pmap from "leanprover-community/mathlib"@"f2ce6086713c78a7f880485f7917ea547a215982"
/-!
# Partially defined linear operators over topological vector spaces
We define basic notions of partially defined linear operators, which we call unbounded operators
for short.
In this file we prove all elementary properties of unbounded operators that do not assume that the
underlying spaces are normed.
## Main definitions
* `LinearPMap.IsClosed`: An unbounded operator is closed iff its graph is closed.
* `LinearPMap.IsClosable`: An unbounded operator is closable iff the closure of its graph is a
graph.
* `LinearPMap.closure`: For a closable unbounded operator `f : LinearPMap R E F` the closure is
the smallest closed extension of `f`. If `f` is not closable, then `f.closure` is defined as `f`.
* `LinearPMap.HasCore`: a submodule contained in the domain is a core if restricting to the core
does not lose information about the unbounded operator.
## Main statements
* `LinearPMap.closable_iff_exists_closed_extension`: an unbounded operator is closable iff it has a
closed extension.
* `LinearPMap.closable.exists_unique`: there exists a unique closure
* `LinearPMap.closureHasCore`: the domain of `f` is a core of its closure
## References
* [J. Weidmann, *Linear Operators in Hilbert Spaces*][weidmann_linear]
## Tags
Unbounded operators, closed operators
-/
open Topology
variable {R E F : Type*}
variable [CommRing R] [AddCommGroup E] [AddCommGroup F]
variable [Module R E] [Module R F]
variable [TopologicalSpace E] [TopologicalSpace F]
namespace LinearPMap
/-! ### Closed and closable operators -/
/-- An unbounded operator is closed iff its graph is closed. -/
def IsClosed (f : E →ₗ.[R] F) : Prop :=
_root_.IsClosed (f.graph : Set (E × F))
#align linear_pmap.is_closed LinearPMap.IsClosed
variable [ContinuousAdd E] [ContinuousAdd F]
variable [TopologicalSpace R] [ContinuousSMul R E] [ContinuousSMul R F]
/-- An unbounded operator is closable iff the closure of its graph is a graph. -/
def IsClosable (f : E →ₗ.[R] F) : Prop :=
∃ f' : LinearPMap R E F, f.graph.topologicalClosure = f'.graph
#align linear_pmap.is_closable LinearPMap.IsClosable
/-- A closed operator is trivially closable. -/
theorem IsClosed.isClosable {f : E →ₗ.[R] F} (hf : f.IsClosed) : f.IsClosable :=
⟨f, hf.submodule_topologicalClosure_eq⟩
#align linear_pmap.is_closed.is_closable LinearPMap.IsClosed.isClosable
/-- If `g` has a closable extension `f`, then `g` itself is closable. -/
theorem IsClosable.leIsClosable {f g : E →ₗ.[R] F} (hf : f.IsClosable) (hfg : g ≤ f) :
g.IsClosable := by
cases' hf with f' hf
have : g.graph.topologicalClosure ≤ f'.graph := by
rw [← hf]
exact Submodule.topologicalClosure_mono (le_graph_of_le hfg)
use g.graph.topologicalClosure.toLinearPMap
rw [Submodule.toLinearPMap_graph_eq]
exact fun _ hx hx' => f'.graph_fst_eq_zero_snd (this hx) hx'
#align linear_pmap.is_closable.le_is_closable LinearPMap.IsClosable.leIsClosable
/-- The closure is unique. -/
theorem IsClosable.existsUnique {f : E →ₗ.[R] F} (hf : f.IsClosable) :
∃! f' : E →ₗ.[R] F, f.graph.topologicalClosure = f'.graph := by
refine' exists_unique_of_exists_of_unique hf fun _ _ hy₁ hy₂ => eq_of_eq_graph _
rw [← hy₁, ← hy₂]
#align linear_pmap.is_closable.exists_unique LinearPMap.IsClosable.existsUnique
open scoped Classical
/-- If `f` is closable, then `f.closure` is the closure. Otherwise it is defined
as `f.closure = f`. -/
noncomputable def closure (f : E →ₗ.[R] F) : E →ₗ.[R] F :=
if hf : f.IsClosable then hf.choose else f
#align linear_pmap.closure LinearPMap.closure
theorem closure_def {f : E →ₗ.[R] F} (hf : f.IsClosable) : f.closure = hf.choose := by
simp [closure, hf]
#align linear_pmap.closure_def LinearPMap.closure_def
theorem closure_def' {f : E →ₗ.[R] F} (hf : ¬f.IsClosable) : f.closure = f := by simp [closure, hf]
#align linear_pmap.closure_def' LinearPMap.closure_def'
/-- The closure (as a submodule) of the graph is equal to the graph of the closure
(as a `LinearPMap`). -/
theorem IsClosable.graph_closure_eq_closure_graph {f : E →ₗ.[R] F} (hf : f.IsClosable) :
f.graph.topologicalClosure = f.closure.graph := by
rw [closure_def hf]
exact hf.choose_spec
#align linear_pmap.is_closable.graph_closure_eq_closure_graph LinearPMap.IsClosable.graph_closure_eq_closure_graph
/-- A `LinearPMap` is contained in its closure. -/
theorem le_closure (f : E →ₗ.[R] F) : f ≤ f.closure := by
by_cases hf : f.IsClosable
· refine' le_of_le_graph _
rw [← hf.graph_closure_eq_closure_graph]
exact (graph f).le_topologicalClosure
rw [closure_def' hf]
#align linear_pmap.le_closure LinearPMap.le_closure
theorem IsClosable.closure_mono {f g : E →ₗ.[R] F} (hg : g.IsClosable) (h : f ≤ g) :
f.closure ≤ g.closure := by
refine' le_of_le_graph _
rw [← (hg.leIsClosable h).graph_closure_eq_closure_graph]
rw [← hg.graph_closure_eq_closure_graph]
exact Submodule.topologicalClosure_mono (le_graph_of_le h)
#align linear_pmap.is_closable.closure_mono LinearPMap.IsClosable.closure_mono
/-- If `f` is closable, then the closure is closed. -/
theorem IsClosable.closure_isClosed {f : E →ₗ.[R] F} (hf : f.IsClosable) : f.closure.IsClosed := by
rw [IsClosed, ← hf.graph_closure_eq_closure_graph]
exact f.graph.isClosed_topologicalClosure
#align linear_pmap.is_closable.closure_is_closed LinearPMap.IsClosable.closure_isClosed
/-- If `f` is closable, then the closure is closable. -/
theorem IsClosable.closureIsClosable {f : E →ₗ.[R] F} (hf : f.IsClosable) : f.closure.IsClosable :=
hf.closure_isClosed.isClosable
#align linear_pmap.is_closable.closure_is_closable LinearPMap.IsClosable.closureIsClosable
theorem isClosable_iff_exists_closed_extension {f : E →ₗ.[R] F} :
f.IsClosable ↔ ∃ g : E →ₗ.[R] F, g.IsClosed ∧ f ≤ g :=
⟨fun h => ⟨f.closure, h.closure_isClosed, f.le_closure⟩, fun ⟨_, hg, h⟩ =>
hg.isClosable.leIsClosable h⟩
#align linear_pmap.is_closable_iff_exists_closed_extension LinearPMap.isClosable_iff_exists_closed_extension
/-! ### The core of a linear operator -/
/-- A submodule `S` is a core of `f` if the closure of the restriction of `f` to `S` is again `f`.-/
structure HasCore (f : E →ₗ.[R] F) (S : Submodule R E) : Prop where
le_domain : S ≤ f.domain
closure_eq : (f.domRestrict S).closure = f
#align linear_pmap.has_core LinearPMap.HasCore
theorem hasCore_def {f : E →ₗ.[R] F} {S : Submodule R E} (h : f.HasCore S) :
(f.domRestrict S).closure = f :=
h.2
#align linear_pmap.has_core_def LinearPMap.hasCore_def
/-- For every unbounded operator `f` the submodule `f.domain` is a core of its closure.
Note that we don't require that `f` is closable, due to the definition of the closure. -/
theorem closureHasCore (f : E →ₗ.[R] F) : f.closure.HasCore f.domain := by
refine' ⟨f.le_closure.1, _⟩
congr
ext x y hxy
· simp only [domRestrict_domain, Submodule.mem_inf, and_iff_left_iff_imp]
intro hx
exact f.le_closure.1 hx
let z : f.closure.domain := ⟨y.1, f.le_closure.1 y.2⟩
have hyz : (y : E) = z := by simp
rw [f.le_closure.2 hyz]
exact domRestrict_apply (hxy.trans hyz)
#align linear_pmap.closure_has_core LinearPMap.closureHasCore
/-! ### Topological properties of the inverse -/
section Inverse
variable {f : E →ₗ.[R] F}
/-- If `f` is invertible and closable as well as its closure being invertible, then
the graph of the inverse of the closure is given by the closure of the graph of the inverse. -/
theorem closure_inverse_graph (hf : LinearMap.ker f.toFun = ⊥) (hf' : f.IsClosable)
(hcf : LinearMap.ker f.closure.toFun = ⊥) :
f.closure.inverse.graph = f.inverse.graph.topologicalClosure := by
rw [inverse_graph hf, inverse_graph hcf, ← hf'.graph_closure_eq_closure_graph]
apply SetLike.ext'
simp only [Submodule.topologicalClosure_coe, Submodule.map_coe, LinearEquiv.prodComm_apply]
apply (image_closure_subset_closure_image continuous_swap).antisymm
have h1 := Set.image_equiv_eq_preimage_symm f.graph (LinearEquiv.prodComm R E F).toEquiv
have h2 := Set.image_equiv_eq_preimage_symm (_root_.closure f.graph)
(LinearEquiv.prodComm R E F).toEquiv
simp only [LinearEquiv.coe_toEquiv, LinearEquiv.prodComm_apply,
LinearEquiv.coe_toEquiv_symm] at h1 h2
rw [h1, h2]
apply continuous_swap.closure_preimage_subset
/-- Assuming that `f` is invertible and closable, then the closure is invertible if and only
if the inverse of `f` is closable. -/
theorem inverse_isClosable_iff (hf : LinearMap.ker f.toFun = ⊥) (hf' : f.IsClosable) :
f.inverse.IsClosable ↔ LinearMap.ker f.closure.toFun = ⊥ := by
constructor
· intro ⟨f', h⟩
rw [LinearMap.ker_eq_bot']
intro ⟨x, hx⟩ hx'
simp only [Submodule.mk_eq_zero]
rw [toFun_eq_coe, eq_comm, image_iff] at hx'
have : (0, x) ∈ graph f' := by
rw [← h, inverse_graph hf]
rw [← hf'.graph_closure_eq_closure_graph, ← SetLike.mem_coe,
Submodule.topologicalClosure_coe] at hx'
apply image_closure_subset_closure_image continuous_swap
simp only [Set.mem_image, Prod.exists, Prod.swap_prod_mk, Prod.mk.injEq]
exact ⟨x, 0, hx', rfl, rfl⟩
exact graph_fst_eq_zero_snd f' this rfl
· intro h
use f.closure.inverse
exact (closure_inverse_graph hf hf' h).symm
/-- If `f` is invertible and closable, then taking the closure and the inverse commute. -/
theorem inverse_closure (hf : LinearMap.ker f.toFun = ⊥) (hf' : f.IsClosable)
(hcf : LinearMap.ker f.closure.toFun = ⊥) :
f.inverse.closure = f.closure.inverse := by
apply eq_of_eq_graph
rw [closure_inverse_graph hf hf' hcf,
((inverse_isClosable_iff hf hf').mpr hcf).graph_closure_eq_closure_graph]
end Inverse
end LinearPMap