TopologyFiniteCompletion.lean

1 import KomorebiVerification.TopologicalCompletion
2 
3 /-! # The unique finite packet split on a dense completion -/
4 
5 noncomputable section
6 open scoped BigOperators
7 open Set Function
8 
9 namespace PaperIRelease.TopologyFiniteCompletion
10 
11 open KomorebiVerification.TopologicalCompletion
12 
13 variable {𝕜 X ι : Type*} [NontriviallyNormedField 𝕜]
14 variable [NormedAddCommGroup X] [NormedSpace 𝕜 X] [Fintype ι]
15 
16 /-- Bounded operators whose restrictions form a packet system on a dense
17 submodule form the same packet system on the ambient normed space. -/
18 def extendPacketFamily
19     (M : Submodule 𝕜 X) (hM : M.topologicalClosure = ⊤)
20     (P : ι → X →L[𝕜] X) (Q : BoundedProjectorFamily 𝕜 M ι)
21     (hext : ∀ i (x : M), P i x = (Q.proj i x : X)) :
22     BoundedProjectorFamily 𝕜 X ι where
23   proj := P
24   idempotent i x := by
25     have hd : DenseRange (fun y : M ↦ (y : X)) := by
26       exact (Submodule.dense_iff_topologicalClosure_eq_top.mpr hM).denseRange_val
27     have he : (fun y : X ↦ P i (P i y)) = (fun y : X ↦ P i y) := by
28       apply hd.equalizer (by fun_prop) (by fun_prop)
29       funext y
30       change P i (P i (y : X)) = P i (y : X)
31       rw [hext i y, hext i (Q.proj i y), Q.idempotent i y]
32     exact congrFun he x
33   annihilate := by
34     intro i j hij x
35     have hd : DenseRange (fun y : M ↦ (y : X)) := by
36       exact (Submodule.dense_iff_topologicalClosure_eq_top.mpr hM).denseRange_val
37     have he : (fun y : X ↦ P i (P j y)) = (fun _ : X ↦ (0 : X)) := by
38       apply hd.equalizer (by fun_prop) continuous_const
39       funext y
40       change P i (P j (y : X)) = 0
41       rw [hext j y, hext i (Q.proj j y), Q.annihilate hij y]
42       rfl
43     exact congrFun he x
44   complete x := by
45     have hd : DenseRange (fun y : M ↦ (y : X)) := by
46       exact (Submodule.dense_iff_topologicalClosure_eq_top.mpr hM).denseRange_val
47     have he : (fun y : X ↦ ∑ i, P i y) = (fun y : X ↦ y) := by
48       apply hd.equalizer (by fun_prop) continuous_id
49       funext y
50       change (∑ i, P i (y : X)) = (y : X)
51       simp_rw [hext]
52       exact_mod_cast Q.complete y
53     exact congrFun he x
54 
55 /-- Each extended packet is exactly the closure of its dense-subspace
56 packet. No closedness or completeness of the dense subspace is required. -/
57 theorem extended_packet_range
58     (M : Submodule 𝕜 X) (hM : M.topologicalClosure = ⊤)
59     (P : ι → X →L[𝕜] X) (Q : BoundedProjectorFamily 𝕜 M ι)
60     (hext : ∀ i (x : M), P i x = (Q.proj i x : X)) (i : ι) :
61     (M.map (P i).toLinearMap).topologicalClosure = (P i).range :=
62   BoundedProjectorFamily.idempotentRange_eq_closure_map (P i)
63     ((extendPacketFamily M hM P Q hext).idempotent i) M hM
64 
65 /-- There is at most one continuous ambient extension of every projector
66 in the dense packet system. This is uniqueness of the whole split, rather
67 than merely uniqueness of one extracted range. -/
68 theorem extension_unique
69     (M : Submodule 𝕜 X) (hM : M.topologicalClosure = ⊤)
70     (P R : ι → X →L[𝕜] X) (Q : BoundedProjectorFamily 𝕜 M ι)
71     (hP : ∀ i (x : M), P i x = (Q.proj i x : X))
72     (hR : ∀ i (x : M), R i x = (Q.proj i x : X)) : P = R := by
73   have hd : DenseRange (fun y : M ↦ (y : X)) := by
74     exact (Submodule.dense_iff_topologicalClosure_eq_top.mpr hM).denseRange_val
75   funext i
76   apply DFunLike.coe_injective
77   apply hd.equalizer (P i).continuous (R i).continuous
78   funext x
79   exact (hP i x).trans (hR i x).symm
80 
81 end PaperIRelease.TopologyFiniteCompletion

Back to source controls