RealizationFaithfulness.lean

1 import KomorebiSpace.EventualCategory
2 
3 set_option autoImplicit false
4 
5 /-!
6 # When realized functions determine eventual transports
7 
8 Surjectivity of all limit projections is sufficient. It is proved from
9 surjective adjacent bonding maps by an explicit choice-and-recursion lift.
10 -/
11 
12 universe u v
13 namespace KomorebiSpace
14 namespace Resolution
15 
16 /-- Every finite input state is the coordinate of a coherent global input. -/
17 def ProjectionSurjective (X : Resolution.{u}) : Prop :=
18   ∀ n, Function.Surjective (fun x : X.Point => x.val n)
19 
20 namespace ReindexedMap
21 variable {X : Resolution.{u}} {Y : Resolution.{v}}
22 
23 theorem eventuallyEq_of_onLimit_eq (hX : ProjectionSurjective X)
24     (f g : ReindexedMap X Y) (hfg : f.onLimit = g.onLimit) :
25     EventuallyEq f g := by
26   intro n
27   let k := max (f.level n) (g.level n)
28   refine ⟨k, Nat.le_max_left _ _, Nat.le_max_right _ _, ?_⟩
29   intro a
30   obtain ⟨x, hx⟩ := hX k a
31   change x.val k = a at hx
32   have hh := congrArg (fun F : X.Point → Y.Point => (F x).val n) hfg
33   change f.app n (x.val (f.level n)) = g.app n (x.val (g.level n)) at hh
34   have hxf := x.property (f.level n) k (Nat.le_max_left _ _)
35   have hxg := x.property (g.level n) k (Nat.le_max_right _ _)
36   rw [hx] at hxf hxg
37   exact (congrArg (f.app n) hxf).trans (hh.trans (congrArg (g.app n) hxg).symm)
38 
39 theorem eventuallyEq_iff_onLimit_eq (hX : ProjectionSurjective X)
40     (f g : ReindexedMap X Y) : EventuallyEq f g ↔ f.onLimit = g.onLimit :=
41   ⟨onLimit_congr, eventuallyEq_of_onLimit_eq hX f g⟩
42 
43 end ReindexedMap
44 
45 namespace EventualHom
46 variable {X : Resolution.{u}} {Y : Resolution.{v}}
47 
48 theorem onLimit_injective (hX : ProjectionSurjective X) :
49     Function.Injective (onLimit (X := X) (Y := Y)) := by
50   intro f g hfg
51   induction f using Quotient.inductionOn with
52   | _ f => induction g using Quotient.inductionOn with
53     | _ g => exact Quotient.sound (ReindexedMap.eventuallyEq_of_onLimit_eq hX f g hfg)
54 
55 theorem eq_iff_onLimit_eq (hX : ProjectionSurjective X) (f g : EventualHom X Y) :
56     f = g ↔ f.onLimit = g.onLimit :=
57   ⟨fun h => congrArg onLimit h, fun h => onLimit_injective (X := X) (Y := Y) hX h⟩
58 
59 end EventualHom
60 
61 variable (X : Resolution.{u})
62 
63 theorem coherent_of_adjacent (x : ∀ n, X.Obj n)
64     (hx : ∀ n, X.restrict (Nat.le_succ n) (x (n+1)) = x n)
65     {i j : ℕ} (h : i ≤ j) : X.restrict h (x j) = x i := by
66   induction j, h using Nat.le_induction with
67   | base => exact X.restrict_refl i (x i)
68   | succ j hj ih =>
69     exact (X.restrict_trans hj (Nat.le_succ j) (x (j+1))).symm.trans
70       ((congrArg (X.restrict hj) (hx j)).trans ih)
71 
72 variable (up : ∀ n, X.Obj n → X.Obj (n+1))
73     (hup : ∀ n x, X.restrict (Nat.le_succ n) (up n x) = x)
74 
75 def seededSequence (k : ℕ) (seed : X.Obj k) : ∀ n, X.Obj n
76   | 0 => X.restrict (Nat.zero_le k) seed
77   | n+1 => if h : n+1 ≤ k then X.restrict h seed else up n (seededSequence k seed n)
78 
79 theorem seededSequence_below (k n : ℕ) (seed : X.Obj k) (h : n ≤ k) :
80     seededSequence X up k seed n = X.restrict h seed := by
81   cases n with
82   | zero => rfl
83   | succ n => simp only [seededSequence, dite_eq_left h]
84 
85 include hup in
86 theorem seededSequence_coherent (k : ℕ) (seed : X.Obj k) (n : ℕ) :
87     X.restrict (Nat.le_succ n) (seededSequence X up k seed (n+1)) =
88     seededSequence X up k seed n := by
89   by_cases hn : n+1 ≤ k
90   · have hn' : n ≤ k := (Nat.le_succ n).trans hn
91     rw [seededSequence_below X up k (n+1) seed hn,
92       seededSequence_below X up k n seed hn']
93     exact X.restrict_trans (Nat.le_succ n) hn seed
94   · rw [seededSequence, dite_eq_right hn]
95     exact hup n _
96 
97 def seededPoint (k : ℕ) (seed : X.Obj k) : X.Point :=
98   ⟨seededSequence X up k seed, fun _ _ h =>
99     coherent_of_adjacent X _ (seededSequence_coherent X up hup k seed) h⟩
100 
101 @[simp] theorem seededPoint_at_seed (k : ℕ) (seed : X.Obj k) :
102     (seededPoint X up hup k seed).val k = seed :=
103   (seededSequence_below X up k k seed (Nat.le_refl k)).trans (X.restrict_refl k seed)
104 
105 include up hup in
106 theorem projectionSurjective_of_sections : ProjectionSurjective X := by
107   intro k seed
108   exact ⟨seededPoint X up hup k seed, seededPoint_at_seed X up hup k seed⟩
109 
110 theorem projectionSurjective_of_surjective_bonding
111     (hsurj : ∀ n, Function.Surjective (X.restrict (Nat.le_succ n))) :
112     ProjectionSurjective X := by
113   classical
114   let lift : ∀ n, X.Obj n → X.Obj (n+1) :=
115     fun n x => Classical.choose (hsurj n x)
116   have hlift : ∀ n x, X.restrict (Nat.le_succ n) (lift n x) = x :=
117     fun n x => Classical.choose_spec (hsurj n x)
118   exact projectionSurjective_of_sections X lift hlift
119 
120 end Resolution
121 end KomorebiSpace

Back to source controls