ViewBoundaryExamples.lean

1 import KomorebiSpace.ViewCorrespondence
2 import Mathlib.CategoryTheory.Category.Preorder
3 import Mathlib.Order.Fin.Basic
4 
5 set_option autoImplicit false
6 
7 /-!
8 # Boundary examples for ambient sections and local correspondence
9 
10 (1) Covering the objects, without their transitions, need not permit gluing.
11 (2) Every fiber can be nonempty and every transport invertible, while there is
12     no coherent global section.
13 (3) An invertible transport need not be the identity.
14 -/
15 namespace KomorebiSpace
16 open CategoryTheory ViewSystem
17 namespace ViewBoundaryExamples
18 
19 /-- Two separate singleton patches fail to include the arrow 0 -> 1. -/
20 def singletonPatches : Fin 2 → Set (Fin 2) := fun i => {i}
21 
22 theorem singleton_objectCover : ObjectCover singletonPatches := by
23   intro a
24   exact ⟨a, rfl⟩
25 
26 def separatedLocals : Matching (ViewSystem.constant (Fin 2) Bool) singletonPatches where
27   localSection i := ⟨fun _ => decide (i = 1), by intros; rfl⟩
28   agree := by
29     intro i j a hi hj
30     have hi' : a = i := hi
31     have hj' : a = j := hj
32     have hij : i = j := hi'.symm.trans hj'
33     change decide (i = 1) = decide (j = 1)
34     rw [hij]
35 
36 theorem singleton_matching_not_gluable :
37     ¬ ∃ s : (ViewSystem.constant (Fin 2) Bool).Ambient,
38       ∀ i, (ViewSystem.constant (Fin 2) Bool).restrict (singletonPatches i) s =
39         separatedLocals.localSection i := by
40   rintro ⟨s, hs⟩
41   have h0 : s.val 0 = false :=
42     congrArg (fun t : (ViewSystem.constant (Fin 2) Bool).Partial (singletonPatches 0) =>
43       t.val ⟨0, rfl⟩) (hs 0)
44   have h1 : s.val 1 = true :=
45     congrArg (fun t : (ViewSystem.constant (Fin 2) Bool).Partial (singletonPatches 1) =>
46       t.val ⟨1, rfl⟩) (hs 1)
47   have he := s.property 0 1 (homOfLE (by decide))
48   change s.val 1 = s.val 0 at he
49   rw [h0, h1] at he
50   cases he
51 
52 theorem singleton_not_transitionCover : ¬ TransitionCover singletonPatches := by
53   intro h
54   obtain ⟨s, hs, _⟩ := separatedLocals.exists_unique_glue h
55   exact singleton_matching_not_gluable ⟨s, hs⟩
56 
57 inductive LoopView where
58   | only
59   deriving DecidableEq
60 
61 /-- The one-object category with the group of order two as its arrows. -/
62 instance : Category LoopView where
63   Hom _ _ := Bool
64   id _ := false
65   comp f g := Bool.xor f g
66   id_comp := by intro a b f; cases f <;> rfl
67   comp_id := by intro a b f; cases f <;> rfl
68   assoc := by intro a b c d f g h; cases f <;> cases g <;> cases h <;> rfl
69 
70 /-- The nonidentity loop swaps the two available local realizations. -/
71 def swapViews : ViewSystem LoopView where
72   Obj _ := Bool
73   pull := fun f x => Bool.xor f x
74   pull_id := by intro a x; cases x <;> rfl
75   pull_comp := by intro a b c f g x; cases f <;> cases g <;> cases x <;> rfl
76 
77 theorem swap_fibers_nonempty (a : LoopView) : Nonempty (swapViews.Obj a) := ⟨false⟩
78 
79 theorem xor_bijective (f : Bool) : Function.Bijective (fun x : Bool => Bool.xor f x) := by
80   constructor
81   · intro x y h
82     cases f <;> cases x <;> cases y <;> simp_all
83   · intro y
84     refine ⟨Bool.xor f y, ?_⟩
85     cases f <;> cases y <;> rfl
86 
87 theorem swap_transports_bijective (a b : LoopView) (f : a ⟶ b) :
88     Function.Bijective (swapViews.pull f) := xor_bijective f
89 
90 theorem swap_no_ambient : ¬ Nonempty swapViews.Ambient := by
91   rintro ⟨s⟩
92   have h := s.property LoopView.only LoopView.only true
93   change Bool.xor true (s.val LoopView.only) = s.val LoopView.only at h
94   cases he : s.val LoopView.only <;> simp [he] at h
95 
96 theorem bijective_not_identity :
97     Function.Bijective (fun x : Bool => Bool.xor true x) ∧
98       (fun x : Bool => Bool.xor true x) ≠ _root_.id := by
99   constructor
100   · exact xor_bijective true
101   · intro h
102     have he := congrFun h false
103     cases he
104 
105 def unitProjection : Morphism swapViews (ViewSystem.constant LoopView Unit) where
106   app := fun _ _ => ()
107   natural := by intros; rfl
108 
109 def unitAmbient : (ViewSystem.constant LoopView Unit).Ambient :=
110   ViewSystem.constantSection LoopView ()
111 
112 theorem local_bridges_nonempty (a : LoopView) :
113     Nonempty ((bridgeSystem unitProjection unitProjection unitAmbient unitAmbient).Obj a) :=
114   ⟨⟨false, rfl, rfl⟩⟩
115 
116 theorem no_global_bridge :
117     ¬ Nonempty (GlobalBridge unitProjection unitProjection unitAmbient unitAmbient) := by
118   rintro ⟨s⟩
119   exact swap_no_ambient ⟨s.val⟩
120 
121 end ViewBoundaryExamples
122 end KomorebiSpace

Back to source controls