Formalizing the characteristic-two retraction [connes-000U]

✍️source

delta_diagonalconcreteSquareSpanData

L∃∀NAGENTDRAFTED

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.