SimpleModuleClassification.lean

1 import Mathlib.RingTheory.SimpleModule.WedderburnArtin
2 import Mathlib.RepresentationTheory.AlgebraRepresentation.Basic
3 import Mathlib.Analysis.Complex.Polynomial.Basic
4 import Mathlib.LinearAlgebra.Dimension.Constructions
5 import Mathlib.Data.Nat.Sqrt
6 import Mathlib.Tactic
7 
8 /-! Actual simple modules over a finite-dimensional simple complex algebra:
9 uniqueness, automatic finite dimensionality, and the square-root dimension. -/
10 set_option autoImplicit false
11 noncomputable section
12 namespace PaperXI.SimpleModuleClassification
13 
14 variable (R : Type*) [Ring R] [Algebra ℂ R] [FiniteDimensional ℂ R] [IsSimpleRing R]
15 
16 /-- Any two simple modules over the actual algebra are linearly equivalent as modules. -/
17 theorem equivalent (M N : Type*) [AddCommGroup M] [Module R M] [IsSimpleModule R M]
18     [AddCommGroup N] [Module R N] [IsSimpleModule R N] : Nonempty (M ≃ₗ[R] N) := by
19   let : IsArtinianRing R := IsArtinianRing.of_finite ℂ R
20   obtain ⟨I, ⟨e⟩⟩ := IsSemisimpleRing.exists_linearEquiv_ideal_of_isSimpleModule R M
21   obtain ⟨J, ⟨f⟩⟩ := IsSemisimpleRing.exists_linearEquiv_ideal_of_isSimpleModule R N
22   let : IsSimpleModule R I := IsSimpleModule.congr e.symm
23   let : IsSimpleModule R J := IsSimpleModule.congr f.symm
24   exact ⟨e.trans ((IsSimpleRing.isIsotypic R R J I).some.trans f.symm)⟩
25 
26 /-- The regular module is a positive finite sum of copies of any given simple module. -/
27 theorem regular_decomposition (M : Type*) [AddCommGroup M] [Module R M]
28     [IsSimpleModule R M] :
29     ∃ n : ℕ, 0 < n ∧ Nonempty (R ≃ₗ[R] (Fin n → M)) := by
30   let : IsArtinianRing R := IsArtinianRing.of_finite ℂ R
31   obtain ⟨n, hn, S, hS, ⟨e⟩⟩ := (IsSimpleRing.isIsotypic R R).linearEquiv_fun
32   let f : S ≃ₗ[R] M := (equivalent R S M).some
33   exact ⟨n, Nat.pos_of_ne_zero (NeZero.ne n),
34     ⟨e.trans (LinearEquiv.piCongrRight (fun _ : Fin n => f))⟩⟩
35 
36 /-- The algebra has an actual simple left ideal, hence an actual simple module. -/
37 theorem exists_simple_ideal : ∃ I : Ideal R, IsSimpleModule R I := by
38   let : IsArtinianRing R := IsArtinianRing.of_finite ℂ R
39   obtain ⟨_, _, I, hI, _⟩ := (IsSimpleRing.isIsotypic R R).linearEquiv_fun
40   exact ⟨I, hI⟩
41 
42 variable (M : Type*) [AddCommGroup M] [Module R M] [Module ℂ M]
43 variable [IsScalarTower ℂ R M] [IsSimpleModule R M]
44 
45 /-- The module equivalence restricts to a complex linear equivalence preserving the action. -/
46 theorem equivalent_complex (N : Type*) [AddCommGroup N] [Module R N] [Module ℂ N]
47     [IsScalarTower ℂ R N] [IsSimpleModule R N] :
48     ∃ e : M ≃ₗ[ℂ] N, ∀ (r : R) (w : M), e (r • w) = r • e w := by
49   obtain ⟨e⟩ := equivalent R M N
50   exact ⟨e.restrictScalars ℂ, fun r w => e.map_smul r w⟩
51 
52 include R in
53 /-- Finite dimensionality is a conclusion, obtained by identifying a simple module
54 with an actual ideal of the finite-dimensional algebra. -/
55 theorem finiteDimensional : FiniteDimensional ℂ M := by
56   let : IsArtinianRing R := IsArtinianRing.of_finite ℂ R
57   obtain ⟨I, ⟨e⟩⟩ := IsSemisimpleRing.exists_linearEquiv_ideal_of_isSimpleModule R M
58   let : FiniteDimensional ℂ I := Module.Finite.of_injective
59     (I.subtype.restrictScalars ℂ) I.subtype_injective
60   exact (e.restrictScalars ℂ).symm.finiteDimensional
61 
62 include R in
63 /-- Simple modules have positive complex dimension. -/
64 theorem finrank_pos : 0 < Module.finrank ℂ M := by
65   let : FiniteDimensional ℂ M := finiteDimensional R M
66   let : Nontrivial M := IsSimpleModule.nontrivial R M
67   exact Module.finrank_pos
68 
69 /-- Schur's lemma as an algebra equivalence, after deriving finite dimensionality. -/
70 def scalarEndEquiv : ℂ ≃ₐ[ℂ] Module.End R M := by
71   let : FiniteDimensional ℂ M := finiteDimensional R M
72   exact AlgEquiv.ofBijective (Algebra.ofId ℂ (Module.End R M))
73     (IsSimpleModule.algebraMap_end_bijective_of_isAlgClosed ℂ)
74 
75 /-- The actual commuting endomorphism algebra is one-dimensional over the center. -/
76 theorem finrank_end : Module.finrank ℂ (Module.End R M) = 1 := by
77   have h := (scalarEndEquiv R M).toLinearEquiv.finrank_eq
78   simpa using h.symm
79 
80 /-- Every simple module has dimension whose square is the dimension of the algebra. -/
81 theorem finrank_sq : (Module.finrank ℂ M) ^ 2 = Module.finrank ℂ R := by
82   let : FiniteDimensional ℂ M := finiteDimensional R M
83   obtain ⟨n, hn, ⟨e⟩⟩ := regular_decomposition R M
84   have hregular : Module.finrank ℂ R = n * Module.finrank ℂ M := by
85     have h := (e.restrictScalars ℂ).finrank_eq
86     simpa [Module.finrank_pi_fintype] using h
87   let eEnd : Module.End R R ≃ₐ[ℂ] Matrix (Fin n) (Fin n) (Module.End R M) :=
88     (e.conjAlgEquiv ℂ).trans (endVecAlgEquivMatrixEnd (Fin n) ℂ R M)
89   let eSelf : Rᵐᵒᵖ ≃ₐ[ℂ] Module.End R R := AlgEquiv.moduleEndSelf ℂ
90   have hend : Module.finrank ℂ R = n * n := by
91     calc
92       Module.finrank ℂ R = Module.finrank ℂ Rᵐᵒᵖ :=
93         (MulOpposite.opLinearEquiv ℂ).finrank_eq
94       _ = Module.finrank ℂ (Module.End R R) := eSelf.toLinearEquiv.finrank_eq
95       _ = Module.finrank ℂ (Matrix (Fin n) (Fin n) (Module.End R M)) :=
96         eEnd.toLinearEquiv.finrank_eq
97       _ = n * n := by simp [Module.finrank_matrix, finrank_end R M]
98   have hdim : Module.finrank ℂ M = n := Nat.eq_of_mul_eq_mul_left hn
99     (hregular.symm.trans hend)
100   rw [hdim, pow_two, ← hend]
101 
102 /-- The positive simple-module dimension is the natural square root of the algebra dimension. -/
103 theorem finrank_sqrt : Module.finrank ℂ M = Nat.sqrt (Module.finrank ℂ R) := by
104   rw [← finrank_sq R M, Nat.sqrt_eq']
105 
106 end PaperXI.SimpleModuleClassification

Back to source controls