GrammarTyped.lean

1 import PaperIRelease.GrammarAlgebra
2 
3 set_option autoImplicit false
4 set_option maxHeartbeats 2000000
5 set_option linter.unnecessarySimpa false
6 set_option linter.unusedVariables false
7 set_option linter.unusedSimpArgs false
8 
9 noncomputable section
10 
11 namespace Komorebi.PaperIRelease.GrammarAlgebra
12 
13 open scoped BigOperators
14 universe u
15 variable {K V E : Type u} [Field K] [Fintype V]
16 
17 attribute [local instance] Classical.propDecidable
18 
19 variable (G : Grammar K V E)
20 
21 /-- Typed vector spaces and arrow maps, before imposing grammar equations. -/
22 structure TypedData where
23   space : V → Type u
24   [addCommGroup : ∀ v, AddCommGroup (space v)]
25   [module : ∀ v, Module K (space v)]
26   arrow : ∀ a : E, space (G.source a) →ₗ[K] space (G.target a)
27 
28 attribute [instance] TypedData.addCommGroup TypedData.module
29 
30 variable {G}
31 
32 abbrev TypedData.total (X : TypedData G) := (v : V) → X.space v
33 
34 def TypedData.vertexOperator (X : TypedData G) (v : V) : Module.End K X.total :=
35   (LinearMap.single K X.space v).comp (LinearMap.proj v)
36 
37 def TypedData.arrowOperator (X : TypedData G) (a : E) : Module.End K X.total :=
38   (LinearMap.single K X.space (G.target a)).comp
39     ((X.arrow a).comp (LinearMap.proj (G.source a)))
40 
41 def TypedData.freeAction (X : TypedData G) : Free K V E →ₐ[K] Module.End K X.total :=
42   FreeAlgebra.lift K (Sum.elim X.vertexOperator X.arrowOperator)
43 
44 theorem TypedData.vertex_idempotent (X : TypedData G) (v : V) :
45     X.vertexOperator v * X.vertexOperator v = X.vertexOperator v := by
46   ext x w
47   simp [vertexOperator, LinearMap.single_apply]
48 
49 theorem TypedData.vertex_orthogonal (X : TypedData G) {v w : V} (h : v ≠ w) :
50     X.vertexOperator v * X.vertexOperator w = 0 := by
51   ext x z
52   simp [vertexOperator, LinearMap.single_apply, Pi.single_eq_of_ne h]
53 
54 theorem TypedData.vertex_complete (X : TypedData G) : ∑ v, X.vertexOperator v = 1 := by
55   apply LinearMap.ext
56   intro x
57   change (∑ v, X.vertexOperator v) x = x
58   simp only [LinearMap.sum_apply, vertexOperator, LinearMap.comp_apply, LinearMap.proj_apply]
59   exact LinearMap.sum_single_apply X.space x
60 
61 theorem TypedData.arrow_corner (X : TypedData G) (a : E) :
62     X.vertexOperator (G.target a) * X.arrowOperator a * X.vertexOperator (G.source a) =
63       X.arrowOperator a := by
64   ext x v
65   simp [vertexOperator, arrowOperator, LinearMap.single_apply]
66 
67 /-- A typed realization is precisely a family whose declared relations vanish. -/
68 structure TypedRealization extends TypedData G where
69   declared : ∀ x y, G.equations x y → toTypedData.freeAction x = toTypedData.freeAction y
70 
71 abbrev TypedRealization.collapse (X : TypedRealization (G := G)) :
72     CollapsedRealization G X.total where
73   vertex := X.vertexOperator
74   arrow := X.arrowOperator
75   vertex_idempotent := X.vertex_idempotent
76   vertex_orthogonal _ _ h := X.vertex_orthogonal h
77   vertex_complete := X.vertex_complete
78   arrow_corner := X.arrow_corner
79   declared := X.declared
80 
81 variable {M : Type u} [AddCommGroup M] [Module K M]
82 
83 /-- Split an arbitrary collapsed action using the actual vertex-idempotent ranges. -/
84 abbrev CollapsedRealization.splitData (X : CollapsedRealization G M) : TypedData G where
85   space v := LinearMap.range (X.vertex v)
86   arrow := X.typedArrow
87 
88 @[simp] theorem CollapsedRealization.coordinates_apply (X : CollapsedRealization G M)
89     (x : M) (v : V) : (X.coordinates x v : M) = X.vertex v x := rfl
90 
91 theorem CollapsedRealization.vertex_on_range (X : CollapsedRealization G M)
92     (v : V) (x : LinearMap.range (X.vertex v)) : X.vertex v x = (x : M) := by
93   rcases x.property with ⟨y, hy⟩
94   rw [← hy]
95   exact LinearMap.congr_fun (X.vertex_idempotent v) y
96 
97 theorem CollapsedRealization.arrow_right (X : CollapsedRealization G M) (a : E) :
98     X.arrow a * X.vertex (G.source a) = X.arrow a := by
99   calc
100     X.arrow a * X.vertex (G.source a) =
101         (X.vertex (G.target a) * X.arrow a * X.vertex (G.source a)) * X.vertex (G.source a) :=
102       congrArg (· * X.vertex (G.source a)) (X.arrow_corner a).symm
103     _ = X.vertex (G.target a) * X.arrow a * X.vertex (G.source a) := by
104       simp only [mul_assoc, X.vertex_idempotent]
105     _ = X.arrow a := X.arrow_corner a
106 
107 /-- Analysis respects each declared vertex generator. -/
108 theorem CollapsedRealization.coordinates_vertex (X : CollapsedRealization G M)
109     (v : V) (x : M) :
110     X.coordinates (X.vertex v x) = X.splitData.vertexOperator v (X.coordinates x) := by
111   ext w
112   change X.vertex w (X.vertex v x) =
113     ((Pi.single v (X.coordinates x v) : (z : V) → LinearMap.range (X.vertex z)) w : M)
114   by_cases h : w = v
115   · subst w
116     simp only [Pi.single_eq_same, coordinates_apply]
117     exact LinearMap.congr_fun (X.vertex_idempotent v) x
118   · have hvw : X.vertex w (X.vertex v x) = 0 :=
119       LinearMap.congr_fun (X.vertex_orthogonal w v h) x
120     rw [hvw]
121     simp [Pi.single_eq_of_ne h]
122 
123 /-- Analysis respects each declared arrow generator. -/
124 theorem CollapsedRealization.coordinates_arrow (X : CollapsedRealization G M)
125     (a : E) (x : M) :
126     X.coordinates (X.arrow a x) = X.splitData.arrowOperator a (X.coordinates x) := by
127   ext v
128   change X.vertex v (X.arrow a x) =
129     ((Pi.single (G.target a) (X.typedArrow a (X.coordinates x (G.source a))) :
130       (z : V) → LinearMap.range (X.vertex z)) v : M)
131   by_cases h : v = G.target a
132   · subst v
133     simp only [Pi.single_eq_same]
134     have hl := LinearMap.congr_fun (X.arrow_left a) x
135     have hr := LinearMap.congr_fun (X.arrow_right a) x
136     exact hl.trans hr.symm
137   · have hz : X.vertex v * X.arrow a = 0 := by
138       calc
139         X.vertex v * X.arrow a = X.vertex v * (X.vertex (G.target a) * X.arrow a) :=
140           congrArg (X.vertex v * ·) (X.arrow_left a).symm
141         _ = 0 := by rw [← mul_assoc, X.vertex_orthogonal v (G.target a) h, zero_mul]
142     have hz' := LinearMap.congr_fun hz x
143     simpa [Pi.single_eq_of_ne h] using hz'
144 
145 /-- Generator intertwining extends to every free-algebra expression. -/
146 theorem CollapsedRealization.coordinates_freeAction (X : CollapsedRealization G M)
147     (a : Free K V E) (x : M) :
148     X.coordinates (X.freeAction a x) = X.splitData.freeAction a (X.coordinates x) := by
149   induction a using FreeAlgebra.induction generalizing x with
150   | grade0 c => simp
151   | grade1 s =>
152       cases s with
153       | inl v => simpa [freeAction, TypedData.freeAction] using X.coordinates_vertex v x
154       | inr a => simpa [freeAction, TypedData.freeAction] using X.coordinates_arrow a x
155   | mul a b ha hb =>
156       simp only [map_mul, Module.End.mul_apply]
157       rw [ha, hb]
158   | add a b ha hb =>
159       simp only [map_add, LinearMap.add_apply]
160       rw [ha, hb]
161 
162 /-- The split arrow family satisfies every original grammar relation. -/
163 abbrev CollapsedRealization.split (X : CollapsedRealization G M) : TypedRealization (G := G) where
164   toTypedData := X.splitData
165   declared a b h := by
166     apply LinearMap.ext
167     intro x
168     obtain ⟨y, rfl⟩ := X.coordinates.surjective x
169     rw [← X.coordinates_freeAction a, ← X.coordinates_freeAction b]
170     exact congrArg (fun f : Module.End K M => X.coordinates (f y)) (X.declared a b h)
171 
172 end Komorebi.PaperIRelease.GrammarAlgebra

Back to source controls