GrammarEquivalence.lean

1 import PaperIRelease.GrammarTyped
2 import PaperIRelease.GrammarModules
3 
4 set_option autoImplicit false
5 set_option maxHeartbeats 4000000
6 set_option linter.unusedVariables false
7 set_option linter.unnecessarySimpa false
8 set_option linter.unusedSimpArgs false
9 set_option linter.unusedSectionVars false
10 
11 noncomputable section
12 
13 namespace Komorebi.PaperIRelease.GrammarAlgebra
14 
15 open CategoryTheory GrammarModules
16 open scoped BigOperators
17 
18 universe u
19 variable {K V E : Type u} [Field K] [Fintype V]
20 variable {G : Grammar K V E}
21 
22 attribute [local instance] Classical.propDecidable
23 
24 /-- The manuscript's vertexwise maps, satisfying each arrow square. -/
25 structure TypedHom (X Y : TypedRealization (G := G)) where
26   map : ∀ v, X.space v →ₗ[K] Y.space v
27   natural : ∀ a x, map (G.target a) (X.arrow a x) = Y.arrow a (map (G.source a) x)
28 
29 @[ext] theorem TypedHom.ext {X Y : TypedRealization (G := G)}
30     (f g : TypedHom X Y) (h : f.map = g.map) : f = g := by
31   cases f
32   cases g
33   cases h
34   rfl
35 
36 instance typedCategory : Category (TypedRealization (G := G)) where
37   Hom := TypedHom
38   id X := ⟨fun _ => LinearMap.id, fun _ _ => rfl⟩
39   comp f g := ⟨fun v => (g.map v).comp (f.map v), by
40     intro a x
41     simp only [LinearMap.comp_apply]
42     rw [f.natural, g.natural]⟩
43   id_comp f := by apply TypedHom.ext; rfl
44   comp_id f := by apply TypedHom.ext; rfl
45   assoc f g h := by apply TypedHom.ext; rfl
46 
47 def TypedHom.total {X Y : TypedRealization (G := G)} (f : TypedHom X Y) :
48     X.total →ₗ[K] Y.total :=
49   LinearMap.pi (fun v => (f.map v).comp (LinearMap.proj v))
50 
51 @[simp] theorem TypedHom.total_apply {X Y : TypedRealization (G := G)}
52     (f : TypedHom X Y) (x : X.total) (v : V) : f.total x v = f.map v (x v) := rfl
53 
54 theorem TypedHom.total_single {X Y : TypedRealization (G := G)}
55     (f : TypedHom X Y) (v : V) (x : X.space v) :
56     f.total (Pi.single v x) = Pi.single v (f.map v x) := by
57   ext w
58   by_cases h : w = v
59   · subst w
60     simp
61   · simp [Pi.single_eq_of_ne h]
62 
63 theorem TypedHom.vertex_natural {X Y : TypedRealization (G := G)}
64     (f : TypedHom X Y) (v : V) (x : X.total) :
65     f.total (X.vertexOperator v x) = Y.vertexOperator v (f.total x) := by
66   exact f.total_single v (x v)
67 
68 theorem TypedHom.arrow_natural {X Y : TypedRealization (G := G)}
69     (f : TypedHom X Y) (a : E) (x : X.total) :
70     f.total (X.arrowOperator a x) = Y.arrowOperator a (f.total x) := by
71   change f.total (Pi.single (G.target a) (X.arrow a (x (G.source a)))) =
72     Pi.single (G.target a) (Y.arrow a (f.map (G.source a) (x (G.source a))))
73   rw [f.total_single, f.natural]
74 
75 theorem TypedHom.freeAction_natural {X Y : TypedRealization (G := G)}
76     (f : TypedHom X Y) (a : Free K V E) (x : X.total) :
77     f.total (X.freeAction a x) = Y.freeAction a (f.total x) := by
78   induction a using FreeAlgebra.induction generalizing x with
79   | grade0 c => simp
80   | grade1 s =>
81       cases s with
82       | inl v => simpa [TypedData.freeAction] using f.vertex_natural v x
83       | inr a => simpa [TypedData.freeAction] using f.arrow_natural a x
84   | mul a b ha hb => simp only [map_mul, Module.End.mul_apply]; rw [ha, hb]
85   | add a b ha hb => simp only [map_add, LinearMap.add_apply]; rw [ha, hb]
86 
87 theorem TypedHom.action_natural {X Y : TypedRealization (G := G)}
88     (f : TypedHom X Y) (a : Algebra G) (x : X.total) :
89     f.total (X.collapse.action a x) = Y.collapse.action a (f.total x) := by
90   obtain ⟨a, rfl⟩ := RingQuot.mkAlgHom_surjective K (Relation G) a
91   change f.total (X.collapse.action (quotient G a) x) =
92     Y.collapse.action (quotient G a) (f.total x)
93   rw [CollapsedRealization.action_quotient, CollapsedRealization.action_quotient]
94   exact f.freeAction_natural a x
95 
96 /-- Collapse both the typed objects and their vertexwise morphisms. -/
97 abbrev collapseFunctor : TypedRealization (G := G) ⥤ ActionObject K (Algebra G) where
98   obj X := ⟨ModuleCat.of K X.total, X.collapse.action⟩
99   map f := ⟨f.total, f.action_natural⟩
100   map_id X := by apply ActionHom.ext; rfl
101   map_comp f g := by apply ActionHom.ext; rfl
102 
103 instance collapse_faithful : (collapseFunctor (G := G)).Faithful where
104   map_injective {X Y} f g h := by
105     apply TypedHom.ext
106     funext v
107     apply LinearMap.ext
108     intro x
109     have hh := congrArg (fun q : ActionHom (collapseFunctor.obj X) (collapseFunctor.obj Y) =>
110       q.linearMap (Pi.single v x) v) h
111     change f.total (Pi.single v x) v = g.total (Pi.single v x) v at hh
112     simpa only [TypedHom.total_apply, Pi.single_eq_same] using hh
113 
114 theorem actionHom_vertex {X Y : TypedRealization (G := G)}
115     (f : ActionHom (collapseFunctor.obj X) (collapseFunctor.obj Y)) (v : V) (x : X.total) :
116     f.linearMap (X.vertexOperator v x) = Y.vertexOperator v (f.linearMap x) := by
117   have h := f.commute (vertex G v) x
118   change f.linearMap (X.collapse.action (vertex G v) x) =
119     Y.collapse.action (vertex G v) (f.linearMap x) at h
120   simpa only [CollapsedRealization.action_vertex] using h
121 
122 theorem actionHom_arrow {X Y : TypedRealization (G := G)}
123     (f : ActionHom (collapseFunctor.obj X) (collapseFunctor.obj Y)) (a : E) (x : X.total) :
124     f.linearMap (X.arrowOperator a x) = Y.arrowOperator a (f.linearMap x) := by
125   have h := f.commute (arrow G a) x
126   change f.linearMap (X.collapse.action (arrow G a) x) =
127     Y.collapse.action (arrow G a) (f.linearMap x) at h
128   simpa only [CollapsedRealization.action_arrow] using h
129 
130 /-- Recover each vertex map from an arbitrary algebra intertwiner. -/
131 def liftActionHom {X Y : TypedRealization (G := G)}
132     (f : ActionHom (collapseFunctor.obj X) (collapseFunctor.obj Y)) : TypedHom X Y where
133   map v := (LinearMap.proj v).comp (f.linearMap.comp (LinearMap.single K X.space v))
134   natural a x := by
135     have h := congrFun (actionHom_arrow f a (Pi.single (G.source a) x)) (G.target a)
136     change f.linearMap (Pi.single (G.target a) (X.arrow a x)) (G.target a) =
137       Y.arrow a (f.linearMap (Pi.single (G.source a) x) (G.source a))
138     simpa only [TypedData.arrowOperator, LinearMap.comp_apply, LinearMap.single_apply,
139       LinearMap.proj_apply, Pi.single_eq_same] using h
140 
141 theorem total_liftActionHom {X Y : TypedRealization (G := G)}
142     (f : ActionHom (collapseFunctor.obj X) (collapseFunctor.obj Y)) :
143     (liftActionHom f).total = f.linearMap := by
144   apply LinearMap.ext
145   intro x
146   funext v
147   have h := congrFun (actionHom_vertex f v x) v
148   simpa [TypedData.vertexOperator, liftActionHom] using h
149 
150 instance collapse_full : (collapseFunctor (G := G)).Full where
151   map_surjective f := ⟨liftActionHom f, ActionHom.ext _ _ (total_liftActionHom f)⟩
152 
153 theorem CollapsedRealization.coordinates_action
154     {M : Type u} [AddCommGroup M] [Module K M] (X : CollapsedRealization G M)
155     (a : Algebra G) (x : M) :
156     X.coordinates (X.action a x) = X.split.collapse.action a (X.coordinates x) := by
157   obtain ⟨a, rfl⟩ := RingQuot.mkAlgHom_surjective K (Relation G) a
158   change X.coordinates (X.action (quotient G a) x) =
159     X.split.collapse.action (quotient G a) (X.coordinates x)
160   rw [CollapsedRealization.action_quotient, CollapsedRealization.action_quotient]
161   exact X.coordinates_freeAction a x
162 
163 /-- The comparison isomorphism is the actual finite sum of vertex-range vectors. -/
164 def splitActionIso (X : ActionObject K (Algebra G)) :
165     collapseFunctor.obj ((ofAction X.action).split) ≅ X where
166   hom :=
167     { linearMap := (ofAction X.action).coordinates.symm.toLinearMap
168       commute a x := by
169         apply (ofAction X.action).coordinates.injective
170         change (ofAction X.action).coordinates
171           ((ofAction X.action).coordinates.symm ((ofAction X.action).split.collapse.action a x)) =
172           (ofAction X.action).coordinates (X.action a ((ofAction X.action).coordinates.symm x))
173         rw [LinearEquiv.apply_symm_apply]
174         have h := (ofAction X.action).coordinates_action a
175           ((ofAction X.action).coordinates.symm x)
176         rw [action_ofAction, LinearEquiv.apply_symm_apply] at h
177         exact h.symm }
178   inv :=
179     { linearMap := (ofAction X.action).coordinates.toLinearMap
180       commute a x := by
181         have h := (ofAction X.action).coordinates_action a x
182         rw [action_ofAction] at h
183         exact h }
184   hom_inv_id := by
185     apply ActionHom.ext
186     apply LinearMap.ext
187     intro x
188     exact (ofAction X.action).coordinates.apply_symm_apply x
189   inv_hom_id := by
190     apply ActionHom.ext
191     apply LinearMap.ext
192     intro x
193     exact (ofAction X.action).coordinates.symm_apply_apply x
194 
195 instance collapse_essSurj : (collapseFunctor (G := G)).EssSurj where
196   mem_essImage X := ⟨(ofAction X.action).split, ⟨splitActionIso X⟩⟩
197 
198 instance collapse_isEquivalence : (collapseFunctor (G := G)).IsEquivalence where
199 
200 /-- The typed realization category and the constructed quotient-action category are equivalent. -/
201 def typedActionEquivalence : TypedRealization (G := G) ≌ ActionObject K (Algebra G) :=
202   collapseFunctor.asEquivalence
203 
204 /-- PSC-I-T-TYPED-MODULE-EQUIVALENCE: typed arrow realizations versus unital modules. -/
205 def typedModuleEquivalence : TypedRealization (G := G) ≌ ModuleCat.{u} (Algebra G) :=
206   typedActionEquivalence.trans actionModuleEquivalence
207 
208 end Komorebi.PaperIRelease.GrammarAlgebra

Back to source controls