English
The representation of the Clifford conjugate (i.e., reverse of the involute) in the even subalgebra matches the reverse of the representation of the original algebra, i.e., the natural diagram commutes with involution and reverse under the toEven map.
Русский
Представление кларификсации сопряжения (обратное к инволюции) в чётной подпалке совпадает с обратным отображением представления исходной алгебры; диаграмма естественна и коммутирует с инволюцией и обратным отображением через toEven.
LaTeX
$$$ \\uparrow\\bigl( toEven(Q) ( reverse ( involute (x) ) ) \\bigr) = reverse (Q' Q) ( toEven(Q) (x) ) $$$
Lean4
/-- The representation of the clifford conjugate (i.e. the reverse of the involute) in the even
subalgebra is just the reverse of the representation. -/
theorem coe_toEven_reverse_involute (x : CliffordAlgebra Q) :
↑(toEven Q (reverse (involute x))) = reverse (Q := Q' Q) (toEven Q x : CliffordAlgebra (Q' Q)) := by
induction x using CliffordAlgebra.induction with
| algebraMap r => simp only [AlgHom.commutes, Subalgebra.coe_algebraMap, reverse.commutes]
| ι m =>
simp only [involute_ι, Subalgebra.coe_neg, toEven_ι, reverse.map_mul, reverse_v, reverse_e0, reverse_ι,
neg_e0_mul_v, map_neg]
| mul x y hx hy => simp only [map_mul, Subalgebra.coe_mul, reverse.map_mul, hx, hy]
| add x y hx hy => simp only [map_add, Subalgebra.coe_add, hx, hy]
