ActualProfileCandidate110.lean

1 import PaperXI.DegreeIndex110
2 
3 /-! The existing actual candidate from original eta trace support, centralizer
4 character covariance and the oriented ambient index identity. The degree,
5 finite quotient and Heisenberg Hom dimension are derived, not supplied.
6 Actual simple-character and category instantiation remains separate. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.ActualProfileCandidate110
10 open Matrix ValuativeRel Representation
11 open scoped TensorProduct
12 open ActualCharacterType61 ActualCharacterIdentification61 ActualCharacterResidue61
13 open ActualELatticeTopology60 ActualELatticeResidue59 ActualEmbeddedUniformizer58
14 open LatticeCongruenceTopology60 ActualFieldTypeQuotient69
15 open PaperXI.IntertwiningAlong105 ActualCuspidalCandidate105
16 open DegreeIndex110 IntersectionModel108
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 variable (hDc : D ≤ matrixCongruence F E m n e)
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 original candidate retains its literal theta, kappa and tensor carrier.
33 Its eta-dimension input is discharged from the three explicit arithmetic leaves. -/
34 theorem candidate_exists_from_original_profiles
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     (hc : ActualCharacterData108.Contains F E m n e D θ hDc κ)
50     (hθsupport : ∀ g : GL n F,
51       NormalizerIntertwining60.IntertwinedAt D (MonomialInduction.scalarRepresentation θ) g →
52       ∃ j₁ j₂ : compact F E m n e D θ, ∃ y : GL m E,
53         g = (j₁ : GL n F) * centralizerMap F E m n e y * (j₂ : GL n F))
54     (hz : ∀ x : firstSubgroup F E m n e D θ,
55       x ∉ actualScalarSubgroup F E m n e D θ →
56       Representation.character (ActualIntersection108.restriction F E m n e D θ κ) x = 0)
57     (hcov : ∀ y : GL m E,
58       ∀ p : pairs (ActualIntersection108.embedding F E m n e D θ)
59         (centralizerMap F E m n e y),
60       ∀ h₁ : left (ActualIntersection108.embedding F E m n e D θ)
61         (centralizerMap F E m n e y) p ∈ actualScalarSubgroup F E m n e D θ,
62       ∀ h₂ : right (ActualIntersection108.embedding F E m n e D θ)
63         (centralizerMap F E m n e y) p ∈ actualScalarSubgroup F E m n e D θ,
64       actualScalarCharacter F E m n e D θ
65         ⟨left (ActualIntersection108.embedding F E m n e D θ)
66           (centralizerMap F E m n e y) p, h₁⟩ =
67       actualScalarCharacter F E m n e D θ
68         ⟨right (ActualIntersection108.embedding F E m n e D θ)
69           (centralizerMap F E m n e y) p, h₂⟩)
70     (hindex : ∀ y : GL m E,
71       ((ActualIntersection108.embedding F E m n e D θ).range ⊓
72         (ActualIntersection108.embedding F E m n e D θ).range.comap
73           (MulAut.conj (centralizerMap F E m n e y)).toMonoidHom).relIndex
74             (ActualIntersection108.embedding F E m n e D θ).range =
75       (D ⊓ D.comap (MulAut.conj (centralizerMap F E m n e y)).toMonoidHom).relIndex D) :
76     FiniteDimensional ℂ (W ⊗[ℂ] U) ∧
77     ∃ Λ : Representation ℂ (extended F E m n e D θ) (W ⊗[ℂ] U),
78       (∀ j : compact F E m n e D θ,
79         Λ (PrescribedFieldType70.compactInclusion F E n (scalarMatrixEmbedding F E m n e)
80           (compact F E m n e D θ) j) =
81           CompactTypeTensor58.action (reduction F E m n e D θ hmodel) κ σ j) ∧
82       IsIrreducible Λ ∧ SmoothDegreeQuotient.IsSmooth Λ ∧
83       FullIntertwiningLocus69.locus (extended F E m n e D θ) Λ =
84         (extended F E m n e D θ : Set (GL n F)) ∧
85       Function.Injective (TensorTypeOperators70.realize (extended F E m n e D θ) Λ) ∧
86       Nontrivial (IndV (extended F E m n e D θ).subtype Λ) ∧
87       SmoothDegreeQuotient.IsSmooth (ind (extended F E m n e D θ).subtype Λ) ∧
88       IsIrreducible (ind (extended F E m n e D θ).subtype Λ) := by
89   have hηdimension := DegreeIndex110.actual_eta_dimension_ambient F E m n e D θ hDc κ
90     hF hDo hκ hc hz hcov hindex
91   exact ActualCharacterCandidate108.candidate_exists F E m n e D θ hDc hmodel κ σ
92     hF hDo hB hfull hκ hβ hσc hc hθsupport hηdimension
93 
94 end PaperXI.ActualProfileCandidate110

Back to source controls