ActualIntersection108.lean

1 import PaperXI.ActualCharacterCandidate108
2 import PaperXI.FiniteIntersectionCriterion108
3 
4 /-! The canonical finite quotient for the actual first-subgroup intertwining
5 space. This proves existence of the finite model, not its arithmetic profile. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.ActualIntersection108
9 open Matrix ValuativeRel Representation
10 open ActualCharacterType61 ActualCuspidalCandidate105 IntersectionModel108
11 variable (F E : Type*) [Field F] [ValuativeRel F] [TopologicalSpace F]
12   [IsNonarchimedeanLocalField F] [Field E] [ValuativeRel E] [TopologicalSpace E]
13   [IsNonarchimedeanLocalField E] [Algebra F E]
14 variable (m n : Type*) [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n]
15   [Nonempty n] (e : (m → E) ≃L[F] (n → F))
16   (D : Subgroup (GL n F)) (θ : D →* ℂˣ)
17 variable {W : Type*} [AddCommGroup W] [Module ℂ W] [FiniteDimensional ℂ W]
18   (κ : Representation ℂ (compact F E m n e D θ) W)
19 
20 abbrev embedding := (compact F E m n e D θ).subtype.comp
21   (firstSubgroup F E m n e D θ).subtype
22 
23 abbrev restriction := κ.comp (firstSubgroup F E m n e D θ).subtype
24 
25 abbrev quotient (g : GL n F) := FiniteJointQuotient108.quotient
26   ((restriction F E m n e D θ κ).comp (left (embedding F E m n e D θ) g))
27   ((restriction F E m n e D θ κ).comp (right (embedding F E m n e D θ) g))
28 
29 /-- Finiteness at every ambient element, proved for the same prescribed kappa. -/
30 theorem finite (hF : Continuous (algebraMap F E)) (hDo : IsOpen (D : Set (GL n F)))
31     (hκ : SmoothDegreeQuotient.IsSmooth κ) (g : GL n F) :
32     Finite (quotient F E m n e D θ κ g) := by
33   let : CompactSpace (compact F E m n e D θ) := isCompact_iff_compactSpace.mp
34     (compactGroup_compact_open F E m n e D θ hF hDo).1
35   let : CompactSpace (firstSubgroup F E m n e D θ) := isCompact_iff_compactSpace.mp
36     ((firstSubgroup F E m n e D θ).isClosed_of_isOpen
37       (firstSubgroup_open F E m n e D θ hF)).isCompact
38   exact CompactIntersection108.finite_quotient (embedding F E m n e D θ)
39     (continuous_subtype_val.comp continuous_subtype_val)
40     (restriction F E m n e D θ κ)
41     (CompactIntersection108.smooth_comp κ hκ
42       (firstSubgroup F E m n e D θ).subtype continuous_subtype_val) g
43 
44 omit [ValuativeRel F] [IsNonarchimedeanLocalField F] [Fintype m] [DecidableEq m]
45   [Nonempty n] [FiniteDimensional ℂ W] in
46 /-- Actual operator dimension equals the canonical quotient Hom dimension. -/
47 theorem dimension (g : GL n F) :
48     Module.finrank ℂ (IntertwiningSpace107.space (embedding F E m n e D θ)
49       (restriction F E m n e D θ κ) g) =
50     Module.finrank ℂ (IntertwiningMap
51       (FiniteJointQuotient108.first
52         ((restriction F E m n e D θ κ).comp (left (embedding F E m n e D θ) g))
53         ((restriction F E m n e D θ κ).comp (right (embedding F E m n e D θ) g)))
54       (FiniteJointQuotient108.second
55         ((restriction F E m n e D θ κ).comp (left (embedding F E m n e D θ) g))
56         ((restriction F E m n e D θ κ).comp (right (embedding F E m n e D θ) g)))) :=
57   CompactIntersection108.finrank_quotient _ _ _
58 
59 end PaperXI.ActualIntersection108

Back to source controls