English
Let Q be a quadratic form on a module M over a commutative ring R. For every parity n in Z/2Z, the parity submodule evenOdd(Q, n) inside the Clifford algebra CliffordAlgebra Q is invariant under the reverse map; i.e., applying the reverse linear map to the submodule yields the same submodule.
Русский
Пусть Q — квадратичная форма на модуле M над кольцом R. Для каждого значения разряда n в Z/2Z подполя evenOdd(Q, n) внутри CliffordAlgebra Q образуют подмодуль, который останется неизменным под действием оператора reverse, то есть образ от (evenOdd(Q, n)) под reverse равен itself.
LaTeX
$$$ (\\text{evenOdd}(Q, n)).map(\\text{reverse} : \\mathrm{CliffordAlgebra}(Q) \\to \\mathrm{CliffordAlgebra}(Q)) = \\text{evenOdd}(Q, n) $$$
Lean4
@[simp]
theorem evenOdd_map_reverse (n : ZMod 2) :
(evenOdd Q n).map (reverse : CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) = evenOdd Q n := by
simp_rw [evenOdd, Submodule.map_iSup, submodule_map_pow_reverse, ι_range_map_reverse]
