ActualCuspidalCandidate105.lean

1 import PaperXI.FullTypeIntertwining105
2 import PaperXI.ActualPacketTypeRealization70
3 
4 /-! The actual character-dependent constructor of Block 70 now returns an
5 irreducible induced candidate, not a conditional promise requiring its full
6 intertwining locus. The residual cuspidality, arithmetic Cartan decomposition,
7 and BK tensor-to-residue reduction remain explicit. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperXI.ActualCuspidalCandidate105
11 open Matrix ValuativeRel Representation
12 open scoped TensorProduct
13 open ActualCharacterType61 ActualCharacterIdentification61 ActualCharacterResidue61
14 open ActualELatticeTopology60 ActualELatticeResidue59 ActualEmbeddedUniformizer58
15 open LatticeCongruenceTopology60 ActualFieldTypeQuotient69
16 open PaperXI.IntertwiningAlong105
17 
18 variable (F E : Type*) [Field F] [ValuativeRel F] [TopologicalSpace F]
19   [IsNonarchimedeanLocalField F] [Field E] [ValuativeRel E] [TopologicalSpace E]
20   [IsNonarchimedeanLocalField E] [Algebra F E]
21 variable (m n : Type*) [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n]
22   [Nonempty n] (e : (m → E) ≃L[F] (n → F))
23   (D : Subgroup (GL n F)) (θ : D →* ℂˣ)
24 
25 /-- The literal field-centralizer matrices on the original F-carrier. -/
26 def centralizerMap : GL m E →* GL n F :=
27   (coordinateAut e).symm.toMonoidHom.comp (restrictScalarMatrix F E m)
28 
29 abbrev compact := compactGroup F E m n e D θ
30 abbrev extended := fieldGroup F E n (scalarMatrixEmbedding F E m n e)
31   (compact F E m n e D θ)
32 
33 omit [ValuativeRel F] [IsNonarchimedeanLocalField F] [ValuativeRel E]
34   [IsNonarchimedeanLocalField E] [Nonempty n] in
35 /-- The scalar field action agrees with the embedding used by the old constructor. -/
36 theorem centralizer_scalar (c : Eˣ) :
37     centralizerMap F E m n e (GeneralLinearGroup.scalar m c) =
38       unitsEmbedding F E n (scalarMatrixEmbedding F E m n e) c := by
39   apply (coordinateAut e).injective
40   change coordinateAut e ((coordinateAut e).symm
41     (restrictScalarMatrix F E m (GeneralLinearGroup.scalar m c))) = _
42   rw [MulEquiv.apply_symm_apply, coordinateAut_unitsEmbedding]
43   ext v i
44   simp [restrictScalarMatrix_apply, Matrix.mulVec, dotProduct, Matrix.scalar_apply, Matrix.diagonal_apply]
45 
46 variable (hmodel : compact F E m n e D θ ≤ matrixType F E m n e)
47 variable {W U : Type*} [AddCommGroup W] [Module ℂ W] [FiniteDimensional ℂ W]
48   [AddCommGroup U] [Module ℂ U]
49   (κ : Representation ℂ (compact F E m n e D θ) W)
50   (σ : Representation ℂ (GL m 𝓀[E]) U)
51 
52 /-- The constructor keeps the same theta, residue map, kappa and tensor carrier.
53 No whole-type extension, full-H bound, or induced irreducibility is an input. -/
54 theorem candidate_exists
55     (hF : Continuous (algebraMap F E))
56     (hDo : IsOpen (D : Set (GL n F)))
57     (hB : ∀ u : GL m 𝒪[E],
58       (coordinateAut e).symm (integralMatrix F E m u) ∈ CharacterNormalizer61.normalizer D θ)
59     (hfull : ∀ g : GL n F,
60       g ∈ CharacterNormalizer61.normalizer D θ ↔
61         ∃ a : Eˣ, ∃ j : compact F E m n e D θ,
62           unitsEmbedding F E n (scalarMatrixEmbedding F E m n e) a * (j : GL n F) = g)
63     [IsIrreducible (κ.comp (firstSubgroup F E m n e D θ).subtype)] [IsIrreducible σ]
64     (hκ : SmoothDegreeQuotient.IsSmooth κ)
65     (hβ : ∀ g : GL n F,
66       NormalizerIntertwining60.IntertwinedAt D (MonomialInduction.scalarRepresentation θ) g →
67       NormalizerIntertwining60.IntertwinedAt (compact F E m n e D θ) κ g)
68     (π : 𝒪[E]) (hπ : (π : E) ≠ 0) (hπred : IsLocalRing.residue 𝒪[E] π = 0)
69     (hCartan : CuspidalCartan105.HasCartan (ι := m) (valuation E).integer.subtype π hπ)
70     (hσc : CuspidalCartan105.Cuspidal σ)
71     (hBK532 : ∀ g : GL n F,
72       ExistsAt (compact F E m n e D θ).subtype
73         (CompactTypeTensor58.action (reduction F E m n e D θ hmodel) κ σ) g →
74       ∃ j₁ j₂ : compact F E m n e D θ, ∃ y : GL m E,
75         g = (j₁ : GL n F) * centralizerMap F E m n e y * (j₂ : GL n F) ∧
76         ExistsAt (ActualIntegralGeneralLinear.embedding E m)
77           (σ.comp (ActualResidueGeneralLinear.reduction E m)) y) :
78     FiniteDimensional ℂ (W ⊗[ℂ] U) ∧
79     ∃ Λ : Representation ℂ (extended F E m n e D θ) (W ⊗[ℂ] U),
80       (∀ j : compact F E m n e D θ,
81         Λ (PrescribedFieldType70.compactInclusion F E n (scalarMatrixEmbedding F E m n e)
82           (compact F E m n e D θ) j) =
83           CompactTypeTensor58.action (reduction F E m n e D θ hmodel) κ σ j) ∧
84       IsIrreducible Λ ∧ SmoothDegreeQuotient.IsSmooth Λ ∧
85       FullIntertwiningLocus69.locus (extended F E m n e D θ) Λ =
86         (extended F E m n e D θ : Set (GL n F)) ∧
87       Function.Injective (TensorTypeOperators70.realize (extended F E m n e D θ) Λ) ∧
88       Nontrivial (IndV (extended F E m n e D θ).subtype Λ) ∧
89       SmoothDegreeQuotient.IsSmooth (ind (extended F E m n e D θ).subtype Λ) ∧
90       IsIrreducible (ind (extended F E m n e D θ).subtype Λ) := by
91   let : Fintype 𝓀[E] := Fintype.ofFinite 𝓀[E]
92   obtain ⟨_, hfin, Λ, hr, _, hi, hs, hinj, _, _, hcategory⟩ :=
93     ActualPacketTypeRealization70.candidate_exists F E m n e D θ hmodel κ σ
94       hF hDo hB hfull hκ hβ
95   let : Nontrivial (W ⊗[ℂ] U) := GeneratedIrreducibility.nontrivial_space Λ
96   let hJH : compact F E m n e D θ ≤ extended F E m n e D θ := le_sup_left
97   have hrestrict : Λ.comp (Subgroup.inclusion hJH) =
98       CompactTypeTensor58.action (reduction F E m n e D θ hmodel) κ σ := by
99     apply MonoidHom.ext
100     intro j
101     exact hr j
102   have hI := FullTypeIntertwining105.full_locus
103     (valuation E).integer.subtype (IsLocalRing.residue 𝒪[E])
104     IsLocalRing.residue_surjective π hπ hπred hCartan σ hσc
105     (centralizerMap F E m n e) (compact F E m n e D θ)
106     (extended F E m n e D θ) hJH
107     (fun u => integralMatrix_mem_compactGroup F E m n e D θ hB u)
108     (fun c => (show (unitsEmbedding F E n (scalarMatrixEmbedding F E m n e)).range ≤
109       extended F E m n e D θ from le_sup_right)
110         ⟨c, (centralizer_scalar F E m n e c).symm⟩)
111     Λ (by
112       intro g hg
113       rw [hrestrict] at hg
114       exact hBK532 g hg)
115   obtain ⟨hn, hsm, hir, _⟩ := hcategory hI
116   exact ⟨hfin, Λ, hr, hi, hs, hI, hinj, hn, hsm, hir⟩
117 
118 end PaperXI.ActualCuspidalCandidate105

Back to source controls