BanachViewBridge.lean

1 import KomorebiSpace.ResolutionViews
2 import KomorebiSpace.SplitTowerRepair
3 
4 set_option autoImplicit false
5 
6 /-!
7 # The checked Banach-tower repair acts on coherent ambient sections
8 
9 This bridge keeps the actual bonding functions and coordinate actions. It
10 adds no effective-descent or unrestricted realization assumption.
11 -/
12 universe u v
13 noncomputable section
14 namespace KomorebiSpace
15 namespace BanachTower
16 variable {𝕜 : Type u} [NontriviallyNormedField 𝕜]
17 variable (X Y : BanachTower.{u,v} 𝕜)
18 
19 def viewSystem : ViewSystem ℕ :=
20   (Resolution.Adjacent.resolution X.Obj (fun n => X.down n)).views
21 
22 def ambientPointEquiv : X.Point ≃ X.viewSystem.Ambient :=
23   (Resolution.Adjacent.pointEquiv X.Obj (fun n => X.down n)).trans
24     (Resolution.ambientEquiv _).symm
25 
26 @[simp] theorem ambientPointEquiv_coordinate (x : X.Point) (n : ℕ) :
27     (X.ambientPointEquiv x).val n = x.val n := rfl
28 
29 def exactAmbientMorphism (f : Candidates X Y) (hf : Exact X Y f) :
30     ViewSystem.Morphism X.viewSystem Y.viewSystem :=
31   (Resolution.Adjacent.map (fun n => f n) (fun n x =>
32     congrArg (fun T : X.Obj (n+1) →L[𝕜] Y.Obj n => T x) (hf n))).viewMorphism
33 
34 theorem exactAmbient_agrees (f : Candidates X Y) (hf : Exact X Y f) (x : X.Point) :
35     (exactAmbientMorphism X Y f hf).onAmbient (X.ambientPointEquiv x) =
36       Y.ambientPointEquiv (onLimit X Y f hf x) := rfl
37 
38 def repairedAmbientMorphism (L : Splitting Y)
39     (hgap : (L.bound : ℝ) * X.bound < 1) (f : Candidates X Y) :
40     ViewSystem.Morphism X.viewSystem Y.viewSystem :=
41   exactAmbientMorphism X Y (L.repair X hgap f) (L.repair_exact X hgap f)
42 
43 @[simp] theorem repairedAmbient_coordinate (L : Splitting Y)
44     (hgap : (L.bound : ℝ) * X.bound < 1) (f : Candidates X Y)
45     (x : X.viewSystem.Ambient) (n : ℕ) :
46     ((repairedAmbientMorphism X Y L hgap f).onAmbient x).val n =
47       (L.repair X hgap f) n (x.val n) := rfl
48 
49 theorem repairedAmbient_agrees (L : Splitting Y)
50     (hgap : (L.bound : ℝ) * X.bound < 1) (f : Candidates X Y) (x : X.Point) :
51     (repairedAmbientMorphism X Y L hgap f).onAmbient (X.ambientPointEquiv x) =
52       Y.ambientPointEquiv
53         (onLimit X Y (L.repair X hgap f) (L.repair_exact X hgap f) x) := rfl
54 
55 /-- Matching finite-prefix realizations glue to the existing Banach point type. -/
56 def prefixAmbientEquiv :
57     X.Point ≃ ViewSystem.Matching X.viewSystem Resolution.prefixViews :=
58   X.ambientPointEquiv.trans
59     (X.viewSystem.gluingEquiv Resolution.prefixViews Resolution.prefixViews_transitionCover)
60 
61 end BanachTower
62 end KomorebiSpace
63 end

Back to source controls