BanachReindexing.lean

1 import KomorebiSpace.AdjacentResolution
2 import KomorebiSpace.CofinalTransports
3 import KomorebiSpace.FiniteObservation
4 import KomorebiSpace.SplitTowerRepair
5 
6 set_option autoImplicit false
7 
8 /-!
9 # Actual Banach tower repairs enter the cofinal transport category
10 
11 This is a forgetful bridge: all bonding functions and coordinate actions are
12 preserved, but no invariance of sup norms, operator bounds, or residual norms
13 under resampling is asserted.
14 -/
15 
16 universe u v
17 noncomputable section
18 namespace KomorebiSpace
19 namespace BanachTower
20 open CategoryTheory
21 variable {𝕜 : Type u} [NontriviallyNormedField 𝕜]
22 variable (X Y : BanachTower.{u,v} 𝕜)
23 
24 def underlyingResolution : Resolution.{v} :=
25   Resolution.Adjacent.resolution X.Obj (fun n => X.down n)
26 
27 def resolutionPointEquiv : X.Point ≃ X.underlyingResolution.Point :=
28   Resolution.Adjacent.pointEquiv X.Obj (fun n => X.down n)
29 
30 @[simp] theorem resolutionPointEquiv_coordinate (x : X.Point) (n : ℕ) :
31     (X.resolutionPointEquiv x).val n = x.val n := rfl
32 
33 def exactResolutionMap (f : Candidates X Y) (hf : Exact X Y f) :
34     Resolution.Map X.underlyingResolution Y.underlyingResolution :=
35   Resolution.Adjacent.map (fun n => f n) (fun n x =>
36     congrArg (fun T : X.Obj (n+1) →L[𝕜] Y.Obj n => T x) (hf n))
37 
38 def exactEventualHom (f : Candidates X Y) (hf : Exact X Y f) :
39     X.underlyingResolution ⟶ Y.underlyingResolution :=
40   Resolution.EventualHom.ofMap (exactResolutionMap X Y f hf)
41 
42 /-- Agreement with the already proved analytic-tower realization, coordinate by coordinate. -/
43 theorem exactEventualHom_onLimit (f : Candidates X Y) (hf : Exact X Y f)
44     (x : X.Point) :
45     (exactEventualHom X Y f hf).onLimit (X.resolutionPointEquiv x) =
46     Y.resolutionPointEquiv (onLimit X Y f hf x) := rfl
47 
48 variable (φ ψ : ℕ → ℕ) (hφ : Monotone φ) (hψ : Monotone ψ)
49     (hφcof : Resolution.UnboundedSchedule φ) (hψcof : Resolution.UnboundedSchedule ψ)
50 
51 /-- The underlying exact transport class on independently resampled presentations. -/
52 def sampledExactHom (f : Candidates X Y) (hf : Exact X Y f) :
53     X.underlyingResolution.reindex φ hφ ⟶ Y.underlyingResolution.reindex ψ hψ :=
54   Resolution.cofinalHomEquiv X.underlyingResolution Y.underlyingResolution
55     φ ψ hφ hψ hφcof hψcof (exactEventualHom X Y f hf)
56 
57 theorem sampledExactHom_onLimit (f : Candidates X Y) (hf : Exact X Y f)
58     (x : (X.underlyingResolution.reindex φ hφ).Point) :
59     (sampledExactHom X Y φ ψ hφ hψ hφcof hψcof f hf).onLimit x =
60     Resolution.cofinalEquiv Y.underlyingResolution ψ hψ hψcof
61       ((exactEventualHom X Y f hf).onLimit
62         ((Resolution.cofinalEquiv X.underlyingResolution φ hφ hφcof).symm x)) :=
63   Resolution.cofinalHomEquiv_onLimit X.underlyingResolution Y.underlyingResolution
64     φ ψ hφ hψ hφcof hψcof (exactEventualHom X Y f hf) x
65 
66 /-- A transparent output-coordinate statement of the preceding conjugacy. -/
67 theorem sampledExactHom_coordinate (f : Candidates X Y) (hf : Exact X Y f)
68     (x : (X.underlyingResolution.reindex φ hφ).Point) (n : ℕ) :
69     ((sampledExactHom X Y φ ψ hφ hψ hφcof hψcof f hf).onLimit x).val n =
70     f (ψ n) (((Resolution.cofinalEquiv X.underlyingResolution φ hφ hφcof).symm x).val
71       (ψ n)) := by
72   rw [sampledExactHom_onLimit]
73   rfl
74 
75 /-- Reindexing an already exact repair gives the same realized global action. -/
76 def sampledRepair (L : Splitting Y) (hgap : (L.bound : ℝ) * X.bound < 1)
77     (f : Candidates X Y) :
78     X.underlyingResolution.reindex φ hφ ⟶ Y.underlyingResolution.reindex ψ hψ :=
79   sampledExactHom X Y φ ψ hφ hψ hφcof hψcof
80     (L.repair X hgap f) (L.repair_exact X hgap f)
81 
82 theorem sampledRepair_coordinate (L : Splitting Y)
83     (hgap : (L.bound : ℝ) * X.bound < 1) (f : Candidates X Y)
84     (x : (X.underlyingResolution.reindex φ hφ).Point) (n : ℕ) :
85     ((sampledRepair X Y φ ψ hφ hψ hφcof hψcof L hgap f).onLimit x).val n =
86     (L.repair X hgap f) (ψ n)
87       (((Resolution.cofinalEquiv X.underlyingResolution φ hφ hφcof).symm x).val
88         (ψ n)) :=
89   sampledExactHom_coordinate X Y φ ψ hφ hψ hφcof hψcof
90     (L.repair X hgap f) (L.repair_exact X hgap f) x n
91 
92 /-- Split source bonding maps make every finite input extendible to a coherent input. -/
93 theorem underlying_projection_surjective (L : Splitting X) :
94     X.underlyingResolution.ProjectionSurjective := by
95   apply Resolution.projectionSurjective_of_sections X.underlyingResolution (fun n => L.up n)
96   intro n x
97   have hs := Resolution.Adjacent.restrict_succ X.Obj (fun n => X.down n)
98     (Nat.le_refl n) (Nat.le_succ n) (L.up n x)
99   have hr := Resolution.Adjacent.restrict_refl X.Obj (fun n => X.down n) n
100     (X.down n (L.up n x))
101   exact (hs.trans hr).trans (L.down_up_apply n x)
102 
103 /-- With split source bonding maps, equality of realized functions reflects equality of classes. -/
104 theorem eventual_eq_iff_realization_eq (L : Splitting X)
105     (f g : X.underlyingResolution ⟶ Y.underlyingResolution) :
106     f = g ↔ f.onLimit = g.onLimit :=
107   Resolution.EventualHom.eq_iff_onLimit_eq (underlying_projection_surjective X L) f g
108 
109 /-- All eventual transports are exactly the finite-observation functions in this source class. -/
110 def underlyingFiniteObservationEquiv (L : Splitting X) :
111     (X.underlyingResolution ⟶ Y.underlyingResolution) ≃
112     {F : X.underlyingResolution.Point → Y.underlyingResolution.Point //
113       Resolution.FinitelyObserved F} :=
114   Resolution.finiteObservationEquiv (underlying_projection_surjective X L)
115 
116 @[simp] theorem underlyingFiniteObservationEquiv_apply (L : Splitting X)
117     (f : X.underlyingResolution ⟶ Y.underlyingResolution) :
118     (underlyingFiniteObservationEquiv X Y L f).val = f.onLimit := rfl
119 
120 end BanachTower
121 end KomorebiSpace
122 end

Back to source controls