DerivedRealization.lean

1 import PaperXII.PerfectCohomology
2 import PaperXII.DerivedHeckeAction
3 import PaperXII.DerivedPatching
4 import PaperXII.HeckeFibers
5 import PaperXII.GaloisRealization
6 
7 /-!
8 # Derived eigensystems and conditional automorphic realization
9 
10 Cohomology, the induced Hecke action, and the representation intertwiners are
11 actual mathematical objects. The classicality input is applied to a nonzero
12 vector in a proved degree range. Arithmetic occurrence, attached representations,
13 Frobenius density, semisimplification, and general Brauer--Nesbitt remain explicit
14 external inputs. No final representation comparison is assumed.
15 -/
16 
17 noncomputable section
18 
19 open CategoryTheory CategoryTheory.Limits
20 
21 universe u
22 
23 attribute [local instance] HasDerivedCategory.standard
24 
25 namespace PaperXII.DerivedRealization
26 
27 open PerfectDerivedSupport PerfectCohomology DerivedHeckeAction HeckeFibers
28 
29 variable {R T E : Type u} [CommRing R] [CommRing T] [Field E]
30 
31 /-- A nonzero vector with the eigenvalues of the actual induced Hecke operators. -/
32 def IsEigenvector (C : PerfectComplex T) (y : T →+* E) (n : ℤ)
33     (z : cohomology (C.baseChange y) n) : Prop :=
34   z ≠ 0 ∧ ∀ t : T, perfectCohomologyOperator C y n t z = y t • z
35 
36 /-- The tensor relation on the original complex supplies every eigenvalue. -/
37 theorem isEigenvector_of_ne_zero (C : PerfectComplex T) (y : T →+* E) (n : ℤ)
38     (z : cohomology (C.baseChange y) n) (hz : z ≠ 0) : IsEigenvector C y n z :=
39   ⟨hz, fun t => perfectCohomologyOperator_apply C y n t z⟩
40 
41 /-- Full support produces an actual eigensystem within the projective model's bounds. -/
42 theorem derived_pointwise_eigensystem (C : PerfectComplex T) (e : R ≃+* T)
43     (x : R →+* E) (hC : FullSupport C) :
44     ¬IsZero (C.baseChange (transportedPoint e x)).object ∧
45       ∃ n : ℤ, C.model.lower ≤ n ∧ n ≤ C.model.upper ∧
46         ∃ z : cohomology (C.baseChange (transportedPoint e x)) n,
47           IsEigenvector C (transportedPoint e x) n z := by
48   refine ⟨nonzero_fiber_of_fullSupport C (transportedPoint e x) hC, ?_⟩
49   obtain ⟨n, hlo, hhi, z, hz⟩ :=
50     exists_nonzero_fiber_vector_in_range C (transportedPoint e x) hC
51   exact ⟨n, hlo, hhi, z, isEigenvector_of_ne_zero C _ n z hz⟩
52 
53 variable {A : Type u} [CommRing A]
54 
55 /-- The Hecke-side complex is compared by an actual derived isomorphism to
56 scalar transport of the patched finite-level complex. -/
57 theorem completion_hecke_fullSupport (D : DerivedPatching.Datum A R)
58     (e : R ≃+* T) (C : PerfectComplex T)
59     (comparison : C.object ≅ (D.finitePerfect.baseChange e.toRingHom).object)
60     (hD : FullSupport D.patched) : FullSupport C := by
61   unfold FullSupport
62   rw [support_eq_of_iso comparison]
63   exact fullSupport_baseChange D.finitePerfect e.toRingHom
64     (DerivedPatching.fullSupport_descends D hD)
65 
66 /-- The unconditional part of original Theorem 12.4: actual fiber nonvanishing
67 and an actual nonzero Hecke cohomology vector with bounded integer degree. -/
68 theorem derived_completion_eigensystem (D : DerivedPatching.Datum A R)
69     (e : R ≃+* T) (C : PerfectComplex T)
70     (comparison : C.object ≅ (D.finitePerfect.baseChange e.toRingHom).object)
71     (hD : FullSupport D.patched) (x : R →+* E) :
72     ¬IsZero (C.baseChange (transportedPoint e x)).object ∧
73       ∃ n : ℤ, C.model.lower ≤ n ∧ n ≤ C.model.upper ∧
74         ∃ z : cohomology (C.baseChange (transportedPoint e x)) n,
75           IsEigenvector C (transportedPoint e x) n z :=
76   derived_pointwise_eigensystem C e x (completion_hecke_fullSupport D e C comparison hD)
77 
78 section Realization
79 
80 open Matrix RepresentationData DenseFrobenius GaloisRealization
81 
82 variable {Γ Ω ι Auto : Type u} [CharZero E]
83     [TopologicalSpace E] [IsTopologicalRing E] [T2Space E]
84     [Group Γ] [TopologicalSpace Γ] [Fintype ι] [DecidableEq ι]
85 
86 /-- Revised Theorem 9.6. Every degree in the model interval belongs to the
87 specified classicality range. The input supplies an attached representation,
88 its occurrence and its Frobenius polynomials, not the resulting isomorphism. -/
89 theorem derived_pointwise (C : PerfectComplex T) (e : R ≃+* T)
90     (x : R →+* E) (hC : FullSupport C) (degrees : Set ℤ)
91     (hdegrees : ∀ n, C.model.lower ≤ n → n ≤ C.model.upper → n ∈ degrees)
92     (bn : BrauerNesbitt E Γ ι) (ρR : Γ →* GL ι R)
93     (hx : Continuous (specialize ρR x)) (s : Semisimplification (specialize ρR x))
94     (frob : Ω → Γ) (good : Ω → Prop)
95     (hdense : Dense (conjugacySaturation frob good)) (P : Ω → Polynomial T)
96     (hρP : ∀ v, good v → (specialize ρR x (frob v)).val.charpoly =
97       (P v).map (transportedPoint e x))
98     (occurs : ℤ → Auto → Prop) (attached : Auto → Γ →ₜ* GL ι E)
99     (classicality : ∀ n, n ∈ degrees →
100       ∀ z : cohomology (C.baseChange (transportedPoint e x)) n,
101         IsEigenvector C (transportedPoint e x) n z →
102           ∃ π : Auto, occurs n π ∧
103             Representation.IsSemisimpleRepresentation (representation (attached π).toMonoidHom) ∧
104             ∀ v, good v → (attached π (frob v)).val.charpoly =
105               (P v).map (transportedPoint e x)) :
106     ¬IsZero (C.baseChange (transportedPoint e x)).object ∧
107       ∃ n : ℤ, C.model.lower ≤ n ∧ n ≤ C.model.upper ∧ n ∈ degrees ∧
108         ∃ z : cohomology (C.baseChange (transportedPoint e x)) n,
109           IsEigenvector C (transportedPoint e x) n z ∧
110           ∃ π : Auto, occurs n π ∧ Isomorphic s.rep (attached π).toMonoidHom ∧
111             (Representation.IsIrreducible (representation (specialize ρR x)) →
112               Isomorphic (specialize ρR x) (attached π).toMonoidHom) := by
113   obtain ⟨hne, n, hlo, hhi, z, hz⟩ := derived_pointwise_eigensystem C e x hC
114   have hn := hdegrees n hlo hhi
115   obtain ⟨π, hocc, hsemi, hpoly⟩ := classicality n hn z hz
116   exact ⟨hne, n, hlo, hhi, hn, z, hz, π, hocc,
117     universal_pointwise_realization bn ρR x hx s (attached π) hsemi frob good hdense
118       (transportedPoint e x) P hρP hpoly⟩
119 
120 /-- Realization may instead be assumed only for the particular nonzero
121 cohomology eigensystem under consideration, as in Theorem 12.4. -/
122 theorem realize_eigensystem (C : PerfectComplex T) (e : R ≃+* T) (x : R →+* E)
123     (n : ℤ) (z : cohomology (C.baseChange (transportedPoint e x)) n)
124     (hz : IsEigenvector C (transportedPoint e x) n z)
125     (bn : BrauerNesbitt E Γ ι) (ρR : Γ →* GL ι R)
126     (hx : Continuous (specialize ρR x)) (s : Semisimplification (specialize ρR x))
127     (frob : Ω → Γ) (good : Ω → Prop)
128     (hdense : Dense (conjugacySaturation frob good)) (P : Ω → Polynomial T)
129     (hρP : ∀ v, good v → (specialize ρR x (frob v)).val.charpoly =
130       (P v).map (transportedPoint e x))
131     (occurs : ℤ → Auto → Prop) (attached : Auto → Γ →ₜ* GL ι E)
132     (classicality : IsEigenvector C (transportedPoint e x) n z →
133       ∃ π : Auto, occurs n π ∧
134         Representation.IsSemisimpleRepresentation (representation (attached π).toMonoidHom) ∧
135         ∀ v, good v → (attached π (frob v)).val.charpoly =
136           (P v).map (transportedPoint e x)) :
137     ∃ π : Auto, occurs n π ∧ Isomorphic s.rep (attached π).toMonoidHom ∧
138       (Representation.IsIrreducible (representation (specialize ρR x)) →
139         Isomorphic (specialize ρR x) (attached π).toMonoidHom) := by
140   obtain ⟨π, hocc, hsemi, hpoly⟩ := classicality hz
141   exact ⟨π, hocc, universal_pointwise_realization bn ρR x hx s (attached π) hsemi
142     frob good hdense (transportedPoint e x) P hρP hpoly⟩
143 
144 /-- Revised Theorem 12.4, retaining its pointwise applicability condition.
145 The nonzero eigensystem is constructed first. If the declared realization
146 input supplies an attached object for that eigensystem, comparison follows. -/
147 theorem derived_conditional_completion (D : DerivedPatching.Datum A R)
148     (e : R ≃+* T) (C : PerfectComplex T)
149     (comparison : C.object ≅ (D.finitePerfect.baseChange e.toRingHom).object)
150     (hD : FullSupport D.patched) (x : R →+* E)
151     (bn : BrauerNesbitt E Γ ι) (ρR : Γ →* GL ι R)
152     (hx : Continuous (specialize ρR x)) (s : Semisimplification (specialize ρR x))
153     (frob : Ω → Γ) (good : Ω → Prop)
154     (hdense : Dense (conjugacySaturation frob good)) (P : Ω → Polynomial T)
155     (hρP : ∀ v, good v → (specialize ρR x (frob v)).val.charpoly =
156       (P v).map (transportedPoint e x))
157     (occurs : ℤ → Auto → Prop) (attached : Auto → Γ →ₜ* GL ι E) :
158     ¬IsZero (C.baseChange (transportedPoint e x)).object ∧
159       ∃ n : ℤ, C.model.lower ≤ n ∧ n ≤ C.model.upper ∧
160         ∃ z : cohomology (C.baseChange (transportedPoint e x)) n,
161           IsEigenvector C (transportedPoint e x) n z ∧
162           ((∃ π : Auto, occurs n π ∧
163             Representation.IsSemisimpleRepresentation (representation (attached π).toMonoidHom) ∧
164             ∀ v, good v → (attached π (frob v)).val.charpoly =
165               (P v).map (transportedPoint e x)) →
166             ∃ π : Auto, occurs n π ∧ Isomorphic s.rep (attached π).toMonoidHom ∧
167               (Representation.IsIrreducible (representation (specialize ρR x)) →
168                 Isomorphic (specialize ρR x) (attached π).toMonoidHom)) := by
169   obtain ⟨hne, n, hlo, hhi, z, hz⟩ := derived_completion_eigensystem D e C comparison hD x
170   refine ⟨hne, n, hlo, hhi, z, hz, ?_⟩
171   intro hclassical
172   exact realize_eigensystem C e x n z hz bn ρR hx s frob good hdense P hρP
173     occurs attached (fun _ => hclassical)
174 
175 end Realization
176 
177 end PaperXII.DerivedRealization

Back to source controls