FullTypeIntertwining105.lean

1 import PaperXI.CuspidalCartan105
2 import PaperXI.FullIntertwiningLocus69
3 import PaperXI.CompactModCenterInduction68
4 
5 /-!
6 From the actual finite cuspidal factor to full extended-type Mackey vanishing.
7 The BK tensor-to-residue reduction and arithmetic Cartan decomposition remain
8 explicit inputs. The full-H intertwining bound and induced irreducibility do not.
9 -/
10 set_option autoImplicit false
11 noncomputable section
12 namespace PaperXI.FullTypeIntertwining105
13 open Matrix Representation
14 open PaperXI.IntertwiningAlong105 PaperXI.InductionIrreducibility
15 
16 section ExactHom
17 variable {C G V : Type*} [Field C] [Group G] [AddCommGroup V] [Module C V]
18 
19 /-- The elementary equation is equivalent to the actual intersection Hom space. -/
20 def mapOfAlong (H : Subgroup G) (ρ : Representation C H V) (g : G)
21     (T : V →ₗ[C] V) (hT : Along H.subtype ρ g T) :
22     IntertwiningMap (ρ.comp (intersectionSubgroup H g).subtype)
23       (ρ.comp (intersectionConjugation H g)) where
24   toLinearMap := T
25   isIntertwining' x := by
26     ext v
27     exact hT (x : H) (intersectionConjugation H g x) rfl v
28 
29 /-- No equivalence or inverse for the intertwiner is assumed. -/
30 theorem alongOfMap (H : Subgroup G) (ρ : Representation C H V) (g : G)
31     (T : IntertwiningMap (ρ.comp (intersectionSubgroup H g).subtype)
32       (ρ.comp (intersectionConjugation H g))) :
33     Along H.subtype ρ g T.toLinearMap := by
34   intro x y hy v
35   change (y : G) = g * (x : G) * g⁻¹ at hy
36   let z : intersectionSubgroup H g := ⟨x, by
37     change g * (x : G) * g⁻¹ ∈ H
38     rw [← hy]
39     exact y.property⟩
40   have he : intersectionConjugation H g z = y := Subtype.ext hy.symm
41   have ht := LinearMap.congr_fun (T.isIntertwining' z) v
42   change T (ρ x v) = ρ (intersectionConjugation H g z) (T v) at ht
43   change T (ρ x v) = ρ y (T v)
44   rw [he] at ht
45   exact ht
46 
47 theorem existsAt_iff_locus (H : Subgroup G) (ρ : Representation C H V) (g : G) :
48     ExistsAt H.subtype ρ g ↔ g ∈ FullIntertwiningLocus69.locus H ρ := by
49   constructor
50   · rintro ⟨T, hn, ht⟩
51     refine ⟨mapOfAlong H ρ g T ht, ?_⟩
52     intro he
53     apply hn
54     exact congrArg IntertwiningMap.toLinearMap he
55   · rintro ⟨T, hn⟩
56     refine ⟨T.toLinearMap, ?_, alongOfMap H ρ g T⟩
57     intro he
58     apply hn
59     ext v
60     exact LinearMap.congr_fun he v
61 
62 /-- Restriction to J <= H keeps the same nonzero operator and carrier. -/
63 theorem restrict_existsAt (J H : Subgroup G) (hJH : J ≤ H)
64     (Λ : Representation C H V) (g : G) (hg : ExistsAt H.subtype Λ g) :
65     ExistsAt J.subtype (Λ.comp (Subgroup.inclusion hJH)) g := by
66   obtain ⟨T, hn, ht⟩ := hg
67   refine ⟨T, hn, ?_⟩
68   intro x y he v
69   exact ht (Subgroup.inclusion hJH x) (Subgroup.inclusion hJH y) he v
70 
71 /-- An irreducible compact restriction proves irreducibility of its extension. -/
72 theorem extension_irreducible (J H : Subgroup G) (hJH : J ≤ H)
73     (Λ : Representation C H V)
74     [IsIrreducible (Λ.comp (Subgroup.inclusion hJH))] : IsIrreducible Λ := by
75   let : Nontrivial V := GeneratedIrreducibility.nontrivial_space
76     (Λ.comp (Subgroup.inclusion hJH))
77   apply RepresentationStability.irreducible_of_stable
78   intro S hS
79   exact RepresentationStability.eq_bot_or_top (Λ.comp (Subgroup.inclusion hJH)) S
80     (fun j v hv => hS (Subgroup.inclusion hJH j) v hv)
81 end ExactHom
82 
83 section FullLocus
84 variable {ι R F k C Ω V W : Type*} [Fintype ι] [DecidableEq ι]
85   [CommRing R] [Field F] [Field k] [Fintype k] [Field C] [CharZero C]
86   [Group Ω] [AddCommGroup V] [Module C V] [Nontrivial V]
87   [AddCommGroup W] [Module C W]
88 
89 /-- The full locus of the completed type is an output, not a premise.
90 `hBK532` is precisely the source tensor-to-residue reduction, without any
91 cuspidal or maximal-support conclusion built into it. -/
92 theorem full_locus
93     (f : R →+* F) (red : R →+* k) (hred : Function.Surjective red)
94     (π : R) (hπ : f π ≠ 0) (hπred : red π = 0)
95     (hCartan : CuspidalCartan105.HasCartan (ι := ι) f π hπ)
96     (σ : Representation C (GL ι k) W) (hσ : CuspidalCartan105.Cuspidal σ)
97     (b : GL ι F →* Ω) (J H : Subgroup Ω) (hJH : J ≤ H)
98     (hintegral : ∀ u : GL ι R, b (GeneralLinearGroup.map f u) ∈ J)
99     (hscalar : ∀ c : Fˣ, b (GeneralLinearGroup.scalar ι c) ∈ H)
100     (Λ : Representation C H V)
101     (hBK532 : ∀ g : Ω,
102       ExistsAt J.subtype (Λ.comp (Subgroup.inclusion hJH)) g →
103       ∃ j₁ j₂ : J, ∃ y : GL ι F,
104         g = (j₁ : Ω) * b y * (j₂ : Ω) ∧
105         ExistsAt (GeneralLinearGroup.map f) (σ.comp (GeneralLinearGroup.map red)) y) :
106     FullIntertwiningLocus69.locus H Λ = (H : Set Ω) := by
107   apply Set.Subset.antisymm
108   · intro g hg
109     have hg' := restrict_existsAt J H hJH Λ g ((existsAt_iff_locus H Λ g).mpr hg)
110     obtain ⟨j₁, j₂, y, he, hy⟩ := hBK532 g hg'
111     obtain ⟨c, u, hu⟩ := CuspidalCartan105.intertwining_support
112       f red hred π hπ hπred hCartan σ hσ y hy
113     rw [he, hu, map_mul]
114     exact H.mul_mem (H.mul_mem (hJH j₁.property)
115       (H.mul_mem (hscalar c) (hJH (hintegral u)))) (hJH j₂.property)
116   · exact FullIntertwiningLocus69.subgroup_subset H Λ
117 
118 /-- This theorem genuinely calls the existing compact-mod-center induction
119 construction after deriving its formerly missing full-H hypothesis. -/
120 theorem induction_package
121     [TopologicalSpace Ω] [IsTopologicalGroup Ω] [FiniteDimensional C V]
122     (f : R →+* F) (red : R →+* k) (hred : Function.Surjective red)
123     (π : R) (hπ : f π ≠ 0) (hπred : red π = 0)
124     (hCartan : CuspidalCartan105.HasCartan (ι := ι) f π hπ)
125     (σ : Representation C (GL ι k) W) (hσ : CuspidalCartan105.Cuspidal σ)
126     (b : GL ι F →* Ω) (J H : Subgroup Ω) (hJH : J ≤ H)
127     (hintegral : ∀ u : GL ι R, b (GeneralLinearGroup.map f u) ∈ J)
128     (hscalar : ∀ c : Fˣ, b (GeneralLinearGroup.scalar ι c) ∈ H)
129     (Λ : Representation C H V)
130     [IsIrreducible (Λ.comp (Subgroup.inclusion hJH))]
131     (hBK532 : ∀ g : Ω,
132       ExistsAt J.subtype (Λ.comp (Subgroup.inclusion hJH)) g →
133       ∃ j₁ j₂ : J, ∃ y : GL ι F,
134         g = (j₁ : Ω) * b y * (j₂ : Ω) ∧
135         ExistsAt (GeneralLinearGroup.map f) (σ.comp (GeneralLinearGroup.map red)) y)
136     (Z : Subgroup H) [Z.Normal] [CompactSpace (H ⧸ Z)]
137     (χ : Z →* Cˣ)
138     (hcentral : ∀ z : Z, ∀ g : Ω, Commute (((z : H) : Ω)) g)
139     (hscalarZ : ∀ z : Z, ∀ v, Λ (z : H) v = (χ z : C) • v)
140     (hHopen : IsOpen (H : Set Ω)) (hΛ : SmoothDegreeQuotient.IsSmooth Λ) :
141     FullIntertwiningLocus69.locus H Λ = (H : Set Ω) ∧
142       Nontrivial (IndV H.subtype Λ) ∧
143       SmoothDegreeQuotient.IsSmooth (ind H.subtype Λ) ∧
144       IsIrreducible (ind H.subtype Λ) := by
145   let : IsIrreducible Λ := extension_irreducible J H hJH Λ
146   have hI := full_locus f red hred π hπ hπred hCartan σ hσ b J H hJH
147     hintegral hscalar Λ hBK532
148   exact ⟨hI, CompactModCenterInduction68.induction_package H Λ Z χ hcentral
149     hscalarZ hHopen hΛ ((FullIntertwiningLocus69.locus_eq_iff H Λ).mp hI)⟩
150 end FullLocus
151 end PaperXI.FullTypeIntertwining105

Back to source controls