GraphChordCharacters.lean

1 import PaperXI.GraphTree
2 import PaperXI.GraphLoopRepresentation
3 import PaperXI.ScalarHolonomy
4 
5 /-!
6 # Independent scalar tests on fundamental graph cycles
7 
8 Every assignment of unit scalars to the chords of the constructed rooted tree
9 is realized by actual one-dimensional edge transport: tree edges carry one and
10 each chord carries its prescribed scalar. Thus the scalar cycle tests can vary
11 independently. The same realization gives characters on the actual reduced loop
12 group and its abelianization.
13 -/
14 
15 set_option autoImplicit false
16 set_option backward.isDefEq.respectTransparency false
17 noncomputable section
18 
19 namespace PaperXI.GraphChordCharacters
20 
21 variable {K α : Type*} [Field K] [Quiver α] {r : α}
22 
23 /-- Prescribed chord weights, extended by one on the selected tree. -/
24 def weight (T : GraphTree.Rooted α r) (t : GraphTree.Chord T → Kˣ)
25     (e : GraphTree.Edge α) : Kˣ := by
26   classical
27   exact if h : e ∈ GraphTree.treeEdges T then 1 else t ⟨e, h⟩
28 
29 @[simp] theorem weight_tree (T : GraphTree.Rooted α r) (t : GraphTree.Chord T → Kˣ)
30     (e : GraphTree.Edge α) (h : e ∈ GraphTree.treeEdges T) : weight T t e = 1 := by
31   simp [weight, h]
32 
33 @[simp] theorem weight_chord (T : GraphTree.Rooted α r) (t : GraphTree.Chord T → Kˣ)
34     (e : GraphTree.Chord T) : weight T t e.val = t e := by
35   rw [weight, dite_eq_right e.property]
36   rfl
37 
38 /-- An actual one-dimensional linear transport system realizing these edge weights. -/
39 def edgeSystem (T : GraphTree.Rooted α r) (t : GraphTree.Chord T → Kˣ)
40     {u v : α} (e : u ⟶ v) : K ≃ₗ[K] K :=
41   ScalarHolonomy.scalarHom (weight T t ⟨u, v, e⟩)
42 
43 @[simp] theorem edgeSystem_chord (T : GraphTree.Rooted α r)
44     (t : GraphTree.Chord T → Kˣ) (e : GraphTree.Chord T) :
45     edgeSystem T t e.val.2.2 = ScalarHolonomy.scalarHom (t e) := by
46   simp [edgeSystem]
47 
48 /-- Both directions of every selected tree edge have identity transport. -/
49 theorem traversal_tree (T : GraphTree.Rooted α r) (t : GraphTree.Chord T → Kˣ)
50     {u v : α} (e : GraphTree.Traversal u v)
51     (h : GraphTree.underlying e ∈ GraphTree.treeEdges T) :
52     GraphTransport.edge (α := α) (V := fun _ => K) (edgeSystem T t) e = LinearEquiv.refl K K := by
53   cases e using Sum.casesOn with
54   | inl e =>
55     change ScalarHolonomy.scalarHom (weight T t ⟨u, v, e⟩) = _
56     change (⟨u, v, e⟩ : GraphTree.Edge α) ∈ GraphTree.treeEdges T at h
57     rw [weight_tree T t _ h, map_one]
58     rfl
59   | inr e =>
60     change (ScalarHolonomy.scalarHom (weight T t ⟨v, u, e⟩)).symm = _
61     change (⟨v, u, e⟩ : GraphTree.Edge α) ∈ GraphTree.treeEdges T at h
62     rw [weight_tree T t _ h, map_one]
63     rfl
64 
65 /-- The recursively constructed root paths use only identity edge transports. -/
66 @[simp] theorem rootPath_transport (T : GraphTree.Rooted α r)
67     (t : GraphTree.Chord T → Kˣ) (v : α) :
68     GraphTransport.path (α := α) (V := fun _ => K) (edgeSystem T t) (GraphTree.rootPath T v) =
69       LinearEquiv.refl K K := by
70   apply GraphTree.rooted_induction T (fun v =>
71     GraphTransport.path (α := α) (V := fun _ => K) (edgeSystem T t) (GraphTree.rootPath T v) =
72       LinearEquiv.refl K K)
73   · rw [GraphTree.rootPath_root]
74     rfl
75   · intro a ha
76     rw [← GraphTree.rootPath_parent, GraphTransport.cons, ha,
77       traversal_tree T t (T.parentEdge a) (GraphTree.mem_treeEdges T a)]
78     rfl
79 
80 /-- The based fundamental cycle associated with one actual chord. -/
81 def chordLoop (T : GraphTree.Rooted α r) (e : GraphTree.Chord T) :
82     GraphTree.Path r r :=
83   ((GraphTree.rootPath T e.val.1).cons (Sum.inl e.val.2.2)).comp
84     (GraphTree.rootPath T e.val.2.1).reverse
85 
86 /-- Each fundamental cycle recovers exactly its freely assigned scalar. -/
87 @[simp] theorem chordLoop_transport (T : GraphTree.Rooted α r)
88     (t : GraphTree.Chord T → Kˣ) (e : GraphTree.Chord T) :
89     GraphTransport.path (α := α) (V := fun _ => K) (edgeSystem T t) (chordLoop (α := α) T e) =
90       ScalarHolonomy.scalarHom (t e) := by
91   ext x
92   simp [chordLoop]
93 
94 @[simp] theorem chordLoop_holonomy (T : GraphTree.Rooted α r)
95     (t : GraphTree.Chord T → Kˣ) (e : GraphTree.Chord T) :
96     GraphLoop.holonomy (α := α) (V := fun _ => K) (edgeSystem T t) r (GraphLoop.loopClass (chordLoop (α := α) T e)) =
97       ScalarHolonomy.scalarHom (t e) := by
98   rw [GraphLoop.holonomy_loopClass, chordLoop_transport]
99 
100 /-- Every invertible linear map on the scalar field is multiplication by a unit. -/
101 theorem field_equiv_scalar (L : K ≃ₗ[K] K) :
102     ∃ c : Kˣ, L = ScalarHolonomy.scalarHom c := by
103   let c : Kˣ := Units.mk0 (L 1) (L.map_ne_zero_iff.mpr one_ne_zero)
104   refine ⟨c, ?_⟩
105   ext x
106   have h : L x = x * L 1 := by
107     simpa only [smul_eq_mul, mul_one] using L.map_smul x (1 : K)
108   exact h.trans (mul_comm x (L 1))
109 
110 /-- The one-dimensional loop representation is scalar on every reduced loop. -/
111 theorem holonomy_isScalar (T : GraphTree.Rooted α r) (t : GraphTree.Chord T → Kˣ) :
112     ScalarHolonomy.IsScalar (GraphLoop.holonomy (α := α) (V := fun _ => K) (edgeSystem T t) r) := by
113   intro g
114   exact field_equiv_scalar _
115 
116 /-- The actual scalar character realizing a prescribed tuple of chord tests. -/
117 def character (T : GraphTree.Rooted α r) (t : GraphTree.Chord T → Kˣ) :
118     GraphLoop.Loop r →* Kˣ :=
119   ScalarHolonomy.character (GraphLoop.holonomy (α := α) (V := fun _ => K) (edgeSystem T t) r) (holonomy_isScalar T t)
120 
121 @[simp] theorem character_chord (T : GraphTree.Rooted α r)
122     (t : GraphTree.Chord T → Kˣ) (e : GraphTree.Chord T) :
123     character T t (GraphLoop.loopClass (chordLoop (α := α) T e)) = t e := by
124   apply ScalarHolonomy.scalarHom_injective (V := K)
125   rw [character, ScalarHolonomy.character_spec, chordLoop_holonomy]
126 
127 /-- Arbitrary scalar tests on the actual fundamental cycles are simultaneously realizable. -/
128 theorem character_tests_surjective (T : GraphTree.Rooted α r) :
129     Function.Surjective (fun χ : GraphLoop.Loop r →* Kˣ =>
130       fun e : GraphTree.Chord T => χ (GraphLoop.loopClass (chordLoop (α := α) T e))) := by
131   intro t
132   exact ⟨character T t, funext (character_chord T t)⟩
133 
134 /-- Their independence persists for characters of the actual loop abelianization. -/
135 theorem homology_tests_surjective (T : GraphTree.Rooted α r) :
136     Function.Surjective (fun χ : GraphLoop.H1 r →* Kˣ =>
137       fun e : GraphTree.Chord T =>
138         χ (GraphLoop.homologyClass r (GraphLoop.loopClass (chordLoop (α := α) T e)))) := by
139   intro t
140   refine ⟨GraphLoop.factorCharacter r Kˣ (character T t), ?_⟩
141   funext e
142   exact character_chord T t e
143 
144 end PaperXI.GraphChordCharacters

Back to source controls