English
There is an inverse isomorphism between CliffordAlgebra under base change and the base change of CliffordAlgebra, so that applying toBaseChange after ofBaseChange yields the identity on the corresponding tensor product.
Русский
Существует обратное изоморфное отображение между CliffordAlgebra после изменения базы и изменением базы CliffordAlgebra; применение toBaseChange после ofBaseChange даёт тождественность на соответствующем тензорном произведении.
LaTeX
$$$(toBaseChange A Q) \circ (ofBaseChange A Q) = \mathrm{Id}$$$
Lean4
/-- `reverse` acts only on the right of the tensor product. -/
theorem toBaseChange_reverse (Q : QuadraticForm R V) (x : CliffordAlgebra (Q.baseChange A)) :
toBaseChange A Q (reverse x) = TensorProduct.map LinearMap.id reverse (toBaseChange A Q x) :=
by
have := DFunLike.congr_fun (toBaseChange_comp_reverseOp A Q) x
refine (congr_arg unop this).trans ?_; clear this
refine (LinearMap.congr_fun (TensorProduct.AlgebraTensorModule.map_comp _ _ _ _).symm _).trans ?_
rw [reverse, ← AlgEquiv.toLinearMap, ← AlgEquiv.toLinearEquiv_toLinearMap, AlgEquiv.toLinearEquiv_toOpposite]
dsimp
-- `simp` fails here due to a timeout looking for a `Subsingleton` instance!?
rw [LinearEquiv.self_trans_symm]
rfl
