CentralCharacterAction.lean

1 import PaperXI.CentralExtensionCocycle
2 import PaperXI.TwistedAction
3 import Mathlib.RepresentationTheory.Basic
4 
5 /-! An actual representation with a prescribed central character yields an
6 actual action of its section's twisted group algebra. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.CentralCharacter
10 open PaperXI.CentralExtension
11 variable {Z H A V W : Type*} [CommGroup Z] [Group H] [CommGroup A]
12 variable [AddCommGroup V] [Module ℂ V] [AddCommGroup W] [Module ℂ W]
13 
14 /-- Section operators preserve the normalized identity. -/
15 theorem section_operators_one (D : Datum Z H A) (σ : Representation ℂ H W) :
16     σ (sectionMap D 1) = 1 := by
17   rw [section_one, map_one]
18 
19 /-- Section operators satisfy the actual scalar cocycle multiplication law. -/
20 theorem section_operators_mul (D : Datum Z H A) (ζ : Z →* ℂˣ)
21     (σ : Representation ℂ H W)
22     (hcentral : ∀ z, σ (D.i z) = (ζ z : ℂ) • LinearMap.id) (a b : A) :
23     σ (sectionMap D a) * σ (sectionMap D b) =
24       ((scalarCocycle D ζ).coeff a b : ℂ) • σ (sectionMap D (a * b)) := by
25   rw [← map_mul, section_mul, map_mul, hcentral]
26   change ((ζ (defect D a b) : ℂ) • (1 : Module.End ℂ W)) *
27       σ (sectionMap D (a * b)) =
28     (ζ (defect D a b) : ℂ) • σ (sectionMap D (a * b))
29   rw [smul_mul_assoc, one_mul]
30 
31 /-- The twisted algebra attached to the actual extension and central character. -/
32 abbrev Algebra (D : Datum Z H A) (ζ : Z →* ℂˣ) :=
33   TwistedAlgebra.Algebra (scalarCocycle D ζ) (normalized_scalarCocycle D ζ)
34 
35 variable [Fintype A]
36 
37 /-- Its canonical basis is indexed by the actual quotient group. -/
38 abbrev basis (D : Datum Z H A) (ζ : Z →* ℂˣ) :=
39   TwistedAlgebra.basis (scalarCocycle D ζ) (normalized_scalarCocycle D ζ)
40 
41 /-- Linear extension of the actual section operators to an algebra action. -/
42 def toAlgebraAction (D : Datum Z H A) (ζ : Z →* ℂˣ)
43     (σ : Representation ℂ H W)
44     (hcentral : ∀ z, σ (D.i z) = (ζ z : ℂ) • LinearMap.id) :
45     Algebra D ζ →ₐ[ℂ] Module.End ℂ W :=
46   TwistedAction.action (scalarCocycle D ζ) (normalized_scalarCocycle D ζ)
47     (fun a => σ (sectionMap D a)) (section_operators_one D σ)
48     (section_operators_mul D ζ σ hcentral)
49 
50 @[simp] theorem toAlgebraAction_basis (D : Datum Z H A) (ζ : Z →* ℂˣ)
51     (σ : Representation ℂ H W)
52     (hcentral : ∀ z, σ (D.i z) = (ζ z : ℂ) • LinearMap.id) (a : A) :
53     toAlgebraAction D ζ σ hcentral (basis D ζ a) = σ (sectionMap D a) :=
54   TwistedAction.action_basis (scalarCocycle D ζ) (normalized_scalarCocycle D ζ)
55     (fun a => σ (sectionMap D a)) (section_operators_one D σ)
56     (section_operators_mul D ζ σ hcentral) a
57 
58 /-- The algebra action recovers every group operator by the actual normal form. -/
59 theorem action_normal_form (D : Datum Z H A) (ζ : Z →* ℂˣ)
60     (σ : Representation ℂ H W)
61     (hcentral : ∀ z, σ (D.i z) = (ζ z : ℂ) • LinearMap.id) (h : H) :
62     σ h = (ζ (coordinate D h) : ℂ) •
63       toAlgebraAction D ζ σ hcentral (basis D ζ (D.q h)) := by
64   rw [toAlgebraAction_basis]
65   calc
66     σ h = σ (D.i (coordinate D h) * sectionMap D (D.q h)) :=
67       congrArg σ (normal_form D h)
68     _ = (ζ (coordinate D h) : ℂ) • σ (sectionMap D (D.q h)) := by
69       rw [map_mul, hcentral]
70       change ((ζ (coordinate D h) : ℂ) • (1 : Module.End ℂ W)) *
71           σ (sectionMap D (D.q h)) = _
72       rw [smul_mul_assoc, one_mul]
73 
74 /-- A complex subspace is stable under the algebra action exactly when it
75 is stable under the original group representation. -/
76 theorem action_stable_iff (D : Datum Z H A) (ζ : Z →* ℂˣ)
77     (σ : Representation ℂ H W)
78     (hcentral : ∀ z, σ (D.i z) = (ζ z : ℂ) • LinearMap.id)
79     (S : Submodule ℂ W) :
80     (∀ b : Algebra D ζ, ∀ w ∈ S, toAlgebraAction D ζ σ hcentral b w ∈ S) ↔
81       ∀ h : H, ∀ w ∈ S, σ h w ∈ S := by
82   constructor
83   · intro hb h w hw
84     rw [action_normal_form D ζ σ hcentral h, LinearMap.smul_apply]
85     exact S.smul_mem _ (hb (basis D ζ (D.q h)) w hw)
86   · intro hh b w hw
87     rw [← (basis D ζ).sum_repr b, map_sum]
88     simp only [map_smul, LinearMap.sum_apply, LinearMap.smul_apply, toAlgebraAction_basis]
89     exact S.sum_mem (fun a _ => S.smul_mem _ (hh (sectionMap D a) w hw))
90 
91 /-- Group intertwiners are exactly the complex-linear maps intertwining the
92 constructed algebra actions. -/
93 theorem action_intertwines_iff (D : Datum Z H A) (ζ : Z →* ℂˣ)
94     (σ : Representation ℂ H V) (τ : Representation ℂ H W)
95     (hσ : ∀ z, σ (D.i z) = (ζ z : ℂ) • LinearMap.id)
96     (hτ : ∀ z, τ (D.i z) = (ζ z : ℂ) • LinearMap.id)
97     (F : V →ₗ[ℂ] W) :
98     (∀ h v, F (σ h v) = τ h (F v)) ↔
99       ∀ b : Algebra D ζ, ∀ v,
100         F (toAlgebraAction D ζ σ hσ b v) = toAlgebraAction D ζ τ hτ b (F v) := by
101   constructor
102   · intro hF b v
103     rw [← (basis D ζ).sum_repr b]
104     simp only [map_sum, map_smul, LinearMap.sum_apply, LinearMap.smul_apply,
105       toAlgebraAction_basis, hF]
106   · intro hF h v
107     rw [action_normal_form D ζ σ hσ h, action_normal_form D ζ τ hτ h]
108     simp only [LinearMap.smul_apply, map_smul]
109     rw [hF]
110 
111 end PaperXI.CentralCharacter

Back to source controls