PacketTopology.lean

1 import PaperIRelease.PacketExactSequence
2 import KomorebiVerification.TopologicalCompletion
3 
4 /-!
5 # Closed invariant subspaces and Banach packet exact sequences
6 
7 The continuous maps bundle the same algebraic maps constructed in
8 `PacketDescent`, and their exactness is proved by those literal identifications.
9 The quotient carries its quotient norm; closedness supplies separation.
10 -/
11 
12 noncomputable section
13 set_option autoImplicit false
14 set_option linter.style.haveILetI false
15 
16 namespace Komorebi.Foundation.LinearProjectorFamily
17 
18 universe u v w
19 
20 variable {𝕜 : Type u} {X : Type v} {ι : Type w}
21 variable [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X]
22 variable [Fintype ι]
23 
24 /-- Bundle the original projector with its asserted continuity. -/
25 def boundedProjector (P : LinearProjectorFamily 𝕜 X ι)
26     (hP : ∀ i, Continuous (P.proj i)) (i : ι) : X →L[𝕜] X :=
27   ⟨P.proj i, hP i⟩
28 
29 theorem isClosed_range_of_bounded (P : LinearProjectorFamily 𝕜 X ι)
30     (hP : ∀ i, Continuous (P.proj i)) (i : ι) :
31     IsClosed (LinearMap.range (P.proj i) : Set X) := by
32   apply ContinuousLinearMap.IsIdempotentElem.isClosed_range
33     (p := P.boundedProjector hP i)
34   apply ContinuousLinearMap.ext
35   intro x
36   exact P.idempotent i x
37 
38 variable (P : LinearProjectorFamily 𝕜 X ι)
39 variable (hP : ∀ i, Continuous (P.proj i))
40 variable (K : Submodule 𝕜 X) (hK : P.Preserves K)
41 
42 /-- The original restricted projector, with inherited continuity. -/
43 def restrictedProjectorCLM (i : ι) : K →L[𝕜] K where
44   toLinearMap := (P.restrictTo K hK).proj i
45   cont := ((hP i).comp continuous_subtype_val).subtype_mk _
46 
47 @[simp] theorem restrictedProjectorCLM_toLinearMap (i : ι) :
48     (P.restrictedProjectorCLM hP K hK i).toLinearMap =
49       (P.restrictTo K hK).proj i := rfl
50 
51 /-- The quotient projector is the continuous quotient lift of `π ∘ P_i`. -/
52 def quotientProjectorCLM (i : ι) : (X ⧸ K) →L[𝕜] (X ⧸ K) :=
53   K.liftQL (K.mkQL.comp (P.boundedProjector hP i)) (by
54     intro x hx
55     change K.mkQ (P.proj i x) = 0
56     exact (Submodule.Quotient.mk_eq_zero K).mpr (hK i x hx))
57 
58 @[simp] theorem quotientProjectorCLM_toLinearMap (i : ι) :
59     (P.quotientProjectorCLM hP K hK i).toLinearMap =
60       (P.descendTo K hK).proj i := rfl
61 
62 @[simp] theorem quotientProjectorCLM_mkQ (i : ι) (x : X) :
63     P.quotientProjectorCLM hP K hK i (K.mkQ x) = K.mkQ (P.proj i x) := rfl
64 
65 /-- Quotient projectors satisfy the sharp inherited operator bound. -/
66 theorem quotientProjector_norm_apply_le (i : ι) (z : X ⧸ K) :
67     ‖P.quotientProjectorCLM hP K hK i z‖ ≤ ‖P.boundedProjector hP i‖ * ‖z‖ := by
68   let C := ‖P.boundedProjector hP i‖
69   have hC : 0 ≤ C := norm_nonneg _
70   apply le_of_forall_pos_le_add
71   intro ε hε
72   obtain ⟨x, hx, hnorm⟩ := Submodule.Quotient.norm_mk_lt z
73     (show 0 < ε / (C + 1) by positivity)
74   have hbase : ‖P.quotientProjectorCLM hP K hK i z‖ ≤ C * ‖x‖ := by
75     rw [← hx]
76     exact (Submodule.Quotient.norm_mk_le K (P.proj i x)).trans
77       ((P.boundedProjector hP i).le_opNorm x)
78   have hmul : C * ‖x‖ ≤ C * (‖z‖ + ε / (C + 1)) :=
79     mul_le_mul_of_nonneg_left hnorm.le hC
80   have hsmall : C * (ε / (C + 1)) ≤ ε := by
81     have hpos : 0 < C + 1 := by positivity
82     rw [← mul_div_assoc]
83     apply (div_le_iff₀ hpos).mpr
84     nlinarith
85   exact hbase.trans (hmul.trans (by nlinarith))
86 
87 /-- The quotient operator norm cannot exceed that of the original projector. -/
88 theorem quotientProjector_norm_le (i : ι) :
89     ‖P.quotientProjectorCLM hP K hK i‖ ≤ ‖P.boundedProjector hP i‖ :=
90   ContinuousLinearMap.opNorm_le_bound _ (norm_nonneg _)
91     (P.quotientProjector_norm_apply_le hP K hK i)
92 
93 /-- The actual packet inclusion is bounded as a composition of subtype maps. -/
94 def packetInclusionCLM (i : ι) :
95     LinearMap.range ((P.restrictTo K hK).proj i) →L[𝕜]
96       LinearMap.range (P.proj i) :=
97   (K.subtypeL.comp (LinearMap.range ((P.restrictTo K hK).proj i)).subtypeL).codRestrict
98     (LinearMap.range (P.proj i)) (fun x ↦ (P.packetInclusion K hK i x).property)
99 
100 @[simp] theorem packetInclusionCLM_toLinearMap (i : ι) :
101     (P.packetInclusionCLM K hK i).toLinearMap = P.packetInclusion K hK i := rfl
102 
103 /-- The actual packet quotient map is bounded as the restriction and
104 corestriction of the ambient quotient map. -/
105 def packetQuotientCLM (i : ι) :
106     LinearMap.range (P.proj i) →L[𝕜]
107       LinearMap.range ((P.descendTo K hK).proj i) :=
108   (K.mkQL.comp (LinearMap.range (P.proj i)).subtypeL).codRestrict
109     (LinearMap.range ((P.descendTo K hK).proj i))
110     (fun x ↦ (P.packetQuotientMap K hK i x).property)
111 
112 @[simp] theorem packetQuotientCLM_toLinearMap (i : ι) :
113     (P.packetQuotientCLM K hK i).toLinearMap = P.packetQuotientMap K hK i := rfl
114 
115 theorem packetQuotientCLM_norm_le_one (i : ι) :
116     ‖P.packetQuotientCLM K hK i‖ ≤ 1 := by
117   apply ContinuousLinearMap.opNorm_le_bound _ zero_le_one
118   intro x
119   change ‖(Submodule.Quotient.mk (x : X) : X ⧸ K)‖ ≤ 1 * ‖x‖
120   simpa using (Submodule.Quotient.norm_mk_le K (x : X))
121 
122 /-- The submodule `X_i ∩ K`, expressed inside `X_i`. -/
123 abbrev packetIntersection (i : ι) : Submodule 𝕜 (LinearMap.range (P.proj i)) :=
124   K.comap (LinearMap.range (P.proj i)).subtype
125 
126 /-- Factor the actual continuous packet quotient map through its kernel. -/
127 def packetQuotientLiftCLM (i : ι) :
128     (LinearMap.range (P.proj i) ⧸ P.packetIntersection K i) →L[𝕜]
129       LinearMap.range ((P.descendTo K hK).proj i) :=
130   (P.packetIntersection K i).liftQL (P.packetQuotientCLM K hK i) (by
131     rw [packetQuotientCLM_toLinearMap, P.packetQuotientMap_ker])
132 
133 /-- Project and then take the quotient of the source packet. -/
134 def projectToPacketQuotient (i : ι) :
135     X →L[𝕜] (LinearMap.range (P.proj i) ⧸ P.packetIntersection K i) :=
136   (P.packetIntersection K i).mkQL.comp
137     ((P.boundedProjector hP i).codRestrict (LinearMap.range (P.proj i))
138       (fun x ↦ ⟨x, rfl⟩))
139 
140 /-- This inverse is induced from the actual bounded projector, using
141 invariance to prove that the projected map vanishes on `K`. -/
142 def packetQuotientInverseAmbient (i : ι) :
143     (X ⧸ K) →L[𝕜] (LinearMap.range (P.proj i) ⧸ P.packetIntersection K i) :=
144   K.liftQL (P.projectToPacketQuotient hP K i) (by
145     intro x hx
146     change Submodule.Quotient.mk (⟨P.proj i x, ⟨x, rfl⟩⟩ : LinearMap.range (P.proj i)) = 0
147     apply (Submodule.Quotient.mk_eq_zero (P.packetIntersection K i)).mpr
148     exact hK i x hx)
149 
150 def packetQuotientInverseCLM (i : ι) :
151     LinearMap.range ((P.descendTo K hK).proj i) →L[𝕜]
152       (LinearMap.range (P.proj i) ⧸ P.packetIntersection K i) :=
153   (P.packetQuotientInverseAmbient hP K hK i).comp
154     (LinearMap.range ((P.descendTo K hK).proj i)).subtypeL
155 
156 /-- The quotient identification is a bounded linear equivalence. Its inverse
157 is constructed from `P_i`, so no open-mapping hypothesis or supplied inverse
158 is being smuggled into the statement. -/
159 def packetQuotientEquivL (i : ι) :
160     (LinearMap.range (P.proj i) ⧸ P.packetIntersection K i) ≃L[𝕜]
161       LinearMap.range ((P.descendTo K hK).proj i) :=
162   ContinuousLinearEquiv.equivOfInverse
163     (P.packetQuotientLiftCLM K hK i) (P.packetQuotientInverseCLM hP K hK i)
164     (by
165       intro z
166       obtain ⟨x, rfl⟩ := (P.packetIntersection K i).mkQ_surjective z
167       change Submodule.Quotient.mk
168         (⟨P.proj i (x : X), ⟨(x : X), rfl⟩⟩ : LinearMap.range (P.proj i)) =
169         Submodule.Quotient.mk x
170       congr 1
171       exact Subtype.ext (P.proj_eq_self_of_mem_range i x.property))
172     (by
173       intro z
174       apply Subtype.ext
175       obtain ⟨x, hx⟩ := K.mkQ_surjective (z : X ⧸ K)
176       have hz := (P.descendTo K hK).proj_eq_self_of_mem_range i z.property
177       rw [← hx] at hz
178       change K.mkQ (P.proj i x) = K.mkQ x at hz
179       change (P.packetQuotientLiftCLM K hK i
180         (P.packetQuotientInverseAmbient hP K hK i (z : X ⧸ K)) : X ⧸ K) = _
181       rw [← hx]
182       exact hz)
183 
184 @[simp] theorem packetQuotientEquivL_mk (i : ι)
185     (x : LinearMap.range (P.proj i)) :
186     (P.packetQuotientEquivL hP K hK i (Submodule.Quotient.mk x) : X ⧸ K) =
187       K.mkQ (x : X) := rfl
188 
189 include hK in
190 /-- The projector is the identity modulo `K` on the sum `X_i + K`. -/
191 theorem packetSum_proj_modK (i : ι) (x : ↥(LinearMap.range (P.proj i) ⊔ K)) :
192     K.mkQ (P.proj i (x : X)) = K.mkQ (x : X) := by
193   obtain ⟨a, ha, b, hb, hab⟩ := Submodule.mem_sup.mp x.property
194   have hb0 : K.mkQ b = 0 := (Submodule.Quotient.mk_eq_zero K).mpr hb
195   have hPb0 : K.mkQ (P.proj i b) = 0 :=
196     (Submodule.Quotient.mk_eq_zero K).mpr (hK i b hb)
197   rw [← hab, map_add, P.proj_eq_self_of_mem_range i ha, map_add, map_add, hb0, hPb0]
198 
199 /-- Restrict the quotient map to `X_i + K` and corestrict to the quotient packet. -/
200 def packetSumQuotientMapCLM (i : ι) :
201     ↥(LinearMap.range (P.proj i) ⊔ K) →L[𝕜]
202       LinearMap.range ((P.descendTo K hK).proj i) :=
203   (K.mkQL.comp (LinearMap.range (P.proj i) ⊔ K).subtypeL).codRestrict
204     (LinearMap.range ((P.descendTo K hK).proj i))
205     (fun x ↦ ⟨K.mkQ (x : X), P.packetSum_proj_modK K hK i x⟩)
206 
207 def packetSumQuotientLiftCLM (i : ι) :
208     (↥(LinearMap.range (P.proj i) ⊔ K) ⧸
209       K.comap (LinearMap.range (P.proj i) ⊔ K).subtype) →L[𝕜]
210         LinearMap.range ((P.descendTo K hK).proj i) :=
211   (K.comap (LinearMap.range (P.proj i) ⊔ K).subtype).liftQL
212     (P.packetSumQuotientMapCLM K hK i) (by
213       intro x hx
214       apply Subtype.ext
215       exact (Submodule.Quotient.mk_eq_zero K).mpr hx)
216 
217 /-- Project from the ambient quotient into the sum quotient. -/
218 def packetSumQuotientInverseAmbient (i : ι) :
219     (X ⧸ K) →L[𝕜]
220       (↥(LinearMap.range (P.proj i) ⊔ K) ⧸
221         K.comap (LinearMap.range (P.proj i) ⊔ K).subtype) :=
222   K.liftQL
223     ((K.comap (LinearMap.range (P.proj i) ⊔ K).subtype).mkQL.comp
224       ((P.boundedProjector hP i).codRestrict (LinearMap.range (P.proj i) ⊔ K)
225         (fun x ↦ Submodule.mem_sup.mpr ⟨P.proj i x, ⟨x, rfl⟩, 0, K.zero_mem, add_zero _⟩)))
226     (by
227       intro x hx
228       apply (Submodule.Quotient.mk_eq_zero
229         (K.comap (LinearMap.range (P.proj i) ⊔ K).subtype)).mpr
230       exact hK i x hx)
231 
232 /-- The quotient packet is also boundedly isomorphic to `(X_i + K)/K`. -/
233 def packetSumQuotientEquivL (i : ι) :
234     (↥(LinearMap.range (P.proj i) ⊔ K) ⧸
235       K.comap (LinearMap.range (P.proj i) ⊔ K).subtype) ≃L[𝕜]
236         LinearMap.range ((P.descendTo K hK).proj i) :=
237   ContinuousLinearEquiv.equivOfInverse
238     (P.packetSumQuotientLiftCLM K hK i)
239     ((P.packetSumQuotientInverseAmbient hP K hK i).comp
240       (LinearMap.range ((P.descendTo K hK).proj i)).subtypeL)
241     (by
242       intro z
243       obtain ⟨x, rfl⟩ :=
244         (K.comap (LinearMap.range (P.proj i) ⊔ K).subtype).mkQ_surjective z
245       apply (Submodule.Quotient.eq
246         (K.comap (LinearMap.range (P.proj i) ⊔ K).subtype)).mpr
247       exact (Submodule.Quotient.eq K).mp (P.packetSum_proj_modK K hK i x))
248     (by
249       intro z
250       apply Subtype.ext
251       obtain ⟨x, hx⟩ := K.mkQ_surjective (z : X ⧸ K)
252       have hz := (P.descendTo K hK).proj_eq_self_of_mem_range i z.property
253       rw [← hx] at hz
254       change K.mkQ (P.proj i x) = K.mkQ x at hz
255       change (P.packetSumQuotientLiftCLM K hK i
256         (P.packetSumQuotientInverseAmbient hP K hK i (z : X ⧸ K)) : X ⧸ K) = _
257       rw [← hx]
258       exact hz)
259 
260 include hP
261 
262 theorem isClosed_restricted_packet (i : ι) :
263     IsClosed (LinearMap.range ((P.restrictTo K hK).proj i) : Set K) :=
264   (P.restrictTo K hK).isClosed_range_of_bounded
265     (fun j ↦ (P.restrictedProjectorCLM hP K hK j).continuous) i
266 
267 variable [hclosed : IsClosed (K : Set X)]
268 
269 theorem isClosed_quotient_packet (i : ι) :
270     IsClosed (LinearMap.range ((P.descendTo K hK).proj i) : Set (X ⧸ K)) :=
271   (P.descendTo K hK).isClosed_range_of_bounded
272     (fun j ↦ (P.quotientProjectorCLM hP K hK j).continuous) i
273 
274 include hK in
275 /-- Invariance makes `X_i + K` closed: it is the inverse image of the closed
276 quotient packet. This is stronger than closedness of two arbitrary summands. -/
277 theorem isClosed_packet_sum (i : ι) :
278     IsClosed ((LinearMap.range (P.proj i) ⊔ K : Submodule 𝕜 X) : Set X) := by
279   have h := (P.isClosed_quotient_packet hP K hK i).preimage K.mkQL.continuous
280   change IsClosed ((LinearMap.range ((P.descendTo K hK).proj i)).comap K.mkQ : Set X) at h
281   rwa [P.descendTo_range_preimage] at h
282 
283 /-- Every term of the packet sequence is complete under the inherited norm. -/
284 theorem packet_sequence_complete [CompleteSpace X] (i : ι) :
285     CompleteSpace (LinearMap.range ((P.restrictTo K hK).proj i)) ∧
286       CompleteSpace (LinearMap.range (P.proj i)) ∧
287       CompleteSpace (LinearMap.range ((P.descendTo K hK).proj i)) := by
288   letI : IsClosed (LinearMap.range ((P.restrictTo K hK).proj i) : Set K) :=
289     P.isClosed_restricted_packet hP K hK i
290   letI : IsClosed (LinearMap.range (P.proj i) : Set X) :=
291     P.isClosed_range_of_bounded hP i
292   letI : IsClosed (LinearMap.range ((P.descendTo K hK).proj i) : Set (X ⧸ K)) :=
293     P.isClosed_quotient_packet hP K hK i
294   exact ⟨inferInstance, inferInstance, inferInstance⟩
295 
296 /-- Paper I's topological packet exact sequence: the actual packet maps are
297 bounded, injective/exact/surjective, their three spaces are Banach, and the
298 constructed quotient projector has norm at most the original projector. -/
299 theorem banach_packet_shortExact [CompleteSpace X] (i : ι) :
300     CompleteSpace (LinearMap.range ((P.restrictTo K hK).proj i)) ∧
301       CompleteSpace (LinearMap.range (P.proj i)) ∧
302       CompleteSpace (LinearMap.range ((P.descendTo K hK).proj i)) ∧
303       Function.Injective (P.packetInclusionCLM K hK i) ∧
304       LinearMap.range (P.packetInclusionCLM K hK i).toLinearMap =
305         LinearMap.ker (P.packetQuotientCLM K hK i).toLinearMap ∧
306       Function.Surjective (P.packetQuotientCLM K hK i) ∧
307       ‖P.quotientProjectorCLM hP K hK i‖ ≤ ‖P.boundedProjector hP i‖ := by
308   obtain ⟨h1, h2, h3⟩ := P.packet_sequence_complete hP K hK i
309   obtain ⟨hinj, hexact, hsurj⟩ := P.packet_shortExact K hK i
310   exact ⟨h1, h2, h3, hinj, hexact, hsurj, P.quotientProjector_norm_le hP K hK i⟩
311 
312 end Komorebi.Foundation.LinearProjectorFamily
313 
314 #print axioms Komorebi.Foundation.LinearProjectorFamily.banach_packet_shortExact
315 #print axioms Komorebi.Foundation.LinearProjectorFamily.quotientProjector_norm_le
316 #print axioms Komorebi.Foundation.LinearProjectorFamily.packetQuotientEquivL
317 #print axioms Komorebi.Foundation.LinearProjectorFamily.packetSumQuotientEquivL

Back to source controls