IsotypicEvaluation.lean

1 import Mathlib.RingTheory.SimpleModule.Isotypic
2 import Mathlib.RepresentationTheory.AlgebraRepresentation.Basic
3 import Mathlib.LinearAlgebra.TensorProduct.Basic
4 import Mathlib.LinearAlgebra.Complex.FiniteDimensional
5 import Mathlib.Analysis.Complex.Polynomial.Basic
6 
7 set_option autoImplicit false
8 noncomputable section
9 
10 namespace PaperXI.IsotypicEvaluation
11 
12 open scoped TensorProduct
13 
14 variable {R W X : Type*} [Ring R] [Algebra ℂ R]
15   [AddCommGroup W] [Module ℂ W] [Module R W] [IsScalarTower ℂ R W]
16   [AddCommGroup X] [Module ℂ X] [Module R X] [IsScalarTower ℂ R X]
17 
18 /-- Canonical evaluation on the actual space of module maps. -/
19 def map : W ⊗[ℂ] (W →ₗ[R] X) →ₗ[ℂ] X :=
20   TensorProduct.lift
21     { toFun := fun w =>
22         { toFun := fun f => f w
23           map_add' := fun _ _ => rfl
24           map_smul' := fun _ _ => rfl }
25       map_add' := by intro w v; ext f; exact f.map_add w v
26       map_smul' := by intro c w; ext f; exact f.map_smul_of_tower c w }
27 
28 @[simp] theorem map_tmul (w : W) (f : W →ₗ[R] X) : map (w ⊗ₜ[ℂ] f) = f w := rfl
29 
30 /-- A chosen finite decomposition into copies yields the inverse of canonical evaluation. -/
31 theorem bijective_of_copies [IsSimpleModule R W] [FiniteDimensional ℂ W]
32     {n : ℕ} (e : X ≃ₗ[R] (Fin n → W)) : Function.Bijective (map (R := R) (W := W) (X := X)) := by
33   classical
34   let inc (i : Fin n) : W →ₗ[R] X := e.symm.toLinearMap.comp (LinearMap.single R (fun _ : Fin n => W) i)
35   let inv : X →ₗ[ℂ] W ⊗[ℂ] (W →ₗ[R] X) :=
36     ∑ i : Fin n, ((TensorProduct.mk ℂ W (W →ₗ[R] X)).flip (inc i)).comp
37       (((LinearMap.proj i).comp e.toLinearMap).restrictScalars ℂ)
38   have hinv (x : X) : inv x = ∑ i : Fin n, (e x i) ⊗ₜ[ℂ] inc i := by
39     simp [inv]
40   have right : Function.RightInverse inv map := by
41     intro x
42     rw [hinv, map_sum]
43     simp only [map_tmul, inc, LinearMap.comp_apply, LinearEquiv.coe_coe]
44     rw [← map_sum]
45     simp only [LinearMap.single_apply, LinearMap.sum_single_apply, e.symm_apply_apply]
46   have left : Function.LeftInverse inv map := by
47     intro t
48     induction t using TensorProduct.induction_on with
49     | zero => simp
50     | add u v hu hv => simp [hu, hv]
51     | tmul w f =>
52       have hscalar (i : Fin n) : ∃ c : ℂ,
53           (LinearMap.proj i).comp (e.toLinearMap.comp f) =
54             algebraMap ℂ (Module.End R W) c := by
55         obtain ⟨c, hc⟩ :=
56           (IsSimpleModule.algebraMap_end_bijective_of_isAlgClosed (A := R) (V := W) ℂ).2
57             ((LinearMap.proj i).comp (e.toLinearMap.comp f))
58         exact ⟨c, hc.symm⟩
59       choose c hc using hscalar
60       have hcoord (i : Fin n) (v : W) : e (f v) i = c i • v := by
61         exact congrArg (fun q : Module.End R W => q v) (hc i)
62       have esmul (c : ℂ) (x : X) : e (c • x) = c • e x :=
63         (e.restrictScalars ℂ).map_smul c x
64       have hf : f = ∑ i : Fin n, c i • inc i := by
65         ext v
66         apply e.injective
67         simp only [LinearMap.sum_apply, LinearMap.smul_apply, map_sum,
68           esmul, inc, LinearMap.comp_apply, LinearEquiv.coe_coe,
69           e.apply_symm_apply]
70         have hx := LinearMap.sum_single_apply (fun _ : Fin n => W) (fun i : Fin n => e (f v) i)
71         simp_rw [hcoord] at hx
72         rw [show e (f v) = (fun i => c i • v) from funext (fun i => hcoord i v)]
73         simpa only [LinearMap.single_apply, Pi.single_smul] using hx.symm
74       rw [map_tmul, hinv]
75       simp_rw [hcoord, TensorProduct.smul_tmul]
76       rw [← TensorProduct.tmul_sum, ← hf]
77   exact ⟨left.injective, right.surjective⟩
78 
79 /-- Genuine isotypy implies bijectivity of canonical evaluation. -/
80 theorem bijective [IsSimpleModule R W] [FiniteDimensional ℂ W]
81     [IsSemisimpleModule R X] [Module.Finite R X]
82     (h : IsIsotypicOfType R X W) : Function.Bijective (map (R := R) (W := W) (X := X)) := by
83   obtain ⟨n, ⟨e⟩⟩ := h.linearEquiv_fun
84   exact bijective_of_copies e
85 
86 /-- The isotypic evaluation equivalence, with its canonical underlying map. -/
87 def equiv [IsSimpleModule R W] [FiniteDimensional ℂ W]
88     [IsSemisimpleModule R X] [Module.Finite R X]
89     (h : IsIsotypicOfType R X W) : W ⊗[ℂ] (W →ₗ[R] X) ≃ₗ[ℂ] X :=
90   LinearEquiv.ofBijective map (bijective h)
91 
92 @[simp] theorem equiv_tmul [IsSimpleModule R W] [FiniteDimensional ℂ W]
93     [IsSemisimpleModule R X] [Module.Finite R X]
94     (h : IsIsotypicOfType R X W) (w : W) (f : W →ₗ[R] X) :
95     equiv h (w ⊗ₜ[ℂ] f) = f w := rfl
96 
97 end PaperXI.IsotypicEvaluation

Back to source controls