ActualCartanCandidate106.lean

1 import PaperXI.ActualLocalCartan106
2 import PaperXI.ActualCuspidalCandidate105
3 
4 /-! The same candidate constructor with Cartan decomposition discharged from
5 actual local-field structure. The BK tensor reduction remains explicit. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.ActualCartanCandidate106
9 open Matrix ValuativeRel Representation
10 open scoped TensorProduct
11 open ActualCharacterType61 ActualCharacterIdentification61 ActualCharacterResidue61
12 open ActualELatticeTopology60 ActualELatticeResidue59 ActualEmbeddedUniformizer58
13 open LatticeCongruenceTopology60 ActualFieldTypeQuotient69
14 open PaperXI.IntertwiningAlong105 ActualCuspidalCandidate105
15 
16 variable (F E : Type*) [Field F] [ValuativeRel F] [TopologicalSpace F]
17   [IsNonarchimedeanLocalField F] [Field E] [ValuativeRel E] [TopologicalSpace E]
18   [IsNonarchimedeanLocalField E] [Algebra F E]
19 variable (m n : Type*) [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n]
20   [Nonempty n] (e : (m → E) ≃L[F] (n → F))
21   (D : Subgroup (GL n F)) (θ : D →* ℂˣ)
22 
23 variable (hmodel : compact F E m n e D θ ≤ matrixType F E m n e)
24 variable {W U : Type*} [AddCommGroup W] [Module ℂ W] [FiniteDimensional ℂ W]
25   [AddCommGroup U] [Module ℂ U]
26   (κ : Representation ℂ (compact F E m n e D θ) W)
27   (σ : Representation ℂ (GL m 𝓀[E]) U)
28 
29 /-- The constructor keeps the same theta, residue map, kappa and tensor carrier.
30 No whole-type extension, full-H bound, or induced irreducibility is an input. -/
31 theorem candidate_exists
32     (hF : Continuous (algebraMap F E))
33     (hDo : IsOpen (D : Set (GL n F)))
34     (hB : ∀ u : GL m 𝒪[E],
35       (coordinateAut e).symm (integralMatrix F E m u) ∈ CharacterNormalizer61.normalizer D θ)
36     (hfull : ∀ g : GL n F,
37       g ∈ CharacterNormalizer61.normalizer D θ ↔
38         ∃ a : Eˣ, ∃ j : compact F E m n e D θ,
39           unitsEmbedding F E n (scalarMatrixEmbedding F E m n e) a * (j : GL n F) = g)
40     [IsIrreducible (κ.comp (firstSubgroup F E m n e D θ).subtype)] [IsIrreducible σ]
41     (hκ : SmoothDegreeQuotient.IsSmooth κ)
42     (hβ : ∀ g : GL n F,
43       NormalizerIntertwining60.IntertwinedAt D (MonomialInduction.scalarRepresentation θ) g →
44       NormalizerIntertwining60.IntertwinedAt (compact F E m n e D θ) κ g)
45     (hσc : CuspidalCartan105.Cuspidal σ)
46     (hBK532 : ∀ g : GL n F,
47       ExistsAt (compact F E m n e D θ).subtype
48         (CompactTypeTensor58.action (reduction F E m n e D θ hmodel) κ σ) g →
49       ∃ j₁ j₂ : compact F E m n e D θ, ∃ y : GL m E,
50         g = (j₁ : GL n F) * centralizerMap F E m n e y * (j₂ : GL n F) ∧
51         ExistsAt (ActualIntegralGeneralLinear.embedding E m)
52           (σ.comp (ActualResidueGeneralLinear.reduction E m)) y) :
53     FiniteDimensional ℂ (W ⊗[ℂ] U) ∧
54     ∃ Λ : Representation ℂ (extended F E m n e D θ) (W ⊗[ℂ] U),
55       (∀ j : compact F E m n e D θ,
56         Λ (PrescribedFieldType70.compactInclusion F E n (scalarMatrixEmbedding F E m n e)
57           (compact F E m n e D θ) j) =
58           CompactTypeTensor58.action (reduction F E m n e D θ hmodel) κ σ j) ∧
59       IsIrreducible Λ ∧ SmoothDegreeQuotient.IsSmooth Λ ∧
60       FullIntertwiningLocus69.locus (extended F E m n e D θ) Λ =
61         (extended F E m n e D θ : Set (GL n F)) ∧
62       Function.Injective (TensorTypeOperators70.realize (extended F E m n e D θ) Λ) ∧
63       Nontrivial (IndV (extended F E m n e D θ).subtype Λ) ∧
64       SmoothDegreeQuotient.IsSmooth (ind (extended F E m n e D θ).subtype Λ) ∧
65       IsIrreducible (ind (extended F E m n e D θ).subtype Λ) := by
66   let : Nonempty m := by
67     classical
68     by_contra h
69     let : IsEmpty m := not_nonempty_iff.mp h
70     have he : (0 : n → F) = 1 := e.symm.injective (Subsingleton.elim _ _)
71     exact zero_ne_one he
72   let π := ActualLocalUnitDecomposition.uniformizer E
73   have hp0 : (π : E) ≠ 0 := ActualLocalUnitDecomposition.uniformizer_ne_zero E
74   have hpred := ActualLocalCartan106.uniformizer_residue_zero E
75   have hc := ActualLocalCartan106.hasCartan E m
76   exact ActualCuspidalCandidate105.candidate_exists F E m n e D θ hmodel κ σ
77     hF hDo hB hfull hκ hβ π hp0 hpred hc hσc hBK532
78 
79 end PaperXI.ActualCartanCandidate106

Back to source controls