English
Let Q be a quadratic form on a module M over a commutative ring R, and for each n in Z/2Z consider the submodule evenOdd(Q, n) of the Clifford algebra Clifford(Q). Then the reversal automorphism of the Clifford algebra preserves this submodule, i.e., the submodule is fixed by reverse. Equivalently, (evenOdd(Q, n)) comap reverse = evenOdd(Q, n).
Русский
Пусть Q — квадратичная форма на модуле M над кольцом R, и для каждого n ∈ Z/2Z возьмем подпространство evenOdd(Q, n) клиффордовой алгебры Clifford(Q). Тогда обратное отображение (обратный перестановочный) сохраняет это подпространство, то есть подпространство инвариантно относительно обратного отображения: (evenOdd(Q, n)) comap reverse = evenOdd(Q, n).
LaTeX
$$$ (\\mathrm{evenOdd}(Q,n))^{\\mathrm{comap}\\,\\mathrm{reverse}} = \\mathrm{evenOdd}(Q,n) $$$
Lean4
@[simp]
theorem evenOdd_comap_reverse (n : ZMod 2) :
(evenOdd Q n).comap (reverse : CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) = evenOdd Q n := by
rw [← submodule_map_reverse_eq_comap, evenOdd_map_reverse]
