ActualCharacterCandidate108.lean

1 import PaperXI.ActualCharacterData108
2 
3 /-! Character attachment removes a redundant beta-support input. Character
4 support and the Heisenberg Hom dimension are still arithmetic hypotheses. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperXI.ActualCharacterCandidate108
8 open Matrix ValuativeRel Representation
9 open scoped TensorProduct
10 open ActualCharacterType61 ActualCharacterIdentification61 ActualCharacterResidue61
11 open ActualELatticeTopology60 ActualELatticeResidue59 ActualEmbeddedUniformizer58
12 open LatticeCongruenceTopology60 ActualFieldTypeQuotient69
13 open PaperXI.IntertwiningAlong105 ActualCuspidalCandidate105
14 
15 variable (F E : Type*) [Field F] [ValuativeRel F] [TopologicalSpace F]
16   [IsNonarchimedeanLocalField F] [Field E] [ValuativeRel E] [TopologicalSpace E]
17   [IsNonarchimedeanLocalField E] [Algebra F E]
18 variable (m n : Type*) [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n]
19   [Nonempty n] (e : (m → E) ≃L[F] (n → F))
20   (D : Subgroup (GL n F)) (θ : D →* ℂˣ)
21 
22 variable (hDc : D ≤ matrixCongruence F E m n e)
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     (hc : ActualCharacterData108.Contains F E m n e D θ hDc κ)
47     (hθsupport : ∀ g : GL n F,
48       NormalizerIntertwining60.IntertwinedAt D (MonomialInduction.scalarRepresentation θ) 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     (hηdimension : ∀ y : GL m E,
52       Module.finrank ℂ (IntertwiningSpace107.space
53         ((compact F E m n e D θ).subtype.comp (firstSubgroup F E m n e D θ).subtype)
54         (κ.comp (firstSubgroup F E m n e D θ).subtype) (centralizerMap F E m n e y)) = 1) :
55     FiniteDimensional ℂ (W ⊗[ℂ] U) ∧
56     ∃ Λ : Representation ℂ (extended F E m n e D θ) (W ⊗[ℂ] U),
57       (∀ j : compact F E m n e D θ,
58         Λ (PrescribedFieldType70.compactInclusion F E n (scalarMatrixEmbedding F E m n e)
59           (compact F E m n e D θ) j) =
60           CompactTypeTensor58.action (reduction F E m n e D θ hmodel) κ σ j) ∧
61       IsIrreducible Λ ∧ SmoothDegreeQuotient.IsSmooth Λ ∧
62       FullIntertwiningLocus69.locus (extended F E m n e D θ) Λ =
63         (extended F E m n e D θ : Set (GL n F)) ∧
64       Function.Injective (TensorTypeOperators70.realize (extended F E m n e D θ) Λ) ∧
65       Nontrivial (IndV (extended F E m n e D θ).subtype Λ) ∧
66       SmoothDegreeQuotient.IsSmooth (ind (extended F E m n e D θ).subtype Λ) ∧
67       IsIrreducible (ind (extended F E m n e D θ).subtype Λ) := by
68   have hs := ActualCharacterData108.scalar_restriction F E m n e D θ hDc κ hc
69   have hDJ := ActualCharacterData108.domain_le_compact F E m n e D θ hDc
70   have hDN := ActualCharacterData108.intoCompact_mem_first F E m n e D θ hDc
71   have hηsupport : ∀ g : GL n F,
72       ExistsAt ((compact F E m n e D θ).subtype.comp
73         (firstSubgroup F E m n e D θ).subtype)
74         (κ.comp (firstSubgroup F E m n e D θ).subtype) g →
75       ∃ j₁ j₂ : compact F E m n e D θ, ∃ y : GL m E,
76         g = (j₁ : GL n F) * centralizerMap F E m n e y * (j₂ : GL n F) := by
77     intro g hg
78     exact hθsupport g ((CharacterSupport108.restricted_iff_character D
79       (compact F E m n e D θ) hDJ (firstSubgroup F E m n e D θ) hDN θ κ hs hβ g).mp hg)
80   have hβB : ∀ y : GL m E,
81       ExistsAt (compact F E m n e D θ).subtype κ (centralizerMap F E m n e y) := by
82     intro y
83     exact CharacterSupport108.beta_of_dimension_pos D (compact F E m n e D θ)
84       hDJ (firstSubgroup F E m n e D θ) hDN θ κ hs hβ (centralizerMap F E m n e y)
85       (by rw [hηdimension]; exact Nat.zero_lt_one)
86   exact ActualHeisenbergCandidate107.candidate_exists F E m n e D θ hmodel κ σ
87     hF hDo hB hfull hκ hβ hσc hηsupport hηdimension hβB
88 
89 end PaperXI.ActualCharacterCandidate108

Back to source controls