B. Lifting a summand inside a supplied finite-group carrier (Block 18)

Let \(R\) be a commutative integral domain complete and separated for the \((\pi)\)-adic filtration. Let \(\Gamma\) be a finite group, and let \(\rho:\Gamma\to\mathrm{GL}_n(R)\) be an actual integral representation. Assume that \(a=|\Gamma|\ne0\) in \(R\) and \(a\mid\pi^e\). For \(k>0\), suppose

There is an actual integral matrix \(E\) satisfying

No integral summand or coherent family of quotient projectors is assumed. No local-ring assumption or finiteness of the residue field is needed.

To prove this, apply the preceding averaging correction with both representations equal to \(\rho\). This produces an exact equivariant matrix \(A\) with the prescribed reduction at depth \(k\), so that \(A^2-A\in(\pi)^kM_n(R)\). Averaging alone need not preserve idempotence. Use the integral polynomial

The identities

show that successive corrections preserve the retained reduction and improve the idempotence defect. In these formulas scalar constants denote scalar matrices. The Lean proof establishes at least one additional ideal digit at each step, constructs the resulting compatible family of finite-level matrices, and uses completeness and separatedness to recover \(E\). Every matrix commuting with \(A\) commutes with \(E\). There is no division by \(2\), so the correction also works in residue characteristic \(2\).

The actual submodules \(U=\operatorname{im}E\) and \(W=\ker E\) are invariant, and addition gives an equivariant isomorphism

The inclusion \(i:U\hookrightarrow R^n\) and retraction \(r(v)=Ev\) are constructed as linear maps and satisfy \(ri=1_U\) and \(ir=E\). Their equivariance is proved. Coordinatewise reduction maps \(U\) onto \(\operatorname{im}(\bar E\bmod(\pi)^k)\) and maps \(W\) onto \(\ker(\bar E\bmod(\pi)^k)\). Both equalities are surjectivity statements onto the actual submodules over the finite-level quotient, not merely containment. The same projector defines a summand after pullback through any group homomorphism to \(\Gamma\).

For \(R=\mathbb Z_2\) and the sign carrier \(\rho(s)=\operatorname{diag}(1,-1)\), the projector

is equivariant and the theorem constructs a nonzero proper equivariant projector retaining its reduction modulo \(2\). No exact equivariant endomorphism retains this prescribed matrix modulo \(4\). At the insufficient input depth \(1\), the projector \(\left(\begin{smallmatrix}1&1\\0&0\end{smallmatrix}\right)\pmod2\) has no exact equivariant lift retaining its reduction. These are statements about the supplied carrier and prescribed projectors, not about nonexistence of all integral summands.

This block constructs one summand and its complement inside a supplied finite-group carrier. It advances the carrier step in Claim 9.2. It does not identify the intended arithmetic packets, construct the arithmetic Weil–Deligne attachment, establish the Hodge–Tate comparisons, or prove universal occupancy. At the Block 18 checkpoint, the ledger recorded fifteen checked claims and five partially formalized claims; see the Block 23 conditional-scope correction above.

Permalink · Source line 2083