OrdinaryCompletion.lean

1 import PaperXII.OrdinaryPatching
2 import PaperXII.HeckeFibers
3 import PaperXII.GaloisRealization
4 
5 /-! Paper XII, revised Corollary 9.5 and Theorem 12.2.
6 The inputs are the printed patched module, quotient identifications, patched
7 full support, and Hecke identification. Finite-level support is derived.
8 The arithmetic occurrence and attached-representation statements remain declared
9 classicality inputs. Hausdorff coefficient topology and representation continuity
10 are explicit, as in the revised pointwise realization theorem. -/
11 set_option autoImplicit false
12 namespace PaperXII.OrdinaryCompletion
13 
14 open scoped TensorProduct
15 open ModuleSupport FieldFibers HeckeFibers
16 
17 section Support
18 
19 variable {A R T E P H : Type*}
20     [CommRing A] [IsNoetherianRing A] [CommRing R] [CommRing T] [Field E]
21     [Algebra A R] [Algebra R T]
22     [AddCommGroup P] [Module A P] [Module.Finite A P]
23     [AddCommGroup H] [Module A H] [Module R H] [Module T H]
24     [IsScalarTower A R H] [IsScalarTower R T H]
25 
26 omit [IsNoetherianRing A] in
27 /-- Finite generation at finite level follows from the actual control isomorphism. -/
28 theorem finite_level_finite (I : Ideal A)
29     (eM : (P ⧸ (I • ⊤ : Submodule A P)) ≃ₗ[A] H) : Module.Finite R H := by
30   let : Module.Finite A H := Module.Finite.equiv eM
31   exact Module.Finite.of_restrictScalars_finite A R H
32 
33 /-- The full finite-level support needed by completion is a conclusion of the
34 patched support and actual quotient identifications. -/
35 theorem finite_level_fullSupport (I : Ideal A)
36     (eR : (A ⧸ I) ≃ₐ[A] R)
37     (eM : (P ⧸ (I • ⊤ : Submodule A P)) ≃ₗ[A] H)
38     (hP : FullSupport A P) : FullSupport R H :=
39   (OrdinaryPatching.conclusions_of_quotient_identifications I eR eM hP).1
40 
41 /-- Full Hecke support is transported along the supplied ring identification. -/
42 theorem hecke_fullSupport (I : Ideal A)
43     (eR : (A ⧸ I) ≃ₐ[A] R)
44     (eM : (P ⧸ (I • ⊤ : Submodule A P)) ≃ₗ[A] H)
45     (eT : R ≃ₐ[R] T) (hP : FullSupport A P) : FullSupport T H := by
46   have he : eT.toRingHom = algebraMap R T := by
47     ext r
48     exact eT.commutes r
49   have hbij : Function.Bijective (algebraMap R T) := by
50     rw [← he]
51     exact eT.bijective
52   exact (SupportTransport.fullSupport_iff hbij).mp
53     (finite_level_fullSupport I eR eM hP)
54 
55 /-- The ordinary completion datum produces a nonzero actual Hecke tensor fiber
56 and the prescribed action of every Hecke operator. -/
57 theorem ordinary_hecke_eigensystem (I : Ideal A)
58     (eR : (A ⧸ I) ≃ₐ[A] R)
59     (eM : (P ⧸ (I • ⊤ : Submodule A P)) ≃ₗ[A] H)
60     (eT : R ≃ₐ[R] T) (hP : FullSupport A P) (x : R →+* E) :
61     letI : Algebra T E := (transportedPoint eT.toRingEquiv x).toAlgebra
62     Nontrivial (E ⊗[T] H) ∧
63       ∀ t : T, heckeOperator (H := H) (transportedPoint eT.toRingEquiv x) t =
64         transportedPoint eT.toRingEquiv x t •
65           (LinearMap.id : Module.End E (E ⊗[T] H)) := by
66   let : Module.Finite R H := finite_level_finite (R := R) I eM
67   let : Module.Finite T H := Module.Finite.of_restrictScalars_finite R T H
68   apply support_gives_hecke_eigensystem eT x
69   exact (fullSupport_iff_localizations R H).mp
70     (finite_level_fullSupport I eR eM hP) _
71 
72 /-- The tensor order displayed in the manuscript is nonzero as well. -/
73 theorem ordinary_right_hecke_fiber (I : Ideal A)
74     (eR : (A ⧸ I) ≃ₐ[A] R)
75     (eM : (P ⧸ (I • ⊤ : Submodule A P)) ≃ₗ[A] H)
76     (eT : R ≃ₐ[R] T) (hP : FullSupport A P) (x : R →+* E) :
77     letI : Algebra T E := (transportedPoint eT.toRingEquiv x).toAlgebra
78     Nontrivial (H ⊗[T] E) := by
79   let : Algebra T E := (transportedPoint eT.toRingEquiv x).toAlgebra
80   exact (TensorProduct.comm T H E).nontrivial_congr.mpr
81     (ordinary_hecke_eigensystem I eR eM eT hP x).1
82 
83 /-- A genuine nonzero vector in the fiber carries all prescribed Hecke values. -/
84 theorem ordinary_eigenvector (I : Ideal A)
85     (eR : (A ⧸ I) ≃ₐ[A] R)
86     (eM : (P ⧸ (I • ⊤ : Submodule A P)) ≃ₗ[A] H)
87     (eT : R ≃ₐ[R] T) (hP : FullSupport A P) (x : R →+* E) :
88     letI : Algebra T E := (transportedPoint eT.toRingEquiv x).toAlgebra
89     ∃ z : E ⊗[T] H, z ≠ 0 ∧
90       ∀ t : T, heckeOperator (H := H) (transportedPoint eT.toRingEquiv x) t z =
91         transportedPoint eT.toRingEquiv x t • z := by
92   let : Algebra T E := (transportedPoint eT.toRingEquiv x).toAlgebra
93   obtain ⟨hne, haction⟩ := ordinary_hecke_eigensystem I eR eM eT hP x
94   let : Nontrivial (E ⊗[T] H) := hne
95   obtain ⟨z, hz⟩ := exists_ne (0 : E ⊗[T] H)
96   refine ⟨z, hz, fun t ↦ ?_⟩
97   rw [haction t]
98   rfl
99 
100 end Support
101 
102 section Realization
103 
104 open Matrix RepresentationData DenseFrobenius GaloisRealization
105 
106 variable {R T E H Γ Ω ι Auto : Type*} [CommRing R] [CommRing T]
107     [Field E] [CharZero E] [TopologicalSpace E] [IsTopologicalRing E] [T2Space E]
108     [Group Γ] [TopologicalSpace Γ] [Fintype ι] [DecidableEq ι]
109     [Algebra R T] [AddCommGroup H] [Module R H] [Module T H]
110     [IsScalarTower R T H]
111 
112 /-- The declared classicality input produces an actual attached representation
113 at the supported point. `occurs x π` is the external arithmetic assertion that
114 the classical automorphic object `π` occurs in the Hecke fiber at `x`.
115 The input is conditional on nonvanishing; it contains no final isomorphism. -/
116 theorem supported_pointwise_realization [Module.Finite T H]
117     (eT : R ≃ₐ[R] T) (x : R →+* E)
118     (hxSupport : pointPrime x ∈ Module.support R H)
119     (bn : BrauerNesbitt E Γ ι) (ρR : Γ →* GL ι R)
120     (hx : Continuous (specialize ρR x)) (s : Semisimplification (specialize ρR x))
121     (frob : Ω → Γ) (good : Ω → Prop)
122     (hdense : Dense (conjugacySaturation frob good)) (P : Ω → Polynomial T)
123     (hρP : ∀ v, good v → (specialize ρR x (frob v)).val.charpoly =
124       (P v).map (transportedPoint eT.toRingEquiv x))
125     (occurs : (R →+* E) → Auto → Prop) (attached : Auto → Γ →ₜ* GL ι E)
126     (classicality :
127       letI : Algebra T E := (transportedPoint eT.toRingEquiv x).toAlgebra
128       Nontrivial (E ⊗[T] H) → ∃ π : Auto, occurs x π ∧
129         Representation.IsSemisimpleRepresentation (representation (attached π).toMonoidHom) ∧
130         ∀ v, good v → (attached π (frob v)).val.charpoly =
131           (P v).map (transportedPoint eT.toRingEquiv x)) :
132     letI : Algebra T E := (transportedPoint eT.toRingEquiv x).toAlgebra
133     Nontrivial (H ⊗[T] E) ∧ ∃ π : Auto, occurs x π ∧
134       Isomorphic s.rep (attached π).toMonoidHom ∧
135       (Representation.IsIrreducible (representation (specialize ρR x)) →
136         Isomorphic (specialize ρR x) (attached π).toMonoidHom) := by
137   let : Algebra T E := (transportedPoint eT.toRingEquiv x).toAlgebra
138   have hne := supported_hecke_fiber eT x hxSupport
139   obtain ⟨π, hoccurs, hsemi, hpoly⟩ := classicality hne
140   exact ⟨(TensorProduct.comm T H E).nontrivial_congr.mpr hne, π, hoccurs,
141     universal_pointwise_realization bn ρR x hx s (attached π) hsemi frob good hdense
142       (transportedPoint eT.toRingEquiv x) P hρP hpoly⟩
143 
144 /-- Revised Corollary 9.5: full support supplies nonzero fibers throughout the
145 declared locus, and the pointwise arithmetic inputs give each attached witness.
146 Continuity and semisimplification are required only at points of that locus. -/
147 theorem full_support_pointwise_realization [Module.Finite T H]
148     (eT : R ≃ₐ[R] T) (hH : FullSupport R H) (U : Set (PrimeSpectrum R))
149     (bn : BrauerNesbitt E Γ ι) (ρR : Γ →* GL ι R)
150     (hx : ∀ x : R →+* E, pointPrime x ∈ U → Continuous (specialize ρR x))
151     (s : ∀ x : R →+* E, pointPrime x ∈ U → Semisimplification (specialize ρR x))
152     (frob : Ω → Γ) (good : Ω → Prop)
153     (hdense : Dense (conjugacySaturation frob good)) (P : Ω → Polynomial T)
154     (hρP : ∀ x : R →+* E, pointPrime x ∈ U → ∀ v, good v →
155       (specialize ρR x (frob v)).val.charpoly =
156         (P v).map (transportedPoint eT.toRingEquiv x))
157     (occurs : (R →+* E) → Auto → Prop) (attached : Auto → Γ →ₜ* GL ι E)
158     (classicality : ∀ x : R →+* E, pointPrime x ∈ U →
159       letI : Algebra T E := (transportedPoint eT.toRingEquiv x).toAlgebra
160       Nontrivial (E ⊗[T] H) → ∃ π : Auto, occurs x π ∧
161         Representation.IsSemisimpleRepresentation (representation (attached π).toMonoidHom) ∧
162         ∀ v, good v → (attached π (frob v)).val.charpoly =
163           (P v).map (transportedPoint eT.toRingEquiv x)) :
164     ∀ (x : R →+* E) (hxU : pointPrime x ∈ U),
165       letI : Algebra T E := (transportedPoint eT.toRingEquiv x).toAlgebra
166       Nontrivial (H ⊗[T] E) ∧ ∃ π : Auto, occurs x π ∧
167         Isomorphic (s x hxU).rep (attached π).toMonoidHom ∧
168         (Representation.IsIrreducible (representation (specialize ρR x)) →
169           Isomorphic (specialize ρR x) (attached π).toMonoidHom) := by
170   intro x hxU
171   exact supported_pointwise_realization eT x
172     ((fullSupport_iff_localizations R H).mp hH _) bn ρR (hx x hxU) (s x hxU)
173     frob good hdense P (hρP x hxU) occurs attached (classicality x hxU)
174 
175 variable {A Pinf : Type*} [CommRing A] [IsNoetherianRing A] [Algebra A R]
176     [AddCommGroup Pinf] [Module A Pinf] [Module.Finite A Pinf]
177     [Module A H] [IsScalarTower A R H]
178 
179 /-- Revised Theorem 12.2, including its actual nonzero tensor fiber, the supplied
180 classical object's occurrence, semisimplified identification, and irreducible
181 identification. Finite-level support and finite generation are derived from
182 the printed patched quotient datum; classicality is used only after this. -/
183 theorem ordinary_conditional_completion (I : Ideal A)
184     (eR : (A ⧸ I) ≃ₐ[A] R)
185     (eM : (Pinf ⧸ (I • ⊤ : Submodule A Pinf)) ≃ₗ[A] H)
186     (eT : R ≃ₐ[R] T) (hP : FullSupport A Pinf) (x : R →+* E)
187     (bn : BrauerNesbitt E Γ ι) (ρR : Γ →* GL ι R)
188     (hx : Continuous (specialize ρR x)) (s : Semisimplification (specialize ρR x))
189     (frob : Ω → Γ) (good : Ω → Prop)
190     (hdense : Dense (conjugacySaturation frob good)) (P : Ω → Polynomial T)
191     (hρP : ∀ v, good v → (specialize ρR x (frob v)).val.charpoly =
192       (P v).map (transportedPoint eT.toRingEquiv x))
193     (occurs : (R →+* E) → Auto → Prop) (attached : Auto → Γ →ₜ* GL ι E)
194     (classicality :
195       letI : Algebra T E := (transportedPoint eT.toRingEquiv x).toAlgebra
196       Nontrivial (E ⊗[T] H) → ∃ π : Auto, occurs x π ∧
197         Representation.IsSemisimpleRepresentation (representation (attached π).toMonoidHom) ∧
198         ∀ v, good v → (attached π (frob v)).val.charpoly =
199           (P v).map (transportedPoint eT.toRingEquiv x)) :
200     letI : Algebra T E := (transportedPoint eT.toRingEquiv x).toAlgebra
201     Nontrivial (H ⊗[T] E) ∧ ∃ π : Auto, occurs x π ∧
202       Isomorphic s.rep (attached π).toMonoidHom ∧
203       (Representation.IsIrreducible (representation (specialize ρR x)) →
204         Isomorphic (specialize ρR x) (attached π).toMonoidHom) := by
205   let : Module.Finite R H := finite_level_finite (R := R) I eM
206   let : Module.Finite T H := Module.Finite.of_restrictScalars_finite R T H
207   exact supported_pointwise_realization eT x
208     ((fullSupport_iff_localizations R H).mp (finite_level_fullSupport I eR eM hP) _)
209     bn ρR hx s frob good hdense P hρP occurs attached classicality
210 
211 end Realization
212 
213 end PaperXII.OrdinaryCompletion

Back to source controls