DerivedCentralCharacter69.lean

1 import Mathlib.RepresentationTheory.Irreducible
2 import Mathlib.Algebra.Algebra.Equiv
3 
4 /-! Construct the central character of the given irreducible finite-dimensional representation. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperXI.DerivedCentralCharacter69
8 open Representation
9 variable {k H V : Type*} [Field k] [IsAlgClosed k] [Group H]
10   [AddCommGroup V] [Module k V] [FiniteDimensional k V]
11   (ρ : Representation k H V) [IsIrreducible ρ]
12   (Z : Subgroup H) (hZ : ∀ z : Z, ∀ h : H, Commute (z : H) h)
13 
14 /-- Central representation operators, as actual endomorphism intertwiners. -/
15 def centralAction : Z →* IntertwiningMap ρ ρ where
16   toFun z :=
17     { toLinearMap := ρ (z : H)
18       isIntertwining' h := by
19         change ρ (z : H) * ρ h = ρ h * ρ (z : H)
20         rw [← map_mul, ← map_mul, (hZ z h).eq] }
21   map_one' := by ext v; simp
22   map_mul' z w := by ext v; simp [← map_mul]
23 
24 /-- Schur's lemma identifies the entire endomorphism-intertwiner algebra with scalars. -/
25 def scalarEquiv : k ≃ₐ[k] IntertwiningMap ρ ρ :=
26   AlgEquiv.ofBijective (Algebra.ofId k (IntertwiningMap ρ ρ))
27     (IsIrreducible.algebraMap_intertwiningMap_bijective_of_isAlgClosed (ρ := ρ))
28 
29 /-- The central scalar function is a multiplicative character with values in units. -/
30 def character : Z →* kˣ :=
31   MonoidHom.toHomUnits ((scalarEquiv ρ).symm.toMonoidHom.comp (centralAction ρ Z hZ))
32 
33 /-- The constructed character acts by precisely the given central operators. -/
34 theorem character_apply (z : Z) (v : V) :
35     ρ (z : H) v = (character ρ Z hZ z : k) • v := by
36   have he := (scalarEquiv ρ).apply_symm_apply (centralAction ρ Z hZ z)
37   have hev := congrArg (fun f : IntertwiningMap ρ ρ => f v) he
38   change ((scalarEquiv ρ).symm (centralAction ρ Z hZ z)) • v = ρ (z : H) v at hev
39   exact hev.symm
40 
41 end PaperXI.DerivedCentralCharacter69

Back to source controls