opAlgEquiv_symm_apply — Mathlib

English

For x ∈ (A ⊗_R B)^{op}, the inverse map (opAlgEquiv)^{-1} is given by applying the factorwise map on x.unop.

Русский

Для x ∈ (A ⊗_R B)^{op}, обратное отображение (opAlgEquiv)^{-1} задаётся применением поперечного отображения к x.unop.

LaTeX

$$$(opAlgEquiv R S A B)^{-1}(x) = \mathrm{TensorProduct.map}((opLinearEquiv R).toLinearMap,(opLinearEquiv R).toLinearMap)(x^{\mathrm{unop}}).$$$

Lean4

theorem opAlgEquiv_symm_apply (x : (A ⊗[R] B)ᵐᵒᵖ) :
    (opAlgEquiv R S A B).symm x =
      _root_.TensorProduct.map (opLinearEquiv R).toLinearMap (opLinearEquiv R).toLinearMap x.unop :=
  rfl

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