ProjectiveHolonomy.lean

1 import PaperXI.ScalarHolonomy
2 import PaperXI.GraphTransport
3 import PaperXI.GraphLoopRepresentation
4 
5 /-! Vertex rescaling of actual graph transport and scalar ratio characters. -/
6 set_option autoImplicit false
7 noncomputable section
8 
9 namespace PaperXI.ProjectiveHolonomy
10 
11 open Quiver
12 open PaperXI.ScalarHolonomy
13 
14 attribute [local instance] GraphTransport.symmetrifyAdd GraphTransport.symmetrifyModule
15 
16 variable {K α : Type*} [Field K] [Quiver α]
17 variable {V : α → Type*} [∀ u, AddCommGroup (V u)] [∀ u, Module K (V u)]
18 
19 /-- Change the representative at each vertex by its chosen nonzero scalar. -/
20 def rescale (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v)) (a : α → Kˣ)
21     {u v : α} (e : u ⟶ v) : V u ≃ₗ[K] V v :=
22   ((scalarHom (a u)).symm.trans (A e)).trans (scalarHom (a v))
23 
24 theorem rescale_apply (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v))
25     (a : α → Kˣ) {u v : α} (e : u ⟶ v) (x : V u) :
26     rescale A a e x = ((a v * (a u)⁻¹ : Kˣ) : K) • A e x := by
27   change (a v : K) • A e ((((a u)⁻¹ : Kˣ) : K) • x) = _
28   rw [map_smul, smul_smul, Units.val_mul]
29 
30 /-- The rescaled edge family is related to the original by actual vertex gauges. -/
31 theorem rescale_gauge (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v))
32     (a : α → Kˣ) {u v : α} (e : u ⟶ v) (x : V u) :
33     scalarHom (a v) (A e x) = rescale A a e (scalarHom (a u) x) := by
34   change scalarHom (a v) (A e x) =
35     scalarHom (a v) (A e ((scalarHom (a u)).symm (scalarHom (a u) x)))
36   rw [LinearEquiv.symm_apply_apply]
37 
38 /-- Every path retains only the two endpoint rescalings. -/
39 theorem rescale_path (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v))
40     (a : α → Kˣ) {u v : Symmetrify α} (p : Path u v) :
41     GraphTransport.path (rescale A a) p =
42       ((scalarHom (a u)).symm.trans (GraphTransport.path A p)).trans
43         (scalarHom (a v)) := by
44   ext x
45   have h := GraphTransport.gauge_path A (rescale A a)
46     (fun v => (scalarHom (a v)).toLinearMap)
47     (fun e y => rescale_gauge A a e y) p ((scalarHom (a u)).symm x)
48   simpa using h.symm
49 
50 theorem rescale_path_apply (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v))
51     (a : α → Kˣ) {u v : Symmetrify α} (p : Path u v) (x : V u) :
52     GraphTransport.path (rescale A a) p x =
53       ((a v * (a u)⁻¹ : Kˣ) : K) • GraphTransport.path A p x := by
54   rw [rescale_path]
55   change (a v : K) • GraphTransport.path A p ((((a u)⁻¹ : Kˣ) : K) • x) = _
56   rw [map_smul, smul_smul, Units.val_mul]
57 
58 /-- Vertex rescaling leaves the actual closed-path operator unchanged, at every rank. -/
59 theorem rescale_loop (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v))
60     (a : α → Kˣ) {r : Symmetrify α} (p : Path r r) :
61     GraphTransport.path (rescale A a) p = GraphTransport.path A p := by
62   ext x
63   simp [rescale_path_apply]
64 
65 /-- Cancellation on represented loops gives equality of the full reduced-loop representations. -/
66 theorem rescale_holonomy (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v))
67     (a : α → Kˣ) (r : α) :
68     GraphLoop.holonomy (rescale A a) r = GraphLoop.holonomy A r := by
69   apply MonoidHom.ext
70   intro g
71   obtain ⟨p, rfl⟩ := GraphLoop.loopClass_surjective r g
72   rw [GraphLoop.holonomy_loopClass, GraphLoop.holonomy_loopClass]
73   exact rescale_loop A a p
74 
75 theorem rescale_isScalar (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v))
76     (a : α → Kˣ) (r : α) (hA : IsScalar (GraphLoop.holonomy A r)) :
77     IsScalar (GraphLoop.holonomy (rescale A a) r) := by
78   rwa [rescale_holonomy]
79 
80 /-- Scalarity on ordinary closed paths is exactly scalarity on their reduced quotient. -/
81 theorem isScalar_iff_paths (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v)) (r : α) :
82     IsScalar (GraphLoop.holonomy A r) ↔
83       ∀ p : @Quiver.Path (Quiver.Symmetrify α) _ r r,
84         ∃ c : Kˣ, GraphTransport.path A p = scalarHom c := by
85   constructor
86   · intro h p
87     simpa only [GraphLoop.holonomy_loopClass] using h (GraphLoop.loopClass p)
88   · intro h g
89     obtain ⟨p, rfl⟩ := GraphLoop.loopClass_surjective r g
90     simpa only [GraphLoop.holonomy_loopClass] using h p
91 
92 /-- The unique scalar character extracted from actual loop transport. -/
93 def loopCharacter (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v))
94     (r : α) [Nontrivial (V r)] (hA : IsScalar (GraphLoop.holonomy A r)) :
95     GraphLoop.Loop r →* Kˣ := character (GraphLoop.holonomy A r) hA
96 
97 @[simp] theorem loopCharacter_spec
98     (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v))
99     (r : α) [Nontrivial (V r)] (hA : IsScalar (GraphLoop.holonomy A r))
100     (g : GraphLoop.Loop r) :
101     scalarHom (loopCharacter A r hA g) = GraphLoop.holonomy A r g :=
102   character_spec _ _ _
103 
104 /-- Vertex rescaling leaves the extracted scalar character unchanged. -/
105 theorem rescale_character (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v))
106     (a : α → Kˣ) (r : α) [Nontrivial (V r)]
107     (hA : IsScalar (GraphLoop.holonomy A r)) :
108     loopCharacter (rescale A a) r (rescale_isScalar A a r hA) =
109       loopCharacter A r hA := by
110   apply (character_unique (GraphLoop.holonomy (rescale A a) r)
111     (rescale_isScalar A a r hA) (loopCharacter A r hA) ?_).symm
112   intro g
113   rw [loopCharacter_spec, rescale_holonomy]
114 
115 /-- The ratio of two scalar loop characters factors through the actual abelianization. -/
116 def ratioH1 (r : α) (χ ψ : GraphLoop.Loop r →* Kˣ) : GraphLoop.H1 r →* Kˣ :=
117   GraphLoop.factorCharacter r Kˣ (ratio χ ψ)
118 
119 @[simp] theorem ratioH1_class (r : α) (χ ψ : GraphLoop.Loop r →* Kˣ)
120     (g : GraphLoop.Loop r) :
121     ratioH1 r χ ψ (GraphLoop.homologyClass r g) = ψ g * (χ g)⁻¹ := rfl
122 
123 theorem ratioH1_unique (r : α) (χ ψ : GraphLoop.Loop r →* Kˣ)
124     (δ : GraphLoop.H1 r →* Kˣ)
125     (hδ : ∀ g, δ (GraphLoop.homologyClass r g) = ψ g * (χ g)⁻¹) :
126     δ = ratioH1 r χ ψ := GraphLoop.factorCharacter_unique (ratio χ ψ) δ hδ
127 
128 /-- The first-homology character is trivial exactly when the scalar holonomies agree. -/
129 theorem ratioH1_eq_one_iff (r : α) (χ ψ : GraphLoop.Loop r →* Kˣ) :
130     ratioH1 r χ ψ = 1 ↔ χ = ψ := by
131   constructor
132   · intro h
133     apply (ratio_eq_one_iff χ ψ).mp
134     apply MonoidHom.ext
135     intro g
136     exact DFunLike.congr_fun h (GraphLoop.homologyClass r g)
137   · intro h
138     apply (GraphLoop.factorCharacter r Kˣ).symm.injective
139     change ratio χ ψ = 1
140     exact (ratio_eq_one_iff χ ψ).mpr h
141 
142 variable {W : α → Type*} [∀ u, AddCommGroup (W u)] [∀ u, Module K (W u)]
143 
144 /-- The first-homology character obtained from the two actual scalar transport systems. -/
145 def transportRatioH1
146     (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v))
147     (B : ∀ {u v : α}, (u ⟶ v) → (W u ≃ₗ[K] W v))
148     (r : α) [Nontrivial (V r)] [Nontrivial (W r)]
149     (hA : IsScalar (GraphLoop.holonomy A r)) (hB : IsScalar (GraphLoop.holonomy B r)) :
150     GraphLoop.H1 r →* Kˣ := ratioH1 r (loopCharacter A r hA) (loopCharacter B r hB)
151 
152 @[simp] theorem transportRatioH1_class
153     (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v))
154     (B : ∀ {u v : α}, (u ⟶ v) → (W u ≃ₗ[K] W v))
155     (r : α) [Nontrivial (V r)] [Nontrivial (W r)]
156     (hA : IsScalar (GraphLoop.holonomy A r)) (hB : IsScalar (GraphLoop.holonomy B r))
157     (g : GraphLoop.Loop r) :
158     transportRatioH1 A B r hA hB (GraphLoop.homologyClass r g) =
159       loopCharacter B r hB g * (loopCharacter A r hA g)⁻¹ := rfl
160 
161 /-- Both vertex rescalings cancel before the ratio is factored through first homology. -/
162 theorem transportRatioH1_rescale
163     (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v))
164     (B : ∀ {u v : α}, (u ⟶ v) → (W u ≃ₗ[K] W v))
165     (a b : α → Kˣ) (r : α) [Nontrivial (V r)] [Nontrivial (W r)]
166     (hA : IsScalar (GraphLoop.holonomy A r)) (hB : IsScalar (GraphLoop.holonomy B r)) :
167     transportRatioH1 (rescale A a) (rescale B b) r
168       (rescale_isScalar A a r hA) (rescale_isScalar B b r hB) =
169         transportRatioH1 A B r hA hB := by
170   unfold transportRatioH1
171   rw [rescale_character, rescale_character]
172 
173 end PaperXI.ProjectiveHolonomy

Back to source controls