GrammarModules.lean

1 import Mathlib.Algebra.Category.ModuleCat.Basic
2 import Mathlib.Algebra.Algebra.Tower
3 import Mathlib.CategoryTheory.Equivalence
4 import PaperIRelease.GrammarAlgebra
5 
6 set_option autoImplicit false
7 set_option maxHeartbeats 2000000
8 set_option linter.unusedVariables false
9 set_option linter.unnecessarySimpa false
10 
11 noncomputable section
12 
13 namespace Komorebi.PaperIRelease.GrammarModules
14 
15 open CategoryTheory
16 open scoped ModuleCat.Algebra
17 
18 universe u
19 variable (K A : Type u) [Field K] [Ring A] [Algebra K A]
20 
21 /-- A unital K-algebra action on a K-vector space. -/
22 structure ActionObject where
23   space : ModuleCat.{u} K
24   action : A →ₐ[K] Module.End K space
25 
26 variable {K A}
27 
28 /-- Algebra-action morphisms are the actual K-linear intertwiners. -/
29 structure ActionHom (X Y : ActionObject K A) where
30   linearMap : X.space →ₗ[K] Y.space
31   commute : ∀ a x, linearMap (X.action a x) = Y.action a (linearMap x)
32 
33 @[ext] theorem ActionHom.ext {X Y : ActionObject K A}
34     (f g : ActionHom X Y) (h : f.linearMap = g.linearMap) : f = g := by
35   cases f
36   cases g
37   cases h
38   rfl
39 
40 instance actionCategory : Category (ActionObject K A) where
41   Hom := ActionHom
42   id X := ⟨LinearMap.id, fun _ _ => rfl⟩
43   comp {X Y Z} f g := ⟨g.linearMap.comp f.linearMap, by
44     intro a x
45     change g.linearMap (f.linearMap (X.action a x)) = Z.action a (g.linearMap (f.linearMap x))
46     rw [f.commute, g.commute]⟩
47   id_comp f := by apply ActionHom.ext; rfl
48   comp_id f := by apply ActionHom.ext; rfl
49   assoc f g h := by apply ActionHom.ext; rfl
50 
51 /-- Every algebra action induces a genuine unital left module. -/
52 abbrev ActionObject.module (X : ActionObject K A) : Module A X.space :=
53   Module.compHom X.space X.action.toRingHom
54 
55 abbrev ActionObject.moduleObject (X : ActionObject K A) : ModuleCat.{u} A := by
56   letI := X.module
57   exact ModuleCat.of A X.space
58 
59 theorem ActionObject.module_smul (X : ActionObject K A) (a : A) (x : X.space) :
60     @SMul.smul A X.space X.module.toSMul a x = X.action a x := rfl
61 
62 /-- The algebra-action category maps to the ordinary category of all unital A-modules. -/
63 def toModules : ActionObject K A ⥤ ModuleCat.{u} A where
64   obj := ActionObject.moduleObject
65   map {X Y} f := by
66     letI := X.module
67     letI := Y.module
68     exact ModuleCat.ofHom
69       { toFun := f.linearMap
70         map_add' := f.linearMap.map_add
71         map_smul' := fun a x => f.commute a x }
72   map_id X := by ext x; rfl
73   map_comp f g := by ext x; rfl
74 
75 instance toModules_faithful : (toModules (K := K) (A := A)).Faithful where
76   map_injective {X Y} f g h := by
77     apply ActionHom.ext
78     ext x
79     exact congrArg (fun f : X.moduleObject ⟶ Y.moduleObject => f x) h
80 
81 theorem ActionObject.coefficient_action (X : ActionObject K A) (c : K) (x : X.space) :
82     X.action (algebraMap K A c) x = c • x := by
83   rw [X.action.commutes]
84   rfl
85 
86 /-- An A-linear map is K-linear because scalar coefficients act through algebraMap. -/
87 def fromModuleHom {X Y : ActionObject K A} (f : X.moduleObject ⟶ Y.moduleObject) :
88     ActionHom X Y where
89   linearMap :=
90     { toFun := f
91       map_add' := f.hom.map_add
92       map_smul' := fun c x => by
93         change f (c • x) = c • f x
94         rw [← X.coefficient_action c x, ← Y.coefficient_action c (f x)]
95         exact f.hom.map_smul (algebraMap K A c) x }
96   commute a x := f.hom.map_smul a x
97 
98 instance toModules_full : (toModules (K := K) (A := A)).Full where
99   map_surjective f := ⟨fromModuleHom f, by ext x; rfl⟩
100 
101 /-- The inverse construction starts from any unital A-module, with its canonical K-action. -/
102 def ofModule (M : ModuleCat.{u} A) : ActionObject K A where
103   space := ModuleCat.of K M
104   action := Algebra.lsmul K K M
105 
106 def ofModuleIso (M : ModuleCat.{u} A) : (ofModule (K := K) M).moduleObject ≅ M := by
107   letI := (ofModule (K := K) M).module
108   exact LinearEquiv.toModuleIso
109     { toFun := fun x => x
110       invFun := fun x => x
111       left_inv := fun _ => rfl
112       right_inv := fun _ => rfl
113       map_add' := fun _ _ => rfl
114       map_smul' := fun _ _ => rfl }
115 
116 instance toModules_essSurj : (toModules (K := K) (A := A)).EssSurj where
117   mem_essImage M := ⟨ofModule M, ⟨ofModuleIso M⟩⟩
118 
119 instance toModules_isEquivalence : (toModules (K := K) (A := A)).IsEquivalence where
120 
121 /-- The complete category equivalence with ordinary unital left modules. -/
122 def actionModuleEquivalence : ActionObject K A ≌ ModuleCat.{u} A :=
123   (toModules (K := K) (A := A)).asEquivalence
124 
125 end Komorebi.PaperIRelease.GrammarModules

Back to source controls