AdjacentResolution.lean

1 import KomorebiSpace.Realization
2 
3 set_option autoImplicit false
4 
5 /-! All-pairs restriction maps, derived from actual adjacent bonding functions. -/
6 
7 universe u v
8 namespace KomorebiSpace
9 namespace Resolution
10 namespace Adjacent
11 
12 variable (V : ℕ → Type u) (down : ∀ n, V (n+1) → V n)
13 
14 def restrict {i j : ℕ} (h : i ≤ j) : V j → V i :=
15   Nat.leRecOn (C := fun n => V n → V i) h (fun {n} f => f ∘ down n) _root_.id
16 
17 @[simp] theorem restrict_refl (n : ℕ) (x : V n) :
18     restrict V down (Nat.le_refl n) x = x := by
19   simp [restrict, Nat.leRecOn_self]
20 
21 theorem restrict_succ {i j : ℕ} (h : i ≤ j) (h' : i ≤ j+1) (x : V (j+1)) :
22     restrict V down h' x = restrict V down h (down j x) := by
23   simp only [restrict, Nat.leRecOn_succ h, Function.comp_apply]
24 
25 theorem restrict_trans {i j k : ℕ} (hij : i ≤ j) (hjk : j ≤ k) :
26     ∀ x : V k,
27       restrict V down hij (restrict V down hjk x) =
28       restrict V down (Nat.le_trans hij hjk) x := by
29   induction k, hjk using Nat.le_induction with
30   | base => intro x; rw [restrict_refl]
31   | succ k hk ih =>
32     intro x
33     rw [restrict_succ V down hk, restrict_succ V down (Nat.le_trans hij hk)]
34     exact ih (down k x)
35 
36 def resolution : Resolution.{u} where
37   Obj := V
38   restrict := restrict V down
39   restrict_refl := restrict_refl V down
40   restrict_trans := fun hij hjk => restrict_trans V down hij hjk
41 
42 /-- Adjacent coherence implies coherence at every ordered pair of levels. -/
43 theorem coherent_all (x : ∀ n, V n) (hx : ∀ n, down n (x (n+1)) = x n)
44     {i j : ℕ} (h : i ≤ j) : restrict V down h (x j) = x i := by
45   induction j, h using Nat.le_induction with
46   | base => exact restrict_refl V down i (x i)
47   | succ j hj ih => rw [restrict_succ V down hj, hx j, ih]
48 
49 /-- No original space is identified with its limit without a separate equivalence. -/
50 def pointEquiv : {x : ∀ n, V n // ∀ n, down n (x (n+1)) = x n} ≃
51     (resolution V down).Point where
52   toFun x := ⟨x.val, fun _ _ h => coherent_all V down x.val x.property h⟩
53   invFun x := ⟨x.val, by
54     intro n
55     have h := x.property n (n+1) (Nat.le_succ n)
56     change restrict V down (Nat.le_succ n) (x.val (n+1)) = x.val n at h
57     have hs := restrict_succ V down (Nat.le_refl n) (Nat.le_succ n) (x.val (n+1))
58     have hr := restrict_refl V down n (down n (x.val (n+1)))
59     exact (hs.trans hr).symm.trans h⟩
60   left_inv _ := rfl
61   right_inv _ := rfl
62 
63 variable {V down} {W : ℕ → Type v} {downW : ∀ n, W (n+1) → W n}
64 
65 theorem map_all (f : ∀ n, V n → W n)
66     (hf : ∀ n x, downW n (f (n+1) x) = f n (down n x))
67     {i j : ℕ} (h : i ≤ j) : ∀ x : V j,
68     restrict W downW h (f j x) = f i (restrict V down h x) := by
69   induction j, h using Nat.le_induction with
70   | base => intro x; simp
71   | succ j hj ih =>
72     intro x
73     rw [restrict_succ W downW hj, hf j, ih, restrict_succ V down hj]
74 
75 def map (f : ∀ n, V n → W n)
76     (hf : ∀ n x, downW n (f (n+1) x) = f n (down n x)) :
77     Map (resolution V down) (resolution W downW) where
78   app := f
79   exact := fun _ _ h => map_all f hf h
80 
81 @[simp] theorem map_onLimit (f : ∀ n, V n → W n)
82     (hf : ∀ n x, downW n (f (n+1) x) = f n (down n x))
83     (x : (resolution V down).Point) (n : ℕ) :
84     ((map f hf).onLimit x).val n = f n (x.val n) := rfl
85 
86 end Adjacent
87 end Resolution
88 end KomorebiSpace

Back to source controls