Paper XII: Patching Support, Hecke Packets, and Conditional Automorphic Completion

Download original file

This is the original TeX manuscript source. Use the paper’s PDF for typeset equations.

Included manuscript sections

• Paper_XII_Traditional_Final.bib
• reading_route.tex

Read the typeset paper

Read this chapter with formatted equations

1 % Final traditional edition. Raw manuscript snapshots are preserved in source_preserved/.
2 \pdfinfoomitdate=1
3 \pdfsuppressptexinfo=15
4 \pdftrailerid{}
5 \documentclass[11pt]{amsart}
6 \usepackage[margin=1.05in]{geometry}
7 
8 \usepackage[T1]{fontenc}
9 \usepackage{lmodern}
10 \usepackage[nopatch=footnote]{microtype}
11 \usepackage{amssymb,mathtools}
12 \usepackage{amscd}
13 \usepackage{bm}
14 \usepackage{aliascnt}
15 \usepackage{enumitem}
16 \usepackage{graphicx}
17 \usepackage{booktabs}
18 \usepackage{array}
19 \usepackage{longtable}
20 \usepackage[colorlinks=true,linkcolor=blue,citecolor=blue,urlcolor=blue]{hyperref}
21 \usepackage[nameinlink,noabbrev]{cleveref}
22 
23 \allowdisplaybreaks
24 \hyphenpenalty=10000
25 \exhyphenpenalty=10000
26 \tolerance=2600
27 \emergencystretch=4em
28 
29 
30 
31 \setlist[enumerate]{topsep=4pt,itemsep=2pt}
32 \setlist[itemize]{topsep=4pt,itemsep=2pt}
33 
34 \newtheorem{theorem}{Theorem}[section]
35 \newaliascnt{proposition}{theorem}
36 \newtheorem{proposition}[proposition]{Proposition}
37 \aliascntresetthe{proposition}
38 \newaliascnt{lemma}{theorem}
39 \newtheorem{lemma}[lemma]{Lemma}
40 \aliascntresetthe{lemma}
41 \newaliascnt{corollary}{theorem}
42 \newtheorem{corollary}[corollary]{Corollary}
43 \aliascntresetthe{corollary}
44 \theoremstyle{definition}
45 \newaliascnt{definition}{theorem}
46 \newtheorem{definition}[definition]{Definition}
47 \aliascntresetthe{definition}
48 \newaliascnt{example}{theorem}
49 \newtheorem{example}[example]{Example}
50 \aliascntresetthe{example}
51 \newaliascnt{standardfact}{theorem}
52 \newtheorem{standardfact}[standardfact]{Standard Fact}
53 \aliascntresetthe{standardfact}
54 \theoremstyle{remark}
55 \newaliascnt{remark}{theorem}
56 \newtheorem{remark}[remark]{Remark}
57 \aliascntresetthe{remark}
58 
59 \crefname{theorem}{theorem}{theorems}
60 \crefname{proposition}{proposition}{propositions}
61 \crefname{lemma}{lemma}{lemmas}
62 \crefname{corollary}{corollary}{corollaries}
63 \crefname{definition}{definition}{definitions}
64 \crefname{example}{example}{examples}
65 \crefname{standardfact}{standard fact}{standard facts}
66 \crefname{remark}{remark}{remarks}
67 
68 \newcommand{\OO}{\mathcal O}
69 \newcommand{\FF}{\mathbb F}
70 \newcommand{\QQ}{\mathbb Q}
71 \newcommand{\ZZ}{\mathbb Z}
72 \newcommand{\CC}{\mathbb C}
73 \newcommand{\NN}{\mathbb N}
74 \newcommand{\EE}{\mathbb E}
75 \newcommand{\TT}{\mathbb T}
76 \newcommand{\Spec}{\operatorname{Spec}}
77 \newcommand{\Spf}{\operatorname{Spf}}
78 \newcommand{\Supp}{\operatorname{Supp}}
79 \newcommand{\Ann}{\operatorname{Ann}}
80 \newcommand{\Fitt}{\operatorname{Fitt}}
81 \newcommand{\Hom}{\operatorname{Hom}}
82 \newcommand{\End}{\operatorname{End}}
83 \newcommand{\Ext}{\operatorname{Ext}}
84 \newcommand{\Tor}{\operatorname{Tor}}
85 \newcommand{\coker}{\operatorname{coker}}
86 \newcommand{\im}{\operatorname{im}}
87 \newcommand{\rank}{\operatorname{rank}}
88 \newcommand{\Tr}{\operatorname{Tr}}
89 \newcommand{\Frob}{\operatorname{Frob}}
90 \newcommand{\Gal}{\operatorname{Gal}}
91 \newcommand{\GL}{\operatorname{GL}}
92 \newcommand{\ad}{\operatorname{ad}}
93 \newcommand{\Max}{\operatorname{Max}}
94 \newcommand{\Perf}{\operatorname{Perf}}
95 \newcommand{\nil}{\operatorname{Nil}}
96 \newcommand{\rad}{\operatorname{rad}}
97 \newcommand{\length}{\operatorname{length}}
98 \newcommand{\id}{\operatorname{id}}
99 \newcommand{\e}{\mathrm e}
100 \newcommand{\one}{\bm 1}
101 \newcommand{\norm}[1]{\left\lVert#1\right\rVert}
102 \newcommand{\abs}[1]{\left\lvert#1\right\rvert}
103 \newcommand{\calA}{\mathcal A}
104 \newcommand{\calC}{\mathcal C}
105 \newcommand{\calD}{\mathcal D}
106 \newcommand{\calF}{\mathcal F}
107 \newcommand{\calH}{\mathcal H}
108 \newcommand{\calM}{\mathcal M}
109 \newcommand{\calP}{\mathcal P}
110 \newcommand{\calR}{\mathcal R}
111 \newcommand{\calS}{\mathcal S}
112 \newcommand{\calT}{\mathcal T}
113 \newcommand{\calV}{\mathcal V}
114 \newcommand{\calW}{\mathcal W}
115 \newcommand{\frakC}{\mathfrak C}
116 \newcommand{\frakF}{\mathfrak F}
117 \newcommand{\frakm}{\mathfrak m}
118 \newcommand{\frakp}{\mathfrak p}
119 \newcommand{\fraka}{\mathfrak a}
120 \newcommand{\wideotimes}{\mathbin{\widehat\otimes}}
121 
122 \graphicspath{{figures/}}
123 
124 \title[Patching support and automorphic completion]{Patching Support, Hecke Packets, and Conditional Automorphic Completion}
125 \author[Komorebi P.]{Komorebi P.}
126 \subjclass[2020]{11F80, 11F70, 13C14, 13D09, 11R34}
127 \keywords{automorphy lifting, Taylor Wiles patching, module support, Hecke algebra, compatible system, adequate image}
128 \date{10 October 2026. Reading release 1.0.0.}
129 
130 \pdfstringdefDisableCommands{\let\unskip\relax}
131 \hypersetup{
132   pdftitle={Patching Support, Hecke Packets, and Conditional Automorphic Completion},
133   pdfauthor={Komorebi P.},
134   pdfsubject={Global deformation conditions, patching support, Hecke packets, compatible systems, and conditional automorphic realization}
135 }
136 
137 
138 % Operation Komorebi: shared publication profile.
139 \usepackage{komorebi-publication}
140 \renewcommand{\KomorebiTitle}{Patching Support and Hecke Packets}
141 \renewcommand{\KomorebiSubtitle}{Conditional automorphic completion}
142 \renewcommand{\KomorebiSeries}{Core series XII}
143 \renewcommand{\KomorebiKind}{Monograph}
144 \renewcommand{\KomorebiEdition}{Reading release 1.0.0 / 10 October 2026}
145 \renewcommand{\KomorebiShortTitle}{Paper XII / Conditional automorphic completion}
146 \renewcommand{\KomorebiTitleSize}{31}
147 \renewcommand{\KomorebiTitleLeading}{36}
148 \renewcommand{\KomorebiProfile}{classical}
149 \renewcommand{\KomorebiOrientation}{portrait}
150 \KomorebiSetup
151 \makeatletter
152 \providecommand\@dotsep{4.5}
153 \renewcommand\l@section{\@dottedtocline{1}{0pt}{2.8em}}
154 \renewcommand\numberline[1]{\hb@xt@\@tempdima{#1\hfil}}
155 \makeatother
156 \begin{document}
157 \KomorebiCover
158 \input{reading_route.tex}
159 
160 \begin{abstract}
161 Let \(\bar\rho\) be a residual Galois representation and let \(R\) be a global deformation ring with declared local conditions. We separate the global automorphy problem into residual occupancy, deformation support, Hecke occupancy, and arithmetic realization. Local conditions are encoded by quotient rings rather than by idempotents, since irreducible components of a local deformation ring need not be clopen. For an ordinary or derived patching datum, full support descends through the augmentation quotient. Near faithfulness is shown to be equivalent to full support for finite modules over Noetherian rings. An isomorphism \(R\cong\TT\) transports support, Fitting ideals, and point fibers, but a quotient map can erase an entire component. Finite Hecke algebras are resolved into canonical Artin packets, so simultaneous generalized eigenspaces are available without assuming semisimplicity. Nested packets in one finite carrier stabilize; for changing finite carriers, nonzero stable cores give compatible inverse limit vectors. These results give a pointwise criterion: a characteristic zero deformation point in automorphic support produces a Hecke eigensystem. With attached Galois representations, local global compatibility, and classicality, the point is automorphic. A fixed compatible system then propagates the conclusion to every coefficient place. For finite coefficient quotients, compatible conjugacy classes admit compatible continuous representatives. Declared polynomial quotient conditions survive their adic reconstruction. These completion statements require explicit finite occupancy, continuity, and integral Frobenius data. Universal companion existence and unrestricted reciprocity are not proved.
162 \end{abstract}
163 \makeatletter\@setabstract\makeatother
164 \thispagestyle{plain}
165 
166 \section*{Publication and supporting files}
167 This reading edition, dated 10 October 2026, retains the complete revised mathematical proofs. Fourteen inherited vector figures are unchanged. Four diagrams have been redrawn to separate their arrows, expose the supplied inputs, and synchronize the final architecture with the five gates of Theorem~\ref{thm:five_gate_completion}. Supporting Markdown (\texttt{.md}) files are included with the source: the publication note, formal-evidence boundary, original-to-revised claim crosswalk, current status, source-preservation ledger, and build instructions. They record the statement hypotheses, evidence scope, and editorial changes alongside the preserved original and revised source snapshots.
168 
169 The saved release reports complete mapped formal evidence for all forty-nine revised internal claims, while the original-wording census is forty-one complete, seven partial, and one unchecked. These are different contracts. The completed tensor and point-factorization results are algebraic deductions for supplied deformation data; representability, residual occupancy, applicable patching and classicality theorems, attached Galois representations, Frobenius density, semisimplification, and the general Brauer--Nesbitt theorem remain external arithmetic or algebraic inputs. Neither Paper XI's general Conjecture~66 nor universal companion existence is assumed.
170 
171 \section{Introduction}\label{sec:introduction}
172 
173 Automorphy lifting joins several kinds of mathematics that are easy to conflate. A residual representation must first occur in an automorphic carrier. The chosen characteristic zero representation must lie on a deformation problem controlled by local conditions. A patching argument must show that the automorphic module reaches the relevant part of the deformation space. A comparison such as \(R\cong\TT\) must identify the arithmetic and Hecke coordinates. Finally, the resulting Hecke point must be classical and must carry the expected Galois representation with the required local compatibility.
174 
175 None of these steps is merely a change of notation. A deeper lift above one residual representation cannot create a missing residual companion. Freeness over an auxiliary group algebra does not imply that every component of a deformation ring is occupied. An isomorphism of rings transports support that already exists, but it does not create a nonzero automorphic vector. A nonzero class in completed or torsion cohomology need not be classical without a theorem that says so.
176 
177 The Taylor Wiles method and its later forms solve these problems in many important settings \cite{Wiles1995,TaylorWiles1995,Diamond1997,Kisin2009,Gee2022}. Higher dimensional and derived versions use a broader range of local deformation rings, residual image conditions, torsion classes, and cohomological carriers \cite{ClozelHarrisTaylor2008,BarnetLambGeeGeraghtyTaylor2014,CalegariGeraghty2018,Thorne2012,MiagkovThorne2023,Scholze2015,CaraianiScholze2017,NewtonThorne2016}. The present article does not replace those theorems. It isolates the algebraic support statements that explain exactly what a patching package supplies once its arithmetic hypotheses have been verified.
178 
179 The first correction concerns local packets. A local deformation ring is usually complete and local. Its irreducible components are rarely open and closed. They cannot generally be represented by central idempotents. The correct object is a quotient ring defining a local condition, together with the support of a module or complex on the resulting spectrum. Central idempotents reappear later, where they belong, inside finite Artin Hecke algebras and finite dimensional characteristic zero carriers.
180 
181 The second correction concerns patching. The useful global conclusion is full support, often expressed as near faithfulness. For a finite module over a Noetherian ring, near faithfulness is equivalent to full support. Full support descends through the quotient that removes the auxiliary variables. This statement is elementary, but it is the exact bridge from a patched module to componentwise occupancy at finite level. The same conclusion holds for perfect complexes through derived support.
182 
183 The third correction concerns Hecke packets. Semisimplicity is not required to isolate a maximal Hecke packet. Every finite commutative algebra over a field is a product of Artin local algebras. Its canonical central idempotents project onto simultaneous generalized eigenspaces. Trace is only a secondary criterion in characteristic zero. Support and localization are the primary notions.
184 
185 The last part assembles these statements into a conditional theorem. A characteristic zero point of \(R\) is automorphic when it lies in the support of the automorphic carrier, the comparison with the Hecke algebra is available, and the corresponding Hecke fiber satisfies the declared realization theorem. If the point belongs to a fixed strictly compatible system, equality of Frobenius polynomials propagates the automorphic identification to every coefficient place by Chebotarev density and Brauer Nesbitt \cite{BrauerNesbitt1941,Neukirch1999,Gee2022}.
186 
187 \begin{figure}[t]
188 \centering
189 \includegraphics[width=.98\textwidth]{01_global_gates.pdf}
190 \caption{The global argument has several logically separate gates.}
191 \label{fig:global_gates}
192 \end{figure}
193 
194 The organization is as follows. Local quotient conditions are developed in \cref{sec:local_conditions}. Adequacy and residual occupancy appear in \cref{sec:adequacy}. Auxiliary group algebras are treated in \cref{sec:auxiliary}. Ordinary and derived patching support appear in \cref{sec:patching_support}. The effect of \(R\cong\TT\) is isolated in \cref{sec:rt}. Finite Hecke packets and infinite occupancy are developed in \cref{sec:hecke_packets}. Pointwise automorphy and compatible systems appear in \cref{sec:pointwise,sec:compatible}. The coefficient prime two is discussed in \cref{sec:two}. The final conditional theorem is stated in \cref{sec:completion}.
195 
196 \section{Global deformation data and exact boundaries}\label{sec:global_data}
197 
198 Throughout, \(S\) is a finite set of places. Frobenius elements are geometric Frobenius elements; all Hecke polynomials, attached representations, and common algebraic spines use that same convention and the normalization specified by the declared realization theorem.
199 
200 
201 Let \(F\) be a number field. Fix a prime \(p\), a finite extension \(E/\QQ_p\), its valuation ring \(\OO\), uniformizer \(\varpi\), and residue field \(k\). Let
202 \[
203 \bar\rho:G_{F,S}\longrightarrow\GL_n(k)
204 \]
205 be a continuous residual representation, where \(S\) is a finite set of places containing every place at which the deformation problem is allowed to ramify.
206 
Statement: Global deformation datum207 \begin{definition}[Global deformation datum]\label{def:global_datum}
208 A global deformation datum consists of the following objects.
209 \begin{enumerate}
210 \item A residual representation \(\bar\rho\).
211 \item For every \(v\in S\), a framed local deformation ring \(R_v^\square\).
212 \item A quotient \(R_v^{\tau_v}\) representing the chosen local condition whenever such a quotient is known to exist.
213 \item A global deformation ring \(R^\square\) with a continuous local map
214 \[
215 R^{\mathrm{loc}}:=\wideotimes_{v\in S,\OO}R_v^\square
216 \longrightarrow R^\square.
217 \]
218 \item The induced global ring with local conditions
219 \[
220 R^{\tau}:=R^\square\wideotimes_{R^{\mathrm{loc}}}R^{\mathrm{loc},\tau},
221 \qquad
222 R^{\mathrm{loc},\tau}:=\wideotimes_{v\in S,\OO}R_v^{\tau_v}.
223 \]
224 \end{enumerate}
225 \end{definition}
226 
227 Representability of deformation functors and the construction of local condition quotients require hypotheses. The standard foundations are due to Mazur and Schlessinger, with many later refinements for local conditions and pseudorepresentations \cite{Mazur1989,Schlessinger1968,BellaicheChenevier2009}.
228 
Statement: Represented deformation problem229 \begin{standardfact}[Represented deformation problem]\label{fact:represented_deformation}
230 Under the usual finiteness and Schur type hypotheses, framed lifts of \(\bar\rho\) are represented by complete Noetherian local \(\OO\) algebras. A declared local deformation condition is represented by a quotient when the corresponding subfunctor is representable. Tangent and obstruction spaces are described by the appropriate first and second cohomology groups.
231 \end{standardfact}
232 
Statement: Automorphy lifting package233 \begin{standardfact}[Automorphy lifting package]\label{fact:automorphy_package}
234 Published automorphy lifting theorems begin with residual automorphic occupancy and impose hypotheses on the residual image, local deformation conditions, regularity, and the global deformation problem. They then use ordinary or derived patching to compare a deformation ring with a Hecke algebra and to prove automorphy for characteristic zero points in the supported locus. The precise assumptions depend on the theorem being used \cite{ClozelHarrisTaylor2008,BarnetLambGeeGeraghtyTaylor2014,CalegariGeraghty2018,Thorne2012,MiagkovThorne2023,AllenEtAl2023}.
235 \end{standardfact}
236 
237 The article treats \cref{fact:represented_deformation,fact:automorphy_package} as external inputs. Its results begin after the relevant rings, modules, complexes, and comparison maps have been supplied.
238 
Statement: Residual automorphic occupancy239 \begin{definition}[Residual automorphic occupancy]\label{def:residual_occupancy}
240 The residual datum \((\bar\rho,\tau)\) is automorphically occupied when a nonzero localized automorphic or cohomological Hecke carrier realizes the residual representation and the declared local conditions.
241 \end{definition}
242 
243 This is a depth zero hypothesis. A positive depth deformation argument above another residual root cannot produce it.
244 
245 \begin{figure}[t]
246 \centering
247 \includegraphics[width=.94\textwidth]{18_claim_boundary.pdf}
248 \caption{The article proves formal support and occupancy theorems. It does not prove the universal existence statements shown on the right.}
249 \label{fig:claim_boundary_intro}
250 \end{figure}
251 
252 \section{Local conditions are quotient packets}\label{sec:local_conditions}
253 
254 The completed tensor product combines the local deformation conditions. The first theorem records the exact quotient law.
255 
Statement: Completed tensor quotient · Go to proof · Read statement and proof side by side256 \begin{theorem}[Completed tensor quotient]\label{thm:tensor_quotient}
257 Let \(R_1,\ldots,R_s\) be complete Noetherian local \(\OO\) algebras with common residue field \(k\). Let \(I_i\subseteq R_i\) be closed ideals. Put
258 \[
259 R^{\mathrm{loc}}=R_1\wideotimes_{\OO}\cdots\wideotimes_{\OO}R_s
260 \]
261 and let \(J\) be the closed ideal generated by the images of the \(I_i\). Then there is a canonical isomorphism
262 \[
263 \boxed{
264 (R_1/I_1)\wideotimes_{\OO}\cdots\wideotimes_{\OO}(R_s/I_s)
265 \cong
266 R^{\mathrm{loc}}/J.
267 }
268 \]
269 \end{theorem}
270 
Proof block: Completed tensor quotient · Go to statement · Read statement and proof side by side271 \begin{proof}
272 Write \(S=\bigotimes_{i=1}^{s}R_i\) for the ordinary tensor product. Its ideal of definition is
273 \[
274 \fraka=\frakm_{\OO}S+\sum_i\frakm_{R_i}S,
275 \qquad L=\sum_i I_iS.
276 \]
277 The scalar term retains the base adic topology when the family is empty. The ordinary quotient theorem gives a canonical algebra isomorphism
278 \[
279 S/L\cong\bigotimes_{i=1}^{s}(R_i/I_i),
280 \]
281 carrying the image of \(\fraka\) to the defining ideal on the right. The quotient topology on \(S/L\) is precisely this image ideal topology.
282 
283 Here completion means the actual Hausdorff completion for the additive uniformity of the indicated adic topology. For every adic ring \(S\) and ideal \(L\), there is a canonical bicontinuous ring isomorphism
284 \[
285 \widehat S\big/\overline{L\widehat S}\cong\widehat{S/L}.
286 \]
287 Indeed, the completed quotient map kills the closed extended ideal. In the other direction, the quotient map from \(S/L\) to \(\widehat S/\overline{L\widehat S}\) extends to its completion. The latter quotient is complete: the adic uniformity has a countable base, and the quotient of a complete countably based additive group is complete. Its closed defining subgroup makes it Hausdorff. The two composites agree with the identity on dense quotient representatives, so continuity proves both inverse laws.
288 
289 Applying this comparison to the displayed ordinary tensor isomorphism proves the claim. The closed extended ideal is exactly \(J\), since extension commutes with the finite sum of the factor ideals. The maps preserve coefficients and each canonical factor map. The common residue field identifies \(S/\fraka\) with \(k\); finite generation of \(\fraka\), supplied by the Noetherian factor hypotheses, identifies the completed topology with its maximal ideal topology. Proper quotients retain locality. If a condition is the unit ideal, the ring comparison remains valid with the zero ring, without treating it as a local ring with residue field \(k\).
290 \end{proof}
291 
Statement: Simultaneous local conditions · Go to proof · Read statement and proof side by side292 \begin{corollary}[Simultaneous local conditions]\label{cor:simultaneous_local}
293 A continuous point of \(R^{\mathrm{loc}}\) with Hausdorff target factors continuously through \(R^{\mathrm{loc}}/J\) if and only if its restriction to every \(R_i\) factors continuously through \(R_i/I_i\). Each factor is unique. If the original point is local, its quotient factor is local.
294 \end{corollary}
295 
Proof block: Simultaneous local conditions · Go to statement · Read statement and proof side by side296 \begin{proof}
297 Let \(f:R^{\mathrm{loc}}\to A\) be the point. Since \(A\) is Hausdorff and \(f\) is continuous, \(\ker f\) is closed. Thus it contains the closed ideal \(J\) if and only if it contains the algebraic ideal generated by the images of the \(I_i\). This is equivalent to every local restriction killing \(I_i\). The universal property of the actual ideal quotient gives the factors, and the quotient topology gives their continuity. Surjectivity of the quotient map gives uniqueness. If \(f\) reflects units, lift an element of the quotient to the original ring to see that its factor also reflects units.
298 \end{proof}
299 
Statement: Global base change for local conditions · Go to proof · Read statement and proof side by side300 \begin{proposition}[Global base change for local conditions]\label{prop:global_local_basechange}
301 In the global deformation datum of \cref{def:global_datum}, let \(R^\square\) be a complete Noetherian local \(\OO\) algebra receiving a continuous local \(\OO\) algebra map from \(R^{\mathrm{loc}}\). Then
302 \[
303 R^{\tau}
304 =
305 R^\square\wideotimes_{R^{\mathrm{loc}}}R^{\mathrm{loc},\tau}
306 \]
307 represents the base change of the global deformation problem to the simultaneous local conditions. A continuous local \(\OO\) algebra point of \(R^\square\) with complete Hausdorff coefficient target factors uniquely and continuously through \(R^{\tau}\) exactly when all of its local restrictions satisfy the declared quotient conditions.
308 \end{proposition}
309 
Proof block: Global base change for local conditions · Go to statement · Read statement and proof side by side310 \begin{proof}
311 Put \(A=R^{\mathrm{loc}}\), \(B=R^\square\), and let \(J\subseteq A\) be the closed local condition ideal. By \cref{thm:tensor_quotient}, the independently constructed ring \(R^{\mathrm{loc},\tau}\) is canonically \(A/J\). The ordinary tensor identity
312 \[
313 B\otimes_A(A/J)\cong B/JB
314 \]
315 carries the defining ideal of the tensor to the image of \(\frakm_B\). Here the structural map is local by the stated global deformation datum, so it carries \(\frakm_A\) into \(\frakm_B\). Completing, and applying the completion and quotient comparison from the preceding proof, gives a bicontinuous isomorphism
316 \[
317 R^\tau\cong B/\overline{JB}.
318 \]
319 The construction commutes with the canonical map from \(B\), which is therefore surjective. It is also unchanged by transporting the tensor factor from \(A/J\) to the actual completed tensor of the local quotients. The transported ideal is exactly its natural defining ideal.
320 
321 For a continuous algebra point \(x:B\to C\) with complete Hausdorff target, the kernel of \(x\) is closed. Consequently \(x\) has a unique continuous factor through \(R^\tau\) if and only if it kills \(JB\), equivalently if its restriction to \(A\) kills \(J\). By \cref{cor:simultaneous_local}, this is exactly the requirement that all local restrictions satisfy their quotient conditions. The factor is an algebra map because its composite with the canonical global map is \(x\). If \(x\) is local, surjectivity of that map shows that its factor reflects units and is local. Uniqueness also proves naturality under coefficient preserving maps of targets. This identifies the represented base change; it does not supply representability of a new arithmetic deformation problem.
322 \end{proof}
323 
324 The local coefficient points in \cref{prop:global_local_basechange} are test rings in the represented deformation category. Later field valued points \(x:R\to E'\) are algebraic or generic specializations, and continuity of \(\rho_x\) is imposed separately. Such a field specialization need not be a local ring map: under \(\OO\to E\), a uniformizer becomes a unit.
325 
Statement: Idempotents in a local ring · Go to proof · Read statement and proof side by side326 \begin{proposition}[Idempotents in a local ring]\label{prop:local_idempotent}
327 If \(R\) is a commutative local ring, then its only idempotents are zero and one.
328 \end{proposition}
329 
Proof block: Idempotents in a local ring · Go to statement · Read statement and proof side by side330 \begin{proof}
331 Let \(e^2=e\). Since \(e+(1-e)=1\), at least one of \(e\) and \(1-e\) is a unit. If \(e\) is a unit, then \(e=1\). If \(1-e\) is a unit, then \(e=0\).
332 \end{proof}
333 
334 \begin{remark}\label{rem:components_not_idempotents}
335 An irreducible component of \(\Spec R\) for a local deformation ring need not be open and closed. It therefore need not be selected by an idempotent. Components and local conditions should be described by quotient ideals and module support. Idempotent packet formulas are reserved for finite Artin algebras or other settings with an actual product decomposition.
336 \end{remark}
337 
338 \begin{figure}[t]
339 \centering
340 \includegraphics[width=.9\textwidth]{02_local_quotient_packets.pdf}
341 \caption{Local conditions are imposed by quotient rings. Components are support loci unless a genuine product decomposition exists.}
342 \label{fig:local_quotients}
343 \end{figure}
344 
345 \section{Adequacy and the residual input}\label{sec:adequacy}
346 
347 Adequacy is one of the residual image hypotheses used in several automorphy lifting theorems. The definition and its role are external to the support arguments below \cite{GuralnickHerzigTaylorThorne2012,Thorne2012,MiagkovThorne2023}.
348 
Statement: Adequate image349 \begin{standardfact}[Adequate image]\label{fact:adequacy}
350 Let \(G\subseteq\GL(V)\) act absolutely irreducibly over a finite field \(k\) of characteristic \(p\). Under the standard definition, adequacy imposes vanishing conditions on \(H^1(G,k)\) and \(H^1(G,\ad^0V)\), a scalar condition, and a generalized eigenspace detection condition for every irreducible submodule of \(\ad^0V\).
351 \end{standardfact}
352 
353 The following small example makes the projector detection condition explicit. It is a certificate for one finite representation, not a new adequacy criterion.
354 
355 Let \(G=S_3\), let \(k=\FF_7\), and let \(V\) be the standard two dimensional representation. In the basis
356 \[
357 v_1=(1,-1,0),
358 \qquad
359 v_2=(0,1,-1),
360 \]
361 a transposition and a three cycle act by
362 \[
363 s=
364 \begin{pmatrix}
365 6&1\\
366 0&1
367 \end{pmatrix},
368 \qquad
369 t=
370 \begin{pmatrix}
371 0&6\\
372 1&6
373 \end{pmatrix}.
374 \]
375 
Statement: Finite adequacy certificate · Go to proof · Read statement and proof side by side376 \begin{theorem}[Finite adequacy certificate]\label{thm:s3_adequacy}
377 The standard representation of \(S_3\) over \(\FF_7\) is adequate. More precisely,
378 \[
379 H^0(S_3,\ad^0V)=0,
380 \qquad
381 H^1(S_3,\FF_7)=0,
382 \qquad
383 H^1(S_3,\ad^0V)=0,
384 \]
385 and
386 \[
387 \ad^0V\cong\operatorname{sgn}\oplus V.
388 \]
389 The sign summand is detected by an eigenprojector of a three cycle, and the standard summand is detected by an eigenprojector of a transposition.
390 \end{theorem}
391 
Proof block: Finite adequacy certificate · Go to statement · Read statement and proof side by side392 \begin{proof}
393 The coordinate map
394 \[
395 (a,b)\longmapsto(a,-a+b,-b)
396 \]
397 identifies the displayed matrices with the permutation action on the sum zero subspace of \(\FF_7^3\). This action is faithful. The four matrices \(1,s,t,st\) span \(M_2\) over every field of characteristic seven: the determinant of their coordinate matrix is \(4\ne0\). A subspace stable under the group is therefore stable under every endomorphism, so the representation is absolutely irreducible. The characteristic polynomials of the identity, transpositions, and three cycles are respectively
398 \[
399 (X-1)^2,\qquad (X-1)(X+1),\qquad (X-2)(X-4).
400 \]
401 Thus all eigenvalues already lie in \(\FF_7\).
402 
403 A trace zero matrix fixed by conjugation by both \(s\) and \(t\) is zero, as follows by comparing its four entries. This proves \(H^0(S_3,\ad^0V)=0\). For any \(\FF_7[S_3]\) module \(M\) and one cocycle \(f\), put
404 \[
405 u=-6^{-1}\sum_{h\in S_3}f(h).
406 \]
407 Summing \(f(gh)=g f(h)+f(g)\) over \(h\) gives \(gu-u=f(g)\). Hence every one cocycle is a coboundary and \(H^1(S_3,M)=0\), giving both asserted first cohomology vanishings.
408 
409 Write
410 \[
411 W(a,b,c)=\begin{pmatrix}a&b\\c&-a\end{pmatrix},
412 \qquad
413 Z=W(2,3,4),\quad A=W(1,1,2),\quad B=W(1,5,6).
414 \]
415 The three coordinate columns have determinant \(3\ne0\). Under conjugation,
416 \[
417 sZ=-Z,\quad tZ=Z,\qquad
418 sA=-A,\quad sB=A+B,\quad tA=B,\quad tB=-A-B.
419 \]
420 Consequently \((z,(a,b))\mapsto zZ+aA+bB\) is an equivariant isomorphism from \(\operatorname{sgn}\oplus V\) to \(\ad^0V\).
421 
422 The sign witness is \(W_{\mathrm{sgn}}=Z\), while
423 \(W_{\mathrm{std}}=W(6,4,3)=3A+3B\) belongs to the standard summand. The corresponding projectors and trace pairings are
424 \[
425 P_{t,2}=\begin{pmatrix}2&4\\3&6\end{pmatrix},
426 \qquad \Tr(P_{t,2}W_{\mathrm{sgn}})=3\ne0,
427 \]
428 \[
429 P_{s,1}=\begin{pmatrix}0&4\\0&1\end{pmatrix},
430 \qquad \Tr(P_{s,1}W_{\mathrm{std}})=6\ne0.
431 \]
432 For an operator \(D\) with \((D-\alpha I)(D-\beta I)=0\) and \(\alpha\ne\beta\), the canonical projector is
433 \[
434 P_{D,\alpha}=(\alpha-\beta)^{-1}(D-\beta I).
435 \]
436 Its image equals \(\ker((D-\alpha I)^n)\) for every \(n\ge1\), and it kills \(\ker((D-\beta I)^n)\). This identifies the displayed matrices with the generalized eigenspace projectors required in the adequacy definition.
437 
438 For detection on every irreducible submodule, one can check the stronger assertion that canonical projectors detect every nonzero matrix. In addition to the two projectors above, use
439 \[
440 P_{s,-1}=\begin{pmatrix}1&3\\0&0\end{pmatrix},
441 \qquad
442 P_{tst^{-1},1}=\begin{pmatrix}1&0\\4&0\end{pmatrix}.
443 \]
444 The four trace pairings with these matrices have trivial common kernel in \(M_2(\FF_7)\), by row reduction. Every irreducible adjoint submodule contains a nonzero matrix, so some canonical projector has nonzero trace pairing on that submodule. This verifies the last adequacy clause and completes the certificate.
445 \end{proof}
446 
447 \begin{figure}[t]
448 \centering
449 \includegraphics[width=.86\textwidth]{03_adequacy_packets.pdf}
450 \caption{The two irreducible adjoint packets are detected by different generalized eigenspace projectors.}
451 \label{fig:adequacy_packets}
452 \end{figure}
453 
454 \begin{remark}\label{rem:adequacy_boundary}
455 The theorem verifies adequacy for one finite image. A global automorphy lifting argument must verify the published residual image hypothesis for its actual representation. The calculation does not replace that step, and it does not provide a uniform coefficient prime two theorem.
456 \end{remark}
457 
458 \section{Auxiliary group algebras and augmentation}\label{sec:auxiliary}
459 
460 Let \(\Delta\) be a finite abelian \(p\) group and let
461 \[
462 \Lambda=\OO[\Delta].
463 \]
464 The augmentation map is
465 \[
466 \epsilon:\Lambda\longrightarrow\OO,
467 \qquad
468 \sum_{g\in\Delta}a_gg\longmapsto\sum_{g\in\Delta}a_g.
469 \]
470 Its kernel is the augmentation ideal \(\fraka\).
471 
Statement: Functorial group algebra transfer · Go to proof · Read statement and proof side by side472 \begin{proposition}[Functorial group algebra transfer]\label{prop:group_algebra_transfer}
473 A group homomorphism \(q:\Delta'\to\Delta\) induces an \(\OO\) algebra homomorphism
474 \[
475 q_*:\OO[\Delta']\longrightarrow\OO[\Delta].
476 \]
477 If \(q\) is surjective, then \(q_*\) is surjective. Augmentation commutes with the transfer:
478 \[
479 \epsilon_\Delta q_*=\epsilon_{\Delta'}.
480 \]
481 \end{proposition}
482 
Proof block: Functorial group algebra transfer · Go to statement · Read statement and proof side by side483 \begin{proof}
484 Extend \(q\) linearly from the group basis. Multiplicativity follows from \(q(gh)=q(g)q(h)\). Surjectivity follows because every basis element of \(\OO[\Delta]\) has a preimage. Both augmentation maps send every group element to one, which gives the final identity.
485 \end{proof}
486 
Statement: Residual augmentation algebra · Go to proof · Read statement and proof side by side487 \begin{theorem}[Residual augmentation algebra]\label{thm:residual_augmentation_algebra}
488 Suppose
489 \[
490 \Delta\cong
491 \prod_{i=1}^{r}C_{p^{n_i}}.
492 \]
493 Choose generators \(\gamma_i\), and let \(X_i=\gamma_i-1\). Then
494 \[
495 \boxed{
496 k[\Delta]
497 \cong
498 k[X_1,\ldots,X_r]
499 \big/
500 (X_1^{p^{n_1}},\ldots,X_r^{p^{n_r}}).
501 }
502 \]
503 The augmentation ideal is generated by the \(X_i\), and \(k[\Delta]\) is local.
504 \end{theorem}
505 
Proof block: Residual augmentation algebra · Go to statement · Read statement and proof side by side506 \begin{proof}
507 In characteristic \(p\),
508 \[
509 (1+X_i)^{p^{n_i}}-1=X_i^{p^{n_i}}.
510 \]
511 Thus the assignment \(X_i\mapsto\gamma_i-1\) gives a surjective homomorphism from the displayed truncated polynomial ring to \(k[\Delta]\). Both sides have dimension \(\prod_ip^{n_i}=\abs{\Delta}\) over \(k\), so the map is an isomorphism. The quotient by the ideal generated by the \(X_i\) is \(k\). Since each \(X_i\) is nilpotent, that ideal is the unique maximal ideal.
512 \end{proof}
513 
Statement: No residual character splitting · Go to proof · Read statement and proof side by side514 \begin{corollary}[No residual character splitting]\label{cor:no_residual_character_splitting}
515 The residual group algebra \(k[\Delta]\) has no nontrivial idempotents. In particular, character projectors do not split a finite \(p\) group algebra in residue characteristic \(p\).
516 \end{corollary}
517 
Proof block: No residual character splitting · Go to statement · Read statement and proof side by side518 \begin{proof}
519 The first assertion follows from locality in \cref{thm:residual_augmentation_algebra}. For the general finite \(p\) group assertion, let \(e\in k[G]\) be idempotent and write \(\epsilon:k[G]\to k\) for augmentation. Suppose \(\epsilon(e)=0\) and \(e\ne0\). The \(\FF_p\) span \(W\) of the left translates \(ge\) is a nonzero finite dimensional \(\FF_p\) vector space, stable under \(G\). Its cardinality is divisible by \(p\). The orbit counting formula implies that its fixed point set also has cardinality divisible by \(p\). Since zero is fixed, there is a nonzero fixed vector \(v\in W\).
520 
521 A vector in the regular representation fixed by all left translations has constant coefficients. Consequently \(ve=\epsilon(e)v=0\). On the other hand, \(e^2=e\) implies \(we=w\) for every \(w\in W\), hence \(ve=v\), a contradiction. Thus every idempotent of augmentation zero is zero. Since \(\epsilon(e)^2=\epsilon(e)\) in the field \(k\), either \(\epsilon(e)=0\) or \(\epsilon(e)=1\); in the latter case apply the preceding argument to \(1-e\).
522 \end{proof}
523 
524 For \(M\otimes_{\Lambda,\epsilon}\OO\), we use a right \(\Lambda\) module \(M\). The left module convention is \(\OO\otimes_{\Lambda,\epsilon}M\). Throughout, \(\fraka M\) denotes the augmentation relation submodule: it is generated by \(ma\) for right modules and by \(am\) for left modules, with \(a\in\fraka\). This convention also applies to nonabelian groups in \cref{cor:dyadic_coinvariant_recovery}. For abelian groups, both tensor orders agree over the commutative group algebra.
525 
Statement: Coinvariant recovery · Go to proof · Read statement and proof side by side526 \begin{theorem}[Coinvariant recovery]\label{thm:coinvariant_recovery}
527 Let \(M\) be a free \(\Lambda\) module of rank \(d\). Then
528 \[
529 \boxed{
530 M/\fraka M
531 \cong
532 M\otimes_{\Lambda,\epsilon}\OO
533 \cong
534 \OO^d.
535 }
536 \]
537 The statement is valid for every coefficient prime, including two.
538 \end{theorem}
539 
Proof block: Coinvariant recovery · Go to statement · Read statement and proof side by side540 \begin{proof}
541 Choose a \(\Lambda\) basis of \(M\). Tensoring the resulting isomorphism \(M\cong\Lambda^d\) along augmentation gives \(\OO^d\). Tensoring by \(\Lambda/\fraka\) is the same as quotienting by \(\fraka M\).
542 \end{proof}
543 
Statement: Iwasawa limit544 \begin{standardfact}[Iwasawa limit]\label{fact:iwasawa_limit}
545 For \(\Delta_m=(\ZZ/p^m\ZZ)^r\), the inverse limit of \(\OO[\Delta_m]\) is the Iwasawa algebra
546 \[
547 \OO[[\ZZ_p^r]]\cong\OO[[X_1,\ldots,X_r]],
548 \]
549 where \(X_i\) corresponds to a chosen topological generator minus one \cite{RibesZalesskii2010}.
550 \end{standardfact}
551 
552 \begin{figure}[t]
553 \centering
554 \includegraphics[width=.94\textwidth]{04_auxiliary_group_tower.pdf}
555 \caption{Auxiliary group algebras refine through quotient maps, while augmentation recovers the coarse level.}
556 \label{fig:auxiliary_tower}
557 \end{figure}
558 
559 \begin{figure}[t]
560 \centering
561 \includegraphics[width=.88\textwidth]{05_augmentation_algebra.pdf}
562 \caption{The residual auxiliary algebra is a local truncated polynomial algebra at every coefficient prime.}
563 \label{fig:augmentation_algebra}
564 \end{figure}
565 
566 The augmentation formalism is uniform in \(p\). The difficult coefficient two questions lie elsewhere. Residual image hypotheses, local deformation geometry, and classicality may change at two even though coinvariant recovery remains exact.
567 
568 
569 \section{Ordinary and derived patching support}\label{sec:patching_support}
570 
571 The algebraic conclusion supplied by a patching argument is most naturally stated through support. This section isolates the commutative algebra needed to descend that conclusion from a patched object to finite level.
572 
Statement: Support and near faithfulness573 \begin{definition}[Support and near faithfulness]\label{def:support_near_faithful}
574 Let \(R\) be a commutative ring and let \(M\) be an \(R\) module. Its support is
575 \[
576 \Supp_R(M)
577 =
578 \{\frakp\in\Spec R:M_{\frakp}\neq0\}.
579 \]
580 If \(R\) is Noetherian and \(M\) is finite, then \(M\) is \emph{nearly faithful} when \(\Ann_R(M)\) is a nilpotent ideal.
581 \end{definition}
582 
Statement: Finite module support · Go to proof · Read statement and proof side by side583 \begin{theorem}[Finite module support]\label{thm:finite_module_support}
584 Let \(R\) be a commutative ring and let \(M\) be a finite \(R\) module. Then
585 \[
586 \boxed{
587 \Supp_R(M)
588 =
589 V\bigl(\Ann_R(M)\bigr).
590 }
591 \]
592 \end{theorem}
593 
Proof block: Finite module support · Go to statement · Read statement and proof side by side594 \begin{proof}
595 Let \(\frakp\in\Spec R\). If \(\Ann_R(M)\not\subseteq\frakp\), choose
596 \(a\in\Ann_R(M)\setminus\frakp\). The element \(a\) becomes a unit in
597 \(R_{\frakp}\), so \(M_{\frakp}=0\).
598 
599 Conversely, suppose \(M_{\frakp}=0\). Choose generators
600 \(m_1,\ldots,m_d\) of \(M\). For each \(i\), there is an element
601 \(s_i\notin\frakp\) such that \(s_im_i=0\). The product
602 \(s=s_1\cdots s_d\) lies outside \(\frakp\) and annihilates every generator.
603 Thus \(s\in\Ann_R(M)\setminus\frakp\). This proves the equality.
604 \end{proof}
605 
Statement: Fitting support criterion · Go to proof · Read statement and proof side by side606 \begin{theorem}[Fitting support criterion]\label{thm:fitting_support}
607 Let \(R\) be Noetherian and let \(M\) be a finite \(R\) module. Then
608 \[
609 \boxed{
610 \Supp_R(M)
611 =
612 V\bigl(\Fitt_0^R(M)\bigr).
613 }
614 \]
615 \end{theorem}
616 
Proof block: Fitting support criterion · Go to statement · Read statement and proof side by side617 \begin{proof}
618 If \(M=0\), the statement follows from the usual convention \(\Fitt_0(0)=R\). Assume \(M\neq0\), and choose a finite presentation
619 \[
620 R^m\xrightarrow{A}R^n\longrightarrow M\longrightarrow0
621 \]
622 with \(n\geq1\).
623 The zeroth Fitting ideal is generated by the \(n\) by \(n\) minors of \(A\). After localization at a prime \(\frakp\), the module \(M_{\frakp}\) vanishes exactly when \(A_{\frakp}\) is surjective. A map onto the free module \(R_{\frakp}^n\) is surjective exactly when one maximal minor is a unit. Thus \(M_{\frakp}=0\) exactly when \(\Fitt_0^R(M)\not\subseteq\frakp\).
624 \end{proof}
625 
Statement: Higher Fitting strata · Go to proof · Read statement and proof side by side626 \begin{theorem}[Higher Fitting strata]\label{thm:higher_fitting_strata}
627 Let \(R\) be Noetherian and let \(M\) be finite. For \(r\geq1\), put
628 \[
629 \mu_{\frakp}(M)
630 =
631 \dim_{\kappa(\frakp)}
632 \left(M\otimes_R\kappa(\frakp)\right).
633 \]
634 Then
635 \[
636 \boxed{
637 \left\{
638 \frakp\in\Spec R:
639 \mu_{\frakp}(M)\geq r
640 \right\}
641 =
642 V\bigl(\Fitt_{r-1}^R(M)\bigr).
643 }
644 \]
645 \end{theorem}
646 
Proof block: Higher Fitting strata · Go to statement · Read statement and proof side by side647 \begin{proof}
648 Use a finite presentation with target rank \(n\). If \(r>n\), every fiber has dimension at most \(n\), so the left hand locus is empty. The convention \(\Fitt_{r-1}(M)=R\) for \(r-1\geq n\) makes the right hand locus empty as well. It remains to consider \(1\leq r\leq n\). At \(\frakp\), the fiber dimension is
649 \[
650 n-\rank A(\frakp).
651 \]
652 It is at least \(r\) exactly when the rank is at most \(n-r\), which is equivalent to the vanishing of every minor of size \(n-r+1\). Those minors generate \(\Fitt_{r-1}^R(M)\).
653 \end{proof}
654 
Statement: Fitting ideals and base change · Go to proof · Read statement and proof side by side655 \begin{proposition}[Fitting ideals and base change]\label{prop:fitting_base_change}
656 Let \(R\to S\) be a ring map and let \(M\) be a finitely presented \(R\) module. Then for every \(j\geq0\),
657 \[
658 \boxed{
659 \Fitt_j^S(M\otimes_RS)
660 =
661 \Fitt_j^R(M)S.
662 }
663 \]
664 \end{proposition}
665 
Proof block: Fitting ideals and base change · Go to statement · Read statement and proof side by side666 \begin{proof}
667 Base change carries a finite presentation matrix for \(M\) to a presentation matrix for \(M\otimes_RS\). Every defining minor is carried to the corresponding minor over \(S\).
668 \end{proof}
669 
670 \begin{remark}
671 Support records nonvanishing. The higher Fitting strata record lower bounds on the number of generators in each fiber. They should not be confused with automorphic multiplicity formulas, which require additional representation theoretic input.
672 \end{remark}
673 
Statement: Near faithfulness is full support · Go to proof · Read statement and proof side by side674 \begin{theorem}[Near faithfulness is full support]\label{thm:near_faithful_full_support}
675 Let \(R\) be Noetherian and let \(M\) be a finite \(R\) module. The following conditions are equivalent.
676 \begin{enumerate}
677 \item \(M\) is nearly faithful.
678 \item \(\Supp_R(M)=\Spec R\).
679 \item \(\Ann_R(M)\subseteq\nil(R)\).
680 \end{enumerate}
681 If \(R\) is reduced, these conditions are equivalent to faithfulness.
682 \end{theorem}
683 
Proof block: Near faithfulness is full support · Go to statement · Read statement and proof side by side684 \begin{proof}
685 By \cref{thm:finite_module_support}, full support is equivalent to
686 \[
687 V\bigl(\Ann_R(M)\bigr)=\Spec R.
688 \]
689 This holds exactly when \(\Ann_R(M)\) is contained in every prime ideal, hence in the nilradical. Because \(R\) is Noetherian, the ideal \(\Ann_R(M)\) is finitely generated. An ideal generated by finitely many nilpotent elements is nilpotent. This proves the equivalence of the first three conditions. If \(R\) is reduced, its nilradical is zero.
690 \end{proof}
691 
Statement: Support on every irreducible component · Go to proof · Read statement and proof side by side692 \begin{corollary}[Support on every irreducible component]\label{cor:every_component_support}
693 Under the hypotheses of \cref{thm:near_faithful_full_support}, a nearly faithful module is nonzero at the generic point of every irreducible component of \(\Spec R\).
694 \end{corollary}
695 
Proof block: Support on every irreducible component · Go to statement · Read statement and proof side by side696 \begin{proof}
697 Every generic point is a prime of \(R\), and full support contains every prime.
698 \end{proof}
699 
Statement: Support after a quotient · Go to proof · Read statement and proof side by side700 \begin{theorem}[Support after a quotient]\label{thm:quotient_support}
701 Let \(R\) be Noetherian, let \(I\subseteq R\) be an ideal, and let \(M\) be a finite \(R\) module. Under the canonical identification
702 \[
703 \Spec(R/I)\cong V(I)\subseteq\Spec R,
704 \]
705 one has
706 \[
707 \boxed{
708 \Supp_{R/I}(M/IM)
709 =
710 \Supp_R(M)\cap V(I).
711 }
712 \]
713 \end{theorem}
714 
Proof block: Support after a quotient · Go to statement · Read statement and proof side by side715 \begin{proof}
716 Let \(\frakp\supseteq I\). Localizing gives
717 \[
718 (M/IM)_{\frakp}
719 \cong
720 M_{\frakp}/I_{\frakp}M_{\frakp}.
721 \]
722 If \(M_{\frakp}=0\), the quotient is zero. If \(M_{\frakp}\neq0\), then
723 \(I_{\frakp}\) lies in the maximal ideal of the local ring \(R_{\frakp}\). Nakayama's lemma shows that
724 \(M_{\frakp}/I_{\frakp}M_{\frakp}\neq0\). The stated equality follows.
725 \end{proof}
726 
Statement: Ordinary patching datum727 \begin{definition}[Ordinary patching datum]\label{def:ordinary_patching_datum}
728 An ordinary patching datum consists of a Noetherian ring \(R_\infty\), an ideal
729 \(\fraka\subseteq R_\infty\), a finite \(R_\infty\) module \(M_\infty\), and identifications
730 \[
731 R\cong R_\infty/\fraka,
732 \qquad
733 M\cong M_\infty/\fraka M_\infty.
734 \]
735 In automorphy lifting applications, \(R_\infty\) is a patched deformation ring and \(M_\infty\) is a patched automorphic module. The definition itself contains no automorphy assertion.
736 \end{definition}
737 
Statement: Ordinary patching support descent · Go to proof · Read statement and proof side by side738 \begin{theorem}[Ordinary patching support descent]\label{thm:ordinary_support_descent}
739 Let \((R_\infty,\fraka,M_\infty,R,M)\) be an ordinary patching datum. If
740 \[
741 \Supp_{R_\infty}(M_\infty)=\Spec R_\infty,
742 \]
743 then
744 \[
745 \boxed{
746 \Supp_R(M)=\Spec R.
747 }
748 \]
749 Equivalently, if \(M_\infty\) is nearly faithful, then \(M\) is nearly faithful. If \(R\) is reduced, then \(M\) is faithful.
750 \end{theorem}
751 
Proof block: Ordinary patching support descent · Go to statement · Read statement and proof side by side752 \begin{proof}
753 Apply \cref{thm:quotient_support} with \(I=\fraka\). The support of the quotient is
754 \[
755 \Spec R_\infty\cap V(\fraka)=V(\fraka),
756 \]
757 which identifies with \(\Spec R\). The remaining statements follow from
758 \cref{thm:near_faithful_full_support}.
759 \end{proof}
760 
Statement: Componentwise finite level occupancy · Go to proof · Read statement and proof side by side761 \begin{corollary}[Componentwise finite level occupancy]\label{cor:componentwise_occupancy}
762 In the setting of \cref{thm:ordinary_support_descent}, every irreducible component of
763 \(\Spec R\) is contained in the support of \(M\). In particular, no component of the finite level deformation ring is erased by the quotient from the patched level.
764 \end{corollary}
765 
Proof block: Componentwise finite level occupancy · Go to statement · Read statement and proof side by side766 \begin{proof}
767 The module \(M\) has full support by \cref{thm:ordinary_support_descent}.
768 \end{proof}
769 
770 \begin{example}[Freeness over auxiliary variables is not enough]\label{ex:freeness_not_support}
771 Let \(k\) be a field, let \(S=k[[t]]\), and put
772 \[
773 R=S[[x]]/(x(x-t)).
774 \]
775 The ring \(R\) is reduced and has two irreducible components. Let
776 \[
777 M=R/(x)\cong S.
778 \]
779 Then \(M\) is free of rank one over \(S\), but
780 \[
781 \Supp_R(M)=V(x)
782 \]
783 is only one component of \(\Spec R\). Thus freeness over the auxiliary power series ring does not imply full support over the deformation ring.
784 \end{example}
785 
786 \begin{proof}
787 The two nonassociate prime factors \(x\) and \(x-t\) occur with multiplicity one, so the principal quotient is reduced. The displayed isomorphism makes \(M\) free over \(S\). Its annihilator as an \(R\) module is \((x)\), hence
788 \[
789 \Supp_R(M)=V(x)
790 \]
791 by \cref{thm:finite_module_support}. The generic point \((x-t)\) of the other component does not contain \(x\), so it is not in the support.
792 \end{proof}
793 
794 \begin{figure}[t]
795 \centering
796 \includegraphics[width=.94\textwidth]{06_patching_support_descent.pdf}
797 \caption{Full support at the patched level descends through the augmentation quotient.}
798 \label{fig:patching_support_descent}
799 \end{figure}
800 
801 \begin{figure}[t]
802 \centering
803 \includegraphics[width=.86\textwidth]{07_freeness_counterexample.pdf}
804 \caption{A module can be free over the auxiliary ring while occupying only one deformation component.}
805 \label{fig:freeness_counterexample}
806 \end{figure}
807 
808 Derived patching replaces one module by a perfect complex. The correct support is detected after derived specialization.
809 
Statement: Derived support810 \begin{definition}[Derived support]\label{def:derived_support}
811 Let \(R\) be a commutative ring and let \(C\) be a perfect complex of \(R\) modules. Its derived support is
812 \[
813 \Supp_R(C)
814 =
815 \left\{
816 \frakp\in\Spec R:
817 C\mathbin{\mathop{\otimes}\limits_R^{\mathbf L}}\kappa(\frakp)
818 \not\simeq0
819 \right\}.
820 \]
821 \end{definition}
822 
Statement: Cohomological description of derived support823 \begin{standardfact}[Cohomological description of derived support]\label{fact:derived_support_cohomology}
824 If \(R\) is Noetherian and \(C\) is perfect, then
825 \[
826 \Supp_R(C)
827 =
828 \bigcup_i\Supp_R H^i(C).
829 \]
830 In particular, derived support is closed and is empty exactly when \(C\simeq0\) \cite{Weibel1994,Eisenbud1995}.
831 \end{standardfact}
832 
Statement: Derived quotient support · Go to proof · Read statement and proof side by side833 \begin{theorem}[Derived quotient support]\label{thm:derived_quotient_support}
834 Let \(R\) be a commutative ring, let \(I\subseteq R\) be an ideal, and let \(C\) be a perfect complex over \(R\). Under
835 \(\Spec(R/I)\cong V(I)\), one has
836 \[
837 \boxed{
838 \Supp_{R/I}
839 \left(
840 C\mathbin{\mathop{\otimes}\limits_R^{\mathbf L}}R/I
841 \right)
842 =
843 \Supp_R(C)\cap V(I).
844 }
845 \]
846 \end{theorem}
847 
Proof block: Derived quotient support · Go to statement · Read statement and proof side by side848 \begin{proof}
849 Choose a bounded complex \(P\) of finite projective \(R\) modules representing \(C\). Scalar extension to a commutative \(R\) algebra \(S\) is computed degree by degree as \(S\otimes_RP\); the canonical symmetry of tensor products gives the displayed order \(C\otimes_R^{\mathbf L}S\). Scalar extension preserves the bounds, finite generation, and projectivity of the terms. A derived isomorphism between two such projective models lifts to a homotopy equivalence, which scalar extension preserves. The resulting derived object and its residue field fibers are therefore independent of the chosen model.
850 
851 Let \(q\in\Spec(R/I)\), and let \(\frakp\) be its inverse image in \(R\). The composite point \(R\to R/I\to\kappa(q)\) has kernel \(\frakp\), so it factors through a field embedding \(\kappa(\frakp)\to\kappa(q)\). The ordinary tensor associator in every degree gives an isomorphism of complexes
852 \[
853 \kappa(q)\otimes_{R/I}\bigl((R/I)\otimes_RP\bigr)
854 \cong\kappa(q)\otimes_RP
855 \cong\kappa(q)\otimes_{\kappa(\frakp)}
856 \bigl(\kappa(\frakp)\otimes_RP\bigr).
857 \]
858 Extension of fields is faithfully flat. It preserves and reflects exactness in each degree, hence also acyclicity. The left hand complex is thus nonzero in the derived category exactly when the residue field fiber of \(C\) at \(\frakp\) is nonzero. This proves the support identity on corresponding primes. The image of \(\Spec(R/I)\to\Spec R\) is exactly \(V(I)\), giving the stated ambient spectrum equality, including the case \(I=R\).
859 \end{proof}
860 
Statement: Derived patching datum861 \begin{definition}[Derived patching datum]\label{def:derived_patching_datum}
862 A derived patching datum consists of a Noetherian ring \(R_\infty\), an ideal
863 \(\fraka\), a perfect complex \(C_\infty\) over \(R_\infty\), and identifications
864 \[
865 R\cong R_\infty/\fraka,
866 \qquad
867 C\simeq
868 C_\infty
869 \mathbin{\mathop{\otimes}\limits_{R_\infty}^{\mathbf L}}R.
870 \]
871 \end{definition}
872 
Statement: Derived patching support descent · Go to proof · Read statement and proof side by side873 \begin{theorem}[Derived patching support descent]\label{thm:derived_support_descent}
874 Let \((R_\infty,\fraka,C_\infty,R,C)\) be a derived patching datum. If
875 \[
876 \Supp_{R_\infty}(C_\infty)=\Spec R_\infty,
877 \]
878 then
879 \[
880 \boxed{
881 \Supp_R(C)=\Spec R.
882 }
883 \]
884 For every point \(x:R\to E'\) to a field, the derived fiber
885 \[
886 C\mathbin{\mathop{\otimes}\limits_{R,x}^{\mathbf L}}E'
887 \]
888 is nonzero.
889 \end{theorem}
890 
Proof block: Derived patching support descent · Go to statement · Read statement and proof side by side891 \begin{proof}
892 Apply \cref{thm:derived_quotient_support} to the patched complex and use the actual ring identification \(R\cong R_\infty/\fraka\). Full patched support restricts to \(V(\fraka)\), which corresponds to all of \(\Spec R\). The supplied derived isomorphism with \(C\) preserves this support by the projective model argument in that theorem.
893 
894 For a field valued point \(x:R\to E'\), put \(\frakp=\ker x\). The point factors as \(R\to\kappa(\frakp)\to E'\), where the second map is a field embedding. Tensor association on a projective model identifies the fiber at \(x\) with the extension to \(E'\) of the fiber at \(\frakp\). The latter is nonzero by full support. Faithful flatness of the field extension reflects exactness in every degree, so the fiber at \(x\) is nonzero as well. This applies to every field valued point, with no closed point restriction.
895 \end{proof}
896 
Statement: A nonzero cohomological degree survives · Go to proof · Read statement and proof side by side897 \begin{corollary}[A nonzero cohomological degree survives]\label{cor:derived_degree_survives}
898 Under the hypotheses of \cref{thm:derived_support_descent}, for every field valued point \(x:R\to E'\), there is an integer \(i\) such that
899 \[
900 H^i
901 \left(
902 C\mathbin{\mathop{\otimes}\limits_{R,x}^{\mathbf L}}E'
903 \right)
904 \neq0.
905 \]
906 \end{corollary}
907 
Proof block: A nonzero cohomological degree survives · Go to statement · Read statement and proof side by side908 \begin{proof}
909 The derived fiber is nonzero by \cref{thm:derived_support_descent}. If every cohomology object vanished, a cochain model of that fiber would be acyclic. Its image in the derived category would then be zero, a contradiction. Hence some integer degree has nonzero cohomology.
910 \end{proof}
911 
912 \begin{remark}
913 The support theorem does not decide the cohomological degree in which the point occurs. It also does not prove that the surviving class is classical. Those are separate arithmetic inputs.
914 \end{remark}
915 
916 \section{Transport through an isomorphism \texorpdfstring{\(R\cong\TT\)}{R equals T}}\label{sec:rt}
917 
918 An isomorphism between a deformation ring and a Hecke algebra is an exact coordinate change. It transports support and finite presentation data, but it does not create a supported module.
919 
Statement: Support and Fitting transport · Go to proof · Read statement and proof side by side920 \begin{theorem}[Support and Fitting transport]\label{thm:rt_support_transport}
921 Let \(\varphi:R\to\TT\) be an isomorphism of Noetherian rings. Let \(M\) be a finite \(\TT\) module, viewed as an \(R\) module through \(\varphi\). Then the homeomorphism
922 \[
923 \varphi^*:\Spec\TT\longrightarrow\Spec R
924 \]
925 satisfies
926 \[
927 \boxed{
928 \varphi^*\bigl(\Supp_{\TT}(M)\bigr)
929 =
930 \Supp_R(M).
931 }
932 \]
933 For every \(j\geq0\),
934 \[
935 \boxed{
936 \varphi
937 \left(
938 \Fitt_j^R(M)
939 \right)
940 =
941 \Fitt_j^{\TT}(M).
942 }
943 \]
944 \end{theorem}
945 
Proof block: Support and Fitting transport · Go to statement · Read statement and proof side by side946 \begin{proof}
947 Localization commutes with transport along an isomorphism, so a localization of \(M\) vanishes on one side exactly when the corresponding localization vanishes on the other. This proves the support identity. A finite presentation matrix over \(R\) is carried entry by entry to a presentation matrix over \(\TT\). The minors generating each Fitting ideal are therefore carried to the corresponding minors.
948 \end{proof}
949 
Statement: Full support is invariant under texorpdfstring (R cong TT )R equals T · Go to proof · Read statement and proof side by side950 \begin{corollary}[Full support is invariant under \texorpdfstring{\(R\cong\TT\)}{R equals T}]\label{cor:rt_full_support}
951 In the setting of \cref{thm:rt_support_transport}, \(M\) has full \(R\) support if and only if it has full \(\TT\) support.
952 \end{corollary}
953 
Proof block: Full support is invariant under texorpdfstring (R cong TT )R equals T · Go to statement · Read statement and proof side by side954 \begin{proof}
955 Apply the support homeomorphism in \cref{thm:rt_support_transport}.
956 \end{proof}
957 
Statement: A quotient can erase a component · Go to proof · Read statement and proof side by side958 \begin{proposition}[A quotient can erase a component]\label{prop:quotient_erases_component}
959 Let
960 \[
961 R=k[[x,y]]/(xy)
962 \]
963 and let
964 \[
965 \TT=R/(x)\cong k[[y]].
966 \]
967 Viewed as an \(R\) module, \(\TT\) has support \(V(x)\), which misses the generic point \((y)\) of the other irreducible component. Thus a surjection \(R\twoheadrightarrow\TT\) does not by itself imply full component occupancy.
968 \end{proposition}
969 
Proof block: A quotient can erase a component · Go to statement · Read statement and proof side by side970 \begin{proof}
971 The annihilator of the \(R\) module \(\TT\) is \((x)\). Hence its support is \(V(x)\) by \cref{thm:finite_module_support}. The prime \((y)\) does not contain \(x\), so it is not in this support.
972 \end{proof}
973 
Statement: Field fiber criterion · Go to proof · Read statement and proof side by side974 \begin{theorem}[Field fiber criterion]\label{thm:field_fiber_criterion}
975 Let \(R\) be a commutative ring, let \(M\) be a finite \(R\) module, and let
976 \(x:R\to E'\) be a homomorphism to a field. Put \(\frakp=\ker x\). Then
977 \[
978 \boxed{
979 M\otimes_{R,x}E'\neq0
980 \quad\Longleftrightarrow\quad
981 \frakp\in\Supp_R(M).
982 }
983 \]
984 \end{theorem}
985 
Proof block: Field fiber criterion · Go to statement · Read statement and proof side by side986 \begin{proof}
987 The map \(x\) factors through the local ring \(R_{\frakp}\) and then through an embedding of the residue field \(\kappa(\frakp)\) into \(E'\). Since \(M\) is finite, Nakayama's lemma gives
988 \[
989 M_{\frakp}\neq0
990 \quad\Longleftrightarrow\quad
991 M\otimes_R\kappa(\frakp)\neq0.
992 \]
993 Extension of scalars from \(\kappa(\frakp)\) to \(E'\) preserves nonzero vector spaces.
994 \end{proof}
995 
Statement: Supported deformation points give nonzero Hecke fibers · Go to proof · Read statement and proof side by side996 \begin{corollary}[Supported deformation points give nonzero Hecke fibers]\label{cor:supported_hecke_fiber}
997 Let \(R\cong\TT\), and let \(M\) be a finite Hecke module. If a point
998 \(x:R\to E'\) lies in \(\Supp_R(M)\), then the corresponding Hecke fiber
999 \[
1000 M\otimes_{\TT,x}E'
1001 \]
1002 is nonzero.
1003 \end{corollary}
1004 
Proof block: Supported deformation points give nonzero Hecke fibers · Go to statement · Read statement and proof side by side1005 \begin{proof}
1006 Transport the support through \cref{thm:rt_support_transport}, then apply
1007 \cref{thm:field_fiber_criterion}.
1008 \end{proof}
1009 
1010 \begin{figure}[t]
1011 \centering
1012 \includegraphics[width=.94\textwidth]{08_rt_support_transport.pdf}
1013 \caption{An isomorphism transports occupied support exactly. A quotient can remove a component.}
1014 \label{fig:rt_support_transport}
1015 \end{figure}
1016 
1017 \section{Finite Hecke packets and infinite occupancy}\label{sec:hecke_packets}
1018 
1019 Finite Hecke carriers admit canonical packets even when the Hecke action is not semisimple. The packets come from the Artin local factors of the finite commutative Hecke algebra.
1020 
Statement: Artin decomposition1021 \begin{standardfact}[Artin decomposition]\label{fact:artin_decomposition}
1022 Let \(E'\) be a field and let \(\TT\) be a finite dimensional commutative
1023 \(E'\) algebra. Then
1024 \[
1025 \boxed{
1026 \TT
1027 \cong
1028 \prod_{\frakm\in\Max\TT}\TT_{\frakm}.
1029 }
1030 \]
1031 Each factor is an Artin local algebra. Equivalently, there is a unique complete family of central idempotents \((e_{\frakm})\) such that
1032 \[
1033 e_{\frakm}e_{\mathfrak n}=0
1034 \quad(\frakm\neq\mathfrak n),
1035 \qquad
1036 \sum_{\frakm}e_{\frakm}=1,
1037 \]
1038 and \(e_{\frakm}\TT\cong\TT_{\frakm}\) \cite{AtiyahMacdonald1969,Matsumura1989}.
1039 \end{standardfact}
1040 
Statement: Canonical Hecke packet decomposition · Go to proof · Read statement and proof side by side1041 \begin{theorem}[Canonical Hecke packet decomposition]\label{thm:canonical_hecke_packets}
1042 Let \(\TT\) be a finite dimensional commutative algebra over a field \(E'\), and let \(V\) be a finite \(\TT\) module. Then
1043 \[
1044 \boxed{
1045 V
1046 =
1047 \bigoplus_{\frakm\in\Max\TT}e_{\frakm}V.
1048 }
1049 \]
1050 For every maximal ideal \(\frakm\), the canonical map gives
1051 \[
1052 \boxed{
1053 e_{\frakm}V\cong V_{\frakm}.}
1054 \]
1055 The packet \(e_{\frakm}V\) is nonzero exactly when \(\frakm\in\Supp_{\TT}(V)\).
1056 \end{theorem}
1057 
Proof block: Canonical Hecke packet decomposition · Go to statement · Read statement and proof side by side1058 \begin{proof}
1059 The idempotent relations in \cref{fact:artin_decomposition} give the direct sum decomposition. Localization at \(\frakm\) kills every factor except the \(\frakm\) factor, where \(e_{\frakm}\) becomes one. Thus the localization map identifies \(e_{\frakm}V\) with \(V_{\frakm}\). The final statement is the definition of support.
1060 \end{proof}
1061 
Statement: Simultaneous generalized eigenspaces · Go to proof · Read statement and proof side by side1062 \begin{corollary}[Simultaneous generalized eigenspaces]\label{cor:simultaneous_generalized_eigenspaces}
1063 Assume that \(E'\) is algebraically closed and that \(\TT\) is generated by commuting operators \(T_1,\ldots,T_d\) on \(V\). For a maximal ideal
1064 \[
1065 \frakm
1066 =
1067 (T_1-\lambda_1,\ldots,T_d-\lambda_d),
1068 \]
1069 there is an integer \(N\geq1\) such that
1070 \[
1071 \boxed{
1072 e_{\frakm}V
1073 =
1074 \left\{
1075 v\in V:
1076 (T_i-\lambda_i)^Nv=0
1077 \text{ for every }i
1078 \right\}.
1079 }
1080 \]
1081 Thus the canonical Artin packet is the simultaneous generalized eigenspace.
1082 \end{corollary}
1083 
Proof block: Simultaneous generalized eigenspaces · Go to statement · Read statement and proof side by side1084 \begin{proof}
1085 The maximal ideal of the Artin local algebra \(\TT_{\frakm}\) is nilpotent. Hence a common power of every \(T_i-\lambda_i\) kills the local packet. On every other local factor, at least one \(T_i-\lambda_i\) is a unit, so no nonzero vector can satisfy all the displayed nilpotence conditions.
1086 
1087 Conversely, suppose every \((T_i-\lambda_i)^N\) kills \(v\). Every monomial of total degree greater than \(d(N-1)\) contains one factor to exponent at least \(N\). Therefore a power of \(\frakm\) kills \(v\), which places \(v\) in the \(\frakm\) primary packet.
1088 \end{proof}
1089 
Statement: Rank and trace detection in characteristic zero · Go to proof · Read statement and proof side by side1090 \begin{corollary}[Rank and trace detection in characteristic zero]\label{cor:rank_trace_detection}
1091 Assume that \(E'\) has characteristic zero. For every maximal Hecke packet,
1092 \[
1093 \boxed{
1094 \Tr_{E'}(e_{\frakm}|V)
1095 =
1096 \rank_{E'}(e_{\frakm}|V)
1097 =
1098 \dim_{E'}e_{\frakm}V.
1099 }
1100 \]
1101 In particular, the packet is occupied exactly when its projector has positive rank, equivalently nonzero trace.
1102 \end{corollary}
1103 
Proof block: Rank and trace detection in characteristic zero · Go to statement · Read statement and proof side by side1104 \begin{proof}
1105 An idempotent linear map has minimal polynomial dividing \(X(X-1)\), which has distinct roots. It is diagonalizable with eigenvalues zero and one. Its trace and rank both equal the multiplicity of the eigenvalue one. A positive integer is nonzero in characteristic zero.
1106 \end{proof}
1107 
1108 \begin{remark}
1109 The trace criterion can fail in positive characteristic when the packet dimension is divisible by the characteristic. The rank and localization criteria remain valid.
1110 \end{remark}
1111 
1112 \begin{figure}[t]
1113 \centering
1114 \includegraphics[width=.92\textwidth]{09_hecke_artin_packets.pdf}
1115 \caption{A finite commutative Hecke algebra splits into canonical Artin local packets.}
1116 \label{fig:hecke_artin_packets}
1117 \end{figure}
1118 
1119 \begin{figure}[t]
1120 \centering
1121 \includegraphics[width=.9\textwidth]{10_generalized_eigenspaces.pdf}
1122 \caption{An Artin packet is a simultaneous generalized eigenspace, not necessarily an ordinary eigenspace.}
1123 \label{fig:generalized_eigenspaces}
1124 \end{figure}
1125 
1126 \begin{example}[A nonsemisimple Hecke packet]\label{ex:nonsemisimple_hecke_packet}
1127 Let
1128 \[
1129 \TT
1130 =
1131 E'[u]/(u^2)
1132 \times
1133 E'[v]/(v^3)
1134 \]
1135 and let \(V=\TT\) be the regular module. The two canonical central idempotents split
1136 \[
1137 V=V_u\oplus V_v
1138 \]
1139 with dimensions two and three. Multiplication by \(u\) is nilpotent on \(V_u\), and multiplication by \(v\) is nilpotent on \(V_v\). Neither local factor is semisimple, but the two maximal Hecke packets are isolated exactly by the Artin idempotents.
1140 \end{example}
1141 
1142 \begin{proof}
1143 The product decomposition gives the two central idempotents \((1,0)\) and \((0,1)\). Their ranges are the two local factors. The classes of \(u\) and \(v\) are nilpotent of orders two and three, respectively.
1144 \end{proof}
1145 
1146 The next two theorems distinguish a fixed finite carrier from a sequence of changing carriers.
1147 
Statement: Nested packets in one finite carrier · Go to proof · Read statement and proof side by side1148 \begin{theorem}[Nested packets in one finite carrier]\label{thm:nested_finite_carrier}
1149 Let \(V\) be a finite dimensional vector space. Let \(e_1,e_2,\ldots\) be idempotents such that
1150 \[
1151 e_{m+1}e_m=e_me_{m+1}=e_{m+1}
1152 \]
1153 for every \(m\). If \(e_mV\neq0\) for every \(m\), then the descending chain stabilizes and
1154 \[
1155 \boxed{
1156 \bigcap_{m\geq1}e_mV
1157 \neq0.
1158 }
1159 \]
1160 \end{theorem}
1161 
Proof block: Nested packets in one finite carrier · Go to statement · Read statement and proof side by side1162 \begin{proof}
1163 The displayed relations give
1164 \[
1165 e_{m+1}V\subseteq e_mV.
1166 \]
1167 The nonnegative dimensions form a nonincreasing sequence of positive integers, so they eventually become constant. Once two consecutive dimensions agree, the corresponding inclusion is equality. Thus the ranges stabilize at a nonzero subspace, which is their intersection.
1168 \end{proof}
1169 
Statement: Finite witness of incompatibility · Go to proof · Read statement and proof side by side1170 \begin{corollary}[Finite witness of incompatibility]\label{cor:finite_witness_incompatibility}
1171 Under the hypotheses of \cref{thm:nested_finite_carrier}, if
1172 \[
1173 \bigcap_{m\geq1}e_mV=0,
1174 \]
1175 then \(e_mV=0\) for some finite \(m\).
1176 \end{corollary}
1177 
Proof block: Finite witness of incompatibility · Go to statement · Read statement and proof side by side1178 \begin{proof}
1179 This is the contrapositive of \cref{thm:nested_finite_carrier}.
1180 \end{proof}
1181 
1182 \begin{figure}[t]
1183 \centering
1184 \includegraphics[width=.9\textwidth]{11_finite_occupancy_staircase.pdf}
1185 \caption{Nested nonzero packets in one finite carrier stabilize after finitely many steps.}
1186 \label{fig:finite_occupancy_staircase}
1187 \end{figure}
1188 
Statement: Stable core1189 \begin{definition}[Stable core]\label{def:stable_core}
1190 Let
1191 \[
1192 V_1\longleftarrow V_2\longleftarrow V_3\longleftarrow\cdots
1193 \]
1194 be an inverse system of finite dimensional vector spaces. For \(n\geq m\), write
1195 \(f_{n,m}:V_n\to V_m\). The stable core at level \(m\) is
1196 \[
1197 Y_m
1198 =
1199 \bigcap_{n\geq m}\im(f_{n,m}).
1200 \]
1201 \end{definition}
1202 
Statement: Surjectivity on stable cores · Go to proof · Read statement and proof side by side1203 \begin{lemma}[Surjectivity on stable cores]\label{lem:stable_core_surjectivity}
1204 For every \(m\), the transition map \(V_{m+1}\to V_m\) induces a surjection
1205 \[
1206 \boxed{
1207 Y_{m+1}\twoheadrightarrow Y_m.
1208 }
1209 \]
1210 \end{lemma}
1211 
Proof block: Surjectivity on stable cores · Go to statement · Read statement and proof side by side1212 \begin{proof}
1213 Fix \(y\in Y_m\). For \(n\geq m+1\), let
1214 \[
1215 A_n
1216 =
1217 \left\{
1218 z\in\im(f_{n,m+1}):
1219 f_{m+1,m}(z)=y
1220 \right\}.
1221 \]
1222 Each \(A_n\) is a nonempty affine subspace of \(V_{m+1}\), and the sequence
1223 \((A_n)\) is descending. A descending sequence of affine subspaces in a finite dimensional vector space stabilizes whenever every term is nonempty. Choose an element in its stable value. It lies in \(Y_{m+1}\) and maps to \(y\).
1224 \end{proof}
1225 
Statement: Nonzero stable core criterion · Go to proof · Read statement and proof side by side1226 \begin{theorem}[Nonzero stable core criterion]\label{thm:nonzero_stable_core}
1227 Let \((V_m)\) be an inverse system of finite dimensional vector spaces. If
1228 \[
1229 Y_m\neq0
1230 \]
1231 for every \(m\), then
1232 \[
1233 \boxed{
1234 \varprojlim_mV_m
1235 \neq0.
1236 }
1237 \]
1238 More precisely, the inverse limit contains a compatible sequence whose first coordinate is any prescribed nonzero element of \(Y_1\).
1239 \end{theorem}
1240 
Proof block: Nonzero stable core criterion · Go to statement · Read statement and proof side by side1241 \begin{proof}
1242 Choose \(0\neq y_1\in Y_1\). By \cref{lem:stable_core_surjectivity}, choose recursively
1243 \(y_{m+1}\in Y_{m+1}\) mapping to \(y_m\). Every \(y_m\) is nonzero because it maps to the nonzero vector \(y_1\). The sequence \((y_m)\) is a nonzero element of the inverse limit.
1244 \end{proof}
1245 
Statement: Surjective systems · Go to proof · Read statement and proof side by side1246 \begin{corollary}[Surjective systems]\label{cor:surjective_inverse_system}
1247 If every transition map \(V_{m+1}\to V_m\) is surjective and every \(V_m\) is nonzero, then the inverse limit is nonzero.
1248 \end{corollary}
1249 
Proof block: Surjective systems · Go to statement · Read statement and proof side by side1250 \begin{proof}
1251 Surjectivity gives \(Y_m=V_m\). Apply \cref{thm:nonzero_stable_core}.
1252 \end{proof}
1253 
1254 \begin{example}[Tail escape in an infinite carrier]\label{ex:tail_escape}
1255 Let \(V=\ell^2(\NN)\), and let \(P_m\) be the orthogonal projection onto the closed span of
1256 \[
1257 e_m,e_{m+1},e_{m+2},\ldots.
1258 \]
1259 Every range \(P_mV\) is nonzero and the ranges are nested, but
1260 \[
1261 \boxed{
1262 \bigcap_{m\geq1}P_mV=0.
1263 }
1264 \]
1265 Thus the finite carrier hypothesis in \cref{thm:nested_finite_carrier} cannot be removed.
1266 \end{example}
1267 
1268 \begin{proof}
1269 A vector in every tail range has its first \(m-1\) coordinates equal to zero for every \(m\). All of its coordinates vanish.
1270 \end{proof}
1271 
1272 \begin{figure}[t]
1273 \centering
1274 \includegraphics[width=.9\textwidth]{12_stable_core_inverse_limit.pdf}
1275 \caption{Changing finite carriers require a nonzero stable core, not only nonzero individual levels.}
1276 \label{fig:stable_core_inverse_limit}
1277 \end{figure}
1278 
1279 \begin{figure}[t]
1280 \centering
1281 \includegraphics[width=.88\textwidth]{13_tail_escape.pdf}
1282 \caption{Nested nonzero ranges can escape to infinity in an infinite dimensional carrier.}
1283 \label{fig:tail_escape}
1284 \end{figure}
1285 
1286 \section{Pointwise automorphy from support}\label{sec:pointwise}
1287 
1288 Support produces a nonzero Hecke fiber. A realization theorem is still required to turn that fiber into a classical automorphic representation and to identify its Galois representation.
1289 
Statement: Automorphic Hecke datum1290 \begin{definition}[Automorphic Hecke datum]\label{def:automorphic_hecke_datum}
1291 An automorphic Hecke datum consists of the following objects.
1292 \begin{enumerate}
1293 \item A commutative \(\OO\) algebra \(\TT\).
1294 \item A finite \(\TT\) module \(H\), or a perfect \(\TT\) complex \(C\), obtained from an automorphic or cohomological carrier.
1295 \item For every unramified place \(v\) outside a finite set, a polynomial
1296 \[
1297 P_v(X)\in\TT[X].
1298 \]
1299 \item A declared characteristic zero locus on which a nonzero field fiber is known to be classical and is known to carry an attached Galois representation whose Frobenius polynomial at \(v\) is the specialization of \(P_v(X)\).
1300 \end{enumerate}
1301 \end{definition}
1302 
Statement: Chebotarev and Brauer Nesbitt identification1303 \begin{standardfact}[Chebotarev and Brauer Nesbitt identification]\label{fact:chebotarev_brauer_nesbitt}
1304 Let \(E'\) be a Hausdorff topological field of characteristic zero, with continuous ring operations. Let
1305 \[
1306 \rho_1,\rho_2:G_{F,S}\longrightarrow\GL_n(E')
1307 \]
1308 be continuous semisimple representations. If their characteristic polynomials agree at every Frobenius element outside a density zero exceptional set, then
1309 \[
1310 \boxed{\rho_1\cong\rho_2.}
1311 \]
1312 This follows from Chebotarev density and the Brauer Nesbitt theorem
1313 \cite{BrauerNesbitt1941,Neukirch1999,Gee2022}.
1314 \end{standardfact}
1315 
Statement: Support gives a Hecke eigensystem · Go to proof · Read statement and proof side by side1316 \begin{theorem}[Support gives a Hecke eigensystem]\label{thm:support_gives_hecke_system}
1317 Let \(R\cong\TT\), let \(H\) be a finite \(\TT\) module, and let
1318 \(x:R\to E'\) be a field valued point. If
1319 \[
1320 \ker x\in\Supp_R(H),
1321 \]
1322 then
1323 \[
1324 \boxed{
1325 H_x:=H\otimes_{\TT,x}E'\neq0.
1326 }
1327 \]
1328 Every element of \(\TT\) acts on \(H_x\) through the scalar prescribed by \(x\).
1329 \end{theorem}
1330 
Proof block: Support gives a Hecke eigensystem · Go to statement · Read statement and proof side by side1331 \begin{proof}
1332 Nonvanishing follows from \cref{cor:supported_hecke_fiber}. The tensor product relation
1333 \[
1334 th\otimes1=h\otimes x(t)
1335 \]
1336 shows that \(t\in\TT\) acts through \(x(t)\).
1337 \end{proof}
1338 
Statement: Pointwise Galois realization · Go to proof · Read statement and proof side by side1339 \begin{theorem}[Pointwise Galois realization]\label{thm:pointwise_galois_realization}
1340 Let \(E'\) be a Hausdorff topological field of characteristic zero, with continuous ring operations. Require both \(\rho_x=x\circ\rho_R\) and the attached representation below to be continuous. Assume the following data.
1341 \begin{enumerate}
1342 \item A represented deformation ring \(R\) with universal representation
1343 \[
1344 \rho_R:G_{F,S}\longrightarrow\GL_n(R).
1345 \]
1346 \item An isomorphism \(R\cong\TT\).
1347 \item An automorphic Hecke datum \((\TT,H,(P_v))\).
1348 \item A characteristic zero point \(x:R\to E'\) lying in \(\Supp_R(H)\).
1349 \item A classical automorphic representation \(\pi_x\) occurring in the fiber \(H_x\), together with a semisimple attached representation
1350 \[
1351 \rho_{\pi_x}:G_{F,S}\longrightarrow\GL_n(E')
1352 \]
1353 whose unramified characteristic polynomial is \(x(P_v(X))\).
1354 \item Equality
1355 \[
1356 \det\left(X-\rho_x(\Frob_v)\right)=x(P_v(X))
1357 \]
1358 for \(\rho_x=x\circ\rho_R\) at every unramified place in a Chebotarev dense set.
1359 \end{enumerate}
1360 Then
1361 \[
1362 \boxed{
1363 \rho_x^{\mathrm{ss}}
1364 \cong
1365 \rho_{\pi_x}.
1366 }
1367 \]
1368 If \(\rho_x\) is irreducible, then \(\rho_x\cong\rho_{\pi_x}\).
1369 \end{theorem}
1370 
Proof block: Pointwise Galois realization · Go to statement · Read statement and proof side by side1371 \begin{proof}
1372 The coefficients of the characteristic polynomials of \(\rho_x\) and \(\rho_{\pi_x}\) are continuous and constant on conjugacy classes. Their equality on the declared dense union of Frobenius conjugacy classes therefore extends to every element of \(G_{F,S}\), by Hausdorffness. A semisimplification has the same characteristic polynomials as the original representation. The algebraic Brauer Nesbitt input in \cref{fact:chebotarev_brauer_nesbitt} thus gives \(\rho_x^{\mathrm{ss}}\cong\rho_{\pi_x}\). If \(\rho_x\) is irreducible, it is already semisimple.
1373 \end{proof}
1374 
Statement: Full support gives pointwise automorphy on the realized locus · Go to proof · Read statement and proof side by side1375 \begin{corollary}[Full support gives pointwise automorphy on the realized locus]\label{cor:full_support_pointwise_automorphy}
1376 In the setting of \cref{thm:pointwise_galois_realization}, suppose
1377 \[
1378 \Supp_R(H)=\Spec R.
1379 \]
1380 For every characteristic zero point \(x:R\to E'\) with \(\ker x\in U\subseteq\Spec R\), assume the coefficient topology and continuity hypotheses of \cref{thm:pointwise_galois_realization} and the declared classicality and Galois realization input. Then every such point is automorphic in the precise sense of \cref{thm:pointwise_galois_realization}.
1381 \end{corollary}
1382 
Proof block: Full support gives pointwise automorphy on the realized locus · Go to statement · Read statement and proof side by side1383 \begin{proof}
1384 Every point of \(U\) lies in the support, so \cref{thm:support_gives_hecke_system} gives a nonzero Hecke fiber. Apply the declared realization input and then \cref{thm:pointwise_galois_realization}.
1385 \end{proof}
1386 
Statement: Derived pointwise realization · Go to proof · Read statement and proof side by side1387 \begin{theorem}[Derived pointwise realization]\label{thm:derived_pointwise_realization}
1388 Let \(e:R\cong\TT\), and let \(C\) be a perfect automorphic Hecke complex with full derived support. Choose a bounded finite projective model for \(C\), supported in degrees \([a,b]\). For every characteristic zero point \(x:R\to E'\), write \(y=x\circ e^{-1}\). Then some integer \(i\in[a,b]\) has
1389 \[
1390 H^i\left(C\mathbin{\mathop{\otimes}\limits_{\TT,y}^{\mathbf L}}E'\right)\neq0.
1391 \]
1392 Every \(t\in\TT\) acts on this cohomology through \(y(t)\).
1393 
1394 For the realization conclusion, give \(E'\) a Hausdorff topological field structure. Supply a universal representation \(\rho_R\), a continuous specialization \(\rho_x=x\circ\rho_R\), and a semisimplification of \(\rho_x\). Suppose its characteristic polynomials on a Chebotarev dense set are \(y(P_v(X))\). Let the declared classicality range contain \([a,b]\). Assume that every nonzero Hecke eigensystem in that range is realized by a classical automorphic representation occurring in that degree, with a continuous semisimple attached representation whose characteristic polynomials on the same dense set are \(y(P_v(X))\). With the standard Chebotarev density and Brauer Nesbitt inputs of \cref{fact:chebotarev_brauer_nesbitt}, the specialization \(\rho_x\) is automorphic after semisimplification. If \(\rho_x\) is irreducible, it is itself isomorphic to the attached representation.
1395 \end{theorem}
1396 
Proof block: Derived pointwise realization · Go to statement · Read statement and proof side by side1397 \begin{proof}
1398 Full derived support gives a nonzero fiber at \(y\). Scalar extension of the chosen projective model preserves its degree bounds. Its cohomology therefore vanishes below \(a\) and above \(b\). Since vanishing in every degree is equivalent to being zero in the derived category, some degree \(i\in[a,b]\) has nonzero cohomology. Choose a nonzero vector in that cohomology module.
1399 
1400 Multiplication by \(t\in\TT\) is a cochain endomorphism of the original model. In the scalar extension the tensor relation identifies this endomorphism with \(y(t)\) times the identity. Passing to the derived category and then to cohomology preserves this equality. Thus the chosen vector is a common Hecke eigenvector with character \(y\).
1401 
1402 The interval inclusion puts this eigensystem in the declared classicality range. Apply the realization input to obtain an occurring automorphic representation and its continuous semisimple attached representation. Its Frobenius characteristic polynomials agree with those of \(\rho_x\) on the prescribed dense set. Continuity extends the equality to every group element. The supplied semisimplification preserves these polynomials, so the general Brauer Nesbitt input gives an invertible linear intertwiner. If \(\rho_x\) is irreducible, it is already semisimple and the same comparison applies directly.
1403 \end{proof}
1404 
1405 \begin{remark}
1406 Derived support does not identify the cohomological degree, Hodge type, or classical weight of the surviving eigensystem. Those properties must come from the external local and global realization theorem.
1407 \end{remark}
1408 
1409 \begin{figure}[t]
1410 \centering
1411 \includegraphics[width=.94\textwidth]{16_pointwise_automorphy.pdf}
1412 \caption{Support gives a nonzero Hecke fiber. Classicality and Galois realization complete the pointwise argument.}
1413 \label{fig:pointwise_automorphy}
1414 \end{figure}
1415 
1416 \section{Compatible systems and companion completion}\label{sec:compatible}
1417 
1418 Pointwise automorphy at one coefficient place and existence of companions at other coefficient places are different statements. They meet only after a common algebraic Frobenius spine has been fixed.
1419 
Statement: Algebraic Frobenius spine1420 \begin{definition}[Algebraic Frobenius spine]\label{def:frobenius_spine}
1421 An algebraic Frobenius spine consists of a number field \(L\), a finite set of places \(S\) of \(F\), and polynomials
1422 \[
1423 P_v(X)\in L[X]
1424 \]
1425 for every finite place \(v\notin S\), together with any additional local labels required by the declared compatibility problem.
1426 \end{definition}
1427 
Statement: Finite companion forest1428 \begin{definition}[Finite companion forest]\label{def:companion_forest}
1429 Fix a coefficient place \(\lambda\) of \(L\). A finite companion forest for the spine is an inverse system of finite sets
1430 \[
1431 X_{\lambda,1}
1432 \longleftarrow
1433 X_{\lambda,2}
1434 \longleftarrow
1435 X_{\lambda,3}
1436 \longleftarrow\cdots
1437 \]
1438 whose points are admissible realizations modulo \(\lambda^m\), with edges given by reduction. A complete realization is admissible for this forest when all its finite reductions belong to the displayed levels; the empty level obstruction below concerns this declared admissibility problem.
1439 \end{definition}
1440 
Statement: Companion branch criterion · Go to proof · Read statement and proof side by side1441 \begin{theorem}[Companion branch criterion]\label{thm:companion_branch_criterion}
1442 Suppose every level \(X_{\lambda,m}\) is finite and nonempty, and every point reduces along the displayed forest to the fixed residual root. Then
1443 \[
1444 \boxed{
1445 \varprojlim_mX_{\lambda,m}
1446 \neq\varnothing.
1447 }
1448 \]
1449 \end{theorem}
1450 
Proof block: Companion branch criterion · Go to statement · Read statement and proof side by side1451 \begin{proof}
1452 The disjoint union of the levels is an infinite rooted tree. It is locally finite because every level is finite. It contains a vertex at every depth. König's infinity lemma gives an infinite branch \cite{Diestel2017}. That branch is a point of the inverse limit.
1453 \end{proof}
1454 
Statement: Empty finite companion obstruction · Go to proof · Read statement and proof side by side1455 \begin{corollary}[Empty finite companion obstruction]\label{cor:empty_companion_obstruction}
1456 If \(X_{\lambda,m}=\varnothing\) for some \(m\), then no complete \(\lambda\) adic realization admissible for this forest exists.
1457 \end{corollary}
1458 
Proof block: Empty finite companion obstruction · Go to statement · Read statement and proof side by side1459 \begin{proof}
1460 A complete realization would reduce to a point at every finite level.
1461 \end{proof}
1462 
1463 Finite forests alone give compatible classes. To obtain actual continuous representations, we use the following explicit coefficient and admissibility data. They also delimit the meaning of completion in the next theorem.
1464 
1465 Fix a topological group \(\Gamma\), a finite matrix index set \(D\), and a set \(\Lambda\) of coefficient indices. For each \(\lambda\), let \(\OO_\lambda\) be a commutative ring, complete and separated for a finitely generated ideal \(I_\lambda\), with finite residue ring \(\OO_\lambda/I_\lambda\). Give \(\OO_\lambda\) its ideal adic topology and every quotient its discrete topology. Let
1466 \[
1467 i_\lambda:\OO_\lambda\longrightarrow K_\lambda,
1468 \qquad e_\lambda:L\longrightarrow K_\lambda
1469 \]
1470 be supplied ring homomorphisms, where \(L\) and \(K_\lambda\) are fields, \(K_\lambda\) has a declared topology, and \(i_\lambda\) is continuous.
1471 
1472 For every positive integer \(n\), let \(X_{\lambda,n}\) be a finite nonempty set of conjugacy classes of actual continuous representations
1473 \[
1474 \Gamma\longrightarrow\GL_D(\OO_\lambda/I_\lambda^n).
1475 \]
1476 Conjugacy means change of basis by an invertible matrix over that quotient. Assume reduction preserves these sets and that \(X_{\lambda,1}\) consists of the declared residual class. Each admissible class must have a continuous representative. The auxiliary level zero is the unique class over the trivial quotient and imposes no extra occupancy hypothesis.
1477 
1478 Choose elements \(\gamma_v\in\Gamma\) on a sample set \(\Omega\), with declared good subsets \(\Omega_\lambda\subseteq\Omega\). In the arithmetic application these are the chosen Frobenius elements at the permitted places. For each \(v\in\Omega_\lambda\), supply an integral polynomial \(P_{\lambda,v}\in\OO_\lambda[X]\) such that
1479 \[
1480 i_\lambda(P_{\lambda,v})=e_\lambda(P_v)\quad\text{in }K_\lambda[X].
1481 \]
1482 Here and below a ring homomorphism applied to a polynomial acts on its coefficients. Assume every representative of every class in \(X_{\lambda,n}\) has characteristic polynomial \(P_{\lambda,v}\bmod I_\lambda^n\) at \(\gamma_v\). Also supply a subgroup \(H_\lambda\leq\Gamma\) on which all these finite representations are trivial. This is an inertia condition when \(H_\lambda\) is the specified inertia subgroup.
1483 
1484 Finally, put
1485 \[
1486 B_\lambda=\OO_\lambda[x_{g,a,b}:g\in\Gamma,\ a,b\in D].
1487 \]
1488 For each declared local condition index \(u\), supply an ideal \(J_{\lambda,u}\subseteq B_\lambda\). Evaluation at a representation sends \(x_{g,a,b}\) to its \((a,b)\) matrix entry at \(g\). Assume that evaluation at every admissible finite representative kills \(J_{\lambda,u}\), with polynomial coefficients reduced modulo \(I_\lambda^n\). For this class based theorem, the equations must hold in every admissible frame. A condition imposed only in one chosen frame needs a separate compatible frame argument. No arbitrary arithmetic condition is identified with such an ideal without a separate argument.
1489 
Statement: Conditional simultaneous companion completion · Go to proof · Read statement and proof side by side1490 \begin{theorem}[Conditional simultaneous companion completion]\label{thm:simultaneous_companion_completion}
1491 Under the coefficient and finite admissibility hypotheses above, one can choose continuous representations
1492 \[
1493 \rho_\lambda:\Gamma\longrightarrow\GL_D(\OO_\lambda)
1494 \qquad(\lambda\in\Lambda)
1495 \]
1496 whose reduction class belongs to \(X_{\lambda,n}\) for every positive \(n\). They retain the declared residual class. After applying \(i_\lambda\), they are continuous, trivial on \(H_\lambda\), and satisfy
1497 \[
1498 \det\!\left(X- i_\lambda(\rho_\lambda(\gamma_v))\right)
1499 =e_\lambda(P_v),\qquad v\in\Omega_\lambda.
1500 \]
1501 Their integral evaluation points factor through every actual quotient \(B_\lambda/J_{\lambda,u}\).
1502 \end{theorem}
1503 
Proof block: Conditional simultaneous companion completion · Go to statement · Read statement and proof side by side1504 \begin{proof}
1505 The finitely generated ideal and finite residue ring give finite coefficient quotients at every precision. An individual conjugacy class has finitely many frames because the group of invertible basis matrices over each quotient is finite. Thus the finitely many admissible classes give a finite nonempty set of actual continuous representations at each positive level. Continuity is invariant under conjugation. Reduction gives total maps between these sets. Compactness, as in \cref{thm:companion_branch_criterion}, selects strictly compatible representatives. This step neither assumes transition surjectivity nor lifts a prescribed conjugating matrix.
1506 
1507 Completeness and separatedness identify \(\GL_D(\OO_\lambda)\) with the compatible inverse limit of the quotient matrix groups. Lift entries and inverse entries to construct this identification. The two reduction and reconstruction identities hold entrywise. Finite quotient continuity implies continuity for the ideal adic topology, including the matrix inverse, so the reconstructed representation is continuous.
1508 
1509 Each coefficient of its characteristic polynomial agrees with the prescribed integral coefficient modulo every positive power of \(I_\lambda\). Separatedness gives equality of the full polynomials. The same argument applied to the matrix entries of \(\rho_\lambda(g)-1\) gives triviality on \(H_\lambda\). Continuous coefficient change and the matching equations for \(P_{\lambda,v}\) give the asserted common spine over the local fields.
1510 
1511 For \(p\in J_{\lambda,u}\), evaluation commutes with reduction. Its value is zero modulo every positive power of \(I_\lambda\), hence is zero integrally by separatedness. Therefore the evaluation homomorphism kills the whole ideal and factors uniquely through \(B_\lambda/J_{\lambda,u}\). Choose a realization for each \(\lambda\).
1512 \end{proof}
1513 
1514 The quotient conclusion is a proved effectivity statement for the declared polynomial relations. For local conditions presented by continuous maps from represented local rings, \cref{cor:simultaneous_local} also accounts for the closed ideal generated by their defining ideals. Neither statement constructs a deformation ring for a condition that has not been shown representable. Hodge conditions, Weil--Deligne conditions, integral lifts of arbitrary Frobenius polynomials, and the finite occupancy hypotheses still require their own arithmetic inputs. The theorem retains a residual conjugacy class, not a prescribed residual matrix frame, and asserts no uniqueness up to integral conjugacy.
1515 
Statement: Strict compatibility and one member determination1516 \begin{standardfact}[Strict compatibility and one member determination]\label{fact:strict_compatibility}
1517 A strictly compatible semisimple system is determined at every coefficient place by its common unramified characteristic polynomials. If an automorphic representation gives a compatible system with the same polynomials, then Chebotarev density and Brauer Nesbitt identify the two systems member by member after semisimplification
1518 \cite{Serre1977,BarnetLambGeeGeraghtyTaylor2014}.
1519 \end{standardfact}
1520 
Statement: One member propagation in a fixed system · Go to proof · Read statement and proof side by side1521 \begin{theorem}[One member propagation in a fixed system]\label{thm:one_member_propagation}
1522 Let
1523 \[
1524 \{\rho_\lambda\}_{\lambda\in\Lambda}
1525 \]
1526 be a semisimple strictly compatible system with Frobenius spine \((P_v)\). Suppose that for one coefficient place \(\lambda_0\), the representation \(\rho_{\lambda_0}\) is identified with the Galois representation attached to an automorphic representation \(\pi\). Assume that the compatible system attached to \(\pi\) has the same polynomials \(P_v(X)\). Then for every \(\lambda\in\Lambda\),
1527 \[
1528 \boxed{
1529 \rho_\lambda
1530 \cong
1531 \rho_{\pi,\lambda}^{\mathrm{ss}}.
1532 }
1533 \]
1534 \end{theorem}
1535 
Proof block: One member propagation in a fixed system · Go to statement · Read statement and proof side by side1536 \begin{proof}
1537 For every \(\lambda\), the two semisimple representations have the same unramified characteristic polynomials at all places outside one finite set. Apply \cref{fact:chebotarev_brauer_nesbitt}.
1538 \end{proof}
1539 
1540 \begin{remark}
1541 The theorem propagates automorphy inside a compatible system that already exists. It does not construct a missing coefficient place member and does not prove universal companion existence.
1542 \end{remark}
1543 
Statement: Finite Frobenius separator · Go to proof · Read statement and proof side by side1544 \begin{proposition}[Finite Frobenius separator]\label{prop:finite_frobenius_separator}
1545 Let \(t_1,\ldots,t_r\) be linearly independent functions on a set \(\Omega\) with values in a field \(E'\). Then there are points
1546 \(\omega_1,\ldots,\omega_r\in\Omega\) such that the matrix
1547 \[
1548 \left(t_i(\omega_j)\right)_{j,i}
1549 \]
1550 is invertible. In particular, when the trace functions of finitely many compatible constituents are linearly independent on the unramified Frobenius set, finitely many Frobenius traces recover their multiplicities in any known semisimple carrier.
1551 \end{proposition}
1552 
Proof block: Finite Frobenius separator · Go to statement · Read statement and proof side by side1553 \begin{proof}
1554 Let
1555 \[
1556 W
1557 =
1558 \operatorname{span}
1559 \left\{
1560 (t_1(\omega),\ldots,t_r(\omega)):\omega\in\Omega
1561 \right\}
1562 \subseteq E'^r.
1563 \]
1564 If \(W\neq E'^r\), a nonzero linear functional on \(E'^r\) would vanish on every evaluation vector, giving a nontrivial linear relation among the functions. Thus \(W=E'^r\). Choose \(r\) evaluation vectors forming a basis.
1565 \end{proof}
1566 
1567 \begin{figure}[t]
1568 \centering
1569 \includegraphics[width=.94\textwidth]{14_companion_spine.pdf}
1570 \caption{Under the coefficient and effectivity hypotheses of \cref{thm:simultaneous_companion_completion}, local companion branches realize the Frobenius spine fixed in advance.}
1571 \label{fig:companion_spine}
1572 \end{figure}
1573 
1574 \section{The coefficient prime two}\label{sec:two}
1575 
1576 The auxiliary augmentation algebra works at every coefficient prime. What changes at two is the availability of integral character projectors and, in many applications, the residual image and local deformation hypotheses.
1577 
Statement: Failure of integral sign projectors · Go to proof · Read statement and proof side by side1578 \begin{proposition}[Failure of integral sign projectors]\label{prop:dyadic_sign_projectors}
1579 Let \(C_2=\langle g\rangle\). Over \(\QQ_2\), the two sign projectors are
1580 \[
1581 \boxed{
1582 e_+=\frac{1+g}{2},
1583 \qquad
1584 e_-=\frac{1-g}{2}.
1585 }
1586 \]
1587 Neither belongs to \(\ZZ_2[C_2]\). After reduction modulo two,
1588 \[
1589 \boxed{
1590 \FF_2[C_2]
1591 \cong
1592 \FF_2[X]/(X^2),
1593 \qquad
1594 X=g-1.
1595 }
1596 \]
1597 This ring is local and has no nontrivial idempotents.
1598 \end{proposition}
1599 
Proof block: Failure of integral sign projectors · Go to statement · Read statement and proof side by side1600 \begin{proof}
1601 The displayed rational elements are the unique primitive idempotents because they project to the two characters of \(C_2\). Their coefficients contain \(1/2\), so they are not integral. In characteristic two,
1602 \[
1603 (g-1)^2=g^2-2g+1=0.
1604 \]
1605 The map \(X\mapsto g-1\) gives the displayed isomorphism. The quotient by \((X)\) is \(\FF_2\), and \((X)\) is nilpotent. Thus the ring is local.
1606 \end{proof}
1607 
Statement: Dyadic coinvariant recovery · Go to proof · Read statement and proof side by side1608 \begin{corollary}[Dyadic coinvariant recovery]\label{cor:dyadic_coinvariant_recovery}
1609 Let \(\Delta\) be a finite two group, let \(\Lambda=\OO[\Delta]\) with \(\OO\) a finite extension of \(\ZZ_2\), and let \(M\) be finite free over \(\Lambda\). Then
1610 \[
1611 \boxed{
1612 M\otimes_{\Lambda,\epsilon}\OO
1613 \cong
1614 M/\fraka M
1615 }
1616 \]
1617 is free over \(\OO\) of the same \(\Lambda\) rank. No semisimple character decomposition is required.
1618 \end{corollary}
1619 
Proof block: Dyadic coinvariant recovery · Go to statement · Read statement and proof side by side1620 \begin{proof}
1621 Use the right module convention fixed in \cref{sec:auxiliary}. Quotienting by all balancing relations identifies \(M\otimes_{\Lambda,\epsilon}\OO\) with \(M/\fraka M\), without any commutativity assumption on \(\Delta\). Applying \(\epsilon\) to the coordinates of a finite \(\Lambda\) basis gives an \(\OO\) basis with the same index set.
1622 \end{proof}
1623 
1624 \begin{remark}
1625 The corollary is an algebraic statement about augmentation and coinvariants. It does not supply a coefficient two adequacy theorem, a local deformation ring with the desired geometry, or a classicality theorem. Those inputs must be checked in the automorphy lifting theorem being used.
1626 \end{remark}
1627 
1628 \begin{figure}[t]
1629 \centering
1630 \includegraphics[width=.92\textwidth]{15_coefficient_two_boundary.pdf}
1631 \caption{Augmentation survives at two, while semisimple character projectors and arithmetic hypotheses require separate treatment.}
1632 \label{fig:coefficient_two_boundary}
1633 \end{figure}
1634 
1635 \section{Conditional automorphic completion}\label{sec:completion}
1636 
1637 We now assemble the preceding statements. The theorem is deliberately written as a chain of gates. Each gate has a distinct mathematical source.
1638 
Statement: Ordinary completion datum at a point1639 \begin{definition}[Ordinary completion datum at a point]\label{def:ordinary_completion_datum}
1640 An ordinary completion datum at a characteristic zero point \(x:R\to E'\) consists of the following objects.
1641 \begin{enumerate}
1642 \item A represented global deformation ring \(R\) with declared local quotient conditions and universal representation \(\rho_R\).
1643 \item An ordinary patching datum
1644 \[
1645 (R_\infty,\fraka,M_\infty,R,H)
1646 \]
1647 whose finite level module \(H\) is an automorphic Hecke carrier.
1648 \item Full patched support
1649 \[
1650 \Supp_{R_\infty}(M_\infty)=\Spec R_\infty.
1651 \]
1652 \item An isomorphism
1653 \[
1654 R\cong\TT
1655 \]
1656 with the Hecke algebra acting on \(H\). The \(R\) action on \(H\) supplied by the patched control isomorphism is the restriction of this \(\TT\) action along the displayed isomorphism.
1657 \item An automorphic Hecke datum \((\TT,H,(P_v))\) and a pointwise classicality and Galois realization theorem satisfying all the inputs of \cref{thm:pointwise_galois_realization} for the nonzero fiber at \(x\): an occurring classical automorphic representation with a continuous semisimple attached representation; equality of the characteristic polynomials of both that representation and \(\rho_x=x\circ\rho_R\) with \(x(P_v(X))\) on the same declared Chebotarev dense union of Frobenius conjugacy classes; and the standard semisimplification, density, and general Brauer Nesbitt inputs. The coefficient topology and continuity requirements are retained in \cref{thm:ordinary_conditional_completion}.
1658 \end{enumerate}
1659 \end{definition}
1660 
Statement: Ordinary conditional automorphic completion · Go to proof · Read statement and proof side by side1661 \begin{theorem}[Ordinary conditional automorphic completion]\label{thm:ordinary_conditional_completion}
1662 Let \(x:R\to E'\) admit an ordinary completion datum. Assume \(E'\) is a Hausdorff topological field of characteristic zero with continuous ring operations, and that both \(\rho_x=x\circ\rho_R\) and its attached comparison representation are continuous. Then
1663 \[
1664 \boxed{
1665 H\otimes_{\TT,x}E'\neq0.
1666 }
1667 \]
1668 The specialization
1669 \[
1670 \rho_x=x\circ\rho_R
1671 \]
1672 is identified after semisimplification with the Galois representation attached to a classical automorphic representation in that fiber. If \(\rho_x\) is irreducible, it is itself automorphic.
1673 \end{theorem}
1674 
Proof block: Ordinary conditional automorphic completion · Go to statement · Read statement and proof side by side1675 \begin{proof}
1676 Full patched support descends to full support of \(H\) over \(R\) by
1677 \cref{thm:ordinary_support_descent}. The isomorphism \(R\cong\TT\) transports that support by \cref{thm:rt_support_transport}. The field fiber is nonzero by
1678 \cref{thm:support_gives_hecke_system}. The declared classicality and realization theorem supplies an automorphic representation in the fiber and an attached Galois representation. The comparison with \(\rho_x\) follows from \cref{thm:pointwise_galois_realization}.
1679 \end{proof}
1680 
Statement: Derived completion datum at a point1681 \begin{definition}[Derived completion datum at a point]\label{def:derived_completion_datum}
1682 A derived completion datum is defined in the same way, with a perfect patched complex
1683 \(C_\infty\) of full derived support and a finite level automorphic complex
1684 \[
1685 C
1686 \simeq
1687 C_\infty
1688 \mathbin{\mathop{\otimes}\limits_{R_\infty}^{\mathbf L}}R
1689 \]
1690 in place of the ordinary modules. Under the Hecke ring isomorphism \(e:R\cong\TT\), require an actual derived carrier identification between the scalar transport of this finite level complex and the automorphic Hecke complex. This identification retains the \(R\) action induced by patched control as the restriction of the \(\TT\) action along \(e\).
1691 \end{definition}
1692 
Statement: Derived conditional automorphic completion · Go to proof · Read statement and proof side by side1693 \begin{theorem}[Derived conditional automorphic completion]\label{thm:derived_conditional_completion}
1694 Let \(x:R\to E'\) admit a derived completion datum, with Hecke identification \(e:R\cong\TT\), and put \(y=x\circ e^{-1}\). Then
1695 \[
1696 \boxed{
1697 C\mathbin{\mathop{\otimes}\limits_{\TT,y}^{\mathbf L}}E'\not\simeq0.
1698 }
1699 \]
1700 Some integer cohomological degree contains a nonzero Hecke eigensystem with character \(y\). Its degree lies between the bounds of any chosen finite projective model for \(C\).
1701 
1702 For the conditional conclusion, retain the Hausdorff coefficient topology, continuous specialization, supplied semisimplification, and common Frobenius polynomial hypotheses in \cref{thm:derived_pointwise_realization}. If the declared classicality and Galois realization theorem applies to this eigensystem and supplies an occurring classical automorphic representation with a continuous semisimple attached representation and those Frobenius polynomials, then \(\rho_x\) is automorphic after semisimplification. If \(\rho_x\) is irreducible, it is itself isomorphic to the attached representation. This pointwise applicability condition does not require a uniform classicality assertion in other degrees.
1703 \end{theorem}
1704 
Proof block: Derived conditional automorphic completion · Go to statement · Read statement and proof side by side1705 \begin{proof}
1706 Full support descends from the patched perfect complex by \cref{thm:derived_support_descent}. Scalar transport through \(e\), followed by the actual derived isomorphism with the automorphic Hecke complex, gives full support for \(C\). Its fiber at \(y\) is therefore nonzero. The bounded model and induced Hecke action argument in \cref{thm:derived_pointwise_realization} supplies a nonzero cohomology eigenvector in an integer degree within the model's bounds.
1707 
1708 If realization applies to this eigensystem, it supplies the occurring automorphic object and a continuous semisimple attached representation with the declared Frobenius polynomials. The representation comparison in \cref{thm:derived_pointwise_realization} then identifies the supplied semisimplification of \(\rho_x\) with that attached representation. Only applicability to this eigensystem is used; a classicality theorem for every degree in a prescribed interval is unnecessary.
1709 \end{proof}
1710 
Statement: Compatible system completion from one automorphic member · Go to proof · Read statement and proof side by side1711 \begin{theorem}[Compatible system completion from one automorphic member]\label{thm:system_completion}
1712 Let
1713 \[
1714 \{\rho_\lambda\}_{\lambda\in\Lambda}
1715 \]
1716 be a semisimple strictly compatible system with common Frobenius spine. Suppose the member at \(\lambda_0\) admits an ordinary or derived completion datum and is identified with the Galois representation attached to an automorphic representation \(\pi\). Assume that the compatible system attached to \(\pi\) has the same Frobenius spine. Then
1717 \[
1718 \boxed{
1719 \rho_\lambda
1720 \cong
1721 \rho_{\pi,\lambda}^{\mathrm{ss}}
1722 \quad
1723 \text{for every }\lambda\in\Lambda.
1724 }
1725 \]
1726 \end{theorem}
1727 
Proof block: Compatible system completion from one automorphic member · Go to statement · Read statement and proof side by side1728 \begin{proof}
1729 The completion theorem at \(\lambda_0\) gives the automorphic representation \(\pi\). Apply \cref{thm:one_member_propagation} to the two compatible systems.
1730 \end{proof}
1731 
Statement: Five gate formulation · Go to proof · Read statement and proof side by side1732 \begin{theorem}[Five gate formulation]\label{thm:five_gate_completion}
1733 Fix a characteristic zero deformation point \(x:R\to E'\). Give \(E'\) a Hausdorff topological field structure. The conditional argument uses the following five gates.
1734 \begin{enumerate}
1735 \item \textbf{Residual gate.} Residual occupancy in the declared automorphic carrier and representability of the chosen deformation problem are supplied arithmetic inputs. In particular, the deformation ring \(R\) and its universal representation \(\rho_R\) are available.
1736 \item \textbf{Patching gate.} An applicable patching theorem supplies an ordinary finite module or a perfect complex with full patched support, together with the coefficient quotient and the module or derived control isomorphism. Write \(M\) for the resulting finite level carrier over \(R\).
1737 \item \textbf{Comparison gate.} Let \(H\) be a finite ordinary Hecke module or a perfect Hecke complex over \(\TT\). Supply a ring map \(f:R\to\TT\) satisfying
1738 \[
1739 (f^*)^{-1}\bigl(\Supp_R(M)\bigr)\subseteq\Supp_{\TT}(H).
1740 \]
1741 Use ordinary or derived support according to the carrier. Actual scalar extension satisfies this inclusion, as does transport through a ring isomorphism with the corresponding carrier identification.
1742 \item \textbf{Fiber gate.} Supply a Hecke point \(y:\TT\to E'\) with \(y\circ f=x\). Then the fiber of \(H\) at \(y\) is nonzero. It contains a nonzero Hecke eigenvector, in some integer cohomological degree in the derived case, with character \(y\).
1743 \item \textbf{Realization gate.} The declared classicality theorem applies to the resulting eigensystem and supplies an occurring classical automorphic representation \(\pi\), with a continuous semisimple attached representation. Require the specialization \(\rho_x=x\circ\rho_R\) to be continuous and supply its semisimplification. On the same Chebotarev dense set, assume that the characteristic polynomials of both \(\rho_x\) and the attached representation are \(y(P_v(X))\). Retain the standard density and general Brauer Nesbitt inputs of \cref{fact:chebotarev_brauer_nesbitt}.
1744 \end{enumerate}
1745 Then \(\rho_x^{\mathrm{ss}}\) is isomorphic to the representation attached to \(\pi\). If \(\rho_x\) is irreducible, the same conclusion holds for \(\rho_x\) itself.
1746 
1747 For propagation, suppose both a semisimple compatible family \(\{\rho_\lambda\}\) containing \(\rho_x\) and a family \(\{\rho_{\pi,\lambda}\}\) attached to this same \(\pi\) already exist. Require the distinguished members to be \(\rho_x\) and its attached representation, respectively. Assume the coefficient, continuity, density, semisimplification and common algebraic Frobenius spine hypotheses of \cref{thm:one_member_propagation}, with that spine agreeing with the specialized Hecke polynomials at the distinguished place. Then
1748 \[
1749 \rho_\lambda\cong\rho_{\pi,\lambda}^{\mathrm{ss}}
1750 \qquad\text{for every }\lambda.
1751 \]
1752 \end{theorem}
1753 
Proof block: Five gate formulation · Go to statement · Read statement and proof side by side1754 \begin{proof}
1755 The residual and representability inputs specify the setting in which the supplied patching theorem applies. The formal deduction begins with its actual rings, carriers and comparison maps. In the ordinary branch, finite generation and full support at finite level follow from the coefficient quotient and module control isomorphism. In the derived branch, the derived control isomorphism gives a perfect finite level model, and \cref{thm:derived_support_descent} gives full support.
1756 
1757 The comparison inclusion transports this full support to \(H\). More specifically, \(y\circ f=x\) identifies the contraction of \(\ker y\) with \(\ker x\), so support at the source point gives support at the Hecke point. In the ordinary case, \cref{thm:field_fiber_criterion} gives a nonzero actual tensor fiber. In the derived case, the support criterion gives a nonzero actual derived fiber and hence a nonzero cohomology vector. Its integer degree lies within the bounds of the chosen finite projective model. In both cases, multiplication on the original carrier induces the scalar \(y(t)\) on the specialized vector for every \(t\in\TT\).
1758 
1759 Choose this nonzero eigensystem and apply the declared realization theorem to it. No realization statement in other degrees is needed. The two continuous representations have the same characteristic polynomials on the declared dense Frobenius conjugacy classes. Continuity extends their equality to the whole group. The supplied semisimplification preserves those polynomials, and the general Brauer Nesbitt input gives the required invertible linear intertwiner. The irreducible conclusion follows as in \cref{thm:pointwise_galois_realization}.
1760 
1761 Finally, retain the same \(\pi\) in its attached family. The distinguished member identities connect both families to the pointwise construction, while the common algebraic spine gives the required Frobenius polynomials at every coefficient place. Apply \cref{thm:one_member_propagation} to these two existing families. The construction does not produce a missing companion or an attached compatible family.
1762 \end{proof}
1763 
1764 \begin{figure}[t]
1765 \centering
1766 \includegraphics[width=.97\textwidth]{17_final_completion.pdf}
1767 \caption{The final theorem is a composition of separate residual, support, comparison, fiber, and realization gates.}
1768 \label{fig:final_completion}
1769 \end{figure}
1770 
1771 \section{Exact boundary of the article}\label{sec:boundary}
1772 
1773 The formal results above sharpen the logical role of patching support, Hecke packets, and compatible systems. They do not replace the arithmetic theorems that supply the gates.
1774 
1775 \begin{table}[t]
1776 \centering
1777 \caption{Proved formal statements and arithmetic inputs that remain external.}
1778 \label{tab:boundary}
1779 \begin{tabular}{p{.44\textwidth}p{.44\textwidth}}
1780 \toprule
1781 Proved in this article & Not proved in this article\\
1782 \midrule
1783 Local conditions combine through completed quotient rings & Representability of every desired local deformation condition\\
1784 Full ordinary and derived support descends through the patching quotient & Near faithfulness or full support for every global deformation problem\\
1785 An isomorphism \(R\cong\TT\) transports support and Fitting data & An \(R\cong\TT\) theorem outside published hypotheses\\
1786 Finite Hecke algebras split into Artin packets & Positive automorphic occupancy of every residual or characteristic zero packet\\
1787 Nonzero stable cores produce compatible inverse limit points & Universal residual companion existence\\
1788 One automorphic member determines a fixed compatible system & Existence of a compatible system for every geometric representation\\
1789 Augmentation and coinvariant recovery work at coefficient prime two & A universal coefficient two replacement for residual image, local geometry, and classicality hypotheses\\
1790 \bottomrule
1791 \end{tabular}
1792 \end{table}
1793 
1794 \begin{remark}
1795 The strongest global conclusion is conditional automorphic realization inside a declared class for which the five gates have been verified. The article does not prove unrestricted global Langlands reciprocity.
1796 \end{remark}
1797 
1798 \begin{remark}
1799 A numerical certificate can check the finite algebra appearing in an example. It cannot verify a published automorphy lifting theorem, a classicality theorem, or a universal existence statement.
1800 \end{remark}
1801 
1802 \section*{Lean verification and revision scope}
1803 
1804 The preserved Lean release 0.17.0, reverified in evidence release 0.17.1, reports 748 named theorem declarations written for Paper XII, including supporting lemmas and interface results. A further 81 theorem declarations are reused unchanged from Paper X and counted separately. The cumulative verification rebuilds all 96 registered project modules with Lean 4.34.0-rc2 and warnings treated as errors. The transitive axiom audit covers 1,229 named declarations and permits only \texttt{propext}, \texttt{Classical.choice}, and \texttt{Quot.sound}. Three deliberately invalid controls test rejection of a false proof, a placeholder, and an incorrect empty family normalization. The pinned Mathlib dependency cache is not itself rebuilt. Exact compiler results, source hashes, and the verification scope are recorded with the archive.
1805 
1806 The preserved release records complete mapped Lean statements for all 49 internal numbered claims of its revised manuscript. The present traditional edition retains those proof bodies, exposes the local-map and coefficient-target hypotheses in \cref{prop:global_local_basechange}, makes the \(r>n\) convention explicit in the proof of \cref{thm:higher_fitting_strata}, states all the pointwise comparison inputs in \cref{def:ordinary_completion_datum}, and declares a finite ramification set and coherent geometric Frobenius normalization. These editorial clarifications are recorded separately from the inherited eight amendments; they are not counted as newly compiled Lean certificates. No new statement amendment was needed for the completion and tensor results. The eight inherited amendments remain explicitly separate from the original wording, and the cited arithmetic inputs remain outside the internal claim census. Formal proof coverage is recorded claim by claim in the roadmap. These checks certify the formal statements under their explicit hypotheses, not every prose claim, novelty assertion, or external arithmetic result.
1807 
1808 The completion block proves \cref{thm:tensor_quotient,prop:global_local_basechange} using actual algebraic tensor products, actual Hausdorff completions, and the actual closed generated ideals. Both inverse laws, continuity in both directions, and the canonical factor maps are checked. An independent comparison with the algebraic inverse limit completion identifies the topology and local ring structure. The global theorem retains continuous local algebra points and their naturality, rather than only an unstructured point existence statement. The empty family retains the scalar adic topology. The zero condition and unit ideal boundaries are checked separately.
1809 
1810 The preceding Fitting block proves \cref{thm:fitting_support,thm:higher_fitting_strata,prop:fitting_base_change,thm:rt_support_transport}. Its intrinsic Fitting ideals are independent of the chosen finite presentation, including the number of generators and relations. Arbitrary base change, all higher fiber dimension strata, and the complete support and Fitting transport statement are checked. The Noetherian and finite module hypotheses of the manuscript provide the finite presentation needed by the general construction.
1811 
1812 The new checks for \cref{prop:group_algebra_transfer,thm:coinvariant_recovery,cor:dyadic_coinvariant_recovery} include actual group algebra transfer and augmentation. Coinvariant recovery uses the quotient by all balancing relations, with its universal property proved. In the commutative case, this construction is identified with the ordinary tensor product. The augmentation relations generate exactly the augmentation ideal acting on the module. Applying augmentation to the coordinates of a supplied free basis gives a coefficient basis with the same index set. The right module argument applies to arbitrary groups, including nonabelian two groups, and includes rank zero.
1813 
1814 The new checks for \cref{thm:residual_augmentation_algebra,cor:no_residual_character_splitting,cor:rank_trace_detection,prop:dyadic_sign_projectors} construct the full multivariable truncated polynomial algebra isomorphism and identify its augmentation generators. The residual group algebra is local for abelian \(p\) groups in characteristic \(p\). For each supplied Hecke idempotent, the trace is the image dimension cast into the coefficient field; occupancy is equivalent to positive rank and, in characteristic zero, nonzero trace. The dyadic calculation gives the two rational sign projectors, proves that neither lies in the integral group algebra, and identifies the residual algebra with \(\FF_2[X]/(X^2)\).
1815 
1816 Corollary~\ref{cor:no_residual_character_splitting} is now checked for every finite \(p\) group, including nonabelian groups, over every field of characteristic \(p\). The proof uses a finite prime field orbit span and a nonzero fixed vector. The original unrestricted statement is restored, and the earlier explicit abelian restriction is no longer needed.
1817 
1818 The checks for \cref{prop:quotient_erases_component,thm:canonical_hecke_packets,cor:simultaneous_generalized_eigenspaces} now include the actual formal power series quotient and the canonical Hecke packet maps. In the node \(k[[x,y]]/(xy)\), quotienting by \((x)\) gives \(k[[y]]\), with support \(V(x)\); Lean verifies both irreducible components and the exclusion of the generic point \((y)\). The components can still meet, so this is not a claim that their supports are disjoint.
1819 
1820 For the Hecke results, the canonical ring decomposition in \cref{fact:artin_decomposition} remains a declared external input. Its coordinates are the actual localization maps. The module direct sum, the packet identification with the localized module, and the formula \(v\mapsto v/1\) are constructed in Lean. Nilpotence in the selected Artin local factor, together with invertibility of a generator on each other factor, gives a single positive exponent for the simultaneous generalized eigenspace. The result includes the explicit generators \(T_i-\lambda_i\), agrees with the packet used in the trace theorem, and does not assume semisimplicity.
1821 
1822 The revised five gate statement in \cref{thm:five_gate_completion} is now checked for both ordinary and derived carriers and for a general support comparison. The comparison is an actual inclusion of subsets of prime spectra, and scalar extension is proved to satisfy it. The coefficient quotient and ordinary or derived control maps yield finite level support; that conclusion is not supplied as a separate patching assumption. The specialized tensor module or derived cohomology supplies an actual nonzero eigenvector. The declared realization theorem is applied to this particular eigensystem, and the resulting representation comparison is an actual invertible linear intertwiner. The system conclusion uses the family attached to the very same automorphic object, with distinguished member identities and a common algebraic polynomial spine.
1823 
1824 The original comparison wording did not explicitly supply a compatible Hecke point over the fixed coefficient field. Support preservation alone is insufficient: extension from \(\mathbb Q\) to \(\mathbb Q(i)\) preserves full support, but there is no ring map \(\mathbb Q(i)\to\mathbb Q\) extending the identity. The revision therefore states \(y\circ f=x\) and exposes the arithmetic comparison and existing-family inputs. Residual occupancy, representability and the applicable patching theorem remain supplied arithmetic provenance. The original full statement remains partial. The completed tensor quotients and intrinsic Fitting ideals are now checked as described above, including the full Fitting transport clause.
1825 
1826 The derived realization checks cover the revised \cref{thm:derived_pointwise_realization,thm:derived_conditional_completion}. They prove vanishing outside the bounds of an actual finite projective model and construct a nonzero cohomology vector inside those bounds. The Hecke action is induced from multiplication on the original cochain model, carried through scalar extension and derived localization, and proved to act by the specialized character on actual cohomology. The conditional arithmetic step gives an actual invertible linear intertwiner from the declared realization input and common Frobenius polynomials.
1827 
1828 The original formulation of \cref{thm:derived_pointwise_realization} did not ensure that the surviving degree lies in the classicality range. A complex concentrated in degree one has full support over a field, while a classicality condition restricted to degree zero says nothing about its nonzero fiber. The revision requires the declared range to contain the model interval. The conditional conclusion of \cref{thm:derived_conditional_completion} retains applicability at the selected eigensystem itself. Both statements now expose the topology, continuity, semisimplification, and common polynomial inputs needed for the representation comparison. Their original unconditional cohomological conclusions are checked, but their original complete statements remain partial. The general support comparison and compatible-point formulation is now checked in the revised \cref{thm:five_gate_completion}, as described above.
1829 
1830 The derived support checks prove \cref{thm:derived_quotient_support,thm:derived_support_descent,cor:derived_degree_survives} as originally stated. Perfect complexes are actual derived category objects equipped with bounded finite projective models and derived isomorphisms to those models. Scalar extension is constructed on cochain complexes. Its associativity, preservation of homotopy equivalences, and independence under actual derived isomorphisms are checked. The quotient support formula uses the actual map of spectra and its image \(V(I)\). Every field valued point factors through the residue field at its kernel, and faithful flatness of field extensions preserves and reflects acyclicity. The surviving integer degree is expressed using the actual derived cohomology functor, with a corresponding witness in the specialized cochain model. These proofs do not require the external cohomological support description in \cref{fact:derived_support_cohomology}. The external classicality theorems remain supplied arithmetic inputs; the conditional derived realization argument is checked as described above.
1831 
1832 The adequacy checks prove \cref{thm:s3_adequacy} as originally stated. They construct the faithful standard representation from the actual permutation module, prove irreducibility after extension to the algebraic closure, and split every group element's characteristic polynomial over \(\FF_7\). The trace zero adjoint is the kernel of matrix trace with its conjugation action, and its sign plus standard decomposition is an actual equivariant linear isomorphism. The averaging proof is connected to Mathlib's actual first group cohomology, while the invariant calculation gives actual degree zero vanishing. Canonical projectors are identified with generalized eigenspace projectors for every positive exponent. Their trace pairings detect every nonzero endomorphism and hence every irreducible adjoint submodule. The two printed constituent witnesses and their traces are checked exactly. The adequacy definition remains a cited convention; no external adequacy theorem is assumed in this finite certificate.
1833 
1834 The realization checks cover \cref{thm:pointwise_galois_realization,cor:full_support_pointwise_automorphy,thm:one_member_propagation,thm:ordinary_conditional_completion,thm:system_completion}. Characteristic polynomial coefficients are continuous by the principal minor formula. Equality on the declared Frobenius conjugacy classes therefore extends to the whole Galois group. The finite dimensional algebra input is explicit: a supplied semisimple representative preserves every characteristic polynomial, and a general Brauer Nesbitt theorem identifies semisimple representations with equal polynomials. Lean proves independence of this representative and the irreducible conclusion. Construction of semisimplification, the general Brauer Nesbitt theorem, and arithmetic Chebotarev density remain external inputs.
1835 
1836 The ordinary completion argument derives finite generation, full finite level support, and an actual nonzero Hecke tensor fiber from the patched support and control isomorphisms. The declared classicality input then supplies the occurring automorphic object and its attached representation. Both existing compatible systems, with their common polynomial spine, are retained as hypotheses in the propagation results. These results do not construct missing companions or an attached compatible system.
1837 
1838 The pointwise realization and ordinary completion statements now explicitly require Hausdorff coefficient topology and continuity of the compared representations, including the universal specialization. The corresponding locus statement is restricted to such points. These three revised claims are counted as complete; their original wording remains partial. This clarification also makes the coefficient topology in \cref{fact:chebotarev_brauer_nesbitt} explicit without claiming a new proof of that external arithmetic fact.
1839 
1840 The earlier revision made two further substantive corrections. In \cref{cor:componentwise_occupancy}, every irreducible component is contained in the full support. The previous sentence reversed that containment. In \cref{thm:simultaneous_companion_completion}, the coefficient, continuity, integrality, class finiteness, and quotient condition hypotheses are now explicit. Finite forests by themselves establish branches, not all arithmetic effectivity assertions. Corollary~\ref{cor:simultaneous_local} now gives the closed kernel argument and the continuity and uniqueness of its factors.
1841 
1842 The original manuscript and its literal claim records are preserved with the release. In that original census, 41 claims are fully checked, seven are partial, and one is not checked as written. The corrected \cref{cor:componentwise_occupancy} and restricted \cref{thm:simultaneous_companion_completion} are counted as proved only for their revised statements. The original unrestricted completion wording is not retrospectively marked proved. Source hashes, the exact amendments, compiler logs, and a mathematical self-review accompany the code.
1843 
1844 Compiler and axiom checks are distinguished from semantic proof review and external arithmetic results.
1845 
1846 \bibliographystyle{amsplain}
1847 \bibliography{Paper_XII_Traditional_Final}
1848 
1849 \end{document}

Back to source controls

Back to Paper XII: Patching Support, Hecke Packets, and Conditional Automorphic Completion