CofinalTransports.lean

1 import KomorebiSpace.EventualCategory
2 import Mathlib.Data.Nat.Find
3 
4 set_option autoImplicit false
5 
6 /-!
7 # Cofinal schedules are isomorphisms of the eventual transport category
8 
9 The forward and inverse representatives are explicit. Inverse laws hold by
10 finite-stage eventual agreement and do not appeal to faithfulness of realization.
11 -/
12 
13 universe u v
14 namespace KomorebiSpace
15 namespace Resolution
16 open CategoryTheory
17 
18 /-- Least sampled input stage reaching a requested original level. -/
19 noncomputable def ceilingIndex {φ : ℕ → ℕ} (hcof : UnboundedSchedule φ)
20     (n : ℕ) : ℕ := Nat.find (hcof n)
21 
22 theorem ceilingIndex_spec {φ : ℕ → ℕ} (hcof : UnboundedSchedule φ) (n : ℕ) :
23     n ≤ φ (ceilingIndex hcof n) := Nat.find_spec (hcof n)
24 
25 theorem ceilingIndex_monotone {φ : ℕ → ℕ} (hcof : UnboundedSchedule φ) :
26     Monotone (ceilingIndex hcof) := by
27   intro i j hij
28   exact Nat.find_min' (hcof i) (hij.trans (ceilingIndex_spec hcof j))
29 
30 def sampleTransport (X : Resolution.{u}) (φ : ℕ → ℕ) (hφ : Monotone φ) :
31     ReindexedMap X (X.reindex φ hφ) where
32   level := φ
33   monotone := hφ
34   app := fun _ x => x
35   naturality := by intros; rfl
36 
37 noncomputable def recoverTransport (X : Resolution.{u}) (φ : ℕ → ℕ)
38     (hφ : Monotone φ) (hcof : UnboundedSchedule φ) :
39     ReindexedMap (X.reindex φ hφ) X where
40   level := ceilingIndex hcof
41   monotone := ceilingIndex_monotone hcof
42   app := fun n x => X.restrict (ceilingIndex_spec hcof n) x
43   naturality := by
44     intro i j hij x
45     change X.restrict hij (X.restrict (ceilingIndex_spec hcof j) x) =
46       X.restrict (ceilingIndex_spec hcof i)
47         (X.restrict (hφ (ceilingIndex_monotone hcof hij)) x)
48     exact (X.restrict_trans hij (ceilingIndex_spec hcof j) x).trans
49       (X.restrict_trans (ceilingIndex_spec hcof i)
50         (hφ (ceilingIndex_monotone hcof hij)) x).symm
51 
52 theorem sample_recover_eventually (X : Resolution.{u}) (φ : ℕ → ℕ)
53     (hφ : Monotone φ) (hcof : UnboundedSchedule φ) :
54     ReindexedMap.EventuallyEq
55       ((sampleTransport X φ hφ).comp (recoverTransport X φ hφ hcof))
56       (ReindexedMap.id X) := by
57   intro n
58   refine ⟨φ (ceilingIndex hcof n), le_refl _, ceilingIndex_spec hcof n, ?_⟩
59   intro x
60   change X.restrict (ceilingIndex_spec hcof n) (X.restrict (le_refl _) x) =
61     X.restrict (ceilingIndex_spec hcof n) x
62   rw [X.restrict_refl]
63 
64 theorem recover_sample_eventually (X : Resolution.{u}) (φ : ℕ → ℕ)
65     (hφ : Monotone φ) (hcof : UnboundedSchedule φ) :
66     ReindexedMap.EventuallyEq
67       ((recoverTransport X φ hφ hcof).comp (sampleTransport X φ hφ))
68       (ReindexedMap.id (X.reindex φ hφ)) := by
69   intro n
70   refine ⟨max (ceilingIndex hcof (φ n)) n,
71     Nat.le_max_left _ _, Nat.le_max_right _ _, ?_⟩
72   intro x
73   change X.restrict (ceilingIndex_spec hcof (φ n))
74     (X.restrict (hφ (Nat.le_max_left _ _)) x) =
75     X.restrict (hφ (Nat.le_max_right _ _)) x
76   exact X.restrict_trans (ceilingIndex_spec hcof (φ n))
77     (hφ (Nat.le_max_left _ _)) x
78 
79 /-- Actual isomorphism in the newly defined category of eventual transports. -/
80 noncomputable def cofinalIso (X : Resolution.{u}) (φ : ℕ → ℕ)
81     (hφ : Monotone φ) (hcof : UnboundedSchedule φ) :
82     X ≅ X.reindex φ hφ where
83   hom := EventualHom.mk (sampleTransport X φ hφ)
84   inv := EventualHom.mk (recoverTransport X φ hφ hcof)
85   hom_inv_id := Quotient.sound (sample_recover_eventually X φ hφ hcof)
86   inv_hom_id := Quotient.sound (recover_sample_eventually X φ hφ hcof)
87 
88 @[simp] theorem sampleTransport_onLimit (X : Resolution.{u})
89     (φ : ℕ → ℕ) (hφ : Monotone φ) :
90     (sampleTransport X φ hφ).onLimit = sample X φ hφ := rfl
91 
92 theorem recoverTransport_onLimit (X : Resolution.{u}) (φ : ℕ → ℕ)
93     (hφ : Monotone φ) (hcof : UnboundedSchedule φ) :
94     (recoverTransport X φ hφ hcof).onLimit = extend X φ hφ hcof := by
95   funext x
96   apply Point.ext
97   intro n
98   exact (recoveredCoordinate_eq X φ hφ hcof x n (ceilingIndex hcof n)
99     (ceilingIndex_spec hcof n)).symm
100 
101 /-- The new categorical equivalence realizes the previous concrete sampling map. -/
102 @[simp] theorem cofinalIso_hom_onLimit (X : Resolution.{u}) (φ : ℕ → ℕ)
103     (hφ : Monotone φ) (hcof : UnboundedSchedule φ) :
104     (cofinalIso X φ hφ hcof).hom.onLimit = cofinalEquiv X φ hφ hcof := rfl
105 
106 theorem cofinalIso_inv_onLimit (X : Resolution.{u}) (φ : ℕ → ℕ)
107     (hφ : Monotone φ) (hcof : UnboundedSchedule φ) :
108     (cofinalIso X φ hφ hcof).inv.onLimit = (cofinalEquiv X φ hφ hcof).symm :=
109   recoverTransport_onLimit X φ hφ hcof
110 
111 /-- Hom-set equivalence, not only point equivalence, under independent schedules. -/
112 noncomputable def cofinalHomEquiv (X Y : Resolution.{u})
113     (φ ψ : ℕ → ℕ) (hφ : Monotone φ) (hψ : Monotone ψ)
114     (hφcof : UnboundedSchedule φ) (hψcof : UnboundedSchedule ψ) :
115     (X ⟶ Y) ≃ (X.reindex φ hφ ⟶ Y.reindex ψ hψ) where
116   toFun := fun f => (cofinalIso X φ hφ hφcof).inv ≫ f ≫
117     (cofinalIso Y ψ hψ hψcof).hom
118   invFun := fun f => (cofinalIso X φ hφ hφcof).hom ≫ f ≫
119     (cofinalIso Y ψ hψ hψcof).inv
120   left_inv := by intro f; simp [Category.assoc]
121   right_inv := by intro f; simp [Category.assoc]
122 
123 theorem cofinalHomEquiv_onLimit (X Y : Resolution.{u})
124     (φ ψ : ℕ → ℕ) (hφ : Monotone φ) (hψ : Monotone ψ)
125     (hφcof : UnboundedSchedule φ) (hψcof : UnboundedSchedule ψ)
126     (f : X ⟶ Y) (x : (X.reindex φ hφ).Point) :
127     (cofinalHomEquiv X Y φ ψ hφ hψ hφcof hψcof f).onLimit x =
128     cofinalEquiv Y ψ hψ hψcof
129       (f.onLimit ((cofinalEquiv X φ hφ hφcof).symm x)) := by
130   change EventualHom.onLimit
131     (EventualHom.comp (cofinalIso X φ hφ hφcof).inv
132       (EventualHom.comp f (cofinalIso Y ψ hψ hψcof).hom)) x = _
133   simp only [EventualHom.onLimit_comp, cofinalIso_inv_onLimit, cofinalIso_hom_onLimit]
134 
135 namespace Map
136 variable {X Y : Resolution.{u}}
137 
138 @[ext] theorem ext {f g : Map X Y} (h : ∀ n x, f.app n x = g.app n x) : f = g := by
139   cases f with
140   | mk f hf => cases g with
141     | mk g hg =>
142       have hfg : f = g := by
143         cases f; cases g
144         congr
145         funext n x
146         exact h n x
147       cases hfg
148       rfl
149 
150 def sample (f : Map X Y) (φ : ℕ → ℕ) (hφ : Monotone φ) :
151     Map (X.reindex φ hφ) (Y.reindex φ hφ) where
152   app := fun n => f.app (φ n)
153   exact := fun i j h x => f.exact (φ i) (φ j) (hφ h) x
154 
155 @[simp] theorem sample_onLimit (f : Map X Y) (φ : ℕ → ℕ) (hφ : Monotone φ)
156     (x : X.Point) :
157     (sample f φ hφ).onLimit (Resolution.sample X φ hφ x) =
158     Resolution.sample Y φ hφ (f.onLimit x) := rfl
159 
160 theorem sample_square (f : Map X Y) (φ : ℕ → ℕ) (hφ : Monotone φ)
161     (hcof : UnboundedSchedule φ) :
162     EventualHom.ofMap f ≫ (cofinalIso Y φ hφ hcof).hom =
163     (cofinalIso X φ hφ hcof).hom ≫ EventualHom.ofMap (sample f φ hφ) := rfl
164 
165 theorem sample_class (f : Map X Y) (φ : ℕ → ℕ) (hφ : Monotone φ)
166     (hcof : UnboundedSchedule φ) :
167     cofinalHomEquiv X Y φ φ hφ hφ hcof hcof (EventualHom.ofMap f) =
168     EventualHom.ofMap (sample f φ hφ) := by
169   change (cofinalIso X φ hφ hcof).inv ≫
170     (EventualHom.ofMap f ≫ (cofinalIso Y φ hφ hcof).hom) = _
171   rw [sample_square f φ hφ hcof]
172   simp
173 
174 end Map
175 
176 end Resolution
177 end KomorebiSpace

Back to source controls