English
The base-change functor commutes with reversing the order in the tensor product: composing toBaseChange with reverseOp equals composing the tensor-product map with reverseOp composed with toBaseChange, reflecting the right-action of reversal.
Русский
Изменение базы и разворот тензорного произведения коммутируют: композиция toBaseChange с reverseOp равна композиции тензорного произведения с reverseOp и toBaseChange, что отражает правостороннее действие разворота.
LaTeX
$$$(toBaseChange A Q) \circ reverseOp = (Algebra.TensorProduct.map (Id_A) reverseOp) \circ (toBaseChange A Q)$$$
Lean4
/-- Auxiliary theorem used to prove `toBaseChange_reverse` without needing induction. -/
theorem toBaseChange_comp_reverseOp (Q : QuadraticForm R V) :
(toBaseChange A Q).op.comp reverseOp =
((Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q)).toAlgHom.comp <|
(Algebra.TensorProduct.map (AlgEquiv.toOpposite A A).toAlgHom (reverseOp (Q := Q))).comp (toBaseChange A Q)) :=
by
ext v
change
op (toBaseChange A Q (reverse (ι (Q.baseChange A) (1 ⊗ₜ[R] v)))) =
Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q)
(Algebra.TensorProduct.map (AlgEquiv.toOpposite A A).toAlgHom (reverseOp (Q := Q))
(toBaseChange A Q (ι (Q.baseChange A) (1 ⊗ₜ[R] v))))
rw [toBaseChange_ι, reverse_ι, toBaseChange_ι, Algebra.TensorProduct.map_tmul, Algebra.TensorProduct.opAlgEquiv_tmul,
reverseOp_ι]
rfl
