English
Let R be a commutative ring and let Q be a quadratic form on a module M. In the Clifford algebra Cl(Q) there is an involution called reverse. This involution fixes the scalars coming from R, i.e. for every r in R, reverse(algebraMap R (CliffordAlgebra Q) r) = algebraMap R (CliffordAlgebra Q) r.
Русский
Пусть R — коммутативное кольцо и Q — квадратичная форма на модуле M. В клиффордовой алгебре Cl(Q) существует инволюция reverse. Эта инволюция фиксирует скаляры из R, то есть для каждого r в R выполняется reverse(algebraMap R (CliffordAlgebra Q) r) = algebraMap R (CliffordAlgebra Q) r.
LaTeX
$$$ reverse( algebraMap R (CliffordAlgebra Q) r ) = algebraMap R (CliffordAlgebra Q) r $$$
Lean4
@[simp]
theorem commutes (r : R) : reverse (algebraMap R (CliffordAlgebra Q) r) = algebraMap R _ r :=
op_injective <| reverseOp.commutes r
