GraphLoopRepresentation.lean

1 import PaperXI.GraphLoop
2 import PaperXI.GraphTransport
3 
4 /-!
5 # Holonomy as a homomorphism on actual reduced graph loops
6 
7 The free-groupoid extension of the edge system agrees with the recursively
8 defined path transport on every represented path. Surjectivity of path classes
9 then identifies intertwining all based paths with conjugacy of the resulting
10 honest group homomorphisms.
11 -/
12 
13 namespace PaperXI.GraphLoop
14 
15 open CategoryTheory
16 
17 attribute [local instance] GraphTransport.symmetrifyAdd GraphTransport.symmetrifyModule
18 
19 universe u v k w z
20 
21 variable {α : Type u} [Quiver.{v} α] {K : Type k} [Field K]
22 variable {V : α → Type w} [∀ u, AddCommGroup (V u)] [∀ u, Module K (V u)]
23 
24 /-- A vertex regarded as its assigned vector space in the groupoid of fiber isomorphisms. -/
25 structure Fiber (K : Type k) (V : α → Type w) where
26   vertex : α
27 
28 instance fiberGroupoid : Groupoid (Fiber K V) where
29   Hom u v := V u.vertex ≃ₗ[K] V v.vertex
30   id u := LinearEquiv.refl K (V u.vertex)
31   comp f g := f.trans g
32   id_comp f := by ext x; rfl
33   comp_id f := by ext x; rfl
34   assoc f g h := by ext x; rfl
35   inv f := f.symm
36   inv_comp f := f.symm_trans_self
37   comp_inv f := f.self_trans_symm
38 
39 /-- The original edge system as a prefunctor into actual linear isomorphisms. -/
40 def edgePrefunctor (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v)) :
41     α ⥤q Fiber K V where
42   obj u := ⟨u⟩
43   map e := A e
44 
45 /-- The uniquely extended transport functor on reduced paths. -/
46 def transportFunctor (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v)) :
47     Quiver.FreeGroupoid α ⥤ Fiber K V :=
48   Quiver.FreeGroupoid.lift (edgePrefunctor A)
49 
50 /-- Transport of a morphism of the actual graph groupoid. -/
51 def transport (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v))
52     {u v : α} (f : vertex u ⟶ vertex v) : V u ≃ₗ[K] V v :=
53   (transportFunctor A).map f
54 
55 @[simp] theorem transport_id
56     (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v)) (u : α) :
57     transport A (𝟙 (vertex u)) = LinearEquiv.refl K (V u) :=
58   (transportFunctor A).map_id _
59 
60 @[simp] theorem transport_comp
61     (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v))
62     {u v w : α} (f : vertex u ⟶ vertex v) (g : vertex v ⟶ vertex w) :
63     transport A (f ≫ g) = (transport A f).trans (transport A g) :=
64   (transportFunctor A).map_comp f g
65 
66 @[simp] theorem transport_edge
67     (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v))
68     {u v : Quiver.Symmetrify α} (e : u ⟶ v) :
69     transport A (pathClass e.toPath) = GraphTransport.edge A e := by
70   cases e using Sum.casesOn <;> ext x <;> rfl
71 
72 /-- The quotient construction computes exactly the manuscript's path transport. -/
73 @[simp] theorem transport_pathClass
74     (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v))
75     {u v : Quiver.Symmetrify α} (p : Quiver.Path u v) :
76     transport A (pathClass p) = GraphTransport.path A p := by
77   induction p with
78   | nil => exact transport_id A _
79   | cons p e ih =>
80     change transport A (pathClass p ≫ pathClass e.toPath) = _
81     calc
82       transport A (pathClass p ≫ pathClass e.toPath) =
83           (transport A (pathClass p)).trans (transport A (pathClass e.toPath)) :=
84         transport_comp A (pathClass p) (pathClass e.toPath)
85       _ = GraphTransport.path A (p.cons e) := by
86         rw [ih, transport_edge]
87         rfl
88 
89 /-- Based holonomy as an honest representation by linear automorphisms. -/
90 def holonomy (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v)) (r : α) :
91     Loop r →* (V r ≃ₗ[K] V r) where
92   toFun := transport A
93   map_one' := transport_id A r
94   map_mul' x y := transport_comp A y x
95 
96 @[simp] theorem holonomy_loopClass
97     (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v))
98     {r : α} (p : @Quiver.Path (Quiver.Symmetrify α) _ r r) :
99     holonomy A r (loopClass p) = GraphTransport.path A p :=
100   transport_pathClass A p
101 
102 variable {W : α → Type z} [∀ u, AddCommGroup (W u)] [∀ u, Module K (W u)]
103 
104 /-- Conjugacy of the two actual loop representations by a specified root isomorphism. -/
105 def Conjugates
106     (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v))
107     (B : ∀ {u v : α}, (u ⟶ v) → (W u ≃ₗ[K] W v))
108     {r : α} (U : V r ≃ₗ[K] W r) : Prop :=
109   ∀ g : Loop r, ((U.symm.trans (holonomy A r g)).trans U) = holonomy B r g
110 
111 /-- Intertwining every based path is equivalent to conjugacy on the reduced loop group. -/
112 theorem conjugates_iff_paths
113     (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v))
114     (B : ∀ {u v : α}, (u ⟶ v) → (W u ≃ₗ[K] W v))
115     {r : α} (U : V r ≃ₗ[K] W r) :
116     Conjugates A B U ↔
117       ∀ (p : @Quiver.Path (Quiver.Symmetrify α) _ r r) (x : V r),
118         U (GraphTransport.path A p x) = GraphTransport.path B p (U x) := by
119   constructor
120   · intro h p x
121     have hp := LinearEquiv.congr_fun (h (loopClass p)) (U x)
122     simpa using hp
123   · intro h g
124     obtain ⟨p, rfl⟩ := loopClass_surjective r g
125     ext y
126     simpa using h p (U.symm y)
127 
128 /-- The unbased representation comparison allows the conjugating root map to vary. -/
129 theorem exists_conjugates_iff_paths
130     (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v))
131     (B : ∀ {u v : α}, (u ⟶ v) → (W u ≃ₗ[K] W v)) (r : α) :
132     (∃ U : V r ≃ₗ[K] W r, Conjugates A B U) ↔
133       ∃ U : V r ≃ₗ[K] W r,
134         ∀ (p : @Quiver.Path (Quiver.Symmetrify α) _ r r) (x : V r),
135           U (GraphTransport.path A p x) = GraphTransport.path B p (U x) := by
136   exact exists_congr fun U => conjugates_iff_paths A B U
137 
138 end PaperXI.GraphLoop

Back to source controls