English
The even/odd submodule of CliffordAlgebra Q is defined as the supremum over all j of the range of ι_Q raised to the j-th power, restricted to parity i ∈ Z/2Z. In particular, evenOdd(0) is the even submodule and evenOdd(1) is the odd submodule.
Русский
Четная/нечетная подмодуля CliffordAlgebra Q определяются как верхняя грань (супремум) по всем j-го степеням образа ι_Q, а именно, evenOdd(0) — четная подмодуля, evenOdd(1) — нечетная.
LaTeX
$$def evenOdd (i : ZMod 2) : Submodule R (CliffordAlgebra Q) := ⨆ j : { n : ℕ // ↑n = i }, LinearMap.range (ι Q) ^ (j : ℕ)$$
Lean4
/-- The even or odd submodule, defined as the supremum of the even or odd powers of
`(ι Q).range`. `evenOdd 0` is the even submodule, and `evenOdd 1` is the odd submodule. -/
def evenOdd (i : ZMod 2) : Submodule R (CliffordAlgebra Q) :=
⨆ j : { n : ℕ // ↑n = i }, LinearMap.range (ι Q) ^ (j : ℕ)
