TwistedModules.lean

1 import PaperXI.TwistedMatrix
2 import PaperXI.SimpleModuleClassification
3 
4 /-! The simple-module conclusions of Paper XI, Proposition 8.3, for the actual
5 constructed twisted algebra. Existence, uniqueness, finite dimensionality,
6 and the square-root dimension are proved under the source hypotheses. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.TwistedModules
10 open CocycleCommutator
11 
12 variable {A : Type*} [CommGroup A] [Fintype A]
13 variable (c : Cocycle A ℂˣ) (hc : Normalized c) (hnd : radical c = ⊥)
14 include hc hnd
15 
16 set_option backward.isDefEq.respectTransparency false in
17 /-- A genuine simple module exists: it can be taken to be a left ideal. -/
18 theorem exists_simple_ideal :
19     let B : Type _ := TwistedAlgebra.Algebra c hc
20     letI : Ring B := inferInstance
21     ∃ I : Ideal B, IsSimpleModule B I := by
22   let : IsSimpleRing (TwistedAlgebra.Algebra c hc) := TwistedSimple.isSimpleRing c hc hnd
23   exact SimpleModuleClassification.exists_simple_ideal (TwistedAlgebra.Algebra c hc)
24 
25 /-- Any two actual simple twisted-algebra modules are isomorphic as modules. -/
26 theorem equivalent (M N : Type*) [AddCommGroup M] [AddCommGroup N]
27     [Module (TwistedAlgebra.Algebra c hc) M] [Module (TwistedAlgebra.Algebra c hc) N]
28     [IsSimpleModule (TwistedAlgebra.Algebra c hc) M]
29     [IsSimpleModule (TwistedAlgebra.Algebra c hc) N] :
30     Nonempty (M ≃ₗ[TwistedAlgebra.Algebra c hc] N) := by
31   let : IsSimpleRing (TwistedAlgebra.Algebra c hc) := TwistedSimple.isSimpleRing c hc hnd
32   exact SimpleModuleClassification.equivalent (TwistedAlgebra.Algebra c hc) M N
33 
34 variable (M : Type*) [AddCommGroup M] [Module ℂ M]
35 variable [Module (TwistedAlgebra.Algebra c hc) M]
36 variable [IsScalarTower ℂ (TwistedAlgebra.Algebra c hc) M]
37 variable [IsSimpleModule (TwistedAlgebra.Algebra c hc) M]
38 
39 /-- Finite dimensionality is derived for every simple module, not supplied. -/
40 theorem finiteDimensional : FiniteDimensional ℂ M := by
41   let : IsSimpleRing (TwistedAlgebra.Algebra c hc) := TwistedSimple.isSimpleRing c hc hnd
42   exact SimpleModuleClassification.finiteDimensional (TwistedAlgebra.Algebra c hc) M
43 
44 /-- The square of the simple-module dimension equals the index-group order. -/
45 theorem finrank_sq : Module.finrank ℂ M ^ 2 = Fintype.card A := by
46   let : IsSimpleRing (TwistedAlgebra.Algebra c hc) := TwistedSimple.isSimpleRing c hc hnd
47   exact (SimpleModuleClassification.finrank_sq (TwistedAlgebra.Algebra c hc) M).trans
48     (TwistedAlgebra.finrank_eq_card c hc)
49 
50 /-- Every irreducible twisted-algebra module has the dimension claimed in 8.3. -/
51 theorem finrank_sqrt : Module.finrank ℂ M = Nat.sqrt (Fintype.card A) := by
52   rw [← finrank_sq c hc hnd M, Nat.sqrt_eq']
53 
54 end PaperXI.TwistedModules

Back to source controls