ActualDepthZeroExtension.lean

1 import PaperXI.ActualIntegralGeneralLinear
2 import PaperXI.ActualLocalUnitDecomposition
3 import PaperXI.CentralExtensionInductionConsequences
4 
5 /-!
6 # Actual depth-zero inducing data extended by the scalar uniformizer
7 
8 The subgroup, degree, free central direction and smooth inducing representation
9 are constructed from the given local field. The supplied finite representation
10 is inflated through literal residue reduction. Induced irreducibility is a
11 separate theorem: no Mackey vanishing is assumed in this construction.
12 -/
13 set_option autoImplicit false
14 noncomputable section
15 namespace PaperXI.ActualDepthZeroExtension
16 
17 open Matrix ValuativeRel
18 open ActualIntegralGeneralLinear ActualLocalUnitTopology ActualLocalUnitDecomposition
19 
20 variable (K : Type*) [Field K] [ValuativeRel K] [TopologicalSpace K]
21   [IsNonarchimedeanLocalField K]
22 variable (n : Type*) [Fintype n] [DecidableEq n]
23 
24 /-- Normalized valuation of the actual determinant. -/
25 def determinantDegree : GeneralLinearGroup n K →* Multiplicative ℤ :=
26   (degree K).comp GeneralLinearGroup.det
27 
28 /-- The scalar matrix of the chosen actual uniformizer. -/
29 def scalarUniformizer : GeneralLinearGroup n K :=
30   GeneralLinearGroup.scalar n (uniformizerUnit K)
31 
32 theorem scalarUniformizer_central (g : GeneralLinearGroup n K) :
33     Commute (scalarUniformizer K n) g := GeneralLinearGroup.scalar_commute _ _
34 
35 @[simp] theorem determinantDegree_embedding (g : GeneralLinearGroup n 𝒪[K]) :
36     determinantDegree K n (embedding K n g) = 1 := by
37   change degree K (GeneralLinearGroup.det (GeneralLinearGroup.map _ g)) = 1
38   rw [GeneralLinearGroup.map_det]
39   exact degree_unitEmbedding K (GeneralLinearGroup.det g)
40 
41 theorem integralSubgroup_le_degree_kernel :
42     integralSubgroup K n ≤ (determinantDegree K n).ker := by
43   rintro g ⟨a, rfl⟩
44   exact determinantDegree_embedding K n a
45 
46 @[simp] theorem determinantDegree_scalarUniformizer :
47     determinantDegree K n (scalarUniformizer K n) =
48       Multiplicative.ofAdd (Fintype.card n : ℤ) := by
49   simp [determinantDegree, scalarUniformizer, GeneralLinearGroup.det_scalar]
50   change Multiplicative.ofAdd ((Fintype.card n) • (1 : ℤ)) = _
51   simp
52 
53 variable [Nonempty n]
54 
55 /-- No nonzero scalar uniformizer power is integral and integrally invertible. -/
56 theorem scalarUniformizer_free :
57     ∀ r : ℤ, scalarUniformizer K n ^ r ∈ integralSubgroup K n → r = 0 := by
58   apply CentralExtensionInducing.hfree_from_degree _ (determinantDegree K n)
59     (integralSubgroup_le_degree_kernel K n)
60   rw [determinantDegree_scalarUniformizer]
61   intro h
62   have hcard : (Fintype.card n : ℤ) = 0 := congrArg Multiplicative.toAdd h
63   exact (Nat.ne_of_gt (Fintype.card_pos)).elim (Int.ofNat_eq_zero.mp hcard)
64 
65 /-- The actual subgroup obtained by adjoining the scalar uniformizer. -/
66 abbrev extendedSubgroup : Subgroup (GeneralLinearGroup n K) :=
67   CentralExtensionInducing.extendedSubgroup (integralSubgroup K n)
68     (scalarUniformizer K n) (scalarUniformizer_central K n)
69 
70 omit [Nonempty n] in
71 theorem integral_le_extended : integralSubgroup K n ≤ extendedSubgroup K n :=
72   CentralExtensionInducing.le_extendedSubgroup _ _ _
73 
74 omit [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Nonempty n] in
75 /-- Every scalar integer-ring unit is already in the integral subgroup. -/
76 theorem scalar_unit_mem_integral (u : 𝒪[K]ˣ) :
77     GeneralLinearGroup.scalar n (unitEmbedding K u) ∈ integralSubgroup K n := by
78   refine ⟨GeneralLinearGroup.scalar n u, ?_⟩
79   exact GeneralLinearGroup.map_scalar _ _
80 
81 omit [Nonempty n] in
82 /-- The subgroup is precisely the scalar extension `Kˣ GL_n(𝒪[K])`. -/
83 theorem extendedSubgroup_eq_scalar_sup :
84     extendedSubgroup K n = integralSubgroup K n ⊔ (GeneralLinearGroup.scalar n).range := by
85   rw [extendedSubgroup, CentralExtensionInducing.extendedSubgroup_eq_sup]
86   apply le_antisymm
87   · apply sup_le le_sup_left
88     apply Subgroup.zpowers_le.mpr
89     exact (show (GeneralLinearGroup.scalar n).range ≤
90       integralSubgroup K n ⊔ (GeneralLinearGroup.scalar n).range from le_sup_right)
91       (show scalarUniformizer K n ∈ (GeneralLinearGroup.scalar n).range
92       from ⟨uniformizerUnit K, rfl⟩)
93   · apply sup_le le_sup_left
94     rintro g ⟨a, rfl⟩
95     obtain ⟨⟨u, r⟩, rfl⟩ := (ActualLocalUnitDecomposition.normalFormEquiv K).surjective a
96     rw [normalFormEquiv_apply, map_mul, map_zpow]
97     exact Subgroup.mul_mem _
98       ((show integralSubgroup K n ≤ integralSubgroup K n ⊔
99         Subgroup.zpowers (scalarUniformizer K n) from le_sup_left)
100         (scalar_unit_mem_integral K n u))
101       ((show Subgroup.zpowers (scalarUniformizer K n) ≤ integralSubgroup K n ⊔
102         Subgroup.zpowers (scalarUniformizer K n) from le_sup_right)
103         (Subgroup.zpow_mem _ (Subgroup.mem_zpowers _) r.toAdd))
104 
105 omit [Nonempty n] in
106 theorem extendedSubgroup_open :
107     IsOpen (extendedSubgroup K n : Set (GeneralLinearGroup n K)) :=
108   CentralExtensionInducing.extendedSubgroup_isOpen _ _ _ (integralSubgroup_open K n)
109 
110 /-- Inclusion of the actual integral subgroup into the actual extended subgroup. -/
111 abbrev inclusion : integralSubgroup K n →* extendedSubgroup K n :=
112   CentralExtensionInducing.subgroupInclusion _ _ _
113 
114 variable {V : Type*} [AddCommGroup V] [Module ℂ V]
115 variable (σ : Representation ℂ (GeneralLinearGroup n 𝓀[K]) V) (c : ℂˣ)
116 
117 /-- Extend the actual residue inflation with the prescribed uniformizer scalar. -/
118 abbrev extendedRepresentation : Representation ℂ (extendedSubgroup K n) V :=
119   CentralExtensionInducing.extendedRepresentation _ _ _ (scalarUniformizer_free K n)
120     (inflated K n σ) c
121 
122 @[simp] theorem extendedRepresentation_restrict (j : integralSubgroup K n) :
123     extendedRepresentation K n σ c (inclusion K n j) = inflated K n σ j :=
124   CentralExtensionInducing.extendedRepresentation_restrict _ _ _ _ _ _ _
125 
126 theorem extendedRepresentation_irreducible [Representation.IsIrreducible σ] :
127     Representation.IsIrreducible (extendedRepresentation K n σ c) := by
128   let := inflated_irreducible K n σ
129   exact CentralExtensionInducing.extendedRepresentation_irreducible _ _ _ _ _ _
130 
131 theorem extendedRepresentation_smooth :
132     SmoothDegreeQuotient.IsSmooth (extendedRepresentation K n σ c) :=
133   CentralExtensionInducing.extendedRepresentation_smooth _ _ _ _ _ _
134     (integralSubgroup_open K n) (inflated_isSmooth K n σ)
135 
136 /-- Actual algebraic compact induction from the open extended integral subgroup. -/
137 abbrev inducedRepresentation :=
138   CentralExtensionInductionConsequences.inducedRepresentation (integralSubgroup K n)
139     (scalarUniformizer K n) (scalarUniformizer_central K n) (scalarUniformizer_free K n)
140     (inflated K n σ) c
141 
142 theorem induced_smooth : SmoothDegreeQuotient.IsSmooth (inducedRepresentation K n σ c) :=
143   CentralExtensionInductionConsequences.induced_isSmooth _ _ _ _ _ _
144     (integralSubgroup_open K n) (inflated_isSmooth K n σ)
145 
146 theorem induced_nontrivial [Nontrivial V] :
147     Nontrivial (Representation.IndV (extendedSubgroup K n).subtype
148       (extendedRepresentation K n σ c)) :=
149   CentralExtensionInductionConsequences.induced_nontrivial _ _ _ _ _ _
150 
151 theorem induced_scalar : inducedRepresentation K n σ c (scalarUniformizer K n) =
152     (c : ℂ) • LinearMap.id :=
153   CentralExtensionInductionConsequences.induced_central_scalar _ _ _ _ _ _
154 
155 end PaperXI.ActualDepthZeroExtension

Back to source controls