English
There exists an isomorphism of S-algebras between A^{op} ⊗_R B^{op} and (A ⊗_R B)^{op}, given by sending a^{op} ⊗ b^{op} to (a ⊗ b)^{op} on pure tensors.
Русский
Существует изоморфизм S-алгебр между A^{op} ⊗_R B^{op} и (A ⊗_R B)^{op}, который на простых тензорах отправляет a^{op} ⊗ b^{op} в (a ⊗ b)^{op}.
LaTeX
$$$opAlgEquiv: A^{op} \otimes_R B^{op} \cong_S (A \otimes_R B)^{op},\qquad opAlgEquiv(a^{op} \otimes b^{op}) = (a \otimes b)^{op} \text{ for all } a \in A, b \in B.$$$
Lean4
/-- `MulOpposite` distributes over `TensorProduct`. Note this is an `S`-algebra morphism, where
`A/S/R` is a tower of algebras. -/
def opAlgEquiv : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ ≃ₐ[S] (A ⊗[R] B)ᵐᵒᵖ :=
letI e₁ : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ ≃ₗ[S] (A ⊗[R] B)ᵐᵒᵖ :=
TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S).symm (opLinearEquiv R).symm ≪≫ₗ opLinearEquiv S
letI e₂ : A ⊗[R] B ≃ₗ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ :=
TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S) (opLinearEquiv R) ≪≫ₗ opLinearEquiv S
AlgEquiv.ofAlgHom
(algHomOfLinearMapTensorProduct e₁.toLinearMap (fun a₁ a₂ b₁ b₂ => unop_injective (by with_unfolding_all rfl))
(unop_injective rfl))
(AlgHom.opComm <|
algHomOfLinearMapTensorProduct e₂.toLinearMap (fun a₁ a₂ b₁ b₂ => unop_injective (by with_unfolding_all rfl))
(unop_injective rfl))
(AlgHom.op.symm.injective <| by ext <;> rfl) (by ext <;> rfl)
