GluedPacketSections.lean

1 import PaperXI.RepresentationGraph
2 import Mathlib.RepresentationTheory.Intertwining
3 
4 /-! Actual linear spaces of compatible sections, their representation, and the
5 map obtained from root holonomy tests. The final section equivalence is built;
6 a compatible family of comparison maps is not part of the input. -/
7 set_option autoImplicit false
8 set_option backward.isDefEq.respectTransparency false
9 noncomputable section
10 namespace PaperXI.GluedPacketSections
11 open Quiver GraphTransport GraphGauge
12 attribute [local instance] GraphTransport.symmetrifyAdd GraphTransport.symmetrifyModule
13 
14 variable {K α G : Type*} [Field K] [Quiver α] [Monoid G]
15 variable {V W : α → Type*}
16 variable [∀ v, AddCommGroup (V v)] [∀ v, Module K (V v)]
17 variable [∀ v, AddCommGroup (W v)] [∀ v, Module K (W v)]
18 variable (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v))
19 variable (B : ∀ {u v : α}, (u ⟶ v) → (W u ≃ₗ[K] W v))
20 
21 /-- Sections satisfy every original oriented-edge equation, not just tree edges. -/
22 def sections : Submodule K (∀ v, V v) where
23   carrier s := ∀ {u v : α} (e : u ⟶ v), A e (s u) = s v
24   zero_mem' := by intro u v e; simp
25   add_mem' := by intro a b ha hb u v e; simpa using (map_add (A e) (a u) (b u)).trans (congrArg₂ (· + ·) (ha e) (hb e))
26   smul_mem' := by intro c a ha u v e; simpa using (map_smul (A e) c (a u)).trans (congrArg (c • ·) (ha e))
27 
28 theorem section_edge (s : sections A) {u v : α} (e : Traversal u v) :
29     edge A e (s.val u) = s.val v := by
30   cases e using Sum.rec with
31   | inl e => exact s.property e
32   | inr e =>
33     change (A e).symm (s.val u) = s.val v
34     apply (A e).injective
35     simpa using (s.property e).symm
36 
37 theorem section_path (s : sections A) {u v : α} (p : Walk u v) :
38     path A p (s.val u) = s.val v := by
39   induction p with
40   | nil => rfl
41   | cons p e ih =>
42     change edge A e (path A p (s.val u)) = _
43     rw [ih, section_edge A s e]
44 
45 /-- Evaluation at a root is injective when actual paths reach every vertex. -/
46 theorem root_evaluation_injective {r : α} (P : ∀ v, Walk r v) :
47     Function.Injective (fun s : sections A => s.val r) := by
48   intro s t h
49   change s.val r = t.val r at h
50   apply Subtype.ext
51   funext v
52   exact (section_path A s (P v)).symm.trans
53     ((congrArg (path A (P v)) h).trans (section_path A t (P v)))
54 
55 /-- The actual fixed space of the based-loop representation. -/
56 def loopFixed (r : α) : Submodule K (V r) where
57   carrier x := ∀ p : Walk r r, path A p x = x
58   zero_mem' := by intro p; simp
59   add_mem' := by intro x y hx hy p; simp [hx p, hy p]
60   smul_mem' := by intro c x hx p; simp [hx p]
61 
62 /-- A loop-fixed root vector is transported to an edge-compatible global section. -/
63 def extendRoot {r : α} (P : ∀ v, Walk r v) (x : loopFixed A r) : sections A :=
64   ⟨fun v => path A (P v) x.val, by
65     intro u v e
66     have h := congrArg (path A (P v)) (x.property (cycle P e))
67     simpa [cycle, GraphTransport.comp, GraphTransport.cons, GraphTransport.reverse,
68       GraphTransport.edge] using h⟩
69 
70 /-- Global sections are exactly root vectors fixed by all actual loop transports. -/
71 def evaluationEquiv {r : α} (P : ∀ v, Walk r v) (hr : P r = .nil) :
72     sections A ≃ₗ[K] loopFixed A r where
73   toFun s := ⟨s.val r, fun p => section_path A s p⟩
74   invFun x := extendRoot A P x
75   left_inv s := by
76     apply Subtype.ext
77     funext v
78     exact section_path A s (P v)
79   right_inv x := by
80     apply Subtype.ext
81     change path A (P r) x.val = x.val
82     simp [hr]
83   map_add' s t := rfl
84   map_smul' c s := rfl
85 
86 variable (ρ : ∀ v, Representation K G (V v))
87 variable (τ : ∀ v, Representation K G (W v))
88 
89 /-- Coordinatewise action preserves the section space by the actual edge covariance. -/
90 def sectionRepresentation (hA : RepresentationGraph.EdgeEquivariant A ρ) :
91     Representation K G (sections A) where
92   toFun g := {
93     toFun s := ⟨fun v => ρ v g (s.val v), by
94       intro u v e
95       rw [hA e g, s.property e]⟩
96     map_add' s t := by ext v; exact map_add (ρ v g) (s.val v) (t.val v)
97     map_smul' c s := by ext v; exact map_smul (ρ v g) c (s.val v) }
98   map_one' := by ext s v; exact DFunLike.congr_fun (map_one (ρ v)) (s.val v)
99   map_mul' g h := by ext s v; exact DFunLike.congr_fun (map_mul (ρ v) g h) (s.val v)
100 
101 @[simp] theorem sectionRepresentation_apply
102     (hA : RepresentationGraph.EdgeEquivariant A ρ) (g : G) (s : sections A) (v : α) :
103     (sectionRepresentation A ρ hA g s).val v = ρ v g (s.val v) := rfl
104 
105 /-- An edge-compatible gauge induces a genuine invertible map of section spaces. -/
106 def ofGauge (F : ∀ v, V v ≃ₗ[K] W v) (hF : EdgeCompatible A B F) :
107     sections A ≃ₗ[K] sections B where
108   toFun s := ⟨fun v => F v (s.val v), by
109     intro u v e
110     rw [← hF e, s.property e]⟩
111   invFun t := ⟨fun v => (F v).symm (t.val v), by
112     intro u v e
113     apply (F v).injective
114     rw [hF e, LinearEquiv.apply_symm_apply, t.property e,
115       LinearEquiv.apply_symm_apply]⟩
116   left_inv s := by ext v; exact (F v).symm_apply_apply _
117   right_inv t := by ext v; exact (F v).apply_symm_apply _
118   map_add' s t := by ext v; exact map_add (F v) _ _
119   map_smul' c s := by ext v; exact map_smul (F v) c _
120 
121 /-- No numerical proxy: this is a Mathlib representation equivalence of the
122 actual spaces of parallel sections. -/
123 def equivOfGauge (hA : RepresentationGraph.EdgeEquivariant A ρ)
124     (hB : RepresentationGraph.EdgeEquivariant B τ)
125     (F : ∀ v, V v ≃ₗ[K] W v) (hF : EdgeCompatible A B F)
126     (hI : RepresentationGraph.Intertwines ρ τ F) :
127     Representation.Equiv (sectionRepresentation A ρ hA) (sectionRepresentation B τ hB) := by
128   refine Representation.Equiv.mk (ofGauge A B F hF) ?_
129   intro g
130   ext s v
131   exact hI v g (s.val v)
132 
133 /-- Constructed root-path gauge. The tree is derived from connectedness. -/
134 def gluedGauge {r : α} (hc : GraphTree.Connected (α := α)) (U : V r ≃ₗ[K] W r) :=
135   rootGauge A B U (GraphTree.rootPath (GraphTree.ofConnected r hc))
136 
137 /-- A root equivalence and fundamental-cycle tests produce a global equivalence. -/
138 def fromChords {r : α} (hc : GraphTree.Connected (α := α))
139     (hA : RepresentationGraph.EdgeEquivariant A ρ)
140     (hB : RepresentationGraph.EdgeEquivariant B τ)
141     (U : Representation.Equiv (ρ r) (τ r))
142     (hch : ∀ e : GraphTree.Chord (GraphTree.ofConnected r hc),
143       CycleCompatible A B U.toLinearEquiv (GraphTree.rootPath (GraphTree.ofConnected r hc)) e.val) :
144     Representation.Equiv (sectionRepresentation A ρ hA) (sectionRepresentation B τ hB) := by
145   let P := GraphTree.rootPath (GraphTree.ofConnected r hc)
146   apply equivOfGauge A B ρ τ hA hB (rootGauge A B U.toLinearEquiv P)
147   · exact (rootGauge_compatible_iff_chords A B U.toLinearEquiv _).mpr hch
148   · exact RepresentationGraph.rootGauge_intertwines A B ρ τ hA hB U.toLinearEquiv
149       (fun g x => DFunLike.congr_fun (U.toIntertwiningMap.isIntertwining' g) x) P
150 
151 /-- Pointwise description of the constructed map: B(path) U A(path)^(-1). -/
152 theorem fromChords_apply {r : α} (hc : GraphTree.Connected (α := α))
153     (hA : RepresentationGraph.EdgeEquivariant A ρ)
154     (hB : RepresentationGraph.EdgeEquivariant B τ)
155     (U : Representation.Equiv (ρ r) (τ r))
156     (hch : ∀ e : GraphTree.Chord (GraphTree.ofConnected r hc),
157       CycleCompatible A B U.toLinearEquiv (GraphTree.rootPath (GraphTree.ofConnected r hc)) e.val)
158     (s : sections A) (v : α) :
159     (fromChords A B ρ τ hc hA hB U hch s).val v =
160       gluedGauge A B hc U.toLinearEquiv v (s.val v) := rfl
161 
162 /-- The compatible family is unique once the root map is fixed. -/
163 theorem gauge_unique_at_root {r : α} (hc : GraphTree.Connected (α := α))
164     (U : V r ≃ₗ[K] W r) (F : ∀ v, V v ≃ₗ[K] W v)
165     (hF : EdgeCompatible A B F) (hr : F r = U) :
166     F = gluedGauge A B hc U := by
167   rw [GraphGauge.gauge_unique A B F hF (GraphTree.rootPath (GraphTree.ofConnected r hc)), hr]
168   rfl
169 
170 end PaperXI.GluedPacketSections

Back to source controls