SectionObstruction.lean

1 import KomorebiSpace.ViewSections
2 import KomorebiSpace.Correction
3 import Mathlib.Algebra.Group.Pi.Basic
4 import Mathlib.Tactic.Abel
5 
6 set_option autoImplicit false
7 
8 /-!
9 # An actual obstruction to extending a partial additive section
10 
11 The defect compares transported data to the chosen data at every arrow.
12 Allowed corrections vanish on the prescribed view domain. The quotient by
13 these allowed defects is independent of a raw extension, and its vanishing
14 is equivalent to existence of a genuinely coherent extension.
15 -/
16 universe u v w
17 namespace KomorebiSpace
18 open CategoryTheory
19 
20 structure AdditiveViewSystem (V : Type u) [Category.{v} V]
21     (A : V → Type w) [∀ a, AddCommGroup (A a)] where
22   pull : {a b : V} → (a ⟶ b) → (A b →+ A a)
23   pull_id : ∀ a (x : A a), pull (𝟙 a) x = x
24   pull_comp : ∀ {a b c : V} (f : a ⟶ b) (g : b ⟶ c) (x : A c),
25     pull (f ≫ g) x = pull f (pull g x)
26 
27 namespace AdditiveViewSystem
28 variable {V : Type u} [Category.{v} V]
29 variable {A : V → Type w} [∀ a, AddCommGroup (A a)]
30 variable (F : AdditiveViewSystem V A)
31 
32 def views : ViewSystem V where
33   Obj := A
34   pull := fun f => F.pull f
35   pull_id := F.pull_id
36   pull_comp := F.pull_comp
37 
38 /-- Arrow-indexed additive compatibility defects. -/
39 abbrev Residual := ∀ a b : V, (a ⟶ b) → A a
40 
41 def differential : (∀ a, A a) →+ Residual (V := V) (A := A) where
42   toFun x := fun a b f => F.pull f (x b) - x a
43   map_zero' := by funext a b f; simp
44   map_add' := by
45     intro x y
46     funext a b f
47     simp only [Pi.add_apply, map_add]
48     abel
49 
50 @[simp] theorem differential_apply (x : ∀ a, A a) (a b : V) (f : a ⟶ b) :
51     F.differential x a b f = F.pull f (x b) - x a := rfl
52 
53 @[simp] theorem differential_id (x : ∀ a, A a) (a : V) :
54     F.differential x a a (𝟙 a) = 0 := by
55   rw [differential_apply, F.pull_id, sub_self]
56 
57 /-- The actual defects obey the transported additive cocycle identity. -/
58 theorem differential_comp (x : ∀ a, A a) {a b c : V} (f : a ⟶ b) (g : b ⟶ c) :
59     F.differential x a c (f ≫ g) =
60       F.pull f (F.differential x b c g) + F.differential x a b f := by
61   simp only [differential_apply, F.pull_comp, map_sub]
62   abel
63 
64 theorem differential_zero_iff (x : ∀ a, A a) :
65     F.differential x = 0 ↔ ∀ a b (f : a ⟶ b), F.pull f (x b) = x a := by
66   constructor
67   · intro h a b f
68     exact sub_eq_zero.mp (congrFun (congrFun (congrFun h a) b) f)
69   · intro h
70     funext a b f
71     exact sub_eq_zero.mpr (h a b f)
72 
73 /-- The prescribed observations, without declaring them complete semantics. -/
74 def observation (_F : AdditiveViewSystem V A) (U : Set V) :
75     (∀ a, A a) →+ (∀ a : U, A a.val) where
76   toFun x := fun a => x a.val
77   map_zero' := rfl
78   map_add' := by intros; rfl
79 
80 def problem (U : Set V) :
81     CorrectionProblem (∀ a, A a) (Residual (V := V) (A := A)) (∀ a : U, A a.val) where
82   residual := F.differential
83   semantics := F.observation U
84 
85 /-- The old constrained-correction theorem now applies to actual view coherence. -/
86 theorem obstruction_zero_iff_section (U : Set V) (x : ∀ a, A a) :
87     (F.problem U).obstruction x = 0 ↔
88       ∃ s : F.views.Ambient, ∀ a : U, s.val a.val = x a.val := by
89   rw [(F.problem U).flatten_iff]
90   constructor
91   · rintro ⟨y, hy, hp⟩
92     refine ⟨⟨y, (F.differential_zero_iff y).mp hy⟩, ?_⟩
93     intro a
94     exact congrFun hp a
95   · rintro ⟨s, hs⟩
96     refine ⟨s.val, (F.differential_zero_iff s.val).mpr s.property, ?_⟩
97     exact funext hs
98 
99 /-- Equal prescribed data give the same obstruction, independent of raw extension. -/
100 theorem obstruction_same_observation (U : Set V) (x y : ∀ a, A a)
101     (h : F.observation U x = F.observation U y) :
102     (F.problem U).obstruction x = (F.problem U).obstruction y := by
103   have hz : (F.problem U).semantics (x - y) = 0 := by
104     change F.observation U (x - y) = 0
105     rw [map_sub, h, sub_self]
106   have he := (F.problem U).obstruction_invariant x (x - y) hz
107   have hxy : x - (x - y) = y := by abel
108   rw [hxy] at he
109   exact he.symm
110 
111 /-- Zero outside the prescribed domain is one raw extension, not a coherent one. -/
112 noncomputable def rawExtension (U : Set V) (s : F.views.Partial U) : ∀ a, A a :=
113   by
114   classical
115   exact fun a => if h : a ∈ U then s.val ⟨a, h⟩ else 0
116 
117 @[simp] theorem rawExtension_observed (U : Set V) (s : F.views.Partial U) (a : U) :
118     F.rawExtension U s a.val = s.val a := by
119   rcases a with ⟨a, ha⟩
120   exact dite_eq_left ha
121 
122 /-- An explicitly presented quotient class, not a flag defined by solvability. -/
123 noncomputable def extensionClass (U : Set V) (s : F.views.Partial U) :
124     (F.problem U).Obstruction := (F.problem U).obstruction (F.rawExtension U s)
125 
126 theorem extensionClass_zero_iff (U : Set V) (s : F.views.Partial U) :
127     F.extensionClass U s = 0 ↔ Nonempty (F.views.Extensions U s) := by
128   change (F.problem U).obstruction (F.rawExtension U s) = 0 ↔ _
129   rw [F.obstruction_zero_iff_section]
130   constructor
131   · rintro ⟨x, hx⟩
132     refine ⟨⟨x, ?_⟩⟩
133     apply ViewSystem.Partial.ext
134     intro a
135     exact (hx a).trans (F.rawExtension_observed U s a)
136   · rintro ⟨⟨x, hx⟩⟩
137     refine ⟨x, ?_⟩
138     intro a
139     have he := congrArg (fun y : F.views.Partial U => y.val a) hx
140     exact he.trans (F.rawExtension_observed U s a).symm
141 
142 theorem extensionClass_independent (U : Set V) (s : F.views.Partial U)
143     (x : ∀ a, A a) (hx : ∀ a : U, x a.val = s.val a) :
144     (F.problem U).obstruction x = F.extensionClass U s := by
145   apply F.obstruction_same_observation
146   funext a
147   exact (hx a).trans (F.rawExtension_observed U s a).symm
148 
149 end AdditiveViewSystem
150 end KomorebiSpace

Back to source controls