ActualHeisenbergCandidate107.lean

1 import PaperXI.ActualCartanCandidate106
2 import PaperXI.ResidueRestriction107
3 import PaperXI.HeisenbergReduction107
4 import PaperXI.IntertwiningSpace107
5 
6 /-! The same arithmetic candidate, with the BK tensor-to-residue implication
7 proved internally from explicit Heisenberg support and intertwining-line inputs.
8 Those arithmetic Heisenberg inputs remain unproved here. -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace PaperXI.ActualHeisenbergCandidate107
12 open Matrix ValuativeRel Representation
13 open scoped TensorProduct
14 open ActualCharacterType61 ActualCharacterIdentification61 ActualCharacterResidue61
15 open ActualELatticeTopology60 ActualELatticeResidue59 ActualEmbeddedUniformizer58
16 open LatticeCongruenceTopology60 ActualFieldTypeQuotient69
17 open PaperXI.IntertwiningAlong105 ActualCuspidalCandidate105
18 
19 variable (F E : Type*) [Field F] [ValuativeRel F] [TopologicalSpace F]
20   [IsNonarchimedeanLocalField F] [Field E] [ValuativeRel E] [TopologicalSpace E]
21   [IsNonarchimedeanLocalField E] [Algebra F E]
22 variable (m n : Type*) [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n]
23   [Nonempty n] (e : (m → E) ≃L[F] (n → F))
24   (D : Subgroup (GL n F)) (θ : D →* ℂˣ)
25 
26 variable (hmodel : compact F E m n e D θ ≤ matrixType F E m n e)
27 variable {W U : Type*} [AddCommGroup W] [Module ℂ W] [FiniteDimensional ℂ W]
28   [AddCommGroup U] [Module ℂ U]
29   (κ : Representation ℂ (compact F E m n e D θ) W)
30   (σ : Representation ℂ (GL m 𝓀[E]) U)
31 
32 /-- The constructor keeps the same theta, residue map, kappa and tensor carrier.
33 No whole-type extension, full-H bound, or induced irreducibility is an input. -/
34 theorem candidate_exists
35     (hF : Continuous (algebraMap F E))
36     (hDo : IsOpen (D : Set (GL n F)))
37     (hB : ∀ u : GL m 𝒪[E],
38       (coordinateAut e).symm (integralMatrix F E m u) ∈ CharacterNormalizer61.normalizer D θ)
39     (hfull : ∀ g : GL n F,
40       g ∈ CharacterNormalizer61.normalizer D θ ↔
41         ∃ a : Eˣ, ∃ j : compact F E m n e D θ,
42           unitsEmbedding F E n (scalarMatrixEmbedding F E m n e) a * (j : GL n F) = g)
43     [IsIrreducible (κ.comp (firstSubgroup F E m n e D θ).subtype)] [IsIrreducible σ]
44     (hκ : SmoothDegreeQuotient.IsSmooth κ)
45     (hβ : ∀ g : GL n F,
46       NormalizerIntertwining60.IntertwinedAt D (MonomialInduction.scalarRepresentation θ) g →
47       NormalizerIntertwining60.IntertwinedAt (compact F E m n e D θ) κ g)
48     (hσc : CuspidalCartan105.Cuspidal σ)
49     (hηsupport : ∀ g : GL n F,
50       ExistsAt ((compact F E m n e D θ).subtype.comp
51         (firstSubgroup F E m n e D θ).subtype)
52         (κ.comp (firstSubgroup F E m n e D θ).subtype) g →
53       ∃ j₁ j₂ : compact F E m n e D θ, ∃ y : GL m E,
54         g = (j₁ : GL n F) * centralizerMap F E m n e y * (j₂ : GL n F))
55     (hηdimension : ∀ y : GL m E,
56       Module.finrank ℂ (IntertwiningSpace107.space
57         ((compact F E m n e D θ).subtype.comp (firstSubgroup F E m n e D θ).subtype)
58         (κ.comp (firstSubgroup F E m n e D θ).subtype) (centralizerMap F E m n e y)) = 1)
59     (hβB : ∀ y : GL m E,
60       ExistsAt (compact F E m n e D θ).subtype κ (centralizerMap F E m n e y)) :
61     FiniteDimensional ℂ (W ⊗[ℂ] U) ∧
62     ∃ Λ : Representation ℂ (extended F E m n e D θ) (W ⊗[ℂ] U),
63       (∀ j : compact F E m n e D θ,
64         Λ (PrescribedFieldType70.compactInclusion F E n (scalarMatrixEmbedding F E m n e)
65           (compact F E m n e D θ) j) =
66           CompactTypeTensor58.action (reduction F E m n e D θ hmodel) κ σ j) ∧
67       IsIrreducible Λ ∧ SmoothDegreeQuotient.IsSmooth Λ ∧
68       FullIntertwiningLocus69.locus (extended F E m n e D θ) Λ =
69         (extended F E m n e D θ : Set (GL n F)) ∧
70       Function.Injective (TensorTypeOperators70.realize (extended F E m n e D θ) Λ) ∧
71       Nontrivial (IndV (extended F E m n e D θ).subtype Λ) ∧
72       SmoothDegreeQuotient.IsSmooth (ind (extended F E m n e D θ).subtype Λ) ∧
73       IsIrreducible (ind (extended F E m n e D θ).subtype Λ) := by
74   have hN : firstSubgroup F E m n e D θ ≤ (reduction F E m n e D θ hmodel).ker := by
75     rw [reduction_kernel]
76   have hBK532 := HeisenbergReduction107.integral_reduction
77     (compact F E m n e D θ).subtype (firstSubgroup F E m n e D θ)
78     (reduction F E m n e D θ hmodel) hN κ σ (centralizerMap F E m n e)
79     (ActualIntegralGeneralLinear.embedding E m)
80     (ResidueRestriction107.integralInclusion F E m n e D θ hB)
81     (ActualResidueGeneralLinear.reduction E m) (fun _ => rfl)
82     (ResidueRestriction107.reduction_integral F E m n e D θ hmodel hB)
83     hηsupport (fun y => IntertwiningSpace107.line_of_dimension
84       (compact F E m n e D θ).subtype (firstSubgroup F E m n e D θ) κ
85       (centralizerMap F E m n e y) (hηdimension y) (hβB y))
86   exact ActualCartanCandidate106.candidate_exists F E m n e D θ hmodel κ σ
87     hF hDo hB hfull hκ hβ hσc hBK532
88 
89 end PaperXI.ActualHeisenbergCandidate107

Back to source controls