Actual quadratic local conditions and completion (Block 22).
On this page · Permalink · Source line 2410
Continue with the fixed packet \(\mathcal P_q\) above. For a characteristic-zero field \(K\), let
be the actual field-induced homomorphism between absolute Galois groups. It includes a chosen embedding of algebraic closures. Let \(i_K\) be the image of the chosen square root \(i\) under that embedding. Lean proves compatibility with the Galois actions and hence
The fixed-field theorem for the algebraic closure then gives
If no such root exists, the local quotient is surjective onto \(C_2\). These are statements about the actual local Galois map, not a supplied arithmetic interpretation of a scalar label.
For every commutative coefficient ring \(B\) and \(\chi\in\mathcal P_q(B)\), define \(\chi_K=\chi\circ j_K\). The local character is continuous and commutes with coefficient change. The precise local admissibility condition is
Descent through the fixed quadratic quotient proves
No reducedness, characteristic-zero or domain hypothesis is imposed on \(B\). In particular, the formula applies to the finite coefficient quotients used in completion.
The p-adic square-root criterion is proved for every prime:
A root satisfies \(\lvert x\rvert_p^2=1\) and is therefore integral. Reduction modulo three rules out a root in \({\mathbf Q}_3\), and reduction modulo four rules out a root in \({\mathbf Q}_2\). At an odd prime, any residue root of \(X^2+1\) has nonzero derivative and lifts by the pinned Mathlib Hensel theorem. The finite-field square criterion then gives the stated congruence. An explicit Hensel application at the residue root \(2\) modulo \(5\) supplies a root in \({\mathbf Z}_5\). Consequently
The arithmetic prime \(p\) is independent of the coefficient prime. For the two integral \({\mathbf Z}_2\)-valued characters, the sign character is locally trivial exactly at primes congruent to one modulo four. Both distinct global characters are locally trivial at five, while the sign character is nontrivial on the full local Galois groups at three and two.
The inertia theorem uses actual residue actions. For a valuation subring \(A\) of an extension field \(L/K\), let \(D_A\) be its decomposition subgroup in \(\operatorname{Aut}_K(L)\) and put
where \(k_A\) is the residue field. If \(2\) is a unit in \(A\), every member of \(I_A\) fixes every \(y\in L\) with \(y^2=-1\). Indeed \(y^{-1}=-y\), so \(y\) belongs to \(A\) and is a unit there. An automorphism sends \(y\) to \(y\) or \(-y\). Their residues are distinct because \(2\) and \(y\) are units, whereas inertia fixes residues. The second possibility is excluded.
For every prime \(p\), Lean constructs a valuation subring \(A\subseteq\overline{{\mathbf Q}_p}\) containing the integral image of \({\mathbf Z}_p\) such that the induced map \({\mathbf Z}_p\to A\) is local. For odd \(p\), two is a unit. The preceding argument applies to every valuation subring containing that integral image, and hence every member of \(\mathcal P_q(B)\) is trivial on its inertia subgroup after actual local restriction. The existence theorem supplies a locally dominating choice, so this assertion is not vacuous.
This inertia is the actual residue-action kernel inside \(D_A\). No equality \(D_A=G_{{\mathbf Q}_p}\) is established in this block. Nor is ramification at two proved: the nontrivial full local character there is a separate result. At three the \({\mathbf Z}_2\)-valued sign character is nontrivial on the full local Galois group but trivial on every inertia subgroup covered by the theorem. Thus local triviality and the stated inertia triviality are distinguished by checked arithmetic examples.
The local conditions survive coefficient completion by a proved theorem. For an \(I\)-adically separated commutative ring \(R\),
If \(-1\) has a square root in \(K\), every packet member satisfies the condition. Otherwise the condition says that the character is globally trivial, and separatedness detects that equality through all reductions. This proves the closure statement for the independently defined arithmetic property.
Suppose now that \(R\) is \(I\)-adically complete and that every positive quotient \(R/I^m\) is finite. Let \(C_m\subseteq\mathcal P_q(R/I^m)\) be allowed subsets preserved by reduction, and let \((p_s)_{s\in S}\) be any indexed family of arithmetic primes. The index set \(S\) need not be finite. Lean proves the simultaneous arithmetic completion criterion
The constructed character also satisfies every odd-prime valuation-inertia condition stated above. Finite-branch compactness selects all finite characters together; no coherent branch or surjective transition maps are assumed. The new local-closure implication is proved, not supplied. Every-level occupancy remains a substantive hypothesis. One nonsplit selected prime forces the completed global character to be trivial.
For the integral dyadic packet, a single detecting precision is also proved: reduction modulo four detects local triviality uniformly in the arithmetic prime. Modulo two does not suffice. The sign character is nontrivial locally at three, while its reduction modulo two is trivial. This is a coefficient-depth failure, distinct from splitting of the arithmetic field.
Block 22 finishes this actual local admissibility and completion step for the fixed quadratic packet. It does not identify all packets in the manuscript's common arithmetic spine, attach Weil–Deligne objects, or prove coefficient and Hodge–Tate/period comparisons. The decomposition and full local Galois group identification remains a separate inertia obligation, and ramification at two is not claimed. The full arithmetic ledger at the Block 22 checkpoint recorded fifteen checked source claims and five partial claims; the Block 23 conditional-scope correction gives sixteen checked and four partial. Universal occupancy and natural finite seed rank remain conjectures.