toBaseChange_comp_ofBaseChange — Mathlib

English

The composition of toBaseChange with ofBaseChange is the identity map on the appropriate tensor product, i.e., the two-way base-change is invertible with explicit inverse.

Русский

Общее свойство: композиция toBaseChange и ofBaseChange является тождественным отображением на соответствующем тензорном произведении; базовые преобразования являются обратимыми с явным обратным отображением.

LaTeX

$$$(toBaseChange A Q) \circ (ofBaseChange A Q) = \mathrm{Id}_{A \otimes_R CliffordAlgebra Q}$$$

Lean4

theorem toBaseChange_comp_ofBaseChange (Q : QuadraticForm R V) :
    (toBaseChange A Q).comp (ofBaseChange A Q) = AlgHom.id _ _ :=
  by
  ext v
  simp

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