Definition. Internal parity grading [fdip-001J]

Let \(R\) be a commutative unital ring and \(A\) an associative unital \(R\)-algebra. An internal parity grading consists of \(R\)-submodules \(A_0,A_1\subseteq A\), with operations inherited from \(A\), such that every \(a\in A\) has a unique decomposition \(a=a_0+a_1\), with \(a_i\in A_i\), and \[1\in A_0,\qquad A_iA_j\subseteq A_{i+j}.\] Subscripts are added in \(\mathbb Z/2\mathbb Z\). An element of \(A_i\) is homogeneous of parity \(i\); parity \(0\) is even and parity \(1\) is odd. The zero element lies in both submodules. Scalars \(r1\) belong to \(A_0\).

The multiplication condition controls the component of a product; it does not require \(ab=(-1)^{ij}ba\) for \(a\in A_i\), \(b\in A_j\). Nor does it require an odd element to square to zero. Those are additional equations, tested explicitly by the four-cycle.

The internal-submodule viewpoint and multiplication rule follow [wieser2022graded, Section 1, accepted-manuscript pp. 1-2], here specialized to the index group \(\mathbb Z/2\mathbb Z\). Mathlib's GradedRing and GradedAlgebra encode graded multiplication and compatible scalar data. The chosen operator decomposition still needs the proof in Proposition [fdip-001K].