FiniteRepresentation.lean

1 import PaperXI.RepresentationStability
2 import Mathlib.LinearAlgebra.Dimension.Constructions
3 import Mathlib.RingTheory.Finiteness.Basic
4 
5 /-! Finite dimension is derived from the actual finite group action.
6 The generic input is the cyclicity of a nonzero simple module, not a
7 semisimple decomposition or an assumed target dimension. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperXI.FiniteRepresentation
11 
12 variable {k : Type*} [Field k]
13 
14 /-- A simple module over a finite-dimensional algebra is finite-dimensional
15 over the ground field, by the actual cyclic action map. -/
16 theorem simple_finiteDimensional (R M : Type*) [Ring R] [Algebra k R]
17     [FiniteDimensional k R] [AddCommGroup M] [Module R M] [Module k M]
18     [IsScalarTower k R M] [IsSimpleModule R M] : FiniteDimensional k M := by
19   let : Nontrivial M := IsSimpleModule.nontrivial R M
20   obtain ⟨m, hm⟩ := exists_ne (0 : M)
21   exact Module.Finite.of_surjective
22     ((LinearMap.toSpanSingleton R M m).restrictScalars k)
23     (IsSimpleModule.toSpanSingleton_surjective R hm)
24 
25 /-- Every actual irreducible representation of a finite group has finite dimension. -/
26 theorem finiteDimensional {G W : Type*} [Group G] [Finite G]
27     [AddCommGroup W] [Module k W]
28     (ρ : Representation k G W) [Representation.IsIrreducible ρ] :
29     FiniteDimensional k W := by
30   let : FiniteDimensional k ρ.asModule :=
31     simple_finiteDimensional (k := k) (MonoidAlgebra k G) ρ.asModule
32   exact Module.Finite.equiv ρ.asModuleEquiv
33 
34 /-- Such an irreducible representation has strictly positive dimension. -/
35 theorem finrank_pos {G W : Type*} [Group G] [Finite G]
36     [AddCommGroup W] [Module k W]
37     (ρ : Representation k G W) [Representation.IsIrreducible ρ] :
38     0 < Module.finrank k W := by
39   let : FiniteDimensional k W := finiteDimensional ρ
40   let : Nontrivial W := GeneratedIrreducibility.nontrivial_space ρ
41   exact Module.finrank_pos
42 
43 end PaperXI.FiniteRepresentation

Back to source controls