ExtensionFibers.lean

1 import KomorebiSpace.Correction
2 import Mathlib.Tactic.Abel
3 
4 set_option autoImplicit false
5 
6 /-!
7 # All exact lifts of prescribed observations
8 
9 A nonempty exact fiber is parametrized by the homogeneous solutions.
10 Choosing one lift supplies coordinates, not a preferred lift.
11 -/
12 universe u v w
13 namespace KomorebiSpace
14 namespace CorrectionProblem
15 variable {E : Type u} {R : Type v} {S : Type w}
16 variable [AddCommGroup E] [AddCommGroup R] [AddCommGroup S]
17 variable (P : CorrectionProblem E R S)
18 
19 /-- Exact changes that leave all protected observations fixed. -/
20 def homogeneous : AddSubgroup E := P.residual.ker ⊓ P.semantics.ker
21 
22 @[simp] theorem mem_homogeneous (x : E) :
23     x ∈ P.homogeneous ↔ P.residual x = 0 ∧ P.semantics x = 0 := Iff.rfl
24 
25 /-- This fiber is defined for arbitrary prescribed observations, not only liftable ones. -/
26 def ExactFiber (s : S) := {x : E // P.residual x = 0 ∧ P.semantics x = s}
27 
28 @[ext] theorem ExactFiber.ext {s : S} {x y : P.ExactFiber s}
29     (h : x.val = y.val) : x = y := Subtype.ext h
30 
31 /-- Translation by a homogeneous solution preserves the exact fiber. -/
32 def translateFiber {s : S} (h : P.homogeneous) (x : P.ExactFiber s) : P.ExactFiber s :=
33   ⟨x.val + h.val, by
34     constructor
35     · rw [map_add, x.property.1, h.property.1, add_zero]
36     · rw [map_add, x.property.2, h.property.2, add_zero]⟩
37 
38 @[simp] theorem translateFiber_val {s : S} (h : P.homogeneous) (x : P.ExactFiber s) :
39     (P.translateFiber h x).val = x.val + h.val := rfl
40 
41 @[simp] theorem translateFiber_zero {s : S} (x : P.ExactFiber s) :
42     P.translateFiber 0 x = x := by
43   apply Subtype.ext
44   exact add_zero _
45 
46 theorem translateFiber_add {s : S} (h k : P.homogeneous) (x : P.ExactFiber s) :
47     P.translateFiber (h + k) x = P.translateFiber k (P.translateFiber h x) := by
48   apply Subtype.ext
49   exact (add_assoc _ _ _).symm
50 
51 /-- Difference of two exact lifts with the same observations. -/
52 def fiberDifference {s : S} (x y : P.ExactFiber s) : P.homogeneous :=
53   ⟨x.val - y.val, by
54     change P.residual (x.val - y.val) = 0 ∧ P.semantics (x.val - y.val) = 0
55     constructor
56     · rw [map_sub, x.property.1, y.property.1, sub_self]
57     · rw [map_sub, x.property.2, y.property.2, sub_self]⟩
58 
59 @[simp] theorem fiberDifference_val {s : S} (x y : P.ExactFiber s) :
60     (P.fiberDifference x y).val = x.val - y.val := rfl
61 
62 @[simp] theorem translate_difference {s : S} (x y : P.ExactFiber s) :
63     P.translateFiber (P.fiberDifference x y) y = x := by
64   apply Subtype.ext
65   change y.val + (x.val - y.val) = x.val
66   abel
67 
68 /-- The action is simply transitive whenever the fiber is nonempty. -/
69 theorem exists_unique_translation {s : S} (x y : P.ExactFiber s) :
70     ∃! h : P.homogeneous, P.translateFiber h x = y := by
71   refine ⟨P.fiberDifference y x, P.translate_difference y x, ?_⟩
72   intro h hh
73   apply Subtype.ext
74   have he := congrArg Subtype.val hh
75   change x.val + h.val = y.val at he
76   change h.val = y.val - x.val
77   rw [← he]
78   abel
79 
80 /-- Coordinates on the fiber require a supplied base solution. -/
81 def fiberParameters {s : S} (base : P.ExactFiber s) : P.homogeneous ≃ P.ExactFiber s where
82   toFun h := P.translateFiber h base
83   invFun x := P.fiberDifference x base
84   left_inv h := by
85     apply Subtype.ext
86     change base.val + h.val - base.val = h.val
87     abel
88   right_inv x := P.translate_difference x base
89 
90 @[simp] theorem fiberParameters_apply {s : S} (base : P.ExactFiber s) (h : P.homogeneous) :
91     (P.fiberParameters base h).val = base.val + h.val := rfl
92 
93 /-- Uniqueness, separately from existence, is exactly vanishing homogeneous freedom. -/
94 theorem fiber_subsingleton_iff {s : S} (base : P.ExactFiber s) :
95     Subsingleton (P.ExactFiber s) ↔ P.homogeneous = ⊥ := by
96   constructor
97   · intro hsub
98     apply le_antisymm
99     · intro x hx
100       change x = 0
101       have he : P.translateFiber ⟨x,hx⟩ base = base := hsub.elim _ _
102       have hv := congrArg Subtype.val he
103       change base.val + x = base.val at hv
104       exact add_left_cancel (hv.trans (add_zero base.val).symm)
105     · exact bot_le
106   · intro hz
107     refine ⟨fun x y => ?_⟩
108     apply Subtype.ext
109     have hm : x.val - y.val ∈ P.homogeneous := (P.fiberDifference x y).property
110     rw [hz] at hm
111     change x.val - y.val = 0 at hm
112     exact sub_eq_zero.mp hm
113 
114 /-- The old obstruction criterion now records existence of the whole fiber. -/
115 theorem obstruction_zero_iff_fiber (x : E) :
116     P.obstruction x = 0 ↔ Nonempty (P.ExactFiber (P.semantics x)) := by
117   rw [P.flatten_iff]
118   constructor
119   · rintro ⟨y,hd,hp⟩
120     exact ⟨⟨y,hd,hp⟩⟩
121   · rintro ⟨⟨y,hd,hp⟩⟩
122     exact ⟨y,hd,hp⟩
123 
124 /-- Changing the base solution changes coordinates by a translation. -/
125 theorem change_base {s : S} (x y : P.ExactFiber s) (h : P.homogeneous) :
126     (P.fiberParameters y).symm (P.fiberParameters x h) =
127       h + P.fiberDifference x y := by
128   apply Subtype.ext
129   change x.val + h.val - y.val = h.val + (x.val - y.val)
130   abel
131 
132 end CorrectionProblem
133 end KomorebiSpace

Back to source controls