GraphTransport.lean

1 import Mathlib.Combinatorics.Quiver.Symmetric
2 import Mathlib.LinearAlgebra.Pi
3 import Mathlib.Tactic
4 
5 /-! Paper XI, Section 14. Actual typed path transport on the symmetrification
6 of a quiver. An original arrow is one chosen orientation of an underlying edge;
7 parallel arrows and self-loops keep their identities. Concatenation traverses
8 its left argument first. -/
9 set_option autoImplicit false
10 
11 namespace PaperXI.GraphTransport
12 
13 open Quiver
14 
15 variable {K α : Type*} [Field K] [Quiver α]
16 /-- Traversals retain the positive/negative tag of each original edge. -/
17 abbrev Traversal (u v : α) := @Quiver.Hom (Symmetrify α) _ u v
18 
19 /-- Typed walks in the symmetrified original quiver. -/
20 abbrev Walk (u v : α) := @Quiver.Path (Symmetrify α) _ u v
21 
22 variable {V : α → Type*} [iV : ∀ u, AddCommGroup (V u)] [mV : ∀ u, Module K (V u)]
23 
24 /-- The original additive structure on a fiber over the vertex synonym. -/
25 @[instance_reducible] def symmetrifyAdd (u : Symmetrify α) : AddCommGroup (V u) := iV u
26 attribute [local instance] symmetrifyAdd
27 
28 /-- The original module structure on a fiber over the vertex synonym. -/
29 @[instance_reducible] def symmetrifyModule (u : Symmetrify α) : Module K (V u) := mV u
30 attribute [local instance] symmetrifyModule
31 
32 /-- Edge transport on both formal orientations of an original arrow. -/
33 def edge (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v))
34     {u v : Symmetrify α} (e : u ⟶ v) : V u ≃ₗ[K] V v :=
35   match e with
36   | Sum.inl a => A a
37   | Sum.inr a => (A a).symm
38 
39 @[simp] theorem edge_inl (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v))
40     {u v : α} (e : u ⟶ v) : edge A (Sum.inl e) = A e := rfl
41 
42 @[simp] theorem edge_inr (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v))
43     {u v : α} (e : u ⟶ v) : edge A (Sum.inr e) = (A e).symm := rfl
44 
45 @[simp] theorem edge_reverse (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v))
46     {u v : Symmetrify α} (e : u ⟶ v) :
47     edge A (Quiver.reverse e) = (edge A e).symm := by
48   cases e using Sum.rec <;> rfl
49 
50 /-- Transport along an actual path; the last traversal acts last. -/
51 def path (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v))
52     {u : Symmetrify α} : ∀ {v : Symmetrify α}, Path u v → (V u ≃ₗ[K] V v)
53   | _, .nil => LinearEquiv.refl K (V u)
54   | _, .cons p e => (path A p).trans (edge A e)
55 
56 @[simp] theorem nil (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v))
57     (u : Symmetrify α) : path A (Path.nil : Path u u) = LinearEquiv.refl K (V u) := rfl
58 
59 @[simp] theorem cons (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v))
60     {u v w : Symmetrify α} (p : Path u v) (e : v ⟶ w) :
61     path A (p.cons e) = (path A p).trans (edge A e) := rfl
62 
63 @[simp] theorem toPath (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v))
64     {u v : Symmetrify α} (e : u ⟶ v) : path A e.toPath = edge A e := by
65   ext x
66   rfl
67 
68 @[simp] theorem comp (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v))
69     {u v w : Symmetrify α} (p : Path u v) (q : Path v w) :
70     path A (p.comp q) = (path A p).trans (path A q) := by
71   induction q with
72   | nil => ext x; rfl
73   | cons q e ih =>
74     rw [Path.comp_cons, cons, ih, cons]
75     rfl
76 
77 @[simp] theorem reverse (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v))
78     {u v : Symmetrify α} (p : Path u v) : path A p.reverse = (path A p).symm := by
79   induction p with
80   | nil => rfl
81   | cons p e ih =>
82     rw [Path.reverse, comp, toPath, edge_reverse, ih, cons]
83     rfl
84 
85 @[simp] theorem path_reverse_cancel
86     (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v))
87     {u v : Symmetrify α} (p : Path u v) :
88     path A (p.comp p.reverse) = LinearEquiv.refl K (V u) := by
89   ext x
90   simp
91 
92 @[simp] theorem reverse_path_cancel
93     (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v))
94     {u v : Symmetrify α} (p : Path u v) :
95     path A (p.reverse.comp p) = LinearEquiv.refl K (V v) := by
96   ext x
97   simp
98 
99 /-- An inverse pair may be removed inside an arbitrary typed path. -/
100 theorem cancel (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v))
101     {u v w z : Symmetrify α} (p : Path u v) (e : v ⟶ w) (q : Path v z) :
102     path A (((p.cons e).cons (Quiver.reverse e)).comp q) = path A (p.comp q) := by
103   rw [comp, comp, cons, cons, edge_reverse]
104   ext x
105   simp
106 
107 variable {W : α → Type*} [iW : ∀ u, AddCommGroup (W u)] [mW : ∀ u, Module K (W u)]
108 
109 /-- Intertwining original edges also intertwines their formal inverses. -/
110 theorem gauge_edge
111     (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v))
112     (B : ∀ {u v : α}, (u ⟶ v) → (W u ≃ₗ[K] W v))
113     (U : ∀ u, V u →ₗ[K] W u)
114     (hU : ∀ {u v : α} (e : u ⟶ v) (x : V u), U v (A e x) = B e (U u x))
115     {u v : Symmetrify α} (e : u ⟶ v) (x : V u) :
116     U v (edge A e x) = edge B e (U u x) := by
117   cases e using Sum.rec with
118   | inl e => exact hU e x
119   | inr e =>
120     change U v ((A e).symm x) = (B e).symm (U u x)
121     apply (B e).injective
122     simpa using (hU e ((A e).symm x)).symm
123 
124 /-- The actual edge equations imply all path equations by induction. -/
125 theorem gauge_path
126     (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v))
127     (B : ∀ {u v : α}, (u ⟶ v) → (W u ≃ₗ[K] W v))
128     (U : ∀ u, V u →ₗ[K] W u)
129     (hU : ∀ {u v : α} (e : u ⟶ v) (x : V u), U v (A e x) = B e (U u x))
130     {u v : Symmetrify α} (p : Path u v) (x : V u) :
131     U v (path A p x) = path B p (U u x) := by
132   induction p with
133   | nil => rfl
134   | cons p e ih =>
135     change U _ (edge A e (path A p x)) = edge B e (path B p (U _ x))
136     rw [gauge_edge A B U hU, ih]
137 
138 /-- Equivalence-valued formulation of the same path intertwining law. -/
139 theorem gauge_path_equiv
140     (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v))
141     (B : ∀ {u v : α}, (u ⟶ v) → (W u ≃ₗ[K] W v))
142     (U : ∀ u, V u ≃ₗ[K] W u)
143     (hU : ∀ {u v : α} (e : u ⟶ v), (A e).trans (U v) = (U u).trans (B e))
144     {u v : Symmetrify α} (p : Path u v) :
145     (path A p).trans (U v) = (U u).trans (path B p) := by
146   ext x
147   exact gauge_path A B (fun u => (U u).toLinearMap)
148     (fun e y => LinearEquiv.congr_fun (hU e) y) p x
149 
150 end PaperXI.GraphTransport

Back to source controls