RankOneSourceCandidate110.lean

1 import PaperXI.ArithmeticAttachment110
2 import PaperXI.NormalizerDictionary110
3 
4 /-! Residue rank one from the lower-level simple-character support dictionary.
5 The model containment, compact support, integral normalization and finite
6 residue factor are derived. Canonical character data are not manufactured. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.RankOneSourceCandidate110
10 open Matrix ValuativeRel Representation
11 open scoped TensorProduct
12 open ActualCharacterType61 ActualCuspidalCandidate105
13 open ActualELatticeTopology60 LatticeCongruenceTopology60 ActualELatticeResidue59
14 open ActualEmbeddedUniformizer58
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 (n : Type*) [Fintype n] [DecidableEq n] [Nonempty n]
20   (e : (Fin 1 → E) ≃L[F] (n → F))
21   (D J₁ : Subgroup (GL n F)) (θ : D →* ℂˣ)
22   (hDc : D ≤ matrixCongruence F E (Fin 1) n e)
23 variable {W : Type*} [AddCommGroup W] [Module ℂ W] [FiniteDimensional ℂ W]
24   (κ : Representation ℂ (compact F E (Fin 1) n e D θ) W)
25 
26 /-- The original carrier and compact restriction are retained. No supplied
27 sigma, model inclusion, compact support, integral normalization, eta Hom
28 dimension, trace profile or lattice-index identity is an input in this branch. -/
29 theorem candidate_exists
30     (hF : Continuous (algebraMap F E)) (hDo : IsOpen (D : Set (GL n F)))
31     (hJ : J₁ ≤ matrixCongruence F E (Fin 1) n e)
32     (hJN : J₁ ≤ CharacterNormalizer61.normalizer D θ)
33     (hθcentralizer : ∀ g : GL n F,
34       NormalizerIntertwining60.IntertwinedAt D (MonomialInduction.scalarRepresentation θ) g →
35       ∃ a : J₁, ∃ b : (centralizerMap F E (Fin 1) n e).range,
36       ∃ c : J₁, (a : GL n F) * (b : GL n F) * (c : GL n F) = g)
37     (hfull : ∀ g : GL n F,
38       g ∈ CharacterNormalizer61.normalizer D θ ↔
39         ∃ a : Eˣ, ∃ j : compact F E (Fin 1) n e D θ,
40           unitsEmbedding F E n (scalarMatrixEmbedding F E (Fin 1) n e) a *
41             (j : GL n F) = g)
42     [IsIrreducible (κ.comp (firstSubgroup F E (Fin 1) n e D θ).subtype)]
43     (hκ : SmoothDegreeQuotient.IsSmooth κ)
44     (hβ : ∀ g : GL n F,
45       NormalizerIntertwining60.IntertwinedAt D (MonomialInduction.scalarRepresentation θ) g →
46       NormalizerIntertwining60.IntertwinedAt (compact F E (Fin 1) n e D θ) κ g)
47     (hc : ActualCharacterData108.Contains F E (Fin 1) n e D θ hDc κ) :
48     FiniteDimensional ℂ (W ⊗[ℂ] ℂ) ∧
49     ∃ Λ : Representation ℂ (extended F E (Fin 1) n e D θ) (W ⊗[ℂ] ℂ),
50       (∀ j : compact F E (Fin 1) n e D θ,
51         Λ (PrescribedFieldType70.compactInclusion F E n
52           (scalarMatrixEmbedding F E (Fin 1) n e)
53           (compact F E (Fin 1) n e D θ) j) =
54           (κ.tprod (Representation.trivial ℂ (compact F E (Fin 1) n e D θ) ℂ)) j) ∧
55       IsIrreducible Λ ∧ SmoothDegreeQuotient.IsSmooth Λ ∧
56       FullIntertwiningLocus69.locus (extended F E (Fin 1) n e D θ) Λ =
57         (extended F E (Fin 1) n e D θ : Set (GL n F)) ∧
58       Nontrivial (IndV (extended F E (Fin 1) n e D θ).subtype Λ) ∧
59       SmoothDegreeQuotient.IsSmooth (ind (extended F E (Fin 1) n e D θ).subtype Λ) ∧
60       IsIrreducible (ind (extended F E (Fin 1) n e D θ).subtype Λ) := by
61   have hB := ArithmeticAttachment110.integral_normalization_of_full_rank_one
62     F E n e D θ hfull
63   have hmodel := NormalizerDictionary110.actual_model_from_centralizer
64     F E (Fin 1) n e D θ J₁ hJ hJN hθcentralizer hB
65   have hs := NormalizerDictionary110.character_support_compact
66     F E (Fin 1) n e D θ J₁ hJ hJN hθcentralizer
67   obtain ⟨hf, Λ, hr, hi, hsm, hI, hn, hsi, hir⟩ :=
68     ArithmeticAttachment110.rank_one_candidate_exists F E n e D θ hDc hmodel κ
69       hF hDo hfull hκ hβ hc hs
70   refine ⟨hf, Λ, ?_, hi, hsm, hI, hn, hsi, hir⟩
71   intro j
72   rw [hr]
73   ext w
74   simp [CompactTypeTensor58.action, ArithmeticAttachment110.residueOne,
75     Representation.tprod_apply]
76 
77 end PaperXI.RankOneSourceCandidate110

Back to source controls