ArithmeticFieldInduction69.lean

1 import PaperXI.ActualFieldTypeQuotient69
2 import PaperXI.DerivedCentralCharacter69
3 import PaperXI.CompactModCenterInduction68
4 import Mathlib.Analysis.Complex.Polynomial.Basic
5 
6 /-! The compact-mod-center induction theorem specialized to literal local-field matrices.
7 The actual field scalar subgroup and compact quotient are constructed. The common
8 scalar character is derived from finite-dimensional irreducibility, not supplied. -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace PaperXI.ArithmeticFieldInduction69
12 open Matrix ValuativeRel Representation
13 open ActualEmbeddedUniformizer58 ActualFieldTypeQuotient69
14 open PaperXI.InductionIrreducibility PaperXI.SmoothDegreeQuotient
15 
16 variable (F E : Type*) [Field F] [ValuativeRel F] [TopologicalSpace F]
17   [IsNonarchimedeanLocalField F]
18   [Field E] [ValuativeRel E] [TopologicalSpace E]
19   [IsNonarchimedeanLocalField E] [Algebra F E]
20 variable (n : Type*) [Fintype n] [DecidableEq n] [Nonempty n]
21   (ι : E →ₐ[F] Matrix n n F) (J : Subgroup (GeneralLinearGroup n F))
22 variable {V : Type*} [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V]
23   (Λ : Representation ℂ (fieldGroup F E n ι J) V) [IsIrreducible Λ]
24 
25 omit [ValuativeRel E] [TopologicalSpace E] [IsNonarchimedeanLocalField E] [Nonempty n] in
26 /-- Openness of the compact type subgroup implies openness of the actual field join. -/
27 theorem fieldGroup_open (hJ : IsOpen (J : Set (GeneralLinearGroup n F))) :
28     IsOpen (fieldGroup F E n ι J : Set (GeneralLinearGroup n F)) :=
29   Subgroup.isOpen_mono le_sup_left hJ
30 
31 /-- The derived scalar character on the literal base-field scalar subgroup. -/
32 def scalarCharacter : scalarSubgroup F E n ι J →* ℂˣ :=
33   DerivedCentralCharacter69.character Λ (scalarSubgroup F E n ι J)
34     (fun z g => Subtype.ext (scalar_central F E n ι J z g).eq)
35 
36 omit [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F]
37   [ValuativeRel E] [TopologicalSpace E] [IsNonarchimedeanLocalField E] [Nonempty n] in
38 theorem scalarCharacter_action (z : scalarSubgroup F E n ι J) (v : V) :
39     Λ (z : fieldGroup F E n ι J) v = (scalarCharacter F E n ι J Λ z : ℂ) • v :=
40   DerivedCentralCharacter69.character_apply Λ (scalarSubgroup F E n ι J)
41     (fun z g => Subtype.ext (scalar_central F E n ι J z g).eq) z v
42 
43 /-- Actual arithmetic specialization: no compact-quotient or scalar-character
44 hypothesis is received. The full-H intertwining condition remains explicit and
45 must be obtained from the supplied genuine extended type. -/
46 theorem induction_package
47     (hF : Continuous (algebraMap F E))
48     (hJcompact : IsCompact (J : Set (GeneralLinearGroup n F)))
49     (hJopen : IsOpen (J : Set (GeneralLinearGroup n F)))
50     (ht : embeddedUniformizer F E n ι ∈ Subgroup.normalizer (J : Set (GeneralLinearGroup n F)))
51     (hu : ∀ u : 𝒪[E]ˣ, unitsEmbedding F E n ι (ActualLocalUnitTopology.unitEmbedding E u) ∈ J)
52     (hΛ : IsSmooth Λ)
53     (hM : ∀ g : GeneralLinearGroup n F, g ∉ fieldGroup F E n ι J →
54       ∀ A : IntertwiningMap
55         (Λ.comp (intersectionSubgroup (fieldGroup F E n ι J) g).subtype)
56         (Λ.comp (intersectionConjugation (fieldGroup F E n ι J) g)), A = 0) :
57     Nontrivial (IndV (fieldGroup F E n ι J).subtype Λ) ∧
58       IsSmooth (ind (fieldGroup F E n ι J).subtype Λ) ∧
59       IsIrreducible (ind (fieldGroup F E n ι J).subtype Λ) := by
60   let : CompactSpace (fieldGroup F E n ι J ⧸ scalarSubgroup F E n ι J) :=
61     quotient_compact F E n ι J hF hJcompact ht hu
62   exact CompactModCenterInduction68.induction_package
63     (fieldGroup F E n ι J) Λ (scalarSubgroup F E n ι J)
64     (scalarCharacter F E n ι J Λ)
65     (scalar_central F E n ι J)
66     (scalarCharacter_action F E n ι J Λ)
67     (fieldGroup_open F E n ι J hJopen) hΛ hM
68 
69 omit [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F]
70   [ValuativeRel E] [TopologicalSpace E] [IsNonarchimedeanLocalField E] [Nonempty n] in
71 /-- The same derived character acts on every vector of the actual induced carrier. -/
72 theorem induced_scalar (z : scalarSubgroup F E n ι J)
73     (w : IndV (fieldGroup F E n ι J).subtype Λ) :
74     ind (fieldGroup F E n ι J).subtype Λ
75       (((z : fieldGroup F E n ι J) : GeneralLinearGroup n F)) w =
76         (scalarCharacter F E n ι J Λ z : ℂ) • w := by
77   exact CompactModCenterInduction68.induced_central_scalar
78     (fieldGroup F E n ι J) Λ (z : fieldGroup F E n ι J)
79     (scalar_central F E n ι J z)
80     (scalarCharacter F E n ι J Λ z : ℂ)
81     (scalarCharacter_action F E n ι J Λ z) w
82 
83 end PaperXI.ArithmeticFieldInduction69

Back to source controls