AlgebraActionModule.lean

1 import Mathlib.Algebra.Algebra.Hom
2 import Mathlib.Algebra.Algebra.Tower
3 import Mathlib.Algebra.Module.RingHom
4 import Mathlib.LinearAlgebra.BilinearMap
5 import Mathlib.RingTheory.SimpleModule.Basic
6 import Mathlib.Analysis.Complex.Basic
7 import Mathlib.Tactic
8 
9 /-! An algebra action gives an actual module on a separate copy of its vector space.
10 Submodules and intertwiners are identified with the corresponding complex-linear data. -/
11 set_option autoImplicit false
12 noncomputable section
13 namespace PaperXI.AlgebraActionModule
14 
15 variable {B W : Type*} [Ring B] [Algebra ℂ B] [AddCommGroup W] [Module ℂ W]
16 
17 /-- A copy of the original space carrying the module structure specified by the action. -/
18 @[nolint unusedArguments]
19 def Space (_ : B →ₐ[ℂ] Module.End ℂ W) := W
20   deriving AddCommGroup, Module ℂ
21 
22 variable (φ : B →ₐ[ℂ] Module.End ℂ W)
23 
24 /-- The canonical complex linear identification with the original vector space. -/
25 def equiv : Space φ ≃ₗ[ℂ] W := LinearEquiv.refl ℂ W
26 
27 instance instModule : Module B (Space φ) := Module.compHom W φ.toRingHom
28 
29 @[simp] theorem equiv_smul (b : B) (w : Space φ) :
30     equiv φ (b • w) = φ b (equiv φ w) := rfl
31 
32 @[simp] theorem equiv_symm_apply (w : W) : equiv φ ((equiv φ).symm w) = w := rfl
33 
34 instance instScalarTower : IsScalarTower ℂ B (Space φ) where
35   smul_assoc c b w := by
36     change φ (c • b) w = c • φ b w
37     rw [map_smul]
38     rfl
39 
40 /-- Stability under every actual algebra operator. -/
41 def Stable (S : Submodule ℂ W) : Prop :=
42   ∀ (b : B) (w : W), w ∈ S → φ b w ∈ S
43 
44 /-- Restrict an actual module subspace to the compatible complex scalar action. -/
45 def toSubspace (S : Submodule B (Space φ)) : Submodule ℂ W := S.restrictScalars ℂ
46 
47 @[simp] theorem mem_toSubspace (S : Submodule B (Space φ)) (w : W) :
48     w ∈ toSubspace φ S ↔ (equiv φ).symm w ∈ S := Iff.rfl
49 
50 theorem stable_toSubspace (S : Submodule B (Space φ)) : Stable φ (toSubspace φ S) := by
51   intro b w hw
52   exact S.smul_mem b hw
53 
54 /-- Every stable complex subspace is an actual algebra submodule. -/
55 def ofSubspace (S : Submodule ℂ W) (hS : Stable φ S) : Submodule B (Space φ) where
56   carrier := (S : Set W)
57   zero_mem' := S.zero_mem
58   add_mem' := S.add_mem
59   smul_mem' := hS
60 
61 @[simp] theorem mem_ofSubspace (S : Submodule ℂ W) (hS : Stable φ S) (w : Space φ) :
62     w ∈ ofSubspace φ S hS ↔ equiv φ w ∈ S := Iff.rfl
63 
64 @[simp] theorem toSubspace_ofSubspace (S : Submodule ℂ W) (hS : Stable φ S) :
65     toSubspace φ (ofSubspace φ S hS) = S := by ext w; rfl
66 
67 @[simp] theorem ofSubspace_toSubspace (S : Submodule B (Space φ)) :
68     ofSubspace φ (toSubspace φ S) (stable_toSubspace φ S) = S := by ext w; rfl
69 
70 /-- The complete ordered collection of module subspaces is exactly the stable complex subspaces. -/
71 def submoduleOrderIso : Submodule B (Space φ) ≃o {S : Submodule ℂ W // Stable φ S} where
72   toFun S := ⟨toSubspace φ S, stable_toSubspace φ S⟩
73   invFun S := ofSubspace φ S.1 S.2
74   left_inv := ofSubspace_toSubspace φ
75   right_inv S := by apply Subtype.ext; exact toSubspace_ofSubspace φ S.1 S.2
76   map_rel_iff' := Iff.rfl
77 
78 @[simp] theorem toSubspace_bot : toSubspace φ ⊥ = ⊥ := by ext w; rfl
79 @[simp] theorem toSubspace_top : toSubspace φ ⊤ = ⊤ := by ext w; rfl
80 
81 /-- Simplicity is exactly nontriviality and absence of proper stable complex subspaces. -/
82 theorem simple_iff : IsSimpleModule B (Space φ) ↔
83     Nontrivial W ∧ ∀ S : Submodule ℂ W, Stable φ S → S = ⊥ ∨ S = ⊤ := by
84   constructor
85   · intro h
86     let : IsSimpleModule B (Space φ) := h
87     refine ⟨IsSimpleModule.nontrivial B (Space φ), ?_⟩
88     intro S hS
89     have hh := eq_bot_or_eq_top (ofSubspace φ S hS)
90     rcases hh with hh | hh
91     · left
92       have := congrArg (toSubspace φ) hh
93       simpa using this
94     · right
95       have := congrArg (toSubspace φ) hh
96       simpa using this
97   · rintro ⟨hn, hs⟩
98     let : Nontrivial W := hn
99     let : Nontrivial (Space φ) := hn
100     refine { eq_bot_or_eq_top := ?_ }
101     intro S
102     rcases hs (toSubspace φ S) (stable_toSubspace φ S) with h | h
103     · left
104       ext w
105       have hh := congrArg (fun P : Submodule ℂ W => equiv φ w ∈ P) h
106       simpa using hh
107     · right
108       ext w
109       have hh := congrArg (fun P : Submodule ℂ W => equiv φ w ∈ P) h
110       simpa using hh
111 
112 section Intertwiners
113 
114 variable {V U : Type*} [AddCommGroup V] [Module ℂ V]
115 variable [AddCommGroup U] [Module ℂ U]
116 variable (χ : B →ₐ[ℂ] Module.End ℂ V)
117 
118 /-- The original complex-linear map commutes with the two actual algebra actions. -/
119 def Intertwines (f : W →ₗ[ℂ] V) : Prop :=
120   ∀ (b : B) (w : W), f (φ b w) = χ b (f w)
121 
122 /-- An action-preserving complex-linear map is an actual module-linear map. -/
123 def toModuleMap (f : W →ₗ[ℂ] V) (hf : Intertwines φ χ f) :
124     Space φ →ₗ[B] Space χ where
125   toFun := f
126   map_add' := f.map_add
127   map_smul' := hf
128 
129 /-- Restriction of an actual module map to the original complex vector spaces. -/
130 def toComplexMap (f : Space φ →ₗ[B] Space χ) : W →ₗ[ℂ] V :=
131   f.restrictScalars ℂ
132 
133 @[simp] theorem toModuleMap_apply (f : W →ₗ[ℂ] V) (hf : Intertwines φ χ f)
134     (w : Space φ) : equiv χ (toModuleMap φ χ f hf w) = f (equiv φ w) := rfl
135 
136 @[simp] theorem toComplexMap_apply (f : Space φ →ₗ[B] Space χ) (w : W) :
137     toComplexMap φ χ f w = equiv χ (f ((equiv φ).symm w)) := rfl
138 
139 theorem intertwines_toComplexMap (f : Space φ →ₗ[B] Space χ) :
140     Intertwines φ χ (toComplexMap φ χ f) := f.map_smul
141 
142 /-- All complex action intertwiners correspond bijectively to actual module maps. -/
143 def intertwinerEquiv : {f : W →ₗ[ℂ] V // Intertwines φ χ f} ≃
144     (Space φ →ₗ[B] Space χ) where
145   toFun f := toModuleMap φ χ f.1 f.2
146   invFun f := ⟨toComplexMap φ χ f, intertwines_toComplexMap φ χ f⟩
147   left_inv f := by apply Subtype.ext; ext w; rfl
148   right_inv f := by ext w; rfl
149 
150 @[simp] theorem toComplexMap_toModuleMap (f : W →ₗ[ℂ] V) (hf : Intertwines φ χ f) :
151     toComplexMap φ χ (toModuleMap φ χ f hf) = f := by ext w; rfl
152 
153 @[simp] theorem toModuleMap_toComplexMap (f : Space φ →ₗ[B] Space χ) :
154     toModuleMap φ χ (toComplexMap φ χ f) (intertwines_toComplexMap φ χ f) = f := by
155   ext w
156   rfl
157 
158 /-- The correspondence preserves identity maps. -/
159 @[simp] theorem toComplexMap_id :
160     toComplexMap φ φ (LinearMap.id : Space φ →ₗ[B] Space φ) = LinearMap.id := by
161   ext w
162   rfl
163 
164 /-- The correspondence preserves composition. -/
165 @[simp] theorem toComplexMap_comp (θ : B →ₐ[ℂ] Module.End ℂ U)
166     (g : Space χ →ₗ[B] Space θ) (f : Space φ →ₗ[B] Space χ) :
167     toComplexMap φ θ (g.comp f) =
168       (toComplexMap χ θ g).comp (toComplexMap φ χ f) := by
169   ext w
170   rfl
171 
172 /-- An invertible complex intertwiner gives an actual module equivalence. -/
173 def toModuleEquiv (e : W ≃ₗ[ℂ] V) (he : Intertwines φ χ e.toLinearMap) :
174     Space φ ≃ₗ[B] Space χ where
175   toFun := e
176   invFun := e.symm
177   left_inv := e.left_inv
178   right_inv := e.right_inv
179   map_add' := e.map_add
180   map_smul' := he
181 
182 /-- A module equivalence gives an invertible intertwiner on the original spaces. -/
183 def toComplexEquiv (e : Space φ ≃ₗ[B] Space χ) : W ≃ₗ[ℂ] V :=
184   e.restrictScalars ℂ
185 
186 @[simp] theorem toModuleEquiv_apply (e : W ≃ₗ[ℂ] V)
187     (he : Intertwines φ χ e.toLinearMap) (w : Space φ) :
188     equiv χ (toModuleEquiv φ χ e he w) = e (equiv φ w) := rfl
189 
190 @[simp] theorem toComplexEquiv_apply (e : Space φ ≃ₗ[B] Space χ) (w : W) :
191     toComplexEquiv φ χ e w = equiv χ (e ((equiv φ).symm w)) := rfl
192 
193 theorem intertwines_toComplexEquiv (e : Space φ ≃ₗ[B] Space χ) :
194     Intertwines φ χ (toComplexEquiv φ χ e).toLinearMap := e.map_smul
195 
196 /-- Invertible intertwiners correspond bijectively to actual module equivalences. -/
197 def equivalenceEquiv : {e : W ≃ₗ[ℂ] V // Intertwines φ χ e.toLinearMap} ≃
198     (Space φ ≃ₗ[B] Space χ) where
199   toFun e := toModuleEquiv φ χ e.1 e.2
200   invFun e := ⟨toComplexEquiv φ χ e, intertwines_toComplexEquiv φ χ e⟩
201   left_inv e := by apply Subtype.ext; ext w; rfl
202   right_inv e := by ext w; rfl
203 
204 @[simp] theorem toComplexEquiv_toModuleEquiv (e : W ≃ₗ[ℂ] V)
205     (he : Intertwines φ χ e.toLinearMap) :
206     toComplexEquiv φ χ (toModuleEquiv φ χ e he) = e := by ext w; rfl
207 
208 @[simp] theorem toModuleEquiv_toComplexEquiv (e : Space φ ≃ₗ[B] Space χ) :
209     toModuleEquiv φ χ (toComplexEquiv φ χ e) (intertwines_toComplexEquiv φ χ e) = e := by
210   ext w
211   rfl
212 
213 @[simp] theorem toComplexEquiv_refl :
214     toComplexEquiv φ φ (LinearEquiv.refl B (Space φ)) = LinearEquiv.refl ℂ W := by
215   ext w
216   rfl
217 
218 @[simp] theorem toComplexEquiv_trans (θ : B →ₐ[ℂ] Module.End ℂ U)
219     (e : Space φ ≃ₗ[B] Space χ) (f : Space χ ≃ₗ[B] Space θ) :
220     toComplexEquiv φ θ (e.trans f) =
221       (toComplexEquiv φ χ e).trans (toComplexEquiv χ θ f) := by
222   ext w
223   rfl
224 
225 end Intertwiners
226 
227 section ExistingModule
228 
229 variable [Module B W] [IsScalarTower ℂ B W]
230 
231 /-- Starting with an actual compatible module and forming its action recovers that module. -/
232 def ofModuleEquiv : Space (Algebra.lsmul ℂ ℂ W (A := B)) ≃ₗ[B] W where
233   toFun := equiv (Algebra.lsmul ℂ ℂ W (A := B))
234   invFun := (equiv (Algebra.lsmul ℂ ℂ W (A := B))).symm
235   left_inv := (equiv (Algebra.lsmul ℂ ℂ W (A := B))).left_inv
236   right_inv := (equiv (Algebra.lsmul ℂ ℂ W (A := B))).right_inv
237   map_add' := (equiv (Algebra.lsmul ℂ ℂ W (A := B))).map_add
238   map_smul' := fun _ _ => rfl
239 
240 @[simp] theorem ofModuleEquiv_apply (w : Space (Algebra.lsmul ℂ ℂ W (A := B))) :
241     ofModuleEquiv (B := B) (W := W) w = equiv (Algebra.lsmul ℂ ℂ W (A := B)) w := rfl
242 
243 /-- The canonical module round trip preserves simplicity. -/
244 theorem ofModule_simple_iff :
245     IsSimpleModule B (Space (Algebra.lsmul ℂ ℂ W (A := B))) ↔ IsSimpleModule B W :=
246   (ofModuleEquiv (B := B) (W := W)).isSimpleModule_iff
247 
248 end ExistingModule
249 
250 end PaperXI.AlgebraActionModule

Back to source controls