RepresentationGraph.lean

1 import PaperXI.GraphGauge
2 import Mathlib.RepresentationTheory.Basic
3 
4 /-! Gluing within actual representation intertwiners. Edge covariance ensures
5 that tree transport of a root bridge remains a local bridge at every vertex. -/
6 set_option autoImplicit false
7 set_option backward.isDefEq.respectTransparency false
8 noncomputable section
9 namespace PaperXI.RepresentationGraph
10 open Quiver GraphTransport GraphGauge
11 attribute [local instance] GraphTransport.symmetrifyAdd GraphTransport.symmetrifyModule
12 
13 variable {K α G : Type*} [Field K] [Quiver α] [Monoid G]
14 variable {V W : α → Type*}
15   [∀ v, AddCommGroup (V v)] [∀ v, Module K (V v)]
16   [∀ v, AddCommGroup (W v)] [∀ v, Module K (W v)]
17 
18 /-- Every edge transport intertwines the declared local representations. -/
19 def EdgeEquivariant
20     (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v))
21     (ρ : ∀ v, Representation K G (V v)) : Prop :=
22   ∀ {u v : α} (e : u ⟶ v) (g : G) (x : V u), A e (ρ u g x) = ρ v g (A e x)
23 
24 /-- A family of maps lies in the actual local representation bridge spaces. -/
25 def Intertwines (ρ : ∀ v, Representation K G (V v))
26     (τ : ∀ v, Representation K G (W v)) (F : ∀ v, V v ≃ₗ[K] W v) : Prop :=
27   ∀ v g x, F v (ρ v g x) = τ v g (F v x)
28 
29 variable (A : ∀ {u v : α}, (u ⟶ v) → (V u ≃ₗ[K] V v))
30     (B : ∀ {u v : α}, (u ⟶ v) → (W u ≃ₗ[K] W v))
31     (ρ : ∀ v, Representation K G (V v)) (τ : ∀ v, Representation K G (W v))
32 
33 /-- Actual covariance along the entire path follows from its original edge equations. -/
34 theorem path_equivariant (hA : EdgeEquivariant A ρ)
35     {u v : α} (p : Walk u v) (g : G) (x : V u) :
36     path A p (ρ u g x) = ρ v g (path A p x) := by
37   exact (gauge_path A A (fun v => ρ v g) (fun e x => (hA e g x).symm) p x).symm
38 
39 variable {r : α}
40 
41 /-- Root-path transport preserves a genuine representation bridge. -/
42 theorem rootGauge_intertwines (hA : EdgeEquivariant A ρ) (hB : EdgeEquivariant B τ)
43     (U : V r ≃ₗ[K] W r) (hU : ∀ g x, U (ρ r g x) = τ r g (U x))
44     (P : ∀ v, Walk r v) : Intertwines ρ τ (rootGauge A B U P) := by
45   intro v g x
46   have hInv := path_equivariant A ρ hA (P v).reverse g x
47   simp only [GraphTransport.reverse] at hInv
48   change path B (P v) (U ((path A (P v)).symm (ρ v g x))) =
49     τ v g (path B (P v) (U ((path A (P v)).symm x)))
50   rw [hInv, hU]
51   exact path_equivariant B τ hB (P v) g _
52 
53 /-- The matrix chord criterion stays exact within local intertwiner spaces when
54 edge transports themselves satisfy actual representation covariance. -/
55 theorem based_iff_chords (hA : EdgeEquivariant A ρ) (hB : EdgeEquivariant B τ)
56     (U : V r ≃ₗ[K] W r) (hU : ∀ g x, U (ρ r g x) = τ r g (U x))
57     (T : GraphTree.Rooted α r) :
58     (∃ F : ∀ v, V v ≃ₗ[K] W v,
59       F r = U ∧ EdgeCompatible A B F ∧ Intertwines ρ τ F) ↔
60       ∀ e : GraphTree.Chord T, CycleCompatible A B U (GraphTree.rootPath T) e.val := by
61   constructor
62   · rintro ⟨F, hroot, hF, _⟩
63     exact (GraphGauge.based_iff_chords A B U T).mp ⟨F, hroot, hF⟩
64   · intro h
65     exact ⟨rootGauge A B U (GraphTree.rootPath T),
66       rootGauge_root A B U _ (GraphTree.rootPath_root T),
67       (rootGauge_compatible_iff_chords A B U T).mpr h,
68       rootGauge_intertwines A B ρ τ hA hB U hU _⟩
69 
70 /-- The corrected graph source endpoint constructs the actual tree from connectedness. -/
71 theorem connected_iff_chords (hA : EdgeEquivariant A ρ) (hB : EdgeEquivariant B τ)
72     (U : V r ≃ₗ[K] W r) (hU : ∀ g x, U (ρ r g x) = τ r g (U x))
73     (hc : GraphTree.Connected (α := α)) :
74     (∃ F : ∀ v, V v ≃ₗ[K] W v,
75       F r = U ∧ EdgeCompatible A B F ∧ Intertwines ρ τ F) ↔
76       ∀ e : GraphTree.Chord (GraphTree.ofConnected r hc),
77         CycleCompatible A B U (GraphTree.rootPath (GraphTree.ofConnected r hc)) e.val :=
78   based_iff_chords A B ρ τ hA hB U hU (GraphTree.ofConnected r hc)
79 
80 /-- The same constrained gluing criterion is equivalent to all actual based-loop tests. -/
81 theorem based_iff_loops (hA : EdgeEquivariant A ρ) (hB : EdgeEquivariant B τ)
82     (U : V r ≃ₗ[K] W r) (hU : ∀ g x, U (ρ r g x) = τ r g (U x))
83     (T : GraphTree.Rooted α r) :
84     (∃ F : ∀ v, V v ≃ₗ[K] W v,
85       F r = U ∧ EdgeCompatible A B F ∧ Intertwines ρ τ F) ↔
86       LoopCompatible A B U :=
87   (based_iff_chords A B ρ τ hA hB U hU T).trans (GraphGauge.chords_iff_loops A B U T)
88 
89 /-- The root bridge condition and actual holonomy conjugacy classify unbased
90 compatible representation bridges. -/
91 theorem unbased_iff_conjugates (hA : EdgeEquivariant A ρ) (hB : EdgeEquivariant B τ)
92     (r : α) (hc : GraphTree.Connected (α := α)) :
93     (∃ F : ∀ v, V v ≃ₗ[K] W v, EdgeCompatible A B F ∧ Intertwines ρ τ F) ↔
94       ∃ U : V r ≃ₗ[K] W r,
95         (∀ g x, U (ρ r g x) = τ r g (U x)) ∧ GraphLoop.Conjugates A B U := by
96   constructor
97   · rintro ⟨F, hF, hI⟩
98     exact ⟨F r, hI r, (GraphLoop.conjugates_iff_paths A B (F r)).mpr
99       (GraphGauge.edgeCompatible_loops A B F hF)⟩
100   · rintro ⟨U, hU, hC⟩
101     let P := GraphTree.rootPath (GraphTree.ofConnected r hc)
102     exact ⟨rootGauge A B U P,
103       rootGauge_compatible_of_loops A B U P ((GraphLoop.conjugates_iff_paths A B U).mp hC),
104       rootGauge_intertwines A B ρ τ hA hB U hU P⟩
105 
106 end PaperXI.RepresentationGraph

Back to source controls