CentralExtensionUniqueness.lean

1 import PaperXI.CentralCharacterIrreducible
2 import PaperXI.TwistedModules
3 import PaperXI.SchurScalar
4 
5 /-! Finite Stone–von Neumann for actual central extensions with nondegenerate
6 scalar commutator. Only the quotient is required finite. The argument works
7 in every characteristic and derives the dimensions of the given irreducibles. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperXI.CentralExtensionUniqueness
11 open CentralExtension CentralCharacter AlgebraActionModule CocycleCommutator
12 
13 variable {Z H A V W : Type*} [CommGroup Z] [Group H] [CommGroup A] [Fintype A]
14 variable [AddCommGroup V] [Module ℂ V] [AddCommGroup W] [Module ℂ W]
15 
16 /-- Every irreducible representation with the prescribed central action is
17 finite-dimensional; this is not a hypothesis on its space. -/
18 theorem finiteDimensional (D : Datum Z H A) (ζ : Z →* ℂˣ)
19     (hnd : radical (scalarCocycle D ζ) = ⊥)
20     (σ : Representation ℂ H W) [Representation.IsIrreducible σ]
21     (hσ : ∀ z, σ (D.i z) = (ζ z : ℂ) • LinearMap.id) :
22     FiniteDimensional ℂ W := by
23   let φ := toAlgebraAction D ζ σ hσ
24   let : IsSimpleModule (CentralCharacter.Algebra D ζ) (Space (B := ↥(CentralCharacter.Algebra D ζ)) φ) := simpleModule D ζ σ hσ
25   let : IsSimpleRing (CentralCharacter.Algebra D ζ) :=
26     TwistedSimple.isSimpleRing (scalarCocycle D ζ) (normalized_scalarCocycle D ζ) hnd
27   let : FiniteDimensional ℂ (Space (B := ↥(CentralCharacter.Algebra D ζ)) φ) :=
28     SimpleModuleClassification.finiteDimensional (CentralCharacter.Algebra D ζ) (Space (B := ↥(CentralCharacter.Algebra D ζ)) φ)
29   exact FiniteDimensional.of_injective (AlgebraActionModule.equiv (B := ↥(CentralCharacter.Algebra D ζ)) φ).symm.toLinearMap
30     (AlgebraActionModule.equiv (B := ↥(CentralCharacter.Algebra D ζ)) φ).symm.injective
31 
32 /-- The dimension of each actual irreducible is the square root of the quotient order. -/
33 theorem finrank_sqrt (D : Datum Z H A) (ζ : Z →* ℂˣ)
34     (hnd : radical (scalarCocycle D ζ) = ⊥)
35     (σ : Representation ℂ H W) [Representation.IsIrreducible σ]
36     (hσ : ∀ z, σ (D.i z) = (ζ z : ℂ) • LinearMap.id) :
37     Module.finrank ℂ W = Nat.sqrt (Fintype.card A) := by
38   let φ := toAlgebraAction D ζ σ hσ
39   let : IsSimpleModule (CentralCharacter.Algebra D ζ) (Space (B := ↥(CentralCharacter.Algebra D ζ)) φ) := simpleModule D ζ σ hσ
40   rw [← (AlgebraActionModule.equiv (B := ↥(CentralCharacter.Algebra D ζ)) φ).finrank_eq]
41   exact TwistedModules.finrank_sqrt (scalarCocycle D ζ) (normalized_scalarCocycle D ζ)
42     hnd (Space (B := ↥(CentralCharacter.Algebra D ζ)) φ)
43 
44 set_option backward.isDefEq.respectTransparency false in
45 /-- The first equivalence between arbitrary irreducibles is constructed from
46 the equivalence of their actual simple twisted-algebra modules. -/
47 theorem exists_equiv (D : Datum Z H A) (ζ : Z →* ℂˣ)
48     (hnd : radical (scalarCocycle D ζ) = ⊥)
49     (σ : Representation ℂ H V) (τ : Representation ℂ H W)
50     [Representation.IsIrreducible σ] [Representation.IsIrreducible τ]
51     (hσ : ∀ z, σ (D.i z) = (ζ z : ℂ) • LinearMap.id)
52     (hτ : ∀ z, τ (D.i z) = (ζ z : ℂ) • LinearMap.id) :
53     Nonempty (Representation.Equiv σ τ) := by
54   let φ := toAlgebraAction D ζ σ hσ
55   let χ := toAlgebraAction D ζ τ hτ
56   let : IsSimpleModule (CentralCharacter.Algebra D ζ) (Space (B := ↥(CentralCharacter.Algebra D ζ)) φ) := simpleModule D ζ σ hσ
57   let : IsSimpleModule (CentralCharacter.Algebra D ζ) (Space (B := ↥(CentralCharacter.Algebra D ζ)) χ) := simpleModule D ζ τ hτ
58   obtain ⟨e⟩ := TwistedModules.equivalent (scalarCocycle D ζ) (normalized_scalarCocycle D ζ)
59     hnd (Space (B := ↥(CentralCharacter.Algebra D ζ)) φ) (Space (B := ↥(CentralCharacter.Algebra D ζ)) χ)
60   let U : V ≃ₗ[ℂ] W := e.restrictScalars ℂ
61   have hU : ∀ h v, U (σ h v) = τ h (U v) :=
62     (action_intertwines_iff D ζ σ τ hσ hτ U.toLinearMap).mpr
63       (fun b v => e.map_smul b v)
64   let F : Representation.IntertwiningMap σ τ := ⟨U.toLinearMap, fun h => LinearMap.ext (hU h)⟩
65   exact ⟨F.ofBijective U.bijective⟩
66 
67 /-- A chosen equivalence supplied by the existence theorem. -/
68 def equiv (D : Datum Z H A) (ζ : Z →* ℂˣ)
69     (hnd : radical (scalarCocycle D ζ) = ⊥)
70     (σ : Representation ℂ H V) (τ : Representation ℂ H W)
71     [Representation.IsIrreducible σ] [Representation.IsIrreducible τ]
72     (hσ : ∀ z, σ (D.i z) = (ζ z : ℂ) • LinearMap.id)
73     (hτ : ∀ z, τ (D.i z) = (ζ z : ℂ) • LinearMap.id) :
74     Representation.Equiv σ τ := Classical.choice (exists_equiv D ζ hnd σ τ hσ hτ)
75 
76 theorem equiv_intertwines (D : Datum Z H A) (ζ : Z →* ℂˣ)
77     (hnd : radical (scalarCocycle D ζ) = ⊥)
78     (σ : Representation ℂ H V) (τ : Representation ℂ H W)
79     [Representation.IsIrreducible σ] [Representation.IsIrreducible τ]
80     (hσ : ∀ z, σ (D.i z) = (ζ z : ℂ) • LinearMap.id)
81     (hτ : ∀ z, τ (D.i z) = (ζ z : ℂ) • LinearMap.id) (h : H) (v : V) :
82     equiv D ζ hnd σ τ hσ hτ (σ h v) = τ h (equiv D ζ hnd σ τ hσ hτ v) :=
83   Representation.IntertwiningMap.isIntertwining σ τ
84     (equiv D ζ hnd σ τ hσ hτ).toIntertwiningMap h v
85 
86 /-- Every other invertible intertwiner differs by a unique nonzero scalar. -/
87 theorem unique_scalar (D : Datum Z H A) (ζ : Z →* ℂˣ)
88     (hnd : radical (scalarCocycle D ζ) = ⊥)
89     (σ : Representation ℂ H V) (τ : Representation ℂ H W)
90     [Representation.IsIrreducible σ] [Representation.IsIrreducible τ]
91     (hσ : ∀ z, σ (D.i z) = (ζ z : ℂ) • LinearMap.id)
92     (hτ : ∀ z, τ (D.i z) = (ζ z : ℂ) • LinearMap.id)
93     (T : V ≃ₗ[ℂ] W) (hT : ∀ h v, T (σ h v) = τ h (T v)) :
94     ∃! c : ℂˣ, ∀ v, T v = (c : ℂ) • equiv D ζ hnd σ τ hσ hτ v := by
95   let : FiniteDimensional ℂ V := finiteDimensional D ζ hnd σ hσ
96   exact SchurScalar.bridge_unique σ τ (equiv D ζ hnd σ τ hσ hτ).toLinearEquiv T
97     (equiv_intertwines D ζ hnd σ τ hσ hτ) hT
98 
99 end PaperXI.CentralExtensionUniqueness

Back to source controls