ScalarGluing.lean

1 import PaperXI.GraphGauge
2 import PaperXI.ProjectiveHolonomy
3 
4 /-! Scalar gluing on actual graph cycles, with the zero-dimensional branch retained. -/
5 set_option autoImplicit false
6 set_option backward.isDefEq.respectTransparency false
7 noncomputable section
8 
9 namespace PaperXI.ScalarGluing
10 
11 open PaperXI.GraphTransport PaperXI.GraphGauge PaperXI.ScalarHolonomy
12 open PaperXI.ProjectiveHolonomy
13 
14 attribute [local instance] GraphTransport.symmetrifyAdd GraphTransport.symmetrifyModule
15 
16 variable {K α : Type*} [Field K] [Quiver α]
17 variable {V W : α → Type*}
18   [∀ u, AddCommGroup (V u)] [∀ u, Module K (V u)]
19   [∀ u, AddCommGroup (W u)] [∀ u, Module K (W u)]
20 
21 variable (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v))
22   (B : ∀ {u v : α}, (u ⟶ v) → (W u ≃ₗ[K] W v)) {r : α}
23 
24 /-- A cycle test compares the actual operators after identifying the root spaces. -/
25 theorem cycle_operator_iff (U : V r ≃ₗ[K] W r) (P : ∀ v, Walk r v)
26     (e : GraphTree.Edge α) :
27     CycleCompatible A B U P e ↔
28       ((U.symm.trans (path (α := α) A (cycle (α := α) P e.2.2))).trans U) = path (α := α) B (cycle (α := α) P e.2.2) := by
29   constructor
30   · intro h
31     ext y
32     simpa using h (U.symm y)
33   · intro h x
34     simpa using LinearEquiv.congr_fun h (U x)
35 
36 /-- For scalar loop operators, the root identification does not affect any cycle test. -/
37 theorem cycle_independent (hA : IsScalar (GraphLoop.holonomy A r))
38     (U Q : V r ≃ₗ[K] W r) (P : ∀ v, Walk r v) (e : GraphTree.Edge α) :
39     CycleCompatible A B U P e ↔ CycleCompatible A B Q P e := by
40   rw [cycle_operator_iff, cycle_operator_iff]
41   have h := (isScalar_iff_paths A r).mp hA (cycle P e.2.2)
42   rw [scalar_conjugate_independent U Q _ h]
43 
44 /-- At all ranks, gluing with one root identification is tested by actual scalar
45 operators using any other root identification. -/
46 theorem based_iff_scalar_operators (hA : IsScalar (GraphLoop.holonomy A r))
47     (U Q : V r ≃ₗ[K] W r) (T : GraphTree.Rooted α r) :
48     (∃ F : ∀ v, V v ≃ₗ[K] W v, F r = U ∧ EdgeCompatible A B F) ↔
49       ∀ e : GraphTree.Chord T,
50         ((Q.symm.trans (path (α := α) A (cycle (α := α) (GraphTree.rootPath T) e.val.2.2))).trans Q) =
51           path (α := α) B (cycle (α := α) (GraphTree.rootPath T) e.val.2.2) := by
52   rw [based_iff_chords A B U T]
53   apply forall_congr'
54   intro e
55   exact (cycle_independent A B hA U Q _ e.val).trans (cycle_operator_iff A B Q _ e.val)
56 
57 /-- This version of scalar gluing is independent of root gauges even at dimension zero. -/
58 theorem based_root_independent (hA : IsScalar (GraphLoop.holonomy A r))
59     (U Q : V r ≃ₗ[K] W r) (T : GraphTree.Rooted α r) :
60     (∃ F : ∀ v, V v ≃ₗ[K] W v, F r = U ∧ EdgeCompatible A B F) ↔
61       ∃ F : ∀ v, V v ≃ₗ[K] W v, F r = Q ∧ EdgeCompatible A B F := by
62   rw [based_iff_chords A B U T, based_iff_chords A B Q T]
63   exact forall_congr' fun e => cycle_independent A B hA U Q _ e.val
64 
65 /-- When scalar values are identifiable, one cycle equation is precisely equality of values. -/
66 theorem cycle_units_iff [Nontrivial (V r)] [Nontrivial (W r)]
67     (hA : IsScalar (GraphLoop.holonomy A r)) (hB : IsScalar (GraphLoop.holonomy B r))
68     (U : V r ≃ₗ[K] W r) (P : ∀ v, Walk r v) (e : GraphTree.Edge α) :
69     CycleCompatible A B U P e ↔
70       loopCharacter A r hA (GraphLoop.loopClass (cycle P e.2.2)) =
71         loopCharacter B r hB (GraphLoop.loopClass (cycle P e.2.2)) := by
72   have h := intertwines_iff U
73     (loopCharacter A r hA (GraphLoop.loopClass (cycle P e.2.2)))
74     (loopCharacter B r hB (GraphLoop.loopClass (cycle P e.2.2)))
75   simpa only [CycleCompatible, loopCharacter_spec, GraphLoop.holonomy_loopClass] using h
76 
77 /-- Source 14.4's unit-valued formulation, with its necessary nonzero-root hypothesis. -/
78 theorem based_iff_scalar_units [Nontrivial (V r)] [Nontrivial (W r)]
79     (hA : IsScalar (GraphLoop.holonomy A r)) (hB : IsScalar (GraphLoop.holonomy B r))
80     (U : V r ≃ₗ[K] W r) (T : GraphTree.Rooted α r) :
81     (∃ F : ∀ v, V v ≃ₗ[K] W v, F r = U ∧ EdgeCompatible A B F) ↔
82       ∀ e : GraphTree.Chord T,
83         loopCharacter A r hA (GraphLoop.loopClass (cycle (GraphTree.rootPath T) e.val.2.2)) =
84           loopCharacter B r hB (GraphLoop.loopClass (cycle (GraphTree.rootPath T) e.val.2.2)) := by
85   rw [based_iff_chords A B U T]
86   exact forall_congr' fun e => cycle_units_iff A B hA hB U _ e.val
87 
88 /-- Allowing the root map to vary introduces no conjugacy condition for scalar holonomy. -/
89 theorem unbased_iff_scalar_units [Nontrivial (V r)] [Nontrivial (W r)]
90     (hA : IsScalar (GraphLoop.holonomy A r)) (hB : IsScalar (GraphLoop.holonomy B r))
91     (U : V r ≃ₗ[K] W r) (T : GraphTree.Rooted α r) :
92     (∃ F : ∀ v, V v ≃ₗ[K] W v, EdgeCompatible A B F) ↔
93       ∀ e : GraphTree.Chord T,
94         loopCharacter A r hA (GraphLoop.loopClass (cycle (GraphTree.rootPath T) e.val.2.2)) =
95           loopCharacter B r hB (GraphLoop.loopClass (cycle (GraphTree.rootPath T) e.val.2.2)) := by
96   constructor
97   · rintro ⟨F, hF⟩
98     exact (based_iff_scalar_units A B hA hB (F r) T).mp ⟨F, rfl, hF⟩
99   · intro h
100     obtain ⟨F, _, hF⟩ := (based_iff_scalar_units A B hA hB U T).mpr h
101     exact ⟨F, hF⟩
102 
103 /-- Equality of the extracted characters is equivalent to all actual loop equations. -/
104 theorem loops_iff_characters [Nontrivial (V r)] [Nontrivial (W r)]
105     (hA : IsScalar (GraphLoop.holonomy A r)) (hB : IsScalar (GraphLoop.holonomy B r))
106     (U : V r ≃ₗ[K] W r) :
107     LoopCompatible A B U ↔ loopCharacter A r hA = loopCharacter B r hB := by
108   rw [loopCharacter, loopCharacter, ← character_intertwines_iff _ _ hA hB U]
109   constructor
110   · intro h g
111     obtain ⟨p, rfl⟩ := GraphLoop.loopClass_surjective r g
112     simpa only [GraphLoop.holonomy_loopClass] using h p
113   · intro h p
114     simpa only [GraphLoop.holonomy_loopClass] using h (GraphLoop.loopClass p)
115 
116 /-- The first-homology ratio is the exact scalar gluing obstruction. -/
117 theorem based_iff_ratioH1_trivial [Nontrivial (V r)] [Nontrivial (W r)]
118     (hA : IsScalar (GraphLoop.holonomy A r)) (hB : IsScalar (GraphLoop.holonomy B r))
119     (U : V r ≃ₗ[K] W r) (T : GraphTree.Rooted α r) :
120     (∃ F : ∀ v, V v ≃ₗ[K] W v, F r = U ∧ EdgeCompatible A B F) ↔
121       transportRatioH1 A B r hA hB = 1 := by
122   rw [based_iff_loops A B U (GraphTree.rootPath T) (GraphTree.rootPath_root T),
123     loops_iff_characters A B hA hB U]
124   exact (ratioH1_eq_one_iff r _ _).symm
125 
126 /-- A zero root space has automatic loop equations, so connected transport glues without tests. -/
127 theorem zero_root_gluing [Subsingleton (V r)]
128     (U : V r ≃ₗ[K] W r) (T : GraphTree.Rooted α r) :
129     ∃ F : ∀ v, V v ≃ₗ[K] W v, F r = U ∧ EdgeCompatible A B F := by
130   apply (based_iff_loops A B U (GraphTree.rootPath T) (GraphTree.rootPath_root T)).mpr
131   intro p x
132   exact zero_space_intertwines U (path A p) (path B p) x
133 
134 /-- The literal zero-dimensional case of the manuscript has no gluing obstruction. -/
135 theorem zero_finrank_gluing [FiniteDimensional K (V r)]
136     (hzero : Module.finrank K (V r) = 0)
137     (U : V r ≃ₗ[K] W r) (T : GraphTree.Rooted α r) :
138     ∃ F : ∀ v, V v ≃ₗ[K] W v, F r = U ∧ EdgeCompatible A B F := by
139   let : Subsingleton (V r) := (Module.finrank_zero_iff).mp hzero
140   exact zero_root_gluing A B U T
141 
142 /-- The source-facing scalar criterion constructs the root identification from equal
143 dimensions and the rooted spanning tree from connectedness. -/
144 theorem connected_scalar_criterion [FiniteDimensional K (V r)] [FiniteDimensional K (W r)]
145     [Nontrivial (V r)] [Nontrivial (W r)]
146     (hdim : Module.finrank K (V r) = Module.finrank K (W r))
147     (hc : GraphTree.Connected (α := α))
148     (hA : IsScalar (GraphLoop.holonomy A r)) (hB : IsScalar (GraphLoop.holonomy B r)) :
149     (∃ F : ∀ v, V v ≃ₗ[K] W v, EdgeCompatible A B F) ↔
150       ∀ e : GraphTree.Chord (GraphTree.ofConnected r hc),
151         loopCharacter A r hA (GraphLoop.loopClass
152           (cycle (GraphTree.rootPath (GraphTree.ofConnected r hc)) e.val.2.2)) =
153         loopCharacter B r hB (GraphLoop.loopClass
154           (cycle (GraphTree.rootPath (GraphTree.ofConnected r hc)) e.val.2.2)) := by
155   obtain ⟨U⟩ := FiniteDimensional.nonempty_linearEquiv_of_finrank_eq hdim
156   exact unbased_iff_scalar_units A B hA hB U (GraphTree.ofConnected r hc)
157 
158 /-- The equal zero-dimensional source case constructs a global gauge without scalar choices. -/
159 theorem connected_zero_dimensional [FiniteDimensional K (V r)] [FiniteDimensional K (W r)]
160     (hV : Module.finrank K (V r) = 0) (hW : Module.finrank K (W r) = 0)
161     (hc : GraphTree.Connected (α := α)) :
162     ∃ F : ∀ v, V v ≃ₗ[K] W v, EdgeCompatible A B F := by
163   obtain ⟨U⟩ := FiniteDimensional.nonempty_linearEquiv_of_finrank_eq (hV.trans hW.symm)
164   obtain ⟨F, _, hF⟩ := zero_finrank_gluing A B hV U (GraphTree.ofConnected r hc)
165   exact ⟨F, hF⟩
166 
167 end PaperXI.ScalarGluing

Back to source controls