SimpleModuleSeparation.lean

1 import Mathlib.RingTheory.SimpleModule.Basic
2 import Mathlib.LinearAlgebra.Trace
3 
4 /-! Finite families of pairwise nonisomorphic simple modules can be separated
5 by actual elements of their acting ring. No finiteness of that ring is assumed. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperX.SimpleModuleSeparation
9 open scoped BigOperators
10 variable {A : Type*} [Ring A] {I : Type*} [Fintype I] [DecidableEq I]
11 variable {W : I → Type*} [∀ i, AddCommGroup (W i)] [∀ i, Module A (W i)]
12 variable [∀ i, IsSimpleModule A (W i)]
13 variable (hne : ∀ i j, Nonempty (W i ≃ₗ[A] W j) → i = j)
14 
15 omit [Fintype I] in
16 include hne in
17 theorem off_diagonal_zero (f : Module.End A (∀ i, W i)) (i j : I) (hij : i ≠ j) :
18     (LinearMap.proj i).comp (f.comp (LinearMap.single A W j)) = 0 := by
19   by_contra h
20   have hb := LinearMap.bijective_of_ne_zero h
21   exact hij (hne j i ⟨LinearEquiv.ofBijective _ hb⟩).symm
22 
23 include hne in
24 theorem coordinate_of_end (f : Module.End A (∀ i, W i)) (x : ∀ i, W i) (i : I) :
25     f x i = f (Pi.single i (x i)) i := by
26   conv_lhs => rw [← LinearMap.sum_single_apply W x, map_sum]
27   simp only [Finset.sum_apply]
28   apply Finset.sum_eq_single i
29   · intro j _ hji
30     have h := LinearMap.congr_fun (off_diagonal_zero hne f i j hji.symm) (x j)
31     exact h
32   · simp
33 
34 def selector (i : I) : Module.End A (∀ j, W j) :=
35   (LinearMap.single A W i).comp (LinearMap.proj i)
36 
37 include hne in
38 theorem selector_commutes (i : I) (f : Module.End A (∀ j, W j)) (x : ∀ j, W j) :
39     selector (A := A) i (f x) = f (selector (A := A) i x) := by
40   funext j
41   by_cases h : j = i
42   · subst j
43     simpa [selector] using coordinate_of_end hne f x i
44   · have hz := LinearMap.congr_fun (off_diagonal_zero hne f j i h) (x i)
45     simpa [selector, Pi.single_apply, h] using hz.symm
46 
47 /-- A coordinate projector commutes with every module endomorphism, hence is
48 linear for the endomorphism-ring action used by Jacobson density. -/
49 def doubleSelector (i : I) : Module.End (Module.End A (∀ j, W j)) (∀ j, W j) where
50   toFun := selector (A := A) i
51   map_add' := (selector (A := A) i).map_add
52   map_smul' f x := selector_commutes hne i f x
53 
54 variable {K : Type*} [Field K]
55 variable [∀ i, Module K (W i)] [∀ i, SMulCommClass A K (W i)]
56 variable [∀ i, FiniteDimensional K (W i)]
57 
58 include hne in
59 /-- Exact simultaneous action: identity on one simple constituent, zero on all others. -/
60 theorem exists_selecting_element (i : I) :
61     ∃ a : A, ∀ j, Module.toModuleEnd K (W j) a =
62       if j = i then LinearMap.id else 0 := by
63   classical
64   let b := Module.finBasis K (∀ j, W j)
65   obtain ⟨a, ha⟩ := jacobson_density (doubleSelector hne i) (Finset.univ.image b)
66   let s : Module.End K (∀ j, W j) :=
67     (LinearMap.single K W i).comp (LinearMap.proj i)
68   have he : s = Module.toModuleEnd K (∀ j, W j) a := by
69     apply b.ext
70     intro k
71     exact ha (b k) (Finset.mem_image.mpr ⟨k, Finset.mem_univ k, rfl⟩)
72   refine ⟨a, ?_⟩
73   intro j
74   apply LinearMap.ext
75   intro x
76   have h := congrFun (LinearMap.congr_fun he (Pi.single j x)) j
77   by_cases hj : j = i
78   · subst j
79     simpa [s, Module.toModuleEnd_apply] using h.symm
80   · simpa [s, Module.toModuleEnd_apply, hj] using h.symm
81 
82 include hne in
83 /-- Trace functions of pairwise nonisomorphic simple modules are independent
84 in characteristic zero, even when the acting ring is infinite. -/
85 theorem independent_module_traces [CharZero K] :
86     LinearIndependent K (fun j (a : A) =>
87       LinearMap.trace K (W j) (Module.toModuleEnd K (W j) a)) := by
88   rw [Fintype.linearIndependent_iff]
89   intro c hc i
90   obtain ⟨a, ha⟩ := exists_selecting_element (K := K) hne i
91   have h := congrFun hc a
92   simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul, Pi.zero_apply] at h
93   have ht (j : I) : LinearMap.trace K (W j) (Module.toModuleEnd K (W j) a) =
94       if j = i then (Module.finrank K (W j) : K) else 0 := by
95     rw [ha]
96     split <;> simp [LinearMap.trace_id]
97   simp only [ht] at h
98   simp only [mul_ite, mul_zero, Finset.sum_ite_eq', Finset.mem_univ, ite_true] at h
99   have : Nontrivial (W i) := IsSimpleModule.nontrivial A (W i)
100   have hn : (Module.finrank K (W i) : K) ≠ 0 := by
101     exact_mod_cast (ne_of_gt (Module.finrank_pos (R := K) (M := W i)))
102   exact (mul_eq_zero.mp h).resolve_right hn
103 
104 end PaperX.SimpleModuleSeparation

Back to source controls