GraphTreePaths.lean

1 import PaperXI.GraphTree
2 import PaperXI.GraphTransport
3 
4 /-! Actual tree paths intertwine every reversible system of edge transports.
5 Tree membership refers to the chosen original edge identity. -/
6 set_option autoImplicit false
7 set_option backward.isDefEq.respectTransparency false
8 noncomputable section
9 namespace PaperXI.GraphTreePaths
10 
11 open Quiver
12 open GraphTree
13 variable {K α : Type*} [Field K] [Quiver α] {r : α}
14 variable {V : α → Type*} [∀ a, AddCommGroup (V a)] [∀ a, Module K (V a)]
15 attribute [local instance] GraphTransport.symmetrifyAdd GraphTransport.symmetrifyModule
16 
17 variable (T : Rooted α r)
18 variable (A : ∀ {a b : α}, (a ⟶ b) → (V a ≃ₗ[K] V b))
19 
20 theorem parent_transport (a : {a : α // a ≠ r}) :
21     (GraphTransport.path A (rootPath T (T.parent a))).trans
22         (GraphTransport.edge A (T.parentEdge a)) =
23       GraphTransport.path A (rootPath T a.val) := by
24   rw [← GraphTransport.cons, rootPath_parent]
25 
26 /-- Transport is coherent along each selected original tree edge. -/
27 theorem tree_transport (e : Edge α) (he : e ∈ treeEdges T) :
28     (GraphTransport.path A (rootPath T e.1)).trans (A e.2.2) =
29       GraphTransport.path A (rootPath T e.2.1) := by
30   apply treeEdges_induction T (fun e =>
31     (GraphTransport.path A (rootPath T e.1)).trans (A e.2.2) =
32       GraphTransport.path A (rootPath T e.2.1)) ?_ e he
33   intro a
34   have hp := parent_transport T A a
35   cases h : T.parentEdge a with
36   | inl f =>
37     have hs : selected T a = ⟨T.parent a, a.val, f⟩ := by
38       unfold selected
39       rw [h]
40       rfl
41     rw [hs]
42     simpa only [h, GraphTransport.edge_inl] using hp
43   | inr f =>
44     have hs : selected T a = ⟨a.val, T.parent a, f⟩ := by
45       unfold selected
46       rw [h]
47       rfl
48     rw [hs]
49     rw [h, GraphTransport.edge_inr] at hp
50     rw [← hp]
51     ext x
52     simp
53 
54 /-- The same coherence holds in either formal orientation of a tree edge. -/
55 theorem traversal_transport {a b : α} (e : Traversal a b)
56     (he : underlying e ∈ treeEdges T) :
57     (GraphTransport.path A (rootPath T a)).trans (GraphTransport.edge A e) =
58       GraphTransport.path A (rootPath T b) := by
59   have hp := tree_transport T A (underlying e) he
60   cases e with
61   | inl f => exact hp
62   | inr f =>
63     change (GraphTransport.path A (rootPath T b)).trans (A f) =
64       GraphTransport.path A (rootPath T a) at hp
65     rw [hp.symm]
66     ext x
67     simp
68 
69 /-- Every supported path has the endpoint transport forced by the rooted tree. -/
70 theorem supported_transport {a b : Quiver.Symmetrify α} (p : Quiver.Path a b)
71     (hp : Supported T p) :
72     (GraphTransport.path A (rootPath T a)).trans (GraphTransport.path A p) =
73       GraphTransport.path A (rootPath T b) := by
74   induction p with
75   | nil => ext x; rfl
76   | cons p e ih =>
77     rcases hp with ⟨hp, he⟩
78     rw [GraphTransport.cons, ← LinearEquiv.trans_assoc, ih hp]
79     exact traversal_transport T A e he
80 
81 /-- Every based loop supported on the tree has identity transport. -/
82 theorem tree_loop_identity (p : GraphTree.Path r r) (hp : Supported T p) :
83     GraphTransport.path A p = LinearEquiv.refl K (V r) := by
84   have h := supported_transport T A p hp
85   simpa only [rootPath_root, GraphTransport.nil, LinearEquiv.refl_trans] using h
86 
87 end PaperXI.GraphTreePaths

Back to source controls