ReindexedTransports.lean

1 import KomorebiSpace.Cofinal
2 import Mathlib.CategoryTheory.Category.Basic
3 
4 set_option autoImplicit false
5 
6 /-!
7 # Sequential reindexed transports and eventual equality
8 
9 An output coordinate may use a finer input coordinate. Two presentations agree
10 when they agree after restriction from a common sufficiently fine input level,
11 separately for every output coordinate. This is NOT equality of the resulting
12 functions on inverse limits; that weaker identification is not used here.
13 -/
14 
15 universe u v w z
16 namespace KomorebiSpace
17 namespace Resolution
18 
19 structure ReindexedMap (X : Resolution.{u}) (Y : Resolution.{v}) where
20   level : ℕ → ℕ
21   monotone : Monotone level
22   app : ∀ n, X.Obj (level n) → Y.Obj n
23   naturality : ∀ i j (h : i ≤ j) (x : X.Obj (level j)),
24     Y.restrict h (app j x) = app i (X.restrict (monotone h) x)
25 
26 namespace ReindexedMap
27 variable {X : Resolution.{u}} {Y : Resolution.{v}}
28     {Z : Resolution.{w}} {W : Resolution.{z}}
29 
30 def id (X : Resolution.{u}) : ReindexedMap X X where
31   level := fun n => n
32   monotone := fun _ _ h => h
33   app := fun _ x => x
34   naturality := by intros; rfl
35 
36 def ofMap (f : Map X Y) : ReindexedMap X Y where
37   level := fun n => n
38   monotone := fun _ _ h => h
39   app := f.app
40   naturality := f.exact
41 
42 def comp (f : ReindexedMap X Y) (g : ReindexedMap Y Z) : ReindexedMap X Z where
43   level := fun n => f.level (g.level n)
44   monotone := f.monotone.comp g.monotone
45   app := fun n x => g.app n (f.app (g.level n) x)
46   naturality := by
47     intro i j h x
48     rw [g.naturality, f.naturality]
49 
50 @[simp] theorem id_comp (f : ReindexedMap X Y) : comp (id X) f = f := by
51   cases f; rfl
52 
53 @[simp] theorem comp_id (f : ReindexedMap X Y) : comp f (id Y) = f := by
54   cases f; rfl
55 
56 theorem comp_assoc (f : ReindexedMap X Y) (g : ReindexedMap Y Z)
57     (h : ReindexedMap Z W) : comp (comp f g) h = comp f (comp g h) := rfl
58 
59 /-- Agreement is witnessed at a finite stage, not postulated on realized points. -/
60 def EventuallyEq (f g : ReindexedMap X Y) : Prop :=
61   ∀ n, ∃ k, ∃ hf : f.level n ≤ k, ∃ hg : g.level n ≤ k,
62     ∀ x : X.Obj k, f.app n (X.restrict hf x) = g.app n (X.restrict hg x)
63 
64 /-- Equality at a stage persists at every finer stage. -/
65 theorem agree_further (f g : ReindexedMap X Y) (n k l : ℕ)
66     (hf : f.level n ≤ k) (hg : g.level n ≤ k)
67     (hfg : ∀ x : X.Obj k, f.app n (X.restrict hf x) = g.app n (X.restrict hg x))
68     (hkl : k ≤ l) (x : X.Obj l) :
69     f.app n (X.restrict (hf.trans hkl) x) =
70       g.app n (X.restrict (hg.trans hkl) x) := by
71   rw [← X.restrict_trans hf hkl, ← X.restrict_trans hg hkl]
72   exact hfg (X.restrict hkl x)
73 
74 @[refl] theorem eventuallyEq_refl (f : ReindexedMap X Y) : EventuallyEq f f := by
75   intro n
76   exact ⟨f.level n, le_refl _, le_refl _, fun _ => rfl⟩
77 
78 @[symm] theorem eventuallyEq_symm {f g : ReindexedMap X Y}
79     (h : EventuallyEq f g) : EventuallyEq g f := by
80   intro n
81   obtain ⟨k, hf, hg, hk⟩ := h n
82   exact ⟨k, hg, hf, fun x => (hk x).symm⟩
83 
84 @[trans] theorem eventuallyEq_trans {f g h : ReindexedMap X Y}
85     (hfg : EventuallyEq f g) (hgh : EventuallyEq g h) : EventuallyEq f h := by
86   intro n
87   obtain ⟨k, hf, hg, hk⟩ := hfg n
88   obtain ⟨l, hg', hh, hl⟩ := hgh n
89   refine ⟨max k l, hf.trans (Nat.le_max_left _ _),
90     hh.trans (Nat.le_max_right _ _), ?_⟩
91   intro x
92   exact (agree_further f g n k (max k l) hf hg hk (Nat.le_max_left _ _) x).trans
93     (agree_further g h n l (max k l) hg' hh hl (Nat.le_max_right _ _) x)
94 
95 /-- Eventual equality is a congruence for composition of scheduled transports. -/
96 theorem comp_congr {f f' : ReindexedMap X Y} {g g' : ReindexedMap Y Z}
97     (hf : EventuallyEq f f') (hg : EventuallyEq g g') :
98     EventuallyEq (comp f g) (comp f' g') := by
99   intro n
100   obtain ⟨j, hgj, hgj', hj⟩ := hg n
101   obtain ⟨k, hfk, hfk', hk⟩ := hf j
102   refine ⟨k, (f.monotone hgj).trans hfk,
103     (f'.monotone hgj').trans hfk', ?_⟩
104   intro x
105   change g.app n (f.app (g.level n) (X.restrict _ x)) =
106     g'.app n (f'.app (g'.level n) (X.restrict _ x))
107   calc
108     g.app n (f.app (g.level n) (X.restrict _ x)) =
109         g.app n (Y.restrict hgj (f.app j (X.restrict hfk x))) := by
110       rw [f.naturality, X.restrict_trans]
111     _ = g.app n (Y.restrict hgj (f'.app j (X.restrict hfk' x))) := by rw [hk x]
112     _ = g'.app n (Y.restrict hgj' (f'.app j (X.restrict hfk' x))) :=
113       hj (f'.app j (X.restrict hfk' x))
114     _ = g'.app n (f'.app (g'.level n) (X.restrict _ x)) := by
115       rw [f'.naturality, X.restrict_trans]
116 
117 instance eventualSetoid (X : Resolution.{u}) (Y : Resolution.{v}) :
118     Setoid (ReindexedMap X Y) where
119   r := EventuallyEq
120   iseqv := ⟨eventuallyEq_refl, eventuallyEq_symm, eventuallyEq_trans⟩
121 
122 /-- Realization only uses coherent input coordinates at the selected stages. -/
123 def onLimit (f : ReindexedMap X Y) (x : X.Point) : Y.Point :=
124   ⟨fun n => f.app n (x.val (f.level n)), by
125     intro i j h
126     rw [f.naturality, x.property _ _ (f.monotone h)]⟩
127 
128 @[simp] theorem onLimit_apply (f : ReindexedMap X Y) (x : X.Point) (n : ℕ) :
129     (f.onLimit x).val n = f.app n (x.val (f.level n)) := rfl
130 
131 @[simp] theorem onLimit_id (x : X.Point) : (id X).onLimit x = x := rfl
132 
133 @[simp] theorem onLimit_comp (f : ReindexedMap X Y) (g : ReindexedMap Y Z)
134     (x : X.Point) : (comp f g).onLimit x = g.onLimit (f.onLimit x) := rfl
135 
136 @[simp] theorem onLimit_ofMap (f : Map X Y) (x : X.Point) :
137     (ofMap f).onLimit x = f.onLimit x := rfl
138 
139 theorem onLimit_congr {f g : ReindexedMap X Y} (h : EventuallyEq f g) :
140     f.onLimit = g.onLimit := by
141   funext x
142   apply Point.ext
143   intro n
144   obtain ⟨k, hf, hg, hk⟩ := h n
145   have hx := hk (x.val k)
146   rw [x.property _ _ hf, x.property _ _ hg] at hx
147   exact hx
148 
149 end ReindexedMap
150 end Resolution
151 end KomorebiSpace

Back to source controls