Lemma B.2 as an isomorphism: ⊕ coker D_m(E₄) ≅ ⊕_{i∈I} 𝒪/(2) #
characteristic-two-mesh-calculations.tex (lem:integral-mesh-cokernels): with
𝒪 = ℤ/4 and E₄ the mesh category with unit coefficients u reducing to the all-one
coefficients of C⁽²⁾, ⊕_{m≥2} coker D_m(E₄) ≅ ⊕_{i∈I} (𝒪/(2))_{χ_i}, the summand i lying
in coker D_{d_i−1}, d_i = 2s_i + 2.
For rows S spanning the cokernels over 𝔽₂ with independent classes and killed by two over
every ring (Proposition 6.1, residualCorrectionSpaces), in each degree m + 1 ≥ 3:
every family of degree m + 1 over 𝒪 is an 𝒪-combination of the rows of S modulo the
image of D_m (integral_rows_span; a remainder with zero reduction is twice a family of the
same degree, by the degree projections of C(Q, u), degProj), twice each row is a
derivative (two_smul_mem_imageD), and a combination is a derivative exactly when all its
coefficients are even (integral_rows_indep). Thus coker D_m(E₄) is ⊕ 𝒪/(2) over the rows
of S of degree m + 1 (integralMeshCokernels). The weight labels χ_i are not formalized
(no weight grading on E₄ is used).
The degree projection lands in the degree part.
The degree projection fixes the degree part.
Reduction maps derivatives to derivatives.
A sum over a family of rows, regrouped over the distinct rows.
The mesh derivative raises degrees by one.
Spanning over 𝒪: a family of degree m + 1 ≥ 3 is an 𝒪-combination of the rows of
S modulo the image of D_m.
Independence over 𝒪: a combination of rows of S of degree m + 1 is a derivative
exactly when all its coefficients are even.
Lemma B.2 (lem:integral-mesh-cokernels), as an isomorphism. In characteristic two,
under the hypotheses of Proposition 6.1 for C⁽²⁾ = C(Q, c), with E₄ = C(Q, u) over
𝒪 = ℤ/4: there is a set S of rows, one for each residual component i, of degree
d_i = 2s_i + 2, such that in each degree m + 1 ≥ 3 the classes of the rows of S of
degree m + 1 generate coker D_m(E₄), each has order two, and a combination vanishes exactly
when all its coefficients are even; that is, coker D_m(E₄) ≅ ⊕_{i : d_i = m + 1} 𝒪/(2).