FiveGateCompletion.lean

1 import PaperXII.PatchingCarriers
2 import PaperXII.ExistingCompatibleSystems
3 
4 /-!
5 # Five-gate completion for actual ordinary and derived carriers
6 
7 Patching data produce the source carrier. A genuine support inclusion and a
8 compatible lift of the chosen field point produce the Hecke eigensystem.
9 Classicality is required only for that eigensystem. The arithmetic comparison
10 uses explicit continuous representations and common Frobenius polynomials.
11 Both existing compatible families are retained, and the attached family belongs
12 to the very automorphic object obtained at the distinguished point.
13 -/
14 
15 noncomputable section
16 
17 open CategoryTheory CategoryTheory.Limits
18 
19 universe u
20 
21 attribute [local instance] HasDerivedCategory.standard
22 
23 namespace PaperXII.FiveGateCompletion
24 
25 open HeckeCarriers PatchingCarriers
26 
27 variable {A R T E : Type u} [CommRing A] [CommRing R] [CommRing T]
28     [Algebra A R] [Field E]
29 
30 /-- The witness contains the actual degree, vector, and all induced Hecke identities. -/
31 structure Eigensystem (H : Carrier T) (y : T →+* E) where
32   degree : H.Degree
33   inRange : DegreeRange H degree
34   vector : fiberSpace H y degree
35   eigenvector : IsEigenvector H y degree vector
36 
37 /-- The patched source point belongs to its actual finite-level support. -/
38 theorem patched_point_supported (D : PatchedCarrier A R) (x : R →+* E) :
39     FieldFibers.pointPrime x ∈ support D.finiteCarrier := by
40   rw [D.fullSupport]
41   trivial
42 
43 /-- The fiber gate follows from actual patching, comparison and point compatibility. -/
44 theorem five_gate_fiber (D : PatchedCarrier A R) (f : R →+* T) (H : Carrier T)
45     (comparison : SupportComparison f D.finiteCarrier H)
46     (x : R →+* E) (y : T →+* E) (hcomp : y.comp f = x) : FiberNonzero H y :=
47   supportComparison_pointwise_fiber_nonzero f D.finiteCarrier H comparison x y hcomp
48     (patched_point_supported D x)
49 
50 /-- A compatible point gives an actual ordinary or derived eigensystem. -/
51 theorem five_gate_eigensystem (D : PatchedCarrier A R) (f : R →+* T) (H : Carrier T)
52     (comparison : SupportComparison f D.finiteCarrier H)
53     (x : R →+* E) (y : T →+* E) (hcomp : y.comp f = x) :
54     Nonempty (Eigensystem H y) := by
55   obtain ⟨n, hn, z, hz⟩ := supportComparison_pointwise_eigensystem
56     f D.finiteCarrier H comparison x y hcomp (patched_point_supported D x)
57   exact ⟨⟨n, hn, z, hz⟩⟩
58 
59 /-- Select only the witness already proved to exist; no arithmetic realization is selected. -/
60 def chosenEigensystem (D : PatchedCarrier A R) (f : R →+* T) (H : Carrier T)
61     (comparison : SupportComparison f D.finiteCarrier H)
62     (x : R →+* E) (y : T →+* E) (hcomp : y.comp f = x) : Eigensystem H y :=
63   Classical.choice (five_gate_eigensystem D f H comparison x y hcomp)
64 
65 section Realization
66 
67 open Matrix RepresentationData DenseFrobenius GaloisRealization
68 
69 variable {Γ Ω ι Auto : Type u} [CharZero E]
70     [TopologicalSpace E] [IsTopologicalRing E] [T2Space E]
71     [Group Γ] [TopologicalSpace Γ] [Fintype ι] [DecidableEq ι]
72 
73 /-- Conditional realization at the particular constructed eigensystem.
74 The external input supplies occurrence and the attached Frobenius polynomials,
75 never an isomorphism with the universal specialization. -/
76 theorem five_gate_completion (D : PatchedCarrier A R) (f : R →+* T) (H : Carrier T)
77     (comparison : SupportComparison f D.finiteCarrier H)
78     (x : R →+* E) (y : T →+* E) (hcomp : y.comp f = x)
79     (bn : BrauerNesbitt E Γ ι) (ρR : Γ →* GL ι R)
80     (hx : Continuous (specialize ρR x)) (s : Semisimplification (specialize ρR x))
81     (frob : Ω → Γ) (good : Ω → Prop)
82     (hdense : Dense (conjugacySaturation frob good)) (P : Ω → Polynomial T)
83     (hρP : ∀ v, good v → (specialize ρR x (frob v)).val.charpoly = (P v).map y)
84     (occurs : ∀ n : H.Degree, fiberSpace H y n → Auto → Prop)
85     (attached : Auto → Γ →ₜ* GL ι E)
86     (classicality :
87       let w := chosenEigensystem D f H comparison x y hcomp
88       ∃ π : Auto, occurs w.degree w.vector π ∧
89         Representation.IsSemisimpleRepresentation (representation (attached π).toMonoidHom) ∧
90         ∀ v, good v → (attached π (frob v)).val.charpoly = (P v).map y) :
91     FiberNonzero H y ∧
92       let w := chosenEigensystem D f H comparison x y hcomp
93       ∃ π : Auto, occurs w.degree w.vector π ∧
94         Isomorphic s.rep (attached π).toMonoidHom ∧
95         (Representation.IsIrreducible (representation (specialize ρR x)) →
96           Isomorphic (specialize ρR x) (attached π).toMonoidHom) := by
97   obtain ⟨π, hocc, hsemi, hpoly⟩ := classicality
98   exact ⟨five_gate_fiber D f H comparison x y hcomp, π, hocc,
99     universal_pointwise_realization bn ρR x hx s (attached π) hsemi
100       frob good hdense y P hρP hpoly⟩
101 
102 end Realization
103 
104 section Systems
105 
106 open Matrix RepresentationData DenseFrobenius GaloisRealization
107 
108 variable {Λ Ω Γ ι L Auto : Type u} [Field L]
109     [Group Γ] [TopologicalSpace Γ] [Fintype ι] [DecidableEq ι]
110     {K : Λ → Type u} [∀ l, Field (K l)] [∀ l, CharZero (K l)]
111     [∀ l, TopologicalSpace (K l)] [∀ l, IsTopologicalRing (K l)] [∀ l, T2Space (K l)]
112 
113 /-- The compatible-system conclusion uses the family attached to the very
114 object produced by realization. Both existing families, their distinguished
115 member identities, and the common coefficient-field spine are explicit. -/
116 theorem five_gate_system_completion (D : PatchedCarrier A R) (f : R →+* T)
117     (H : Carrier T) (comparison : SupportComparison f D.finiteCarrier H)
118     (l₀ : Λ) (x : R →+* K l₀) (y : T →+* K l₀) (hcomp : y.comp f = x)
119     (ρR : Γ →* GL ι R) (hx : Continuous (specialize ρR x))
120     (s : Semisimplification (specialize ρR x))
121     (ρ : ∀ l, Γ →ₜ* GL ι (K l))
122     (hmember : (ρ l₀).toMonoidHom = specialize ρR x)
123     (hsemi : ∀ l, Representation.IsSemisimpleRepresentation (representation (ρ l).toMonoidHom))
124     (frob : Ω → Γ) (good : Λ → Ω → Prop)
125     (hdense : ∀ l, Dense (conjugacySaturation frob (good l)))
126     (emb : ∀ l, L →+* K l) (P : Ω → Polynomial T) (Q : Ω → Polynomial L)
127     (hspine : ∀ v, good l₀ v → (P v).map y = (Q v).map (emb l₀))
128     (hρ : ∀ l v, good l v → (ρ l (frob v)).val.charpoly = (Q v).map (emb l))
129     (occurs : ∀ n : H.Degree, fiberSpace H y n → Auto → Prop)
130     (attached : Auto → Γ →ₜ* GL ι (K l₀))
131     (bn : ∀ l, BrauerNesbitt (K l) Γ ι)
132     (classicality :
133       let w := chosenEigensystem D f H comparison x y hcomp
134       ∃ π : Auto, occurs w.degree w.vector π ∧
135         Representation.IsSemisimpleRepresentation (representation (attached π).toMonoidHom) ∧
136         ∃ σ : ∀ l, Γ →ₜ* GL ι (K l),
137           σ l₀ = attached π ∧
138           (∀ l v, good l v → (σ l (frob v)).val.charpoly = (Q v).map (emb l)) ∧
139           Nonempty (∀ l, Semisimplification (σ l).toMonoidHom)) :
140     FiberNonzero H y ∧
141       let w := chosenEigensystem D f H comparison x y hcomp
142       ∃ π : Auto, occurs w.degree w.vector π ∧
143         Isomorphic s.rep (attached π).toMonoidHom ∧
144         ∃ σ : ∀ l, Γ →ₜ* GL ι (K l), σ l₀ = attached π ∧
145           ∃ ss : ∀ l, Semisimplification (σ l).toMonoidHom,
146             Nonempty (∀ l, Representation.Equiv (representation (ρ l).toMonoidHom)
147               (representation (ss l).rep)) := by
148   obtain ⟨π, hocc, hatSemi, σ, hatMember, hσ, ⟨ss⟩⟩ := classicality
149   have hρP : ∀ v, good l₀ v →
150       (specialize ρR x (frob v)).val.charpoly = (P v).map y := by
151     intro v hv
152     rw [← hmember]
153     exact (hρ l₀ v hv).trans (hspine v hv).symm
154   have hatP : ∀ v, good l₀ v →
155       (attached π (frob v)).val.charpoly = (P v).map y := by
156     intro v hv
157     rw [← hatMember]
158     exact (hσ l₀ v hv).trans (hspine v hv).symm
159   exact ⟨five_gate_fiber D f H comparison x y hcomp, π, hocc,
160     (universal_pointwise_realization (bn l₀) ρR x hx s (attached π) hatSemi
161       frob (good l₀) (hdense l₀) y P hρP hatP).1,
162     σ, hatMember, ss,
163     ExistingCompatibleSystems.system_completion ρ σ frob good hdense emb Q
164       hρ hσ hsemi ss bn⟩
165 
166 end Systems
167 
168 end PaperXII.FiveGateCompletion

Back to source controls