SectionExtensionFibers.lean

1 import KomorebiSpace.SectionObstruction
2 import KomorebiSpace.ExtensionFibers
3 
4 set_option autoImplicit false
5 
6 /-! # Classification and uniqueness of actual ambient extensions -/
7 universe u v w
8 namespace KomorebiSpace
9 open CategoryTheory
10 namespace AdditiveViewSystem
11 variable {V : Type u} [Category.{v} V]
12 variable {A : V → Type w} [∀ a, AddCommGroup (A a)]
13 variable (F : AdditiveViewSystem V A)
14 
15 /-- Coherent ambient changes invisible on the prescribed views. -/
16 def ambiguity (U : Set V) : AddSubgroup (∀ a, A a) := (F.problem U).homogeneous
17 
18 @[simp] theorem mem_ambiguity (U : Set V) (x : ∀ a, A a) :
19     x ∈ F.ambiguity U ↔ F.differential x = 0 ∧ F.observation U x = 0 := Iff.rfl
20 
21 def extensionsFiberEquiv (U : Set V) (s : F.views.Partial U) :
22     F.views.Extensions U s ≃ (F.problem U).ExactFiber s.val where
23   toFun x := ⟨x.val.val, by
24     constructor
25     · exact (F.differential_zero_iff _).mpr x.val.property
26     · exact congrArg Subtype.val x.property⟩
27   invFun x := ⟨⟨x.val, (F.differential_zero_iff _).mp x.property.1⟩, by
28     apply ViewSystem.Partial.ext
29     intro a
30     exact congrFun x.property.2 a⟩
31   left_inv x := by apply Subtype.ext; apply Subtype.ext; rfl
32   right_inv x := by apply Subtype.ext; rfl
33 
34 /-- A chosen global extension supplies affine coordinates on every extension. -/
35 def extensionParameters (U : Set V) (s : F.views.Partial U)
36     (base : F.views.Extensions U s) : F.ambiguity U ≃ F.views.Extensions U s :=
37   ((F.problem U).fiberParameters (F.extensionsFiberEquiv U s base)).trans
38     (F.extensionsFiberEquiv U s).symm
39 
40 @[simp] theorem extensionParameters_coordinate (U : Set V) (s : F.views.Partial U)
41     (base : F.views.Extensions U s) (h : F.ambiguity U) (a : V) :
42     (F.extensionParameters U s base h).val.val a = (show A a from base.val.val a) + h.val a := rfl
43 
44 /-- Difference coordinates use the actual values in every view. -/
45 @[simp] theorem extensionParameters_inverse (U : Set V) (s : F.views.Partial U)
46     (base x : F.views.Extensions U s) (a : V) :
47     ((F.extensionParameters U s base).symm x).val a = (show A a from x.val.val a) - (show A a from base.val.val a) := rfl
48 
49 theorem extension_subsingleton_iff (U : Set V) (s : F.views.Partial U)
50     (base : F.views.Extensions U s) :
51     Subsingleton (F.views.Extensions U s) ↔ F.ambiguity U = ⊥ := by
52   have e := F.extensionsFiberEquiv U s
53   rw [show F.ambiguity U = (F.problem U).homogeneous from rfl]
54   rw [← (F.problem U).fiber_subsingleton_iff (e base)]
55   constructor
56   · intro h
57     exact ⟨fun x y => e.symm.injective (h.elim _ _)⟩
58   · intro h
59     exact ⟨fun x y => e.injective (h.elim _ _)⟩
60 
61 /-- Solvability and uniqueness are independent obligations. -/
62 theorem unique_extension_iff (U : Set V) (s : F.views.Partial U) :
63     (∃! x : F.views.Ambient, F.views.restrict U x = s) ↔
64       F.extensionClass U s = 0 ∧ F.ambiguity U = ⊥ := by
65   constructor
66   · rintro ⟨x,hx,hu⟩
67     let base : F.views.Extensions U s := ⟨x,hx⟩
68     refine ⟨(F.extensionClass_zero_iff U s).mpr ⟨base⟩, ?_⟩
69     apply (F.extension_subsingleton_iff U s base).mp
70     refine ⟨fun a b => ?_⟩
71     apply Subtype.ext
72     exact (hu a.val a.property).trans (hu b.val b.property).symm
73   · rintro ⟨ho,hh⟩
74     obtain ⟨base⟩ := (F.extensionClass_zero_iff U s).mp ho
75     have hs := (F.extension_subsingleton_iff U s base).mpr hh
76     refine ⟨base.val, base.property, ?_⟩
77     intro x hx
78     exact congrArg Subtype.val (hs.elim (⟨x,hx⟩ : F.views.Extensions U s) base)
79 
80 /-- More prescribed views leave fewer homogeneous changes. -/
81 theorem ambiguity_antitone {U W : Set V} (h : U ⊆ W) :
82     F.ambiguity W ≤ F.ambiguity U := by
83   intro x hx
84   refine ⟨hx.1, ?_⟩
85   change F.observation U x = 0
86   funext a
87   exact congrFun hx.2 (⟨a.val,h a.property⟩ : W)
88 
89 end AdditiveViewSystem
90 
91 namespace ViewSystem
92 variable {V : Type u} [Category.{v} V]
93 variable (F : ViewSystem.{u,v,w} V)
94 
95 /-- Each view can be detected by an injective restriction into a prescribed view. -/
96 theorem restrict_injective_of_detecting_views (U : Set V)
97     (detect : ∀ b : V, ∃ a : U, ∃ f : a.val ⟶ b, Function.Injective (F.pull f)) :
98     Function.Injective (F.restrict U) := by
99   intro x y h
100   apply Ambient.ext
101   intro b
102   obtain ⟨a,f,hf⟩ := detect b
103   apply hf
104   rw [x.property, y.property]
105   exact congrArg (fun s : F.Partial U => s.val a) h
106 
107 end ViewSystem
108 end KomorebiSpace

Back to source controls