CuspidalCartan105.lean

1 import PaperXI.CuspidalContraction105
2 import PaperXI.IntertwiningAlong105
3 import PaperXI.SplitRadical105
4 
5 /-! An inflated finite cuspidal representation has no noncentral Cartan
6 intertwiners. The arithmetic Cartan decomposition remains a separate explicit
7 input; its cuspidal exclusion is proved on actual matrices. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperXI.CuspidalCartan105
11 open Matrix Representation
12 open PaperXI.SplitRadical105 PaperXI.IntertwiningAlong105
13 variable {ι R F k C V : Type*} [Fintype ι] [DecidableEq ι]
14   [CommRing R] [Field F] [Field k] [Fintype k] [Field C] [CharZero C]
15   [AddCommGroup V] [Module C V]
16 
17 /-- The exact invariant-vanishing part of finite cuspidality needed here.
18 The parameter map covers the full radical of each coordinate maximal parabolic. -/
19 def Cuspidal (σ : Representation C (GL ι k) V) : Prop :=
20   ∀ S : Finset ι, S.Nonempty → S ≠ Finset.univ →
21     CuspidalContraction105.NoFixed (σ.comp (radicalMap (R := k) S))
22 
23 theorem diagonal_intertwiner_zero (f : R →+* F) (red : R →+* k)
24     (hred : Function.Surjective red) (π : R) (hπ : f π ≠ 0) (hπred : red π = 0)
25     (σ : Representation C (GL ι k) V) (hσ : Cuspidal σ)
26     (a : ι → ℕ) (ha0 : ∃ i, a i = 0) (ha1 : ∃ i, a i ≠ 0)
27     (T : V →ₗ[C] V)
28     (hT : Along (GeneralLinearGroup.map f) (σ.comp (GeneralLinearGroup.map red))
29       (cartan (f π) hπ a) T) : T = 0 := by
30   have hne : (zeroSet a).Nonempty := by
31     obtain ⟨i, hi⟩ := ha0
32     exact ⟨i, (mem_zeroSet a i).mpr hi⟩
33   have hproper : zeroSet a ≠ Finset.univ := by
34     obtain ⟨i, hi⟩ := ha1
35     intro he
36     apply hi
37     exact (mem_zeroSet a i).mp (he ▸ Finset.mem_univ i)
38   apply CuspidalContraction105.map_eq_zero
39     (σ.comp (radicalMap (R := k) (zeroSet a))) (hσ _ hne hproper) T
40   intro X v
41   obtain ⟨u, w, hu, hw, he⟩ := exists_contracted_lift f red hred π hπ hπred a X.toAdd
42   have ht := hT u w he.symm v
43   simpa only [MonoidHom.comp_apply, hu, hw, map_one, Module.End.one_apply,
44     radicalMap, MonoidHom.coe_mk, OneHom.coe_mk] using ht
45 
46 /-- Normalized Cartan form. This is an arithmetic decomposition, not an
47 intertwining assertion: no representation occurs in its definition. -/
48 def HasCartan (f : R →+* F) (π : R) (hπ : f π ≠ 0) : Prop :=
49   ∀ g : GL ι F, ∃ c : Fˣ, ∃ l r : GL ι R, ∃ a : ι → ℕ,
50     (∃ i, a i = 0) ∧
51     g = GeneralLinearGroup.scalar ι c *
52       (GeneralLinearGroup.map f l * cartan (f π) hπ a * GeneralLinearGroup.map f r)
53 
54 /-- Finite cuspidality forces a scalar-times-integral matrix. This does not
55 assume irreducibility of the inflated representation or a preproved support bound. -/
56 theorem intertwining_support (f : R →+* F) (red : R →+* k)
57     (hred : Function.Surjective red) (π : R) (hπ : f π ≠ 0) (hπred : red π = 0)
58     (hCartan : HasCartan (ι := ι) f π hπ)
59     (σ : Representation C (GL ι k) V) (hσ : Cuspidal σ)
60     (g : GL ι F)
61     (hg : ExistsAt (GeneralLinearGroup.map f) (σ.comp (GeneralLinearGroup.map red)) g) :
62     ∃ c : Fˣ, ∃ u : GL ι R,
63       g = GeneralLinearGroup.scalar ι c * GeneralLinearGroup.map f u := by
64   obtain ⟨c, l, r, a, ha0, he⟩ := hCartan g
65   have hc : ∀ x : GL ι F, Commute (GeneralLinearGroup.scalar ι c) x := by
66     intro x
67     apply Units.ext
68     change Matrix.scalar ι (c : F) * x.val = x.val * Matrix.scalar ι (c : F)
69     exact Matrix.scalar_comm (c : F) (Commute.all _) x.val
70   rw [he] at hg
71   have hg' := existsAt_remove_central (GeneralLinearGroup.map f)
72     (σ.comp (GeneralLinearGroup.map red)) _ _ hc hg
73   obtain ⟨T, hn, ht⟩ := existsAt_of_left_right (GeneralLinearGroup.map f)
74     (σ.comp (GeneralLinearGroup.map red)) l r (cartan (f π) hπ a) hg'
75   have ha : ∀ i, a i = 0 := by
76     by_contra h
77     push Not at h
78     exact hn (diagonal_intertwiner_zero f red hred π hπ hπred σ hσ a ha0 h T ht)
79   refine ⟨c, l * r, ?_⟩
80   rw [he, cartan_zero _ _ a ha, mul_one, map_mul]
81 
82 end PaperXI.CuspidalCartan105

Back to source controls