FinitePrefixBoundary.lean

1 import KomorebiSpace.ResolutionViews
2 
3 set_option autoImplicit false
4 
5 /-!
6 # KS54: finite-prefix solvability need not produce a global realization
7 
8 The fibers are the actual subsets {m : Nat | n ≤ m}. Prefix witnesses inhabit
9 ViewSystem.Partial, and global emptiness concerns the existing Resolution.Point
10 and ViewSystem.Ambient constructions.
11 -/
12 namespace KomorebiSpace
13 namespace FinitePrefixBoundary
14 open CategoryTheory Resolution
15 
16 def escaping : Resolution where
17   Obj n := {m : ℕ // n ≤ m}
18   restrict h x := ⟨x.val, h.trans x.property⟩
19   restrict_refl _ _ := rfl
20   restrict_trans _ _ _ := rfl
21 
22 theorem level_nonempty (n : ℕ) : Nonempty (escaping.Obj n) :=
23   ⟨⟨n, Nat.le_refl n⟩⟩
24 
25 def prefixSection (N : ℕ) : escaping.views.Partial (prefixViews N) :=
26   ⟨fun n => ⟨N, n.property⟩, fun _ _ _ => rfl⟩
27 
28 theorem every_prefix_nonempty (N : ℕ) :
29     Nonempty (escaping.views.Partial (prefixViews N)) := ⟨prefixSection N⟩
30 
31 theorem no_point : IsEmpty escaping.Point := by
32   refine ⟨fun s => ?_⟩
33   let m := (s.val 0).val
34   have he : (s.val (m+1)).val = m :=
35     congrArg Subtype.val (s.property 0 (m+1) (Nat.zero_le _))
36   have hm := (s.val (m+1)).property
37   rw [he] at hm
38   exact Nat.not_succ_le_self m hm
39 
40 theorem no_ambient : IsEmpty escaping.views.Ambient :=
41   ⟨fun s => no_point.false (escaping.ambientEquiv s)⟩
42 
43 /-- The finite witnesses do not form the compatible matching datum needed by gluing. -/
44 theorem no_matching_prefixes :
45     IsEmpty (ViewSystem.Matching escaping.views prefixViews) :=
46   ⟨fun s => no_ambient.false (escaping.prefixSectionEquiv.symm s)⟩
47 
48 end FinitePrefixBoundary
49 end KomorebiSpace

Back to source controls