Simultaneous projector-family lifting and rigidity (Block 19).
On this page · Permalink · Source line 2158
Keep the complete domain, supplied finite-group carrier and group-order hypotheses of Block 18. Let \(J\) be any finite label set and \(k>0\). Suppose \((\bar E_i)_{i\in J}\) is a complete orthogonal family of equivariant idempotents modulo \((\pi)^{e+k}\). There exists an integral equivariant family \((E_i)_{i\in J}\) satisfying
The loss is at most \(e\), independent of \(|J|\) and the ambient matrix rank. There is no local-ring or finite-residue-field hypothesis for existence. The formal theorem also treats empty label sets whenever their input equations can hold.
Average every supplied matrix once. Inductively let \(C\) be the complement of the previously lifted projectors and correct the next averaged matrix inside the corner defined by \(C\). The integral polynomial correction preserves the retained reduction and commutation with \(C\) and the carrier. Multiplication by \(C\) gives the required supported projector. This consumes no further precision. Once every label has been lifted, the complementary idempotent reduces to zero at positive depth. Adic separatedness forces it to vanish, proving the sum-to-identity equation.
The actual invariant images \(U_i=\operatorname{im}E_i\) give an equivariant linear isomorphism
Lean represents the finite direct sum by the finite product of the image submodules. The existing coordinatewise reduction theorem maps every \(U_i\) onto the corresponding reduced projector image. No chosen bases or unproved freeness of the images are used.
For rigidity alone, let \(R\) be a commutative local ring, let \(\pi\) be a nonunit, and let \(E,F\) be complete equivariant families on the same carrier with \(E_i\equiv F_i\pmod{(\pi)^k}\) for every label and \(k>0\). Then
Reduction reflects invertibility in this setting, so \(U\) is an integral unit and \(UE_iU^{-1}=F_i\). It commutes with the carrier and induces actual equivariant isomorphisms \(\operatorname{im}E_i\simeq\operatorname{im}F_i\). This rigidity theorem requires neither a finite acting group, a domain, nor completeness. More generally a unit-reflecting coefficient map suffices. The combined result proves existence and uniqueness up to this labeled conjugacy; exact uniqueness of the matrices is false.
For the continuous \(\mathbb Z_2\) carrier \(\rho(s)=\operatorname{diag}(1,-1,1)\), conjugate the three coordinate projectors by \(1+2e_{01}\) and reduce modulo \(4\). They form a complete equivariant family. The general theorem constructs three nonzero integral summands retaining this family modulo \(2\). No exact equivariant family retains the whole prescribed family modulo \(4\). Separate checked examples show that independent equivariant idempotent lifts can lose orthogonality, and that distinct complete families with the same reduction can be related by the asserted identity-congruent conjugacy.
Block 19 completes this finite-group projector-family step. The actual arithmetic packets, Galois-to-Weil–Deligne attachment, coefficient and Hodge–Tate/period comparisons, and arithmetic Frobenius coverage remain outside this result. At the Block 19 checkpoint, the ledger recorded fifteen checked claims and five partial claims; see the Block 23 conditional-scope correction above. Universal occupancy remains conjectural.