ActualSourceCandidate111.lean

1 import PaperXI.ActualProfileCandidate110
2 import PaperXI.HeisenbergCharacterProfile111
3 import PaperXI.ActualGroupIndex111
4 
5 /-! The original candidate from exact type quotient/form data and literal
6 one-plus/Morita lattice matches. Trace support, covariance, finite quotient,
7 degree-square and the ambient index equality are derived. The input record
8 still requires its canonical type-theoretic instance; this is not Claim16.2. -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace PaperXI.ActualSourceCandidate111
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 open DegreeIndex110 IntersectionModel108
19 open HeisenbergCharacterProfile111 ActualGroupIndex111
20 
21 variable (F E : Type*) [Field F] [ValuativeRel F] [TopologicalSpace F]
22   [IsNonarchimedeanLocalField F] [Field E] [ValuativeRel E] [TopologicalSpace E]
23   [IsNonarchimedeanLocalField E] [Algebra F E]
24 variable (m n : Type*) [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n]
25   [Nonempty n] (e : (m → E) ≃L[F] (n → F))
26   (D : Subgroup (GL n F)) (θ : D →* ℂˣ)
27 
28 variable (hDc : D ≤ matrixCongruence F E m n e)
29 variable (hmodel : compact F E m n e D θ ≤ matrixType F E m n e)
30 variable {W U : Type*} [AddCommGroup W] [Module ℂ W] [FiniteDimensional ℂ W]
31   [AddCommGroup U] [Module ℂ U]
32   (κ : Representation ℂ (compact F E m n e D θ) W)
33   (σ : Representation ℂ (GL m 𝓀[E]) U)
34 
35 variable {k X : Type*} [Field k] [AddCommGroup X] [Module k X]
36 
37 /-- Retain the original theta, kappa and tensor carrier. No trace, covariance,
38 eta Hom dimension, index equality, deep ideal or additive openness is assumed.
39 The source quotient/form and actual lattice dictionary remain explicit inputs. -/
40 theorem candidate_exists_from_source_dictionary
41     (hF : Continuous (algebraMap F E))
42     (hDo : IsOpen (D : Set (GL n F)))
43     (hB : ∀ u : GL m 𝒪[E],
44       (coordinateAut e).symm (integralMatrix F E m u) ∈ CharacterNormalizer61.normalizer D θ)
45     (hfull : ∀ g : GL n F,
46       g ∈ CharacterNormalizer61.normalizer D θ ↔
47         ∃ a : Eˣ, ∃ j : compact F E m n e D θ,
48           unitsEmbedding F E n (scalarMatrixEmbedding F E m n e) a * (j : GL n F) = g)
49     [IsIrreducible (κ.comp (firstSubgroup F E m n e D θ).subtype)] [IsIrreducible σ]
50     (hκ : SmoothDegreeQuotient.IsSmooth κ)
51     (hβ : ∀ g : GL n F,
52       NormalizerIntertwining60.IntertwinedAt D (MonomialInduction.scalarRepresentation θ) g →
53       NormalizerIntertwining60.IntertwinedAt (compact F E m n e D θ) κ g)
54     (hσc : CuspidalCartan105.Cuspidal σ)
55     (hc : ActualCharacterData108.Contains F E m n e D θ hDc κ)
56     (hθsupport : ∀ g : GL n F,
57       NormalizerIntertwining60.IntertwinedAt D (MonomialInduction.scalarRepresentation θ) g →
58       ∃ j₁ j₂ : compact F E m n e D θ, ∃ y : GL m E,
59         g = (j₁ : GL n F) * centralizerMap F E m n e y * (j₂ : GL n F))
60     (τ : ((firstSubgroup F E m n e D θ) ⧸
61       actualScalarSubgroup F E m n e D θ) ≃* Multiplicative X)
62     (B : X →ₗ[k] X →ₗ[k] k) (ψ : AddChar k ℂˣ) (hψ : ψ ≠ 1)
63     (hnd : ∀ v : X, (∀ u : X, B u v = 0) → v = 0)
64     (hform : ∀ x y : firstSubgroup F E m n e D θ,
65       ψ (B (coordinate (actualScalarSubgroup F E m n e D θ) τ x)
66         (coordinate (actualScalarSubgroup F E m n e D θ) τ y)) =
67       characterCommutator (actualScalarSubgroup F E m n e D θ) τ
68         (actualScalarCharacter F E m n e D θ) x y)
69     (hθcentralizer : ∀ y : GL m E, NormalizerIntertwining60.IntertwinedAt D
70       (MonomialInduction.scalarRepresentation θ) (centralizerMap F E m n e y))
71     (data : ActualLatticeData F E m n e D θ) :
72     FiniteDimensional ℂ (W ⊗[ℂ] U) ∧
73     ∃ Λ : Representation ℂ (extended F E m n e D θ) (W ⊗[ℂ] U),
74       (∀ j : compact F E m n e D θ,
75         Λ (PrescribedFieldType70.compactInclusion F E n (scalarMatrixEmbedding F E m n e)
76           (compact F E m n e D θ) j) =
77           CompactTypeTensor58.action (reduction F E m n e D θ hmodel) κ σ j) ∧
78       IsIrreducible Λ ∧ SmoothDegreeQuotient.IsSmooth Λ ∧
79       FullIntertwiningLocus69.locus (extended F E m n e D θ) Λ =
80         (extended F E m n e D θ : Set (GL n F)) ∧
81       Function.Injective (TensorTypeOperators70.realize (extended F E m n e D θ) Λ) ∧
82       Nontrivial (IndV (extended F E m n e D θ).subtype Λ) ∧
83       SmoothDegreeQuotient.IsSmooth (ind (extended F E m n e D θ).subtype Λ) ∧
84       IsIrreducible (ind (extended F E m n e D θ).subtype Λ) := by
85   have : Nonempty m := by
86     by_contra hm
87     have : IsEmpty m := not_nonempty_iff.mp hm
88     have h : (0 : n → F) = 1 := e.symm.injective (Subsingleton.elim _ _)
89     exact zero_ne_one h
90   let c : E →ₗ[F] (m → E) := LinearMap.pi (fun _ => LinearMap.id)
91   have hc_inj : Function.Injective c := by
92     intro x y h
93     exact congrFun h (Classical.choice (inferInstance : Nonempty m))
94   let : FiniteDimensional F E := FiniteDimensional.of_injective
95     (e.toLinearMap.comp c) (e.injective.comp hc_inj)
96   have hηdimension := actual_eta_dimension_from_quotient_form F E m n e D θ hDc κ
97     hF hDo hκ hc τ B ψ hψ hnd hform hθcentralizer
98     (ActualLatticeData.actual_index F n E m e D θ data hF hDo)
99   exact ActualCharacterCandidate108.candidate_exists F E m n e D θ hDc hmodel κ σ
100     hF hDo hB hfull hκ hβ hσc hc hθsupport hηdimension
101 
102 end PaperXI.ActualSourceCandidate111

Back to source controls