SectionExtensionExample.lean

1 import KomorebiSpace.SectionObstruction
2 import Mathlib.CategoryTheory.Category.Preorder
3 import Mathlib.Order.Fin.Basic
4 import Mathlib.Tactic.FinCases
5 import Mathlib.Tactic.NormNum
6 
7 set_option autoImplicit false
8 
9 /-!
10 # A prescribed local integer extends exactly when its parity permits it
11 
12 There are two views 0 -> 1, with integer fibers. Restriction from view 1 to
13 view 0 is multiplication by two. A prescribed value k at view 0 has a coherent
14 extension iff k is even. This is checked through the actual extension class.
15 -/
16 namespace KomorebiSpace
17 open CategoryTheory
18 namespace SectionExtensionExample
19 
20 def doubleMap : ℤ →+ ℤ where
21   toFun x := 2 * x
22   map_zero' := by simp
23   map_add' := by intro x y; exact mul_add 2 x y
24 
25 def integerViews : AdditiveViewSystem (Fin 2) (fun _ => ℤ) where
26   pull := fun {a b} _ => if a = b then AddMonoidHom.id ℤ else doubleMap
27   pull_id := by intro a x; simp
28   pull_comp := by
29     intro a b c f g x
30     have hab := leOfHom f
31     have hbc := leOfHom g
32     fin_cases a <;> fin_cases b <;> fin_cases c
33     all_goals simp_all [doubleMap]
34 
35 def prescribedView : Set (Fin 2) := {0}
36 
37 def localInteger (k : ℤ) : integerViews.views.Partial prescribedView :=
38   ⟨fun _ => k, by
39     intro a b f
40     have ha : a.val = 0 := a.property
41     have hb : b.val = 0 := b.property
42     have hab : a.val = b.val := ha.trans hb.symm
43     change (if a.val = b.val then AddMonoidHom.id ℤ else doubleMap) k = k
44     simp [hab]⟩
45 
46 def globalInteger (m : ℤ) : integerViews.views.Ambient :=
47   ⟨fun a => if a = 0 then 2*m else m, by
48     intro a b f
49     have hab := leOfHom f
50     fin_cases a <;> fin_cases b
51     all_goals simp_all [AdditiveViewSystem.views, integerViews, doubleMap]⟩
52 
53 @[simp] theorem globalInteger_zero (m : ℤ) : (globalInteger m).val 0 = 2*m := rfl
54 @[simp] theorem globalInteger_one (m : ℤ) : (globalInteger m).val 1 = m := rfl
55 
56 theorem globalInteger_restrict (m : ℤ) :
57     integerViews.views.restrict prescribedView (globalInteger m) = localInteger (2*m) := by
58   apply ViewSystem.Partial.ext
59   intro a
60   have ha : a.val = 0 := a.property
61   change (if a.val = 0 then 2*m else m) = 2*m
62   simp [ha]
63 
64 /-- A genuine congruence obstruction to extending a coherent partial section. -/
65 theorem extensionClass_zero_iff_even (k : ℤ) :
66     integerViews.extensionClass prescribedView (localInteger k) = 0 ↔
67       ∃ m : ℤ, k = 2*m := by
68   rw [integerViews.extensionClass_zero_iff]
69   constructor
70   · rintro ⟨⟨s, hs⟩⟩
71     have h0 : s.val 0 = k :=
72       congrArg (fun x : integerViews.views.Partial prescribedView => x.val ⟨0, rfl⟩) hs
73     have hc := s.property 0 1 (homOfLE (by decide))
74     change (2 : ℤ) * (show ℤ from s.val 1) = (show ℤ from s.val 0) at hc
75     exact ⟨s.val 1, h0.symm.trans hc.symm⟩
76   · rintro ⟨m, rfl⟩
77     exact ⟨⟨globalInteger m, globalInteger_restrict m⟩⟩
78 
79 theorem odd_seed_obstructed :
80     integerViews.extensionClass prescribedView (localInteger 1) ≠ 0 := by
81   intro h
82   obtain ⟨m, hm⟩ := (extensionClass_zero_iff_even 1).mp h
83   omega
84 
85 theorem nonzero_seed_extends :
86     Nonempty (integerViews.views.Extensions prescribedView (localInteger 2)) :=
87   ⟨⟨globalInteger 1, globalInteger_restrict 1⟩⟩
88 
89 end SectionExtensionExample
90 end KomorebiSpace

Back to source controls