GraphGauge.lean

1 import PaperXI.GraphTransport
2 import PaperXI.GraphTree
3 import PaperXI.GraphLoopRepresentation
4 import PaperXI.HolonomyResidual
5 
6 /-! Actual graph gauges and the rooted matrix holonomy criterion, Paper XI 14.2–14.3.
7 The cycle tests are the based loops determined by a constructed rooted tree. -/
8 set_option autoImplicit false
9 set_option backward.isDefEq.respectTransparency false
10 noncomputable section
11 namespace PaperXI.GraphGauge
12 
13 open Quiver
14 open GraphTransport
15 attribute [local instance] GraphTransport.symmetrifyAdd GraphTransport.symmetrifyModule
16 
17 variable {K α : Type*} [Field K] [Quiver α]
18 variable {V W : α → Type*}
19   [∀ u, AddCommGroup (V u)] [∀ u, Module K (V u)]
20   [∀ u, AddCommGroup (W u)] [∀ u, Module K (W u)]
21 
22 variable (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v))
23   (B : ∀ {u v : α}, (u ⟶ v) → (W u ≃ₗ[K] W v))
24   {r : α}
25 
26 /-- The actual based loop associated to an original oriented edge and root paths. -/
27 def cycle (P : ∀ v, Walk r v) {u v : α} (e : u ⟶ v) : Walk r r :=
28   ((P u).cons (Sum.inl e)).comp (P v).reverse
29 
30 /-- Vertex gauges transported from a specified root isomorphism. -/
31 def rootGauge (U : V r ≃ₗ[K] W r) (P : ∀ v, Walk r v) (v : α) : V v ≃ₗ[K] W v :=
32   HolonomyResidual.transported U (path A (P v)) (path B (P v))
33 
34 /-- Intertwining equations on every original edge. -/
35 def EdgeCompatible (F : ∀ v, V v ≃ₗ[K] W v) : Prop :=
36   ∀ {u v : α} (e : u ⟶ v) (x : V u), F v (A e x) = B e (F u x)
37 
38 /-- Intertwining equations on all actual based paths. -/
39 def LoopCompatible (U : V r ≃ₗ[K] W r) : Prop :=
40   ∀ (p : Walk r r) (x : V r), U (path A p x) = path B p (U x)
41 
42 /-- One fundamental-cycle intertwining test. -/
43 def CycleCompatible (U : V r ≃ₗ[K] W r) (P : ∀ v, Walk r v)
44     (e : GraphTree.Edge α) : Prop :=
45   ∀ x : V r, U (path A (cycle (α := α) P e.2.2) x) = path B (cycle (α := α) P e.2.2) (U x)
46 
47 @[simp] theorem rootGauge_root (U : V r ≃ₗ[K] W r) (P : ∀ v, Walk r v)
48     (hP : P r = .nil) : rootGauge A B U P r = U := by
49   ext x
50   simp [rootGauge, hP, HolonomyResidual.transported]
51 
52 /-- The fundamental-cycle defect is exactly the edge obstruction for transported gauges. -/
53 theorem rootGauge_edge_iff (U : V r ≃ₗ[K] W r) (P : ∀ v, Walk r v)
54     {u v : α} (e : u ⟶ v) :
55     (∀ x, rootGauge A B U P v (A e x) = B e (rootGauge A B U P u x)) ↔
56       CycleCompatible A B U P ⟨u, v, e⟩ := by
57   constructor
58   · intro h x
59     have hp := congrArg (path B (P v)).symm (h (path A (P u) x))
60     simpa [rootGauge, cycle, CycleCompatible, HolonomyResidual.transported, GraphTransport.comp, GraphTransport.reverse, GraphTransport.cons, GraphTransport.edge] using hp
61   · intro h x
62     have hp := congrArg (path B (P v)) (h ((path A (P u)).symm x))
63     simpa [rootGauge, cycle, CycleCompatible, HolonomyResidual.transported, GraphTransport.comp, GraphTransport.reverse, GraphTransport.cons, GraphTransport.edge] using hp
64 
65 /-- Edge equations propagate along actual paths to every based loop. -/
66 theorem edgeCompatible_loops (F : ∀ v, V v ≃ₗ[K] W v)
67     (hF : EdgeCompatible A B F) : LoopCompatible A B (F r) := by
68   intro p x
69   exact gauge_path A B (fun v => (F v).toLinearMap) hF p x
70 
71 /-- All based-loop equations construct a global gauge for any root path family. -/
72 theorem rootGauge_compatible_of_loops (U : V r ≃ₗ[K] W r)
73     (P : ∀ v, Walk r v) (h : LoopCompatible A B U) :
74     EdgeCompatible A B (rootGauge A B U P) := by
75   intro u v e
76   exact (rootGauge_edge_iff A B U P e).mpr (h (cycle P e))
77 
78 /-- A compatible gauge is uniquely determined by its value at the root. -/
79 theorem gauge_unique (F : ∀ v, V v ≃ₗ[K] W v) (hF : EdgeCompatible A B F)
80     (P : ∀ v, Walk r v) : F = rootGauge A B (F r) P := by
81   funext v
82   ext x
83   have h := gauge_path A B (fun v => (F v).toLinearMap) hF (P v)
84     ((path A (P v)).symm x)
85   simpa [rootGauge, HolonomyResidual.transported] using h
86 
87 /-- Based existence is equivalent to intertwining every actual loop. -/
88 theorem based_iff_loops (U : V r ≃ₗ[K] W r) (P : ∀ v, Walk r v)
89     (hP : P r = .nil) :
90     (∃ F : ∀ v, V v ≃ₗ[K] W v, F r = U ∧ EdgeCompatible A B F) ↔
91       LoopCompatible A B U := by
92   constructor
93   · rintro ⟨F, hroot, hF⟩
94     rw [← hroot]
95     exact edgeCompatible_loops A B F hF
96   · intro h
97     exact ⟨rootGauge A B U P, rootGauge_root A B U P hP,
98       rootGauge_compatible_of_loops A B U P h⟩
99 
100 /-- Transported gauges satisfy each selected parent traversal automatically. -/
101 theorem rootGauge_parent (U : V r ≃ₗ[K] W r) (T : GraphTree.Rooted α r)
102     (a : {a : α // a ≠ r}) (x : V (T.parent a)) :
103     rootGauge A B U (GraphTree.rootPath T) a.val (edge A (T.parentEdge a) x) =
104       edge B (T.parentEdge a) (rootGauge A B U (GraphTree.rootPath T) (T.parent a) x) := by
105   simp only [rootGauge, HolonomyResidual.transported_apply]
106   rw [← GraphTree.rootPath_parent T a]
107   simp [GraphTransport.path]
108 
109 /-- The chosen root gauges intertwine every original edge in the selected tree. -/
110 theorem rootGauge_tree (U : V r ≃ₗ[K] W r) (T : GraphTree.Rooted α r) :
111     ∀ e ∈ GraphTree.treeEdges T,
112       ∀ x : V e.1, rootGauge A B U (GraphTree.rootPath T) e.2.1 (A e.2.2 x) =
113         B e.2.2 (rootGauge A B U (GraphTree.rootPath T) e.1 x) := by
114   apply GraphTree.treeEdges_induction T
115   intro a
116   have h := rootGauge_parent A B U T a
117   unfold GraphTree.selected GraphTree.underlying
118   cases he : T.parentEdge a with
119   | inl e =>
120     simpa [GraphTree.selected, GraphTree.underlying, he] using h
121   | inr e =>
122     intro x
123     have hx := congrArg (B e) (h (A e x))
124     simpa [GraphTree.selected, GraphTree.underlying, he] using hx.symm
125 
126 /-- Chord tests are sufficient: all selected-tree edge equations hold automatically. -/
127 theorem rootGauge_compatible_iff_chords (U : V r ≃ₗ[K] W r)
128     (T : GraphTree.Rooted α r) :
129     EdgeCompatible A B (rootGauge A B U (GraphTree.rootPath T)) ↔
130       ∀ e : GraphTree.Chord T, CycleCompatible A B U (GraphTree.rootPath T) e.val := by
131   classical
132   constructor
133   · intro h e
134     exact (rootGauge_edge_iff A B U (GraphTree.rootPath T) e.val.2.2).mp (h e.val.2.2)
135   · intro h u v e
136     by_cases he : (⟨u, v, e⟩ : GraphTree.Edge α) ∈ GraphTree.treeEdges T
137     · exact rootGauge_tree A B U T ⟨u, v, e⟩ he
138     · exact (rootGauge_edge_iff A B U (GraphTree.rootPath T) e).mpr (h ⟨⟨u,v,e⟩, he⟩)
139 
140 /-- Source 14.2: a fixed root gauge extends exactly when its fundamental-cycle tests pass. -/
141 theorem based_iff_chords (U : V r ≃ₗ[K] W r) (T : GraphTree.Rooted α r) :
142     (∃ F : ∀ v, V v ≃ₗ[K] W v, F r = U ∧ EdgeCompatible A B F) ↔
143       ∀ e : GraphTree.Chord T, CycleCompatible A B U (GraphTree.rootPath T) e.val := by
144   constructor
145   · rintro ⟨F, hroot, hF⟩ e
146     have h := edgeCompatible_loops A B (r := r) F hF
147     rw [hroot] at h
148     exact h (cycle (GraphTree.rootPath T) e.val.2.2)
149   · intro h
150     exact ⟨rootGauge A B U (GraphTree.rootPath T),
151       rootGauge_root A B U _ (GraphTree.rootPath_root T),
152       (rootGauge_compatible_iff_chords A B U T).mpr h⟩
153 
154 /-- The source endpoint obtains its tree from actual connectedness. -/
155 theorem connected_based_iff_chords (U : V r ≃ₗ[K] W r)
156     (hc : GraphTree.Connected (α := α)) :
157     (∃ F : ∀ v, V v ≃ₗ[K] W v, F r = U ∧ EdgeCompatible A B F) ↔
158       ∀ e : GraphTree.Chord (GraphTree.ofConnected r hc),
159         CycleCompatible A B U (GraphTree.rootPath (GraphTree.ofConnected r hc)) e.val :=
160   based_iff_chords A B U (GraphTree.ofConnected r hc)
161 
162 /-- Fundamental-cycle tests imply all based-loop tests, without an abelianization shortcut. -/
163 theorem chords_iff_loops (U : V r ≃ₗ[K] W r) (T : GraphTree.Rooted α r) :
164     (∀ e : GraphTree.Chord T, CycleCompatible A B U (GraphTree.rootPath T) e.val) ↔
165       LoopCompatible A B U :=
166   (based_iff_chords A B U T).symm.trans
167     (based_iff_loops A B U _ (GraphTree.rootPath_root T))
168 
169 /-- The criterion is independent of the rooted spanning tree chosen. -/
170 theorem tree_independence (U : V r ≃ₗ[K] W r)
171     (T S : GraphTree.Rooted α r) :
172     (∀ e : GraphTree.Chord T, CycleCompatible A B U (GraphTree.rootPath T) e.val) ↔
173       ∀ e : GraphTree.Chord S, CycleCompatible A B U (GraphTree.rootPath S) e.val :=
174   (chords_iff_loops A B U T).trans (chords_iff_loops A B U S).symm
175 
176 /-- Source 14.3: graph gauge equivalence is conjugacy of the actual loop representations. -/
177 theorem unbased_iff_conjugates (r : α) (hc : GraphTree.Connected (α := α)) :
178     (∃ F : ∀ v, V v ≃ₗ[K] W v, EdgeCompatible A B F) ↔
179       ∃ U : V r ≃ₗ[K] W r, GraphLoop.Conjugates A B U := by
180   let T := GraphTree.ofConnected r hc
181   constructor
182   · rintro ⟨F, hF⟩
183     exact ⟨F r, (GraphLoop.conjugates_iff_paths A B (F r)).mpr
184       (edgeCompatible_loops A B F hF)⟩
185   · rintro ⟨U, hU⟩
186     have h := (GraphLoop.conjugates_iff_paths A B U).mp hU
187     exact ⟨rootGauge A B U (GraphTree.rootPath T),
188       rootGauge_compatible_of_loops A B U (GraphTree.rootPath T) h⟩
189 
190 end PaperXI.GraphGauge

Back to source controls