SplitDefectCharts.lean

1 import Mathlib.Analysis.Normed.Operator.NormedSpace
2 import Mathlib.Tactic.Abel
3 import Mathlib.Tactic.Ring
4 import Mathlib.Tactic.Linarith
5 
6 set_option autoImplicit false
7 
8 /-!
9 # Intrinsic exact core and changes of residual coordinates
10 
11 The kernel and residual space are fixed by the differential. A bounded right
12 inverse selects a chart and a retraction, not a new exact core. Differences
13 between right inverses take values in that core. No completeness is needed.
14 -/
15 universe u v w
16 noncomputable section
17 namespace KomorebiSpace
18 namespace SplitDefect
19 variable {𝕜 : Type u} [NontriviallyNormedField 𝕜]
20 variable {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
21 variable {R : Type w} [NormedAddCommGroup R] [NormedSpace 𝕜 R]
22 variable (d : E →L[𝕜] R)
23 
24 /-- A chosen bounded right inverse of the fixed differential. -/
25 structure Section where
26   lift : R →L[𝕜] E
27   right_inv : ∀ r, d (lift r) = r
28 
29 /-- This space is independent of any section. -/
30 abbrev Core := d.ker
31 
32 namespace Section
33 variable {d} (A B C : Section d)
34 
35 @[ext] theorem ext (h : A.lift = B.lift) : A = B := by
36   cases A
37   cases B
38   cases h
39   rfl
40 
41 /-- The retraction onto the fixed exact core selected by the section. -/
42 def project : E →L[𝕜] E :=
43   ContinuousLinearMap.id 𝕜 E - A.lift.comp d
44 
45 @[simp] theorem project_apply (f : E) : A.project f = f - A.lift (d f) := rfl
46 
47 @[simp] theorem project_exact (f : E) : d (A.project f) = 0 := by
48   simp only [project_apply, map_sub, A.right_inv, sub_self]
49 
50 @[simp] theorem project_fixes (f : E) (hf : d f = 0) : A.project f = f := by
51   simp [project_apply, hf]
52 
53 @[simp] theorem project_idempotent (f : E) : A.project (A.project f) = A.project f :=
54   A.project_fixes _ (A.project_exact f)
55 
56 @[simp] theorem project_lift (r : R) : A.project (A.lift r) = 0 := by
57   simp only [project_apply, A.right_inv, sub_self]
58 
59 /-- The displacement from chart B to chart A, with values in the exact core. -/
60 def difference : R →L[𝕜] Core d :=
61   (A.lift - B.lift).codRestrict (Core d) (fun r => by
62     change d (A.lift r - B.lift r) = 0
63     rw [map_sub, A.right_inv, B.right_inv, sub_self])
64 
65 @[simp] theorem difference_apply (r : R) :
66     (A.difference B r : E) = A.lift r - B.lift r := rfl
67 
68 @[simp] theorem difference_exact (r : R) : d (A.lift r - B.lift r) = 0 := by
69   rw [map_sub, A.right_inv, B.right_inv, sub_self]
70 
71 @[simp] theorem difference_self : A.difference A = 0 := by
72   ext r
73   simp
74 
75 theorem difference_add (r : R) :
76     A.difference C r = A.difference B r + B.difference C r := by
77   apply Subtype.ext
78   change A.lift r - C.lift r = (A.lift r - B.lift r) + (B.lift r - C.lift r)
79   abel
80 
81 theorem project_change (f : E) :
82     B.project f - A.project f = (A.difference B (d f) : E) := by
83   simp only [project_apply, difference_apply]
84   abel
85 
86 theorem project_change_norm (f : E) :
87     ‖B.project f - A.project f‖ ≤ ‖A.lift - B.lift‖ * ‖d f‖ := by
88   rw [project_change, difference_apply]
89   exact (A.lift - B.lift).le_opNorm (d f)
90 
91 /-- Both retractions act as the identity on the same exact core. -/
92 @[simp] theorem project_other (f : E) : A.project (B.project f) = B.project f :=
93   A.project_fixes _ (B.project_exact f)
94 
95 /-- Retractions onto the same core need not commute. -/
96 theorem projects_commute_iff :
97     A.project.comp B.project = B.project.comp A.project ↔ A.project = B.project := by
98   constructor
99   · intro h
100     ext f
101     have hx := congrArg (fun T : E →L[𝕜] E => T f) h
102     simpa only [ContinuousLinearMap.comp_apply, project_other] using hx.symm
103   · intro h
104     rw [h]
105 
106 /-- Surjectivity of the differential makes the chosen section recoverable from its retraction. -/
107 theorem projects_equal_iff_lifts_equal : A.project = B.project ↔ A.lift = B.lift := by
108   constructor
109   · intro h
110     ext r
111     have h0 : B.project (A.lift r) = 0 := by
112       rw [← h]
113       exact A.project_lift r
114     have hx : A.lift r - B.lift r = 0 := by
115       simpa only [project_apply, A.right_inv] using h0
116     exact sub_eq_zero.mp hx
117   · intro h
118     unfold project
119     rw [h]
120 
121 /-- Explicit linear coordinates: exact component and unchanged residual. -/
122 def chartLinear : E ≃ₗ[𝕜] (Core d × R) where
123   toFun f := (⟨A.project f, A.project_exact f⟩, d f)
124   invFun z := z.1.val + A.lift z.2
125   left_inv f := by
126     change f - A.lift (d f) + A.lift (d f) = f
127     abel
128   right_inv z := by
129     apply Prod.ext
130     · apply Subtype.ext
131       change A.project (z.1.val + A.lift z.2) = z.1.val
132       rw [map_add, project_lift, add_zero]
133       exact A.project_fixes _ z.1.property
134     · change d (z.1.val + A.lift z.2) = z.2
135       have hz : d z.1.val = 0 := z.1.property
136       rw [map_add, hz, A.right_inv, zero_add]
137   map_add' f g := by
138     apply Prod.ext
139     · apply Subtype.ext
140       exact map_add A.project f g
141     · exact map_add d f g
142   map_smul' c f := by
143     apply Prod.ext
144     · apply Subtype.ext
145       exact map_smul A.project c f
146     · exact map_smul d c f
147 
148 theorem chart_bound (f : E) :
149     ‖A.chartLinear f‖ ≤ max ‖A.project‖ ‖d‖ * ‖f‖ := by
150   change max ‖A.project f‖ ‖d f‖ ≤ _
151   apply max_le
152   · exact (A.project.le_opNorm f).trans
153       (mul_le_mul_of_nonneg_right (le_max_left _ _) (norm_nonneg f))
154   · exact (d.le_opNorm f).trans
155       (mul_le_mul_of_nonneg_right (le_max_right _ _) (norm_nonneg f))
156 
157 theorem chart_inverse_bound (z : Core d × R) :
158     ‖A.chartLinear.symm z‖ ≤ (1 + ‖A.lift‖) * ‖z‖ := by
159   have h1 : ‖z.1.val‖ ≤ ‖z‖ := le_max_left _ _
160   have h2 : ‖z.2‖ ≤ ‖z‖ := le_max_right _ _
161   calc
162     ‖A.chartLinear.symm z‖ ≤ ‖z.1.val‖ + ‖A.lift z.2‖ := norm_add_le _ _
163     _ ≤ ‖z‖ + ‖A.lift‖ * ‖z.2‖ := add_le_add h1 (A.lift.le_opNorm _)
164     _ ≤ ‖z‖ + ‖A.lift‖ * ‖z‖ :=
165       add_le_add le_rfl (mul_le_mul_of_nonneg_left h2 (norm_nonneg _))
166     _ = (1 + ‖A.lift‖) * ‖z‖ := by ring
167 
168 /-- A bounded linear isomorphism, not an isometry. -/
169 def chart : E ≃L[𝕜] (Core d × R) :=
170   A.chartLinear.toContinuousLinearEquivOfBounds
171     (max ‖A.project‖ ‖d‖) (1 + ‖A.lift‖) A.chart_bound A.chart_inverse_bound
172 
173 @[simp] theorem chart_exact_component (f : E) : (A.chart f).1.val = A.project f := rfl
174 @[simp] theorem chart_residual (f : E) : (A.chart f).2 = d f := rfl
175 @[simp] theorem chart_inverse (z : Core d × R) : A.chart.symm z = z.1.val + A.lift z.2 := rfl
176 
177 /-- The transition acts on the same product, since neither factor depends on A. -/
178 def transition : (Core d × R) ≃L[𝕜] (Core d × R) := A.chart.symm.trans B.chart
179 
180 /-- All chart changes are triangular shears, fixing the residual coordinate. -/
181 theorem transition_formula (z : Core d × R) :
182     A.transition B z = (z.1 + A.difference B z.2, z.2) := by
183   apply Prod.ext
184   · apply Subtype.ext
185     change B.project (z.1.val + A.lift z.2) = z.1.val + (A.lift z.2 - B.lift z.2)
186     have hz : d z.1.val = 0 := z.1.property
187     rw [project_apply, map_add, hz, A.right_inv, zero_add]
188     abel
189   · change d (z.1.val + A.lift z.2) = z.2
190     have hz : d z.1.val = 0 := z.1.property
191     rw [map_add, hz, A.right_inv, zero_add]
192 
193 @[simp] theorem transition_residual (z : Core d × R) : (A.transition B z).2 = z.2 := by
194   rw [transition_formula]
195 
196 @[simp] theorem transition_exact_slice (e : Core d) : A.transition B (e, 0) = (e, 0) := by
197   rw [transition_formula]
198   simp
199 
200 @[simp] theorem transition_self (z : Core d × R) : A.transition A z = z := by
201   rw [transition_formula]
202   simp
203 
204 /-- The cocycle law is proved for the actual coordinate transitions. -/
205 theorem transition_cocycle (z : Core d × R) :
206     B.transition C (A.transition B z) = A.transition C z := by
207   rw [transition_formula, transition_formula, transition_formula, A.difference_add B C]
208   simp only [Prod.mk.injEq, and_true]
209   abel
210 
211 theorem transition_norm (z : Core d × R) :
212     ‖A.transition B z‖ ≤ (1 + ‖A.lift - B.lift‖) * ‖z‖ := by
213   rw [transition_formula]
214   change max ‖z.1.val + (A.lift z.2 - B.lift z.2)‖ ‖z.2‖ ≤ _
215   have h1 : ‖z.1.val‖ ≤ ‖z‖ := le_max_left _ _
216   have h2 : ‖z.2‖ ≤ ‖z‖ := le_max_right _ _
217   have h3 : ‖A.lift z.2 - B.lift z.2‖ ≤ ‖A.lift - B.lift‖ * ‖z‖ :=
218     ((A.lift - B.lift).le_opNorm _).trans
219       (mul_le_mul_of_nonneg_left h2 (norm_nonneg _))
220   apply max_le
221   · calc
222       _ ≤ ‖z.1.val‖ + ‖A.lift z.2 - B.lift z.2‖ := norm_add_le _ _
223       _ ≤ ‖z‖ + ‖A.lift - B.lift‖ * ‖z‖ := add_le_add h1 h3
224       _ = _ := by ring
225   · have hnon := mul_nonneg (norm_nonneg (A.lift - B.lift)) (norm_nonneg z)
226     nlinarith
227 
228 /-- Add any exact-valued bounded map to a section; it remains a section. -/
229 def translate (T : R →L[𝕜] Core d) : Section d where
230   lift := A.lift + (Core d).subtypeL.comp T
231   right_inv r := by
232     change d (A.lift r + (T r : E)) = r
233     have ht : d (T r : E) = 0 := (T r).property
234     rw [map_add, A.right_inv, ht, add_zero]
235 
236 @[simp] theorem translate_apply (T : R →L[𝕜] Core d) (r : R) :
237     (A.translate T).lift r = A.lift r + (T r : E) := rfl
238 
239 /-- Every other section differs by a unique exact-valued map. -/
240 def sectionParameters : (R →L[𝕜] Core d) ≃ Section d where
241   toFun := A.translate
242   invFun B := B.difference A
243   left_inv T := by
244     ext r
245     simp only [difference_apply, translate_apply]
246     abel
247   right_inv B := by
248     apply Section.ext
249     ext r
250     change A.lift r + (B.lift r - A.lift r) = B.lift r
251     abel
252 
253 end Section
254 end SplitDefect
255 end KomorebiSpace
256 end

Back to source controls