GlobalRangeBundle.lean

1 module
2 public import Mathlib.Geometry.Manifold.Algebra.Structures
3 public import Mathlib.Geometry.Manifold.VectorBundle.Basic
4 public import Mathlib.Analysis.Calculus.ContDiff.Operations
5 public import Mathlib.Analysis.Normed.Ring.Units
6 public import Mathlib.Tactic
7 /-! Author: Komorebi P. Paper VII, item 6.4.
8 Construct the range-bundle atlas from a smooth idempotent, not as a hypothesis.
9 The fibers are the actual fixed subspaces, with their subspace topologies.
10 -/
11 @[expose] public section
12 set_option autoImplicit false
13 set_option backward.isDefEq.respectTransparency false
14 set_option backward.isDefEq.respectTransparency.types false
15 set_option linter.unusedSectionVars false
16 open scoped Manifold ContDiff Topology
17 open Set Filter
18 noncomputable section
19 namespace KomorebiPaperVII.RangeBundle
20 
21 variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
22 
23 /-- The actual fiber, written as the fixed subspace of an idempotent. -/
24 def fiber (p : F →L[ℝ] F) : Submodule ℝ F where
25   carrier := {v | p v = v}
26   zero_mem' := map_zero p
27   add_mem' := by intro u v hu hv; simp_all
28   smul_mem' := by intro c v hv; simp_all
29 
30 @[simp] theorem mem_fiber (p : F →L[ℝ] F) (v : F) : v ∈ fiber p ↔ p v = v := Iff.rfl
31 
32 /-- Projection from the ambient space to the actual fiber. -/
33 def project (p : F →L[ℝ] F) (hp : p*p=p) : F →L[ℝ] fiber p :=
34   p.codRestrict (fiber p) (fun v => congrArg (fun q : F →L[ℝ] F => q v) hp)
35 
36 @[simp] theorem project_coe (p : F →L[ℝ] F) (hp : p*p=p) (v : F) :
37     (project p hp v : F) = p v := rfl
38 
39 @[simp] theorem project_fiber (p : F →L[ℝ] F) (hp : p*p=p) (v : fiber p) :
40     project p hp (v : F) = v := Subtype.ext v.property
41 
42 /-- Canonical intertwiner between two nearby idempotents. -/
43 def transport (p q : F →L[ℝ] F) : F →L[ℝ] F := p*q+(1-p)*(1-q)
44 
45 theorem transport_self (p : F →L[ℝ] F) (hp : p*p=p) : transport p p=1 := by
46   unfold transport
47   noncomm_ring [hp]
48 
49 theorem transport_intertwines (p q : F →L[ℝ] F) (hp : p*p=p) (hq : q*q=q) :
50     p*transport p q=transport p q*q := by
51   unfold transport
52   have ha : p*(p*q)=p*q := by rw [← mul_assoc,hp]
53   have hb : p*(q*q)=p*q := by rw [hq]
54   noncomm_ring [hp,hq,ha,hb]
55 
56 theorem transport_inverse_intertwines (p q : F →L[ℝ] F) (hp : p*p=p) (hq : q*q=q)
57     (h : IsUnit (transport p q)) : q*Ring.inverse (transport p q)=Ring.inverse (transport p q)*p := by
58   calc
59     q*Ring.inverse (transport p q) =
60       Ring.inverse (transport p q)*(transport p q*q)*Ring.inverse (transport p q) := by
61         simp only [← mul_assoc, Ring.inverse_mul_cancel _ h, one_mul]
62     _ = Ring.inverse (transport p q)*(p*transport p q)*Ring.inverse (transport p q) := by
63       rw [transport_intertwines p q hp hq]
64     _ = Ring.inverse (transport p q)*p := by
65       simp only [mul_assoc, Ring.mul_inverse_cancel _ h, mul_one]
66 
67 variable {M : Type*} [TopologicalSpace M]
68 
69 /-- Each base point determines an open local trivialization domain. -/
70 def domain (P : M → F →L[ℝ] F) (a : M) : Set M :=
71   {x | IsUnit (transport (P x) (P a))}
72 
73 theorem mem_domain (P : M → F →L[ℝ] F) (hP : ∀ x, P x*P x=P x) (a : M) :
74     a ∈ domain P a := by simp [domain, transport_self _ (hP a)]
75 
76 theorem isOpen_domain [CompleteSpace F] (P : M → F →L[ℝ] F) (hP : Continuous P) (a : M) :
77     IsOpen (domain P a) :=
78   Units.isOpen.preimage ((hP.mul continuous_const).add
79     ((continuous_const.sub hP).mul continuous_const))
80 
81 /-- Fiber coordinates. The extra fixed projection makes this a total CLM. -/
82 def toCoord (P : M → F →L[ℝ] F) (hP : ∀ x, P x*P x=P x) (a x : M) :
83     F →L[ℝ] fiber (P a) :=
84   (project (P a) (hP a)).comp (Ring.inverse (transport (P x) (P a)))
85 
86 /-- Reconstruction from the coordinate fiber into the ambient space. -/
87 def fromCoord (P : M → F →L[ℝ] F) (a x : M) : fiber (P a) →L[ℝ] F :=
88   (transport (P x) (P a)).comp (fiber (P a)).subtypeL
89 
90 theorem fromCoord_range (P : M → F →L[ℝ] F) (hP : ∀ x, P x*P x=P x)
91     (a x : M) (v : fiber (P a)) : P x (fromCoord P a x v)=fromCoord P a x v := by
92   have ht := congrArg (fun q : F →L[ℝ] F => q (v : F))
93     (transport_intertwines (P x) (P a) (hP x) (hP a))
94   have hv : P a (v : F)=(v : F) := v.property
95   simpa [fromCoord, hv] using ht
96 
97 theorem toCoord_fromCoord (P : M → F →L[ℝ] F) (hP : ∀ x, P x*P x=P x)
98     (a x : M) (hx : x ∈ domain P a) (v : fiber (P a)) :
99     toCoord P hP a x (fromCoord P a x v)=v := by
100   apply Subtype.ext
101   change P a ((Ring.inverse (transport (P x) (P a)) * transport (P x) (P a)) (v : F)) = v
102   rw [Ring.inverse_mul_cancel _ hx]
103   exact v.property
104 
105 theorem fromCoord_toCoord (P : M → F →L[ℝ] F) (hP : ∀ x, P x*P x=P x)
106     (a x : M) (hx : x ∈ domain P a) (v : F) (hv : P x v=v) :
107     fromCoord P a x (toCoord P hP a x v)=v := by
108   have ht := congrArg (fun q : F →L[ℝ] F => q v)
109     (transport_inverse_intertwines (P x) (P a) (hP x) (hP a) hx)
110   change transport (P x) (P a) (P a (Ring.inverse (transport (P x) (P a)) v))=v
111   rw [show P a (Ring.inverse (transport (P x) (P a)) v)=
112     Ring.inverse (transport (P x) (P a)) v from by simpa [hv] using ht]
113   change (transport (P x) (P a)*Ring.inverse (transport (P x) (P a))) v=v
114   rw [Ring.mul_inverse_cancel _ hx]
115   rfl
116 
117 /-- The transition is an actual map between the two fixed coordinate fibers. -/
118 def transition (P : M → F →L[ℝ] F) (hP : ∀ x, P x*P x=P x) (a b x : M) :
119     fiber (P a) →L[ℝ] fiber (P b) := (toCoord P hP b x).comp (fromCoord P a x)
120 
121 theorem transition_self (P : M → F →L[ℝ] F) (hP : ∀ x, P x*P x=P x)
122     (a x : M) (hx : x ∈ domain P a) : transition P hP a a x=1 := by
123   apply ContinuousLinearMap.ext
124   intro v
125   exact toCoord_fromCoord P hP a x hx v
126 
127 theorem transition_cocycle (P : M → F →L[ℝ] F) (hP : ∀ x, P x*P x=P x)
128     (a b c x : M) (hb : x ∈ domain P b) :
129     (transition P hP b c x).comp (transition P hP a b x)=transition P hP a c x := by
130   apply ContinuousLinearMap.ext
131   intro v
132   change toCoord P hP c x (fromCoord P b x (toCoord P hP b x (fromCoord P a x v))) = _
133   rw [fromCoord_toCoord P hP b x hb _ (fromCoord_range P hP a x v)]
134   rfl
135 
136 variable {E H : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H]
137   {I : ModelWithCorners ℝ E H} [ChartedSpace H M] [CompleteSpace F]
138 
139 theorem smooth_transport (P : M → F →L[ℝ] F)
140     (hP : ContMDiff I 𝓘(ℝ, F →L[ℝ] F) ∞ P) (a : M) :
141     ContMDiff I 𝓘(ℝ, F →L[ℝ] F) ∞ (fun x => transport (P x) (P a)) :=
142   (hP.clm_comp contMDiff_const).add ((contMDiff_const.sub hP).clm_comp contMDiff_const)
143 
144 theorem smooth_inverse_transport (P : M → F →L[ℝ] F)
145     (hP : ContMDiff I 𝓘(ℝ, F →L[ℝ] F) ∞ P) (a : M) :
146     ContMDiffOn I 𝓘(ℝ, F →L[ℝ] F) ∞
147       (fun x => Ring.inverse (transport (P x) (P a))) (domain P a) := by
148   intro x hx
149   have hi : ContDiffAt ℝ ∞ Ring.inverse (transport (P x) (P a)) := by
150     simpa only [IsUnit.unit_spec] using (contDiffAt_ringInverse ℝ hx.unit (n := ∞))
151   exact hi.comp_contMDiffWithinAt (f := fun y : M => transport (P y) (P a))
152     ((smooth_transport P hP a x).contMDiffWithinAt)
153 
154 theorem smooth_toCoord (P : M → F →L[ℝ] F) (hPP : ∀ x, P x*P x=P x)
155     (hP : ContMDiff I 𝓘(ℝ, F →L[ℝ] F) ∞ P) (a : M) :
156     ContMDiffOn I 𝓘(ℝ, F →L[ℝ] fiber (P a)) ∞ (toCoord P hPP a) (domain P a) :=
157   contMDiffOn_const.clm_comp (smooth_inverse_transport P hP a)
158 
159 theorem smooth_fromCoord (P : M → F →L[ℝ] F)
160     (hP : ContMDiff I 𝓘(ℝ, F →L[ℝ] F) ∞ P) (a : M) :
161     ContMDiff I 𝓘(ℝ, fiber (P a) →L[ℝ] F) ∞ (fromCoord P a) :=
162   (smooth_transport P hP a).clm_comp contMDiff_const
163 
164 theorem smooth_transition (P : M → F →L[ℝ] F) (hPP : ∀ x, P x*P x=P x)
165     (hP : ContMDiff I 𝓘(ℝ, F →L[ℝ] F) ∞ P) (a b : M) :
166     ContMDiffOn I 𝓘(ℝ, fiber (P a) →L[ℝ] fiber (P b)) ∞
167       (transition P hPP a b) (domain P a ∩ domain P b) :=
168   ((smooth_toCoord P hPP hP b).mono inter_subset_right).clm_comp
169     (smooth_fromCoord P hP a).contMDiffOn
170 
171 
172 /-- Actual global range space, with the topology induced from `M × F`. -/
173 abbrev Total (P : M → F →L[ℝ] F) := {z : M × F // P z.1 z.2=z.2}
174 
175 /-- Restriction of the actual total space to a trivialization domain. -/
176 abbrev LocalTotal (P : M → F →L[ℝ] F) (a : M) :=
177   {z : Total P // z.val.1 ∈ domain P a}
178 
179 /-- The explicitly constructed fiberwise linear local product homeomorphism. -/
180 def localProduct (P : M → F →L[ℝ] F) (hPP : ∀ x, P x*P x=P x)
181     (hP : ContMDiff I 𝓘(ℝ, F →L[ℝ] F) ∞ P) (a : M) :
182     LocalTotal P a ≃ₜ (domain P a × fiber (P a)) where
183   toFun z := (⟨z.val.val.1,z.property⟩,toCoord P hPP a z.val.val.1 z.val.val.2)
184   invFun y := ⟨⟨(y.1.val,fromCoord P a y.1.val y.2),
185     fromCoord_range P hPP a y.1.val y.2⟩,y.1.property⟩
186   left_inv := by
187     intro z
188     apply Subtype.ext
189     apply Subtype.ext
190     apply Prod.ext
191     · rfl
192     · exact fromCoord_toCoord P hPP a _ z.property _ z.val.property
193   right_inv := by
194     intro y
195     apply Prod.ext
196     · rfl
197     · exact toCoord_fromCoord P hPP a _ y.1.property y.2
198   continuous_toFun := by
199     have hx : Continuous (fun z : LocalTotal P a => z.val.val.1) := by fun_prop
200     have hv : Continuous (fun z : LocalTotal P a => z.val.val.2) := by fun_prop
201     have hc : Continuous (fun z : LocalTotal P a => toCoord P hPP a z.val.val.1) :=
202       (smooth_toCoord P hPP hP a).continuousOn.comp_continuous hx (fun z => z.property)
203     exact (hx.subtype_mk _).prodMk (hc.clm_apply hv)
204   continuous_invFun := by
205     have hx : Continuous (fun y : domain P a × fiber (P a) => y.1.val) := by fun_prop
206     have hv : Continuous (fun y : domain P a × fiber (P a) => y.2) := by fun_prop
207     have hc : Continuous (fun y : domain P a × fiber (P a) => fromCoord P a y.1.val) :=
208       (smooth_fromCoord P hP a).continuous.comp hx
209     exact ((hx.prodMk (hc.clm_apply hv)).subtype_mk _).subtype_mk _
210 
211 /-- The local homeomorphism does not change the base point. -/
212 theorem localProduct_base (P : M → F →L[ℝ] F) (hPP : ∀ x, P x*P x=P x)
213     (hP : ContMDiff I 𝓘(ℝ, F →L[ℝ] F) ∞ P) (a : M) (z : LocalTotal P a) :
214     (localProduct P hPP hP a z).1.val=z.val.val.1 := rfl
215 
216 /-- Reconstruction of local coordinates is exactly the transition map. -/
217 theorem localProduct_transition (P : M → F →L[ℝ] F) (hPP : ∀ x, P x*P x=P x)
218     (a b x : M) (v : fiber (P a)) :
219     toCoord P hPP b x (fromCoord P a x v)=transition P hPP a b x v := rfl
220 
221 /-- A local fiber equivalence, derived from the same transport. -/
222 def fiberEquiv (P : M → F →L[ℝ] F) (hPP : ∀ x, P x*P x=P x)
223     (a x : M) (hx : x ∈ domain P a) : fiber (P a) ≃L[ℝ] fiber (P x) where
224   toFun v := ⟨fromCoord P a x v, fromCoord_range P hPP a x v⟩
225   invFun v := toCoord P hPP a x v
226   left_inv := toCoord_fromCoord P hPP a x hx
227   right_inv := fun v => Subtype.ext (fromCoord_toCoord P hPP a x hx v v.property)
228   map_add' := by intros; apply Subtype.ext; exact map_add _ _ _
229   map_smul' := by intros; apply Subtype.ext; exact map_smul _ _ _
230   continuous_toFun := (fromCoord P a x).continuous.subtype_mk _
231   continuous_invFun := (toCoord P hPP a x).continuous.comp continuous_subtype_val
232 
233 /-- Local constancy of rank is a consequence, not an additional hypothesis. -/
234 theorem fiber_rank_locally_constant (P : M → F →L[ℝ] F) (hPP : ∀ x, P x*P x=P x)
235     (hP : ContMDiff I 𝓘(ℝ, F →L[ℝ] F) ∞ P) (a : M) :
236     ∀ᶠ x in 𝓝 a, Module.finrank ℝ (fiber (P x))=Module.finrank ℝ (fiber (P a)) := by
237   filter_upwards [(isOpen_domain P hP.continuous a).mem_nhds (mem_domain P hPP a)] with x hx
238   exact (fiberEquiv P hPP a x hx).toLinearEquiv.finrank_eq.symm
239 
240 /-- All local data come from `P`. This bundles the actual construction and its smooth cocycle. -/
241 theorem smooth_range_bundle_atlas (P : M → F →L[ℝ] F) (hPP : ∀ x, P x*P x=P x)
242     (hP : ContMDiff I 𝓘(ℝ, F →L[ℝ] F) ∞ P) :
243     (∀ a, IsOpen (domain P a) ∧ a ∈ domain P a) ∧
244     (∀ a, Nonempty (LocalTotal P a ≃ₜ (domain P a × fiber (P a)))) ∧
245     (∀ a b, ContMDiffOn I 𝓘(ℝ, fiber (P a) →L[ℝ] fiber (P b)) ∞
246       (transition P hPP a b) (domain P a ∩ domain P b)) ∧
247     (∀ a x, x ∈ domain P a → transition P hPP a a x=1) ∧
248     (∀ a b c x, x ∈ domain P a ∩ domain P b ∩ domain P c →
249       (transition P hPP b c x).comp (transition P hPP a b x)=transition P hPP a c x) := by
250   exact ⟨fun a => ⟨isOpen_domain P hP.continuous a,mem_domain P hPP a⟩,
251     fun a => ⟨localProduct P hPP hP a⟩,smooth_transition P hPP hP,
252     transition_self P hPP,fun a b c x hx => transition_cocycle P hPP a b c x hx.1.2⟩
253 
254 end KomorebiPaperVII.RangeBundle
255 
256 /-! Declaration-level dependency audit. -/
257 #print axioms KomorebiPaperVII.RangeBundle.mem_fiber
258 #print axioms KomorebiPaperVII.RangeBundle.project_coe
259 #print axioms KomorebiPaperVII.RangeBundle.project_fiber
260 #print axioms KomorebiPaperVII.RangeBundle.transport_self
261 #print axioms KomorebiPaperVII.RangeBundle.transport_intertwines
262 #print axioms KomorebiPaperVII.RangeBundle.transport_inverse_intertwines
263 #print axioms KomorebiPaperVII.RangeBundle.mem_domain
264 #print axioms KomorebiPaperVII.RangeBundle.isOpen_domain
265 #print axioms KomorebiPaperVII.RangeBundle.fromCoord_range
266 #print axioms KomorebiPaperVII.RangeBundle.toCoord_fromCoord
267 #print axioms KomorebiPaperVII.RangeBundle.fromCoord_toCoord
268 #print axioms KomorebiPaperVII.RangeBundle.transition_self
269 #print axioms KomorebiPaperVII.RangeBundle.transition_cocycle
270 #print axioms KomorebiPaperVII.RangeBundle.smooth_transport
271 #print axioms KomorebiPaperVII.RangeBundle.smooth_inverse_transport
272 #print axioms KomorebiPaperVII.RangeBundle.smooth_toCoord
273 #print axioms KomorebiPaperVII.RangeBundle.smooth_fromCoord
274 #print axioms KomorebiPaperVII.RangeBundle.smooth_transition
275 #print axioms KomorebiPaperVII.RangeBundle.localProduct_base
276 #print axioms KomorebiPaperVII.RangeBundle.localProduct_transition
277 #print axioms KomorebiPaperVII.RangeBundle.fiber_rank_locally_constant
278 #print axioms KomorebiPaperVII.RangeBundle.smooth_range_bundle_atlas

Back to source controls