ObstructionRestriction.lean

1 import KomorebiSpace.SectionExactSequence
2 
3 set_option autoImplicit false
4 
5 /-!
6 # Restricting prescribed views and transporting their obstruction classes
7 
8 If U is contained in W, the admissible-correction boundary for W is smaller.
9 Consequently Q_W maps canonically onto Q_U. Vanishing at W implies vanishing
10 at U, not conversely. All maps below use the actual view differential.
11 -/
12 universe u v w
13 namespace KomorebiSpace
14 open CategoryTheory
15 namespace AdditiveViewSystem
16 variable {V : Type u} [Category.{v} V]
17 variable {A : V → Type w} [∀ a, AddCommGroup (A a)]
18 variable (F : AdditiveViewSystem V A)
19 
20 /-- Protecting more views permits fewer correction residuals. -/
21 theorem boundaries_antitone {U W : Set V} (h : U ⊆ W) :
22     (F.problem W).boundaries ≤ (F.problem U).boundaries := by
23   rintro r ⟨x,hx,hr⟩
24   refine ⟨x,?_,hr⟩
25   change F.observation U x = 0
26   funext a
27   exact congrFun hx (⟨a.val,h a.property⟩ : W)
28 
29 /-- The canonical quotient homomorphism forgetting some protected views. -/
30 def forgetObstruction {U W : Set V} (h : U ⊆ W) :
31     (F.problem W).Obstruction →+ (F.problem U).Obstruction :=
32   QuotientAddGroup.map (F.problem W).boundaries (F.problem U).boundaries
33     (AddMonoidHom.id _) (F.boundaries_antitone h)
34 
35 @[simp] theorem forgetObstruction_class {U W : Set V} (h : U ⊆ W)
36     (x : ∀ a, A a) :
37     F.forgetObstruction h ((F.problem W).obstruction x) =
38       (F.problem U).obstruction x := rfl
39 
40 @[simp] theorem forgetObstruction_refl (U : Set V)
41     (x : (F.problem U).Obstruction) :
42     F.forgetObstruction (Set.Subset.refl U) x = x := by
43   induction x using QuotientAddGroup.induction_on with
44   | H x => rfl
45 
46 theorem forgetObstruction_comp {U W Z : Set V} (h : U ⊆ W) (k : W ⊆ Z)
47     (x : (F.problem Z).Obstruction) :
48     F.forgetObstruction h (F.forgetObstruction k x) =
49       F.forgetObstruction (h.trans k) x := by
50   induction x using QuotientAddGroup.induction_on with
51   | H x => rfl
52 
53 /-- The map is onto as a map of obstruction groups. It need not be injective. -/
54 theorem forgetObstruction_surjective {U W : Set V} (h : U ⊆ W) :
55     Function.Surjective (F.forgetObstruction h) := by
56   intro x
57   induction x using QuotientAddGroup.induction_on with
58   | H r => exact ⟨(r : (F.problem W).Obstruction),rfl⟩
59 
60 /-- Restriction of a partial realization transports its actual extension class. -/
61 theorem extensionClass_restrict {U W : Set V} (h : U ⊆ W)
62     (s : F.views.Partial W) :
63     F.forgetObstruction h (F.extensionClass W s) =
64       F.extensionClass U (F.views.restrictPartial h s) := by
65   change (F.problem U).obstruction (F.rawExtension W s) = _
66   apply F.extensionClass_independent
67   intro a
68   exact F.rawExtension_observed W s ⟨a.val,h a.property⟩
69 
70 /-- A genuinely obstructed restriction cannot be cured while preserving more data. -/
71 theorem obstruction_persists_under_prescription {U W : Set V} (h : U ⊆ W)
72     (s : F.views.Partial W)
73     (ho : F.extensionClass U (F.views.restrictPartial h s) ≠ 0) :
74     F.extensionClass W s ≠ 0 := by
75   intro hz
76   apply ho
77   rw [← F.extensionClass_restrict h s,hz,map_zero]
78 
79 /-- Compatible extension to W implies compatible extension to every smaller U. -/
80 theorem vanishing_restricts {U W : Set V} (h : U ⊆ W)
81     (s : F.views.Partial W) (ho : F.extensionClass W s = 0) :
82     F.extensionClass U (F.views.restrictPartial h s) = 0 := by
83   rw [← F.extensionClass_restrict h s,ho,map_zero]
84 
85 end AdditiveViewSystem
86 end KomorebiSpace

Back to source controls