ActualCharacterData108.lean

1 import PaperXI.ActualHeisenbergCandidate107
2 import PaperXI.CharacterSupport108
3 
4 /-! Character occurrence on the actual prescribed kappa carrier, with its
5 normality and invariance derived from the literal character normalizer. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.ActualCharacterData108
9 open Matrix ValuativeRel Representation
10 open ActualCharacterType61 ActualCuspidalCandidate105
11 open ActualELatticeTopology60 LatticeCongruenceTopology60
12 variable (F E : Type*) [Field F] [ValuativeRel F] [TopologicalSpace F]
13   [IsNonarchimedeanLocalField F] [Field E] [ValuativeRel E] [TopologicalSpace E]
14   [IsNonarchimedeanLocalField E] [Algebra F E]
15 variable (m n : Type*) [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n]
16   [Nonempty n] (e : (m → E) ≃L[F] (n → F))
17   (D : Subgroup (GL n F)) (θ : D →* ℂˣ)
18   (hDc : D ≤ matrixCongruence F E m n e)
19 
20 omit [ValuativeRel F] [IsNonarchimedeanLocalField F] [Fintype m] [DecidableEq m] [Nonempty n] in
21 include hDc in
22 theorem domain_le_compact : D ≤ compact F E m n e D θ :=
23   domain_le_compactGroup F E m n e D θ
24     (hDc.trans (matrixCongruence_le_chainGroup F E m n e))
25 
26 def intoCompact : D →* compact F E m n e D θ :=
27   Subgroup.inclusion (domain_le_compact F E m n e D θ hDc)
28 
29 omit [ValuativeRel F] [IsNonarchimedeanLocalField F] [Fintype m] [DecidableEq m] [Nonempty n] in
30 theorem intoCompact_mem_first (d : D) :
31     intoCompact F E m n e D θ hDc d ∈ firstSubgroup F E m n e D θ := hDc d.property
32 
33 variable {W : Type*} [AddCommGroup W] [Module ℂ W]
34   (κ : Representation ℂ (compact F E m n e D θ) W)
35 
36 /-- Literal character occurrence on the existing carrier. -/
37 def Contains : Prop :=
38   ∃ v : W, v ≠ 0 ∧ ∀ d : D, κ (intoCompact F E m n e D θ hDc d) v = (θ d : ℂ) • v
39 
40 omit [ValuativeRel F] [IsNonarchimedeanLocalField F] [Fintype m] [DecidableEq m] [Nonempty n] in
41 theorem scalar_restriction [IsIrreducible (κ.comp (firstSubgroup F E m n e D θ).subtype)]
42     (hc : Contains F E m n e D θ hDc κ) (d : D) :
43     κ (intoCompact F E m n e D θ hDc d) = (θ d : ℂ) • LinearMap.id := by
44   let : IsIrreducible κ := CharacterAttachment108.irreducible_of_restriction
45     (firstSubgroup F E m n e D θ) κ
46   exact CharacterAttachment108.scalar_of_contains D (compact F E m n e D θ)
47     (domain_le_compact F E m n e D θ hDc) θ (fun _ h => h.1) κ hc d
48 
49 end PaperXI.ActualCharacterData108

Back to source controls