ofBaseChange_comp_toBaseChange — Mathlib

English

The base-change operation is compatible with reversing tensor factors on the right, i.e., toBaseChange respects the right-acting involution on the Clifford algebra.

Русский

Изменение базы совместимо с разворотом правого множителя в тензорном произведении: toBaseChange сохраняет правосторонний разворот на алгебре Клиффорд.

LaTeX

$$$toBaseChange(A,Q)(\text{reverse}(x)) = (\mathrm{Id}_A \otimes \text{reverse}) (toBaseChange(A,Q)(x))$$$

Lean4

theorem ofBaseChange_comp_toBaseChange (Q : QuadraticForm R V) :
    (ofBaseChange A Q).comp (toBaseChange A Q) = AlgHom.id _ _ :=
  by
  ext x
  change ofBaseChange A Q (toBaseChange A Q (ι (Q.baseChange A) (1 ⊗ₜ[R] x))) = ι (Q.baseChange A) (1 ⊗ₜ[R] x)
  rw [toBaseChange_ι, ofBaseChange_tmul_ι]

Похожие утверждения