ArithmeticTypeCertificate69.lean

1 import PaperXI.ArithmeticFieldInduction69
2 import PaperXI.FullIntertwiningLocus69
3 import Mathlib.Topology.LocallyConstant.Basic
4 
5 /-! The actual base-field central character and the full intertwining-locus
6 application. No auxiliary scalar action or quotient compactness is assumed. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.ArithmeticTypeCertificate69
10 open Matrix ValuativeRel Representation
11 open ActualEmbeddedUniformizer58 ActualFieldTypeQuotient69 ArithmeticFieldInduction69
12 open PaperXI.InductionIrreducibility PaperXI.SmoothDegreeQuotient
13 
14 variable (F E : Type*) [Field F] [ValuativeRel F] [TopologicalSpace F]
15   [IsNonarchimedeanLocalField F]
16   [Field E] [ValuativeRel E] [TopologicalSpace E]
17   [IsNonarchimedeanLocalField E] [Algebra F E]
18 variable (n : Type*) [Fintype n] [DecidableEq n] [Nonempty n]
19   (ι : E →ₐ[F] Matrix n n F) (J : Subgroup (GeneralLinearGroup n F))
20 variable {V : Type*} [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V]
21   (Λ : Representation ℂ (fieldGroup F E n ι J) V) [IsIrreducible Λ]
22 
23 /-- A character on the genuine multiplicative group of the base field. -/
24 def centralCharacter : Fˣ →* ℂˣ :=
25   (scalarCharacter F E n ι J Λ).comp (scalarHom F E n ι J).rangeRestrict
26 
27 omit [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F]
28   [ValuativeRel E] [TopologicalSpace E] [IsNonarchimedeanLocalField E] [Nonempty n] in
29 theorem centralCharacter_action (a : Fˣ) (v : V) :
30     Λ (scalarHom F E n ι J a) v = (centralCharacter F E n ι J Λ a : ℂ) • v :=
31   scalarCharacter_action F E n ι J Λ ((scalarHom F E n ι J).rangeRestrict a) v
32 
33 omit [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F]
34   [ValuativeRel E] [TopologicalSpace E] [IsNonarchimedeanLocalField E] [Nonempty n] in
35 theorem induced_centralCharacter (a : Fˣ)
36     (w : IndV (fieldGroup F E n ι J).subtype Λ) :
37     ind (fieldGroup F E n ι J).subtype Λ (GeneralLinearGroup.scalar n a) w =
38       (centralCharacter F E n ι J Λ a : ℂ) • w :=
39   induced_scalar F E n ι J Λ ((scalarHom F E n ι J).rangeRestrict a) w
40 
41 theorem scalarHom_continuous (hF : Continuous (algebraMap F E)) :
42     Continuous (scalarHom F E n ι J) := by
43   have hc := (unitsEmbedding_continuous F E n ι
44     (algebraEmbedding_continuous F E n ι hF)).comp (hF.units_map (algebraMap F E).toMonoidHom)
45   have he : (fun a : Fˣ => unitsEmbedding F E n ι
46       (Units.map (algebraMap F E).toMonoidHom a)) = GeneralLinearGroup.scalar n := by
47     funext a
48     exact unitsEmbedding_baseScalar F E n ι a
49   change Continuous (fun a : Fˣ => unitsEmbedding F E n ι
50     (Units.map (algebraMap F E).toMonoidHom a)) at hc
51   rw [he] at hc
52   exact hc.subtype_mk _
53 
54 /-- Smoothness of the actual finite-dimensional type gives local constancy
55 of its derived central character on F-times. -/
56 theorem centralCharacter_locallyConstant
57     (hF : Continuous (algebraMap F E)) (hΛ : IsSmooth Λ) :
58     IsLocallyConstant (centralCharacter F E n ι J Λ) := by
59   let χ := centralCharacter F E n ι J Λ
60   let U := Λ.ker.comap (scalarHom F E n ι J)
61   have ho : IsOpen (U : Set Fˣ) :=
62     (isOpen_kernel_of_smooth Λ hΛ).preimage (scalarHom_continuous F E n ι J hF)
63   have hle : U ≤ χ.ker := by
64     intro a ha
65     change Λ (scalarHom F E n ι J a) = 1 at ha
66     let : Nontrivial V := GeneratedIrreducibility.nontrivial_space Λ
67     obtain ⟨v,hv⟩ := exists_ne (0 : V)
68     have he := centralCharacter_action F E n ι J Λ a v
69     rw [ha] at he
70     have he' : (χ a : ℂ) • v = (1 : ℂ) • v := by
71       simpa only [Module.End.one_apply, one_smul] using he.symm
72     apply Units.ext
73     exact smul_left_injective ℂ hv he'
74   have hker : IsOpen (χ.ker : Set Fˣ) := Subgroup.isOpen_mono hle ho
75   apply (IsLocallyConstant.iff_exists_open χ).mpr
76   intro a
77   refine ⟨{b : Fˣ | χ (b * a⁻¹) = 1},
78     hker.preimage (continuous_id.mul continuous_const), ?_, ?_⟩
79   · simp
80   · intro b hb
81     change χ (b * a⁻¹) = 1 at hb
82     rw [map_mul, map_inv] at hb
83     exact mul_inv_eq_one.mp hb
84 
85 /-- The exact source-form of the full extended-type criterion. This applies
86 the proved arithmetic compact quotient and derived central character. -/
87 theorem from_full_intertwining_locus
88     (hF : Continuous (algebraMap F E))
89     (hJcompact : IsCompact (J : Set (GeneralLinearGroup n F)))
90     (hJopen : IsOpen (J : Set (GeneralLinearGroup n F)))
91     (ht : embeddedUniformizer F E n ι ∈ Subgroup.normalizer (J : Set (GeneralLinearGroup n F)))
92     (hu : ∀ u : 𝒪[E]ˣ, unitsEmbedding F E n ι (ActualLocalUnitTopology.unitEmbedding E u) ∈ J)
93     (hΛ : IsSmooth Λ)
94     (hI : FullIntertwiningLocus69.locus (fieldGroup F E n ι J) Λ =
95       (fieldGroup F E n ι J : Set (GeneralLinearGroup n F))) :
96     Nontrivial (IndV (fieldGroup F E n ι J).subtype Λ) ∧
97       IsSmooth (ind (fieldGroup F E n ι J).subtype Λ) ∧
98       IsIrreducible (ind (fieldGroup F E n ι J).subtype Λ) ∧
99       IsLocallyConstant (centralCharacter F E n ι J Λ) := by
100   let : Nontrivial V := GeneratedIrreducibility.nontrivial_space Λ
101   have hM := (FullIntertwiningLocus69.locus_eq_iff (fieldGroup F E n ι J) Λ).mp hI
102   obtain ⟨hn,hs,hi⟩ := ArithmeticFieldInduction69.induction_package F E n ι J Λ
103     hF hJcompact hJopen ht hu hΛ hM
104   exact ⟨hn,hs,hi,centralCharacter_locallyConstant F E n ι J Λ hF hΛ⟩
105 
106 end PaperXI.ArithmeticTypeCertificate69

Back to source controls