ExtensionChoiceExample.lean

1 import KomorebiSpace.ObstructionRestriction
2 import KomorebiSpace.SectionExtensionStages
3 import Mathlib.CategoryTheory.Category.Preorder
4 import Mathlib.Order.Fin.Basic
5 import Mathlib.Tactic.FinCases
6 import Mathlib.Tactic.NormNum
7 
8 set_option autoImplicit false
9 
10 /-!
11 # Nonzero initial data, many global extensions, and a dead-end intermediate choice
12 
13 The views are 0 -> 1 -> 2 with fibers Z x Z. Restriction into 0 forgets
14 the second coordinate. Restriction from 2 to 1 doubles it. A fixed initial
15 value (k,0) has Z-many global extensions, but the intermediate second value
16 must be even. This is stated in the actual section and obstruction objects.
17 -/
18 namespace KomorebiSpace
19 open CategoryTheory
20 namespace ExtensionChoiceExample
21 
22 abbrev Pair := ℤ × ℤ
23 
24 def forgetTail : Pair →+ Pair where
25   toFun x := (x.1,0)
26   map_zero' := rfl
27   map_add' := by intro x y; rfl
28 
29 def doubleTail : Pair →+ Pair where
30   toFun x := (x.1,2*x.2)
31   map_zero' := by simp
32   map_add' := by intro x y; ext <;> simp [mul_add]
33 
34 def threeViews : AdditiveViewSystem (Fin 3) (fun _ => Pair) where
35   pull := fun {a b} _ =>
36     if a = b then AddMonoidHom.id Pair else if a = 0 then forgetTail else doubleTail
37   pull_id := by intro a x; simp
38   pull_comp := by
39     intro a b c f g x
40     have hab := leOfHom f
41     have hbc := leOfHom g
42     fin_cases a <;> fin_cases b <;> fin_cases c
43     all_goals simp_all [forgetTail,doubleTail]
44 
45 def initialDomain : Set (Fin 3) := {0}
46 def middleDomain : Set (Fin 3) := {0,1}
47 
48 theorem initial_subset_middle : initialDomain ⊆ middleDomain := by
49   intro a ha
50   exact Or.inl ha
51 
52 def initialSeed (k : ℤ) : threeViews.views.Partial initialDomain :=
53   ⟨fun _ => (k,0),by
54     intro a b f
55     have ha : a.val = 0 := a.property
56     have hb : b.val = 0 := b.property
57     change (if a.val = b.val then AddMonoidHom.id Pair else
58       if a.val = 0 then forgetTail else doubleTail) (k,0) = (k,0)
59     simp [ha,hb]⟩
60 
61 def middleSeed (k m : ℤ) : threeViews.views.Partial middleDomain :=
62   ⟨fun a => (k, if a.val = 0 then 0 else m),by
63     rintro ⟨a,ha⟩ ⟨b,hb⟩ f
64     have hab := leOfHom f
65     change a = 0 ∨ a = 1 at ha
66     change b = 0 ∨ b = 1 at hb
67     rcases ha with rfl | rfl <;> rcases hb with rfl | rfl
68     all_goals simp_all [AdditiveViewSystem.views,threeViews,forgetTail,doubleTail]⟩
69 
70 def globalSection (k n : ℤ) : threeViews.views.Ambient :=
71   ⟨fun a => (k,if a = 0 then 0 else if a = 1 then 2*n else n),by
72     intro a b f
73     have hab := leOfHom f
74     fin_cases a <;> fin_cases b
75     all_goals simp_all [AdditiveViewSystem.views,threeViews,forgetTail,doubleTail]⟩
76 
77 @[simp] theorem globalSection_zero (k n : ℤ) : (globalSection k n).val 0 = (k,0) := rfl
78 @[simp] theorem globalSection_one (k n : ℤ) : (globalSection k n).val 1 = (k,2*n) := rfl
79 @[simp] theorem globalSection_two (k n : ℤ) : (globalSection k n).val 2 = (k,n) := rfl
80 
81 theorem global_restrict_initial (k n : ℤ) :
82     threeViews.views.restrict initialDomain (globalSection k n) = initialSeed k := by
83   apply ViewSystem.Partial.ext
84   intro a
85   have ha : a.val = 0 := a.property
86   change (k,if a.val = 0 then 0 else if a.val = 1 then 2*n else n) = (k,0)
87   simp [ha]
88 
89 theorem global_restrict_middle (k n : ℤ) :
90     threeViews.views.restrict middleDomain (globalSection k n) = middleSeed k (2*n) := by
91   apply ViewSystem.Partial.ext
92   rintro ⟨a,ha⟩
93   change a = 0 ∨ a = 1 at ha
94   rcases ha with rfl | rfl <;> rfl
95 
96 theorem middle_restrict_initial (k m : ℤ) :
97     threeViews.views.restrictPartial initial_subset_middle (middleSeed k m) = initialSeed k := by
98   apply ViewSystem.Partial.ext
99   intro a
100   have ha : a.val = 0 := a.property
101   change (k,if a.val = 0 then 0 else m) = (k,0)
102   simp [ha]
103 
104 /-- Every initial seed extends, including nonzero ones. -/
105 theorem initial_extends (k : ℤ) :
106     Nonempty (threeViews.views.Extensions initialDomain (initialSeed k)) :=
107   ⟨⟨globalSection k 0,global_restrict_initial k 0⟩⟩
108 
109 /-- The intermediate choice obeys a genuine parity obstruction. -/
110 theorem middle_obstruction_iff_even (k m : ℤ) :
111     threeViews.extensionClass middleDomain (middleSeed k m) = 0 ↔
112       ∃ n : ℤ, m = 2*n := by
113   rw [threeViews.extensionClass_zero_iff]
114   constructor
115   · rintro ⟨⟨x,hx⟩⟩
116     have hv : x.val 1 = (k,m) :=
117       congrArg (fun t : threeViews.views.Partial middleDomain => t.val ⟨1,Or.inr rfl⟩) hx
118     have hc := x.property 1 2 (homOfLE (by decide))
119     change doubleTail (show Pair from x.val 2) = x.val 1 at hc
120     have hh := congrArg Prod.snd (hc.trans hv)
121     exact ⟨(x.val 2).2,hh.symm⟩
122   · rintro ⟨n,rfl⟩
123     exact ⟨⟨globalSection k n,global_restrict_middle k n⟩⟩
124 
125 theorem odd_middle_obstructed (k : ℤ) :
126     threeViews.extensionClass middleDomain (middleSeed k 1) ≠ 0 := by
127   intro h
128   obtain ⟨n,hn⟩ := (middle_obstruction_iff_even k 1).mp h
129   omega
130 
131 /-- Restricting the obstructed middle choice loses its obstruction. -/
132 theorem obstruction_forgotten (k : ℤ) :
133     threeViews.forgetObstruction initial_subset_middle
134       (threeViews.extensionClass middleDomain (middleSeed k 1)) = 0 := by
135   rw [threeViews.extensionClass_restrict,middle_restrict_initial]
136   exact (threeViews.extensionClass_zero_iff _ _).mpr (initial_extends k)
137 
138 theorem forgetting_not_injective :
139     ¬ Function.Injective (threeViews.forgetObstruction initial_subset_middle) := by
140   intro hinj
141   apply odd_middle_obstructed 7
142   apply hinj
143   rw [obstruction_forgotten,map_zero]
144 
145 /-- Every completion of the initial seed has the displayed formula. -/
146 theorem initial_extension_formula (k : ℤ)
147     (x : threeViews.views.Extensions initialDomain (initialSeed k)) :
148     x.val = globalSection k (x.val.val 2).2 := by
149   have h0 : x.val.val 0 = (k,0) :=
150     congrArg (fun t : threeViews.views.Partial initialDomain => t.val ⟨0,rfl⟩) x.property
151   have h02 := x.val.property 0 2 (homOfLE (by decide))
152   change forgetTail (show Pair from x.val.val 2) = x.val.val 0 at h02
153   have hfirst : (x.val.val 2).1 = k := congrArg Prod.fst (h02.trans h0)
154   have h12 := x.val.property 1 2 (homOfLE (by decide))
155   change doubleTail (show Pair from x.val.val 2) = x.val.val 1 at h12
156   apply ViewSystem.Ambient.ext
157   intro a
158   fin_cases a
159   · exact h0
160   · change x.val.val 1 = (k,2*(x.val.val 2).2)
161     exact h12.symm.trans (Prod.ext hfirst rfl)
162   · change x.val.val 2 = (k,(x.val.val 2).2)
163     exact Prod.ext hfirst rfl
164 
165 /-- An explicit infinite family of completions of each fixed initial seed. -/
166 def initialExtensionsEquiv (k : ℤ) :
167     ℤ ≃ threeViews.views.Extensions initialDomain (initialSeed k) where
168   toFun n := ⟨globalSection k n,global_restrict_initial k n⟩
169   invFun x := (x.val.val 2).2
170   left_inv _ := rfl
171   right_inv x := Subtype.ext (initial_extension_formula k x).symm
172 
173 @[simp] theorem initialExtensions_parameter (k n : ℤ) :
174     ((initialExtensionsEquiv k n).val.val 2).2 = n := rfl
175 
176 theorem initial_extensions_not_unique (k : ℤ) :
177     ¬ Subsingleton (threeViews.views.Extensions initialDomain (initialSeed k)) := by
178   intro hs
179   have he := (initialExtensionsEquiv k).injective
180     (hs.elim (initialExtensionsEquiv k 0) (initialExtensionsEquiv k 1))
181   norm_num at he
182 
183 /-- A nonzero initial value extends, but a coherent intermediate choice can fail. -/
184 theorem nonzero_seed_dead_end :
185     Nonempty (threeViews.views.Extensions initialDomain (initialSeed 7)) ∧
186     threeViews.views.restrictPartial initial_subset_middle (middleSeed 7 1) = initialSeed 7 ∧
187     ¬ Nonempty (threeViews.views.Extensions middleDomain (middleSeed 7 1)) := by
188   refine ⟨initial_extends 7,middle_restrict_initial 7 1,?_⟩
189   intro h
190   exact odd_middle_obstructed 7 ((threeViews.extensionClass_zero_iff _ _).mpr h)
191 
192 end ExtensionChoiceExample
193 end KomorebiSpace

Back to source controls