Tensor retraction in characteristic two [connes-001E]
✍️source

    Lemma. Characteristic-two tensor retraction [connes-000C]
    delta_diagonalconcreteSquareSpanData
    L∃∀N

      Let \(k=\mathbb F_2\), \(A=k[t]^3\), and let \[C=(A\otimes _k A)^{\mathrm {Flip}}.\] The diagonal function \(\Delta (a)=a\otimes a\) lands in \(C\). Although \(\Delta \) is not a linear map, Zhou's characteristic-two calculation produces a surjective linear retraction \(\delta :C\to A\) satisfying \(\delta (\Delta (a))=a\) [zhou2026icc, Section 2, Lemma 2.1]. The retraction is equivariant for the diagonal \(\mathrm {SL}_3(k[t])\)-action.

      References

        Reference. ICC property-(T) groups without W-star-superrigidity [zhou2026icc]

        @misc{zhou2026icc,
  title = {ICC Property-(T) Groups Without W*-Superrigidity},
  author = {Zhou, Shuoxing},
  year = {2026},
  eprint = {2608.02327},
  archivePrefix = {arXiv},
  primaryClass = {math.OA},
  url = {https://arxiv.org/abs/2608.02327}
}

        Context

          Characteristic-two tensor kernel (Zhou §2) [connes-0011]

            Tensor retraction in characteristic two [connes-001E]
            ✍️source

              Lemma. Characteristic-two tensor retraction [connes-000C]
              delta_diagonalconcreteSquareSpanData
              L∃∀N

                Let \(k=\mathbb F_2\), \(A=k[t]^3\), and let \[C=(A\otimes _k A)^{\mathrm {Flip}}.\] The diagonal function \(\Delta (a)=a\otimes a\) lands in \(C\). Although \(\Delta \) is not a linear map, Zhou's characteristic-two calculation produces a surjective linear retraction \(\delta :C\to A\) satisfying \(\delta (\Delta (a))=a\) [zhou2026icc, Section 2, Lemma 2.1]. The retraction is equivariant for the diagonal \(\mathrm {SL}_3(k[t])\)-action.

                Formalizing the characteristic-two retraction [connes-000U]
                delta_diagonalconcreteSquareSpanData
                L∃∀N

                  The Lean carriers and diagonal for Lemma [connes-000C] are Connes.Construction.PaperKernel.C and Connes.Construction.PaperKernel.diagonal; the coefficientwise map and retraction equation are Connes.Construction.PaperKernel.delta and Connes.Construction.PaperKernel.delta_diagonal.

                  The implementation fixes the standard polynomial and coordinate bases. It takes the coefficientwise Hadamard product on \(k[t]\), applies it in the three coordinates of \(A\), lifts the resulting bilinear map through the tensor product, and restricts it to \(C\). The Boolean identity \(x^2=x\) gives \(\delta (a\otimes a)=a\).

                  The basis-dependent formula implements a basis-free role: a linear left inverse to the diagonal squares, equivariant for the diagonal \(\mathrm {SL}_3(k[t])\)-action. Equivariance is not proved by expanding an arbitrary fixed tensor. The submodule Connes.Construction.PaperKernel.squareSpan is the span of the squares \(a\otimes a\); the equation is immediate on each square, hence on their span.

                  The basis calculation in Connes.Construction.PaperKernel.concreteSquareSpanData proves that every flip-fixed tensor belongs to this span. The SquareSpanData interface therefore hides the coordinates from later sections. Consumers need only the spanning result, so a future basis-free construction could replace the formula without changing the action or theorem interfaces.