Cofinal.lean

1 import KomorebiSpace.Realization
2 import Mathlib.Order.Monotone.Basic
3 
4 set_option autoImplicit false
5 
6 /-!
7 # Cofinal invariance of realized exact information
8 
9 This proves an equivalence of inverse-limit point types. It does not assert
10 invariance of an arbitrary weighted residual sum or of an undefined cohomology.
11 -/
12 universe u
13 namespace KomorebiSpace
14 namespace Resolution
15 
16 abbrev UnboundedSchedule (φ : ℕ → ℕ) : Prop := ∀ n, ∃ j, n ≤ φ j
17 
18 def reindex (X : Resolution.{u}) (φ : ℕ → ℕ) (hφ : Monotone φ) : Resolution.{u} where
19   Obj := fun n => X.Obj (φ n)
20   restrict := fun h => X.restrict (hφ h)
21   restrict_refl := fun n x => X.restrict_refl (φ n) x
22   restrict_trans := fun hij hjk x => X.restrict_trans (hφ hij) (hφ hjk) x
23 
24 def sample (X : Resolution.{u}) (φ : ℕ → ℕ) (hφ : Monotone φ)
25     (x : X.Point) : (X.reindex φ hφ).Point :=
26   ⟨fun n => x.val (φ n), fun i j h => x.property (φ i) (φ j) (hφ h)⟩
27 
28 noncomputable def pickIndex {φ : ℕ → ℕ} (hcof : UnboundedSchedule φ) (n : ℕ) : ℕ :=
29   Classical.choose (hcof n)
30 
31 theorem pickIndex_spec {φ : ℕ → ℕ} (hcof : UnboundedSchedule φ) (n : ℕ) :
32     n ≤ φ (pickIndex hcof n) := Classical.choose_spec (hcof n)
33 
34 noncomputable def recoveredCoordinate (X : Resolution.{u}) (φ : ℕ → ℕ)
35     (hφ : Monotone φ) (hcof : UnboundedSchedule φ)
36     (y : (X.reindex φ hφ).Point) (n : ℕ) : X.Obj n :=
37   X.restrict (pickIndex_spec hcof n) (y.val (pickIndex hcof n))
38 
39 /-- The recovered coordinate is independent of the chosen sufficiently fine sample. -/
40 theorem recoveredCoordinate_eq (X : Resolution.{u}) (φ : ℕ → ℕ)
41     (hφ : Monotone φ) (hcof : UnboundedSchedule φ)
42     (y : (X.reindex φ hφ).Point) (n j : ℕ) (h : n ≤ φ j) :
43     recoveredCoordinate X φ hφ hcof y n = X.restrict h (y.val j) := by
44   let p := pickIndex hcof n
45   let k := max p j
46   have hp : p ≤ k := Nat.le_max_left _ _
47   have hj : j ≤ k := Nat.le_max_right _ _
48   have yp : X.restrict (hφ hp) (y.val k) = y.val p := y.property p k hp
49   have yj : X.restrict (hφ hj) (y.val k) = y.val j := y.property j k hj
50   change X.restrict (pickIndex_spec hcof n) (y.val p) = X.restrict h (y.val j)
51   calc
52     X.restrict (pickIndex_spec hcof n) (y.val p) =
53         X.restrict (pickIndex_spec hcof n) (X.restrict (hφ hp) (y.val k)) :=
54       congrArg (X.restrict (pickIndex_spec hcof n)) yp.symm
55     _ = X.restrict (Nat.le_trans (pickIndex_spec hcof n) (hφ hp)) (y.val k) :=
56       X.restrict_trans _ _ _
57     _ = X.restrict h (X.restrict (hφ hj) (y.val k)) :=
58       (X.restrict_trans h (hφ hj) (y.val k)).symm
59     _ = X.restrict h (y.val j) := congrArg (X.restrict h) yj
60 
61 noncomputable def extend (X : Resolution.{u}) (φ : ℕ → ℕ)
62     (hφ : Monotone φ) (hcof : UnboundedSchedule φ)
63     (y : (X.reindex φ hφ).Point) : X.Point := by
64   refine ⟨recoveredCoordinate X φ hφ hcof y, ?_⟩
65   intro i j hij
66   let p := pickIndex hcof j
67   have hj : j ≤ φ p := pickIndex_spec hcof j
68   calc
69     X.restrict hij (recoveredCoordinate X φ hφ hcof y j) =
70         X.restrict hij (X.restrict hj (y.val p)) :=
71       congrArg (X.restrict hij) (recoveredCoordinate_eq X φ hφ hcof y j p hj)
72     _ = X.restrict (Nat.le_trans hij hj) (y.val p) := X.restrict_trans _ _ _
73     _ = recoveredCoordinate X φ hφ hcof y i :=
74       (recoveredCoordinate_eq X φ hφ hcof y i p (Nat.le_trans hij hj)).symm
75 
76 @[simp] theorem extend_sample (X : Resolution.{u}) (φ : ℕ → ℕ)
77     (hφ : Monotone φ) (hcof : UnboundedSchedule φ) (x : X.Point) :
78     extend X φ hφ hcof (sample X φ hφ x) = x := by
79   apply Point.ext
80   intro n
81   exact x.property n (φ (pickIndex hcof n)) (pickIndex_spec hcof n)
82 
83 @[simp] theorem sample_extend (X : Resolution.{u}) (φ : ℕ → ℕ)
84     (hφ : Monotone φ) (hcof : UnboundedSchedule φ)
85     (y : (X.reindex φ hφ).Point) :
86     sample X φ hφ (extend X φ hφ hcof y) = y := by
87   apply Point.ext
88   intro n
89   change recoveredCoordinate X φ hφ hcof y (φ n) = y.val n
90   rw [recoveredCoordinate_eq X φ hφ hcof y (φ n) n (Nat.le_refl _)]
91   exact X.restrict_refl _ _
92 
93 /-- Canonical restriction equivalence; its inverse is independent of choice. -/
94 noncomputable def cofinalEquiv (X : Resolution.{u}) (φ : ℕ → ℕ)
95     (hφ : Monotone φ) (hcof : UnboundedSchedule φ) :
96     X.Point ≃ (X.reindex φ hφ).Point where
97   toFun := sample X φ hφ
98   invFun := extend X φ hφ hcof
99   left_inv := extend_sample X φ hφ hcof
100   right_inv := sample_extend X φ hφ hcof
101 
102 theorem sample_injective (X : Resolution.{u}) (φ : ℕ → ℕ)
103     (hφ : Monotone φ) (hcof : UnboundedSchedule φ) :
104     Function.Injective (sample X φ hφ) := (cofinalEquiv X φ hφ hcof).injective
105 
106 theorem double_monotone : Monotone (fun n : ℕ => 2*n) := by
107   intro a b h; change 2*a ≤ 2*b; omega
108 
109 theorem double_unbounded : UnboundedSchedule (fun n : ℕ => 2*n) := by
110   intro n; exact ⟨n, by change n ≤ 2*n; omega⟩
111 
112 end Resolution
113 end KomorebiSpace

Back to source controls