HolonomyTransport.lean

1 import KomorebiSpace.OverlapPathRepair
2 import Mathlib.Combinatorics.SimpleGraph.Walk.Operations
3 
4 set_option autoImplicit false
5 
6 /-!
7 # Isometric edge transports without a global trivialization
8 
9 Reverse edges are inverse isometries. No triangle composition law is assumed.
10 Transport along a walk is constructed from its edges. Its discrepancy is
11 bounded by the sum of the actual edge discrepancies.
12 -/
13 universe u v
14 noncomputable section
15 namespace KomorebiSpace
16 namespace HolonomyTransport
17 variable {V : Type u} {H : Type v}
18 variable [NormedAddCommGroup H] [NormedSpace ℝ H]
19 
20 structure Connection (V : Type u) (H : Type v)
21     [NormedAddCommGroup H] [NormedSpace ℝ H] where
22   transport : V → V → H ≃ₗᵢ[ℝ] H
23   self_apply : ∀ i z, transport i i z = z
24   reverse_apply : ∀ i j z, transport i j (transport j i z) = z
25 
26 namespace Connection
27 variable (T : Connection V H) {graph : SimpleGraph V}
28 
29 def ofFrames (e : OverlapTransport.Frames (V := V) (H := H)) : Connection V H where
30   transport := OverlapTransport.transport e
31   self_apply := OverlapTransport.transport_self e
32   reverse_apply := by
33     intro i j z
34     rw [OverlapTransport.transport_comp, OverlapTransport.transport_self]
35 
36 def defect (x : V → H) (i j : V) : H := T.transport i j (x j) - x i
37 
38 def Parallel (graph : SimpleGraph V) (x : V → H) : Prop :=
39   ∀ i j, graph.Adj i j → T.transport i j (x j) = x i
40 
41 def walkTransport : {i j : V} → graph.Walk i j → H ≃ₗᵢ[ℝ] H
42   | _, _, .nil => LinearIsometryEquiv.refl ℝ H
43   | i, _, @SimpleGraph.Walk.cons _ _ _ j _ _ p =>
44       (walkTransport p).trans (T.transport i j)
45 
46 @[simp] theorem walkTransport_nil (i : V) (z : H) :
47     T.walkTransport (SimpleGraph.Walk.nil (G := graph) (u := i)) z = z := rfl
48 
49 @[simp] theorem walkTransport_cons {i j k : V} (h : graph.Adj i j)
50     (p : graph.Walk j k) (z : H) :
51     T.walkTransport (.cons h p) z = T.transport i j (T.walkTransport p z) := rfl
52 
53 theorem walkTransport_append {i j k : V} (p : graph.Walk i j)
54     (q : graph.Walk j k) (z : H) :
55     T.walkTransport (p.append q) z = T.walkTransport p (T.walkTransport q z) := by
56   induction p with
57   | nil => rfl
58   | @cons i j k h p ih =>
59     simpa only [SimpleGraph.Walk.cons_append, walkTransport_cons] using
60       congrArg (T.transport i j) (ih q)
61 
62 /-- Reverse edge consistency supplies inverse transport along every reversed walk. -/
63 theorem walkTransport_reverse {i j : V} (p : graph.Walk i j) (z : H) :
64     T.walkTransport p.reverse (T.walkTransport p z) = z := by
65   induction p with
66   | nil => rfl
67   | @cons i k j h p ih =>
68     rw [SimpleGraph.Walk.reverse_cons,
69       walkTransport_append, walkTransport_cons, walkTransport_nil, walkTransport_cons,
70       T.reverse_apply]
71     exact ih
72 
73 theorem walkTransport_reverse_eq_symm {i j : V} (p : graph.Walk i j) (z : H) :
74     T.walkTransport p.reverse z = (T.walkTransport p).symm z := by
75   have he := T.walkTransport_reverse p ((T.walkTransport p).symm z)
76   simpa only [LinearIsometryEquiv.apply_symm_apply] using he
77 
78 theorem parallel_walk (x : V → H) (hx : T.Parallel graph x)
79     {i j : V} (p : graph.Walk i j) : T.walkTransport p (x j) = x i := by
80   induction p with
81   | nil => rfl
82   | cons h p ih => rw [walkTransport_cons, ih, hx _ _ h]
83 
84 theorem parallel_iff_all_walks (x : V → H) :
85     T.Parallel graph x ↔ ∀ i j (p : graph.Walk i j), T.walkTransport p (x j) = x i := by
86   constructor
87   · intro hx i j p; exact T.parallel_walk x hx p
88   · intro hx i j h
89     exact hx i j (.cons h .nil)
90 
91 section Finite
92 variable [Fintype V]
93 abbrev Edges (graph : SimpleGraph V) := OverlapTransport.Edges graph
94 
95 def differentialLinear (graph : SimpleGraph V) : (V → H) →ₗ[ℝ] (Edges graph → H) where
96   toFun x a := T.defect x a.val.1 a.val.2
97   map_add' := by
98     intro x y
99     funext a
100     simp only [defect, Pi.add_apply, map_add]
101     abel
102   map_smul' := by
103     intro c x
104     funext a
105     simp [defect, map_smul, smul_sub]
106 
107 theorem differentialLinear_bound (graph : SimpleGraph V) (x : V → H) :
108     ‖T.differentialLinear graph x‖ ≤ 2 * ‖x‖ := by
109   apply (pi_norm_le_iff_of_nonneg (mul_nonneg (by norm_num) (norm_nonneg x))).mpr
110   intro a
111   change ‖T.transport a.val.1 a.val.2 (x a.val.2) - x a.val.1‖ ≤ _
112   calc
113     _ ≤ ‖T.transport a.val.1 a.val.2 (x a.val.2)‖ + ‖x a.val.1‖ := norm_sub_le _ _
114     _ = ‖x a.val.2‖ + ‖x a.val.1‖ := by rw [LinearIsometryEquiv.norm_map]
115     _ ≤ 2 * ‖x‖ := by
116       have hi := norm_le_pi_norm x a.val.1
117       have hj := norm_le_pi_norm x a.val.2
118       linarith
119 
120 def differential (graph : SimpleGraph V) : (V → H) →L[ℝ] (Edges graph → H) :=
121   (T.differentialLinear graph).mkContinuous 2 (T.differentialLinear_bound graph)
122 
123 @[simp] theorem differential_apply (x : V → H) (a : Edges graph) :
124     T.differential graph x a = T.defect x a.val.1 a.val.2 := rfl
125 
126 theorem differential_opNorm (graph : SimpleGraph V) : ‖T.differential graph‖ ≤ 2 := by
127   apply (T.differential graph).opNorm_le_bound (by norm_num)
128   exact T.differentialLinear_bound graph
129 
130 theorem parallel_iff_differential_zero (x : V → H) :
131     T.Parallel graph x ↔ T.differential graph x = 0 := by
132   constructor
133   · intro hx; funext a; exact sub_eq_zero.mpr (hx _ _ a.property)
134   · intro hx i j h
135     exact sub_eq_zero.mp (congrFun hx (⟨(i,j),h⟩ : Edges graph))
136 
137 theorem walk_error (x : V → H) {i j : V} (p : graph.Walk i j) :
138     ‖T.walkTransport p (x j) - x i‖ ≤ (p.length : ℝ) * ‖T.differential graph x‖ := by
139   induction p with
140   | nil => simp
141   | @cons i k j h p ih =>
142     have he : ‖T.transport i k (x k) - x i‖ ≤ ‖T.differential graph x‖ :=
143       norm_le_pi_norm (T.differential graph x) ⟨(i,k),h⟩
144     calc
145       _ = ‖T.transport i k (T.walkTransport p (x j) - x k) +
146           (T.transport i k (x k) - x i)‖ := by
147             rw [walkTransport_cons, map_sub]
148             congr 1
149             abel
150       _ ≤ ‖T.transport i k (T.walkTransport p (x j) - x k)‖ +
151           ‖T.transport i k (x k) - x i‖ := norm_add_le _ _
152       _ = ‖T.walkTransport p (x j) - x k‖ +
153           ‖T.transport i k (x k) - x i‖ := by rw [LinearIsometryEquiv.norm_map]
154       _ ≤ (p.length : ℝ) * ‖T.differential graph x‖ + ‖T.differential graph x‖ :=
155         add_le_add ih he
156       _ = ((SimpleGraph.Walk.cons h p).length : ℝ) * ‖T.differential graph x‖ := by
157         simp only [SimpleGraph.Walk.length_cons, Nat.cast_add, Nat.cast_one]
158         ring
159 
160 @[simp] theorem ofFrames_differential
161     (e : OverlapTransport.Frames (V := V) (H := H)) (x : V → H) :
162     (ofFrames e).differential graph x = OverlapTransport.edgeDifferential e graph x := rfl
163 
164 end Finite
165 end Connection
166 end HolonomyTransport
167 end KomorebiSpace
168 end

Back to source controls