4 Tangent and obstruction packets
On this page · Permalink · Source line 334
For a residual representation \(\bar\rho\), first-order deformations and lifting obstructions are classically controlled by cohomology of the adjoint module. The projector calculus does not replace that theory. It resolves the controlling complex into invariant packets when suitable projectors exist.
Classical input 4.1: Tangent and obstruction spaces
For a framed representation problem, first-order lifts are described by \(Z^1(G,{\operatorname{ad}}\bar\rho)\). For an unframed Schur problem, tangent directions are described by \(H^1(G,{\operatorname{ad}}\bar\rho)\). Relations in a presentation of a deformation ring map into \(H^2(G,{\operatorname{ad}}\bar\rho)\), which contains the obstruction classes.
Permalink · Source line 338 · Claim record · Lean coverage · Code · Worked examples
Let
be a cochain complex over a field. Suppose a finite family of projectors \(P_j^r:C^r\to C^r\) satisfies
Theorem 4.2: Cohomology packet decomposition
Under these hypotheses, each packet is a subcomplex and
In particular,
so tangent and obstruction spaces reconstruct exactly from their packet components.
Read proof · Visual guide: See cycles, boundaries, and classes · Visual guide: An arbitrary cut need not descend · Read statement and proof side by side · Permalink · Source line 355 · Claim record · Lean coverage · Code · Worked examples
Proof of Theorem 4.2
For each packet, use the actual image submodules \(C_j^r=\operatorname{im}P_j^r\). Commutation with the differential makes these a subcomplex. Write
and define \(Z_j^r,B_j^r,H_j^r\) using the restricted differentials of \(C_j^\bullet\). The inclusion \(i_j:C_j^\bullet\to C^\bullet\) and the image-valued projection \(p_j:C^\bullet\to C_j^\bullet\) are cochain maps, so they induce maps on these genuine quotients.
For \(i\ne j\), orthogonality gives \(H(p_i)H(i_j)=0\). Idempotence gives \(H(p_j)H(i_j)=I\), and completeness gives \(\sum_j H(i_j)H(p_j)=I\). Thus the maps
are inverse linear maps. The finite product equals the direct sum, proving the assertion. In the formalization, both sides are also identified with Mathlib's standard homology objects of the genuine graded complexes.
Back to statement · Read statement and proof side by side · Permalink · Source line 373 · Claim record · Lean coverage · Code · Worked examples
Scope of the splitting.
On this page · Permalink · Source line 400
The algebraic proof works over any commutative ring and does not divide by \(2\), so it applies in characteristic two when the stated integral chain projectors exist. It does not construct those projectors. The identification of a particular Galois tangent or obstruction problem with this cohomology remains the preceding classical input. The splitting detects vanishing:
It does not force either side to vanish or decouple nonlinear deformation equations. Moreover, commutation with the differential is essential: complementary idempotents on the underlying vector spaces need not preserve cocycles or coboundaries.
Naturality.
On this page · Permalink · Source line 416
If a cochain map \(F:C^\bullet\to D^\bullet\) intertwines the supplied projectors, it restricts to maps \(F_j:C_j^\bullet\to D_j^\bullet\). The direct-sum decomposition commutes with \(H^r(F)\) and the family \(H^r(F_j)\). This is checked using representatives in the actual quotients, independently of any dimension computation.
Remark 4.3: Odd and dyadic nonlinear equations
At odd residue characteristic, a differential graded Lie model may be written in Maurer–Cartan form
and a cyclic grading converts this into exact packet convolutions. At residue characteristic two, division by \(2\) is not integral. A quadratic or divided-square refinement must be retained. This is one reason the dyadic residual forest is weighted rather than obtained by formal substitution into the odd-prime formulas.
Numerical certificate 4.4: Finite packet complex
The exact modular test uses two invariant subcomplexes over \({\mathbf F}_5\). Their cohomology dimensions are
and the reconstructed total is
The packet-sum residual is zero.
Permalink · Source line 432 · Claim record · Lean coverage · Code · Worked examples
New checked realization of the finite pattern.
On this page · Permalink · Source line 446
The Block 04 implementation separately uses
The first packet is the exact complex with dimensions \((1,2,1)\), and the second packet has zero differentials and dimensions \((1,2,1)\). The actual middle cohomology is linearly isomorphic to \(\mathbf F_5^2\), which is checked in Lean. Independent exhaustive coset tests check all three cohomology degrees after changes of basis. This is a new specified realization of the displayed dimension pattern, not a claimed rerun of the original companion implementation.
