GrammarAlgebra.lean

1 import Mathlib.Algebra.FreeAlgebra
2 import Mathlib.Algebra.RingQuot
3 import Mathlib.LinearAlgebra.Pi
4 import KomorebiVerification.ExactCoordinates
5 
6 /-!
7 The finite-vertex quiver algebra is constructed by generators and relations,
8 not assumed as an operator algebra.  Vertices and arrows are independent
9 generators.  Quotient relations impose the vertex idempotents, their sum, and
10 the source/target corners of every arrow, together with the declared relations.
11 -/
12 
13 set_option autoImplicit false
14 set_option maxHeartbeats 2000000
15 set_option linter.unnecessarySimpa false
16 set_option linter.unusedVariables false
17 
18 noncomputable section
19 
20 namespace Komorebi.PaperIRelease.GrammarAlgebra
21 
22 open scoped BigOperators
23 open Foundation
24 
25 universe u
26 
27 variable (K V E : Type u) [Field K] [Fintype V]
28 
29 abbrev Free := FreeAlgebra K (V ⊕ E)
30 
31 def vertexWord (v : V) : Free K V E := FreeAlgebra.ι K (.inl v)
32 def arrowWord (a : E) : Free K V E := FreeAlgebra.ι K (.inr a)
33 
34 /-- A finite-vertex typed grammar with arbitrary arrow set and declared equations. -/
35 structure Grammar where
36   source : E → V
37   target : E → V
38   equations : Free K V E → Free K V E → Prop
39 
40 variable {K V E}
41 
42 inductive Relation (G : Grammar K V E) : Free K V E → Free K V E → Prop where
43   | vertex_idempotent (v : V) :
44       Relation G (vertexWord K V E v * vertexWord K V E v) (vertexWord K V E v)
45   | vertex_orthogonal (v w : V) (h : v ≠ w) :
46       Relation G (vertexWord K V E v * vertexWord K V E w) 0
47   | vertex_complete : Relation G (∑ v, vertexWord K V E v) 1
48   | arrow_corner (a : E) :
49       Relation G (vertexWord K V E (G.target a) * arrowWord K V E a *
50         vertexWord K V E (G.source a)) (arrowWord K V E a)
51   | declared {x y : Free K V E} : G.equations x y → Relation G x y
52 
53 abbrev Algebra (G : Grammar K V E) := RingQuot (Relation G)
54 
55 def quotient (G : Grammar K V E) : Free K V E →ₐ[K] Algebra G :=
56   RingQuot.mkAlgHom K (Relation G)
57 
58 def vertex (G : Grammar K V E) (v : V) : Algebra G := quotient G (vertexWord K V E v)
59 def arrow (G : Grammar K V E) (a : E) : Algebra G := quotient G (arrowWord K V E a)
60 
61 theorem vertex_idempotent (G : Grammar K V E) (v : V) : vertex G v * vertex G v = vertex G v := by
62   simpa only [vertex, quotient, map_mul] using
63     RingQuot.mkAlgHom_rel K (Relation.vertex_idempotent (G := G) v)
64 
65 theorem vertex_orthogonal (G : Grammar K V E) {v w : V} (h : v ≠ w) :
66     vertex G v * vertex G w = 0 := by
67   simpa only [vertex, quotient, map_mul, map_zero] using
68     RingQuot.mkAlgHom_rel K (Relation.vertex_orthogonal (G := G) v w h)
69 
70 theorem vertex_complete (G : Grammar K V E) : ∑ v, vertex G v = 1 := by
71   simpa only [vertex, quotient, map_sum, map_one] using
72     RingQuot.mkAlgHom_rel K (Relation.vertex_complete (G := G))
73 
74 theorem arrow_corner (G : Grammar K V E) (a : E) :
75     vertex G (G.target a) * arrow G a * vertex G (G.source a) = arrow G a := by
76   simpa only [vertex, arrow, quotient, map_mul] using
77     RingQuot.mkAlgHom_rel K (Relation.arrow_corner (G := G) a)
78 
79 theorem declared_relation (G : Grammar K V E) {x y : Free K V E}
80     (h : G.equations x y) : quotient G x = quotient G y :=
81   RingQuot.mkAlgHom_rel K (Relation.declared h)
82 
83 variable (G : Grammar K V E) (M : Type u) [AddCommGroup M] [Module K M]
84 
85 /-- A collapsed realization specifies actual vertex and arrow operators. -/
86 structure CollapsedRealization where
87   vertex : V → Module.End K M
88   arrow : E → Module.End K M
89   vertex_idempotent : ∀ v, vertex v * vertex v = vertex v
90   vertex_orthogonal : ∀ v w, v ≠ w → vertex v * vertex w = 0
91   vertex_complete : ∑ v, vertex v = 1
92   arrow_corner : ∀ a, vertex (G.target a) * arrow a * vertex (G.source a) = arrow a
93   declared : ∀ x y, G.equations x y →
94     FreeAlgebra.lift K (Sum.elim vertex arrow) x =
95       FreeAlgebra.lift K (Sum.elim vertex arrow) y
96 
97 variable {G M}
98 
99 @[ext] theorem CollapsedRealization.ext (X Y : CollapsedRealization G M)
100     (hv : X.vertex = Y.vertex) (ha : X.arrow = Y.arrow) : X = Y := by
101   cases X
102   cases Y
103   cases hv
104   cases ha
105   rfl
106 
107 def CollapsedRealization.freeAction (X : CollapsedRealization G M) :
108     Free K V E →ₐ[K] Module.End K M :=
109   FreeAlgebra.lift K (Sum.elim X.vertex X.arrow)
110 
111 theorem CollapsedRealization.respects (X : CollapsedRealization G M)
112     {x y : Free K V E} (h : Relation G x y) : X.freeAction x = X.freeAction y := by
113   cases h with
114   | vertex_idempotent v =>
115       simpa [freeAction, vertexWord] using X.vertex_idempotent v
116   | vertex_orthogonal v w h =>
117       simpa [freeAction, vertexWord] using X.vertex_orthogonal v w h
118   | vertex_complete =>
119       simpa [freeAction, vertexWord] using X.vertex_complete
120   | arrow_corner a =>
121       simpa [freeAction, vertexWord, arrowWord] using X.arrow_corner a
122   | declared h => exact X.declared _ _ h
123 
124 /-- The quotient action is constructed by the universal property. -/
125 def CollapsedRealization.action (X : CollapsedRealization G M) :
126     Algebra G →ₐ[K] Module.End K M :=
127   RingQuot.liftAlgHom K ⟨X.freeAction, fun _ _ h => X.respects h⟩
128 
129 @[simp] theorem CollapsedRealization.action_quotient
130     (X : CollapsedRealization G M) (x : Free K V E) :
131     X.action (quotient G x) = X.freeAction x :=
132   RingQuot.liftAlgHom_mkAlgHom_apply K X.freeAction (fun _ _ h => X.respects h) x
133 
134 @[simp] theorem CollapsedRealization.action_vertex
135     (X : CollapsedRealization G M) (v : V) :
136     X.action (GrammarAlgebra.vertex G v) = X.vertex v := by
137   simp [GrammarAlgebra.vertex, freeAction, vertexWord]
138 
139 @[simp] theorem CollapsedRealization.action_arrow
140     (X : CollapsedRealization G M) (a : E) :
141     X.action (GrammarAlgebra.arrow G a) = X.arrow a := by
142   simp [GrammarAlgebra.arrow, freeAction, arrowWord]
143 
144 /-- Recover the declared generators from any unital algebra action. -/
145 def ofAction (ρ : Algebra G →ₐ[K] Module.End K M) : CollapsedRealization G M where
146   vertex v := ρ (vertex G v)
147   arrow a := ρ (arrow G a)
148   vertex_idempotent v := by rw [← map_mul, vertex_idempotent]
149   vertex_orthogonal v w h := by rw [← map_mul, vertex_orthogonal G h, map_zero]
150   vertex_complete := by rw [← map_sum, vertex_complete, map_one]
151   arrow_corner a := by rw [← map_mul, ← map_mul, arrow_corner]
152   declared x y h := by
153     have heq : FreeAlgebra.lift K
154         (Sum.elim (fun v => ρ (vertex G v)) (fun a => ρ (arrow G a))) =
155         ρ.comp (quotient G) := by
156       apply FreeAlgebra.hom_ext
157       funext s
158       cases s <;> simp [vertex, arrow, vertexWord, arrowWord]
159     rw [heq]
160     exact congrArg ρ (declared_relation G h)
161 
162 theorem ofAction_action (X : CollapsedRealization G M) : ofAction X.action = X := by
163   apply CollapsedRealization.ext
164   · funext v
165     exact X.action_vertex v
166   · funext a
167     exact X.action_arrow a
168 
169 theorem action_ofAction (ρ : Algebra G →ₐ[K] Module.End K M) : (ofAction ρ).action = ρ := by
170   apply RingQuot.ringQuot_ext'
171   apply FreeAlgebra.hom_ext
172   funext s
173   cases s with
174   | inl v => exact (ofAction ρ).action_vertex v
175   | inr a => exact (ofAction ρ).action_arrow a
176 
177 /-- The full universal correspondence, with both inverse laws proved. -/
178 def collapsedActionEquiv : CollapsedRealization G M ≃ (Algebra G →ₐ[K] Module.End K M) where
179   toFun := CollapsedRealization.action
180   invFun := ofAction
181   left_inv := ofAction_action
182   right_inv := action_ofAction
183 
184 def CollapsedRealization.projectors (X : CollapsedRealization G M) :
185     LinearProjectorFamily K M V where
186   proj := X.vertex
187   idempotent v x := LinearMap.congr_fun (X.vertex_idempotent v) x
188   orthogonal h x := LinearMap.congr_fun (X.vertex_orthogonal _ _ h) x
189   complete x := by
190     have h := LinearMap.congr_fun X.vertex_complete x
191     simpa using h
192 
193 /-- The vertex spaces are actual ranges, and their direct-sum coordinates are proved exact. -/
194 def CollapsedRealization.coordinates (X : CollapsedRealization G M) :
195     M ≃ₗ[K] ((v : V) → LinearMap.range (X.vertex v)) :=
196   X.projectors.exactPacketCoordinates
197 
198 theorem CollapsedRealization.arrow_left (X : CollapsedRealization G M) (a : E) :
199     X.vertex (G.target a) * X.arrow a = X.arrow a := by
200   calc
201     X.vertex (G.target a) * X.arrow a =
202         X.vertex (G.target a) * (X.vertex (G.target a) * X.arrow a * X.vertex (G.source a)) :=
203       congrArg (X.vertex (G.target a) * ·) (X.arrow_corner a).symm
204     _ = X.vertex (G.target a) * X.arrow a * X.vertex (G.source a) := by
205       simp only [← mul_assoc, X.vertex_idempotent]
206     _ = X.arrow a := X.arrow_corner a
207 
208 /-- Every arrow restricts to precisely its declared source and target vertex spaces. -/
209 def CollapsedRealization.typedArrow (X : CollapsedRealization G M) (a : E) :
210     LinearMap.range (X.vertex (G.source a)) →ₗ[K]
211       LinearMap.range (X.vertex (G.target a)) where
212   toFun x := ⟨X.arrow a x, ⟨X.arrow a x, LinearMap.congr_fun (X.arrow_left a) x⟩⟩
213   map_add' x y := by apply Subtype.ext; exact (X.arrow a).map_add x y
214   map_smul' c x := by apply Subtype.ext; exact (X.arrow a).map_smul c x
215 
216 end Komorebi.PaperIRelease.GrammarAlgebra

Back to source controls