ReindexingExamples.lean

1 import KomorebiSpace.AdjacentResolution
2 import KomorebiSpace.CofinalTransports
3 import KomorebiSpace.RealizationFaithfulness
4 
5 set_option autoImplicit false
6 
7 /-!
8 # Boundaries: transient strict information and nonfaithful realization
9 
10 These examples show why we use finite-stage eventual agreement rather than
11 literal equality of strict presentations or equality of functions on limits.
12 -/
13 
14 namespace KomorebiSpace
15 namespace ReindexingExamples
16 open Resolution
17 
18 /-- Nonempty at every level, but there is no natural number at least every n. -/
19 def tails : Resolution where
20   Obj n := {m : ℕ // n ≤ m}
21   restrict := fun h x => ⟨x.val, h.trans x.property⟩
22   restrict_refl := by intro n x; rfl
23   restrict_trans := by intros; rfl
24 
25 theorem tails_level_nonempty (n : ℕ) : Nonempty (tails.Obj n) :=
26   ⟨⟨n, Nat.le_refl n⟩⟩
27 
28 theorem tails_no_point (x : tails.Point) : False := by
29   let m := (x.val 0).val
30   have he := congrArg Subtype.val (x.property 0 (m+1) (Nat.zero_le _))
31   have hb : m+1 ≤ (x.val (m+1)).val := (x.val (m+1)).property
32   change (x.val (m+1)).val = m at he
33   omega
34 
35 def boolConstant : Resolution where
36   Obj _ := Bool
37   restrict := fun _ x => x
38   restrict_refl := by intros; rfl
39   restrict_trans := by intros; rfl
40 
41 def constantToBool (b : Bool) : ReindexedMap tails boolConstant where
42   level := fun n => n
43   monotone := fun _ _ h => h
44   app := fun _ _ => b
45   naturality := by intros; rfl
46 
47 theorem constants_not_eventually_equal :
48     ¬ ReindexedMap.EventuallyEq (constantToBool false) (constantToBool true) := by
49   intro h
50   obtain ⟨k, hf, hg, hk⟩ := h 0
51   have hbad : false = true := hk ⟨k, Nat.le_refl k⟩
52   cases hbad
53 
54 theorem distinct_classes_same_realization :
55     EventualHom.mk (constantToBool false) ≠ EventualHom.mk (constantToBool true) ∧
56     (EventualHom.mk (constantToBool false)).onLimit =
57       (EventualHom.mk (constantToBool true)).onLimit := by
58   constructor
59   · intro h
60     exact constants_not_eventually_equal
61       ((EventualHom.mk_eq_iff _ _).mp h)
62   · funext x
63     exact False.elim (tails_no_point x)
64 
65 /-- A single transient Boolean coordinate, absent at all subsequent levels. -/
66 def transientObj : ℕ → Type
67   | 0 => Bool
68   | _+1 => PUnit
69 
70 def transientDown : ∀ n, transientObj (n+1) → transientObj n
71   | 0 => fun _ => false
72   | _+1 => fun x => x
73 
74 def transient : Resolution := Adjacent.resolution transientObj transientDown
75 
76 def eraseApp : ∀ n, transientObj n → transientObj n
77   | 0 => fun _ => false
78   | _+1 => fun x => x
79 
80 def erase : Map transient transient := Adjacent.map eraseApp (by
81   intro n x
82   cases n <;> rfl)
83 
84 theorem strict_maps_differ : Map.id transient ≠ erase := by
85   intro h
86   have hb := congrArg (fun f : Map transient transient => f.app 0 true) h
87   change true = false at hb
88   cases hb
89 
90 theorem successor_monotone : Monotone Nat.succ := by
91   intro i j h; omega
92 
93 theorem successor_cofinal : UnboundedSchedule Nat.succ := by
94   intro n; exact ⟨n, Nat.le_succ n⟩
95 
96 /-- Literal strict maps can become equal after a cofinal schedule drops an initial level. -/
97 theorem sampled_strict_maps_equal :
98     Map.sample (Map.id transient) Nat.succ successor_monotone =
99     Map.sample erase Nat.succ successor_monotone := by
100   apply Map.ext
101   intro n x
102   rfl
103 
104 /-- In the eventual quotient the transient difference was already removed. -/
105 theorem transient_classes_equal :
106     EventualHom.ofMap (Map.id transient) = EventualHom.ofMap erase := by
107   apply (cofinalHomEquiv transient transient Nat.succ Nat.succ
108     successor_monotone successor_monotone successor_cofinal successor_cofinal).injective
109   rw [Map.sample_class, Map.sample_class, sampled_strict_maps_equal]
110 
111 theorem strict_reindexing_not_injective :
112     ¬ Function.Injective (fun f : Map transient transient =>
113       Map.sample f Nat.succ successor_monotone) := by
114   intro h
115   exact strict_maps_differ (h sampled_strict_maps_equal)
116 
117 end ReindexingExamples
118 end KomorebiSpace

Back to source controls