MulOpposite distributes over ⊗

The main result in this file is:

• Algebra.TensorProduct.opAlgEquiv R S A B : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ ≃ₐ[S] (A ⊗[R] B)ᵐᵒᵖ

noncomputable def Algebra.TensorProduct.opAlgEquiv (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R S] [Algebra R A] [Algebra R B] [Algebra S A] [IsScalarTower R S A] : TensorProduct R Aᵐᵒᵖ Bᵐᵒᵖ ≃ₐ[S] (TensorProduct R A B)ᵐᵒᵖ

MulOpposite distributes over TensorProduct. Note this is an S-algebra morphism, where A/S/R is a tower of algebras.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebra.TensorProduct.opAlgEquiv_apply (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R S] [Algebra R A] [Algebra R B] [Algebra S A] [IsScalarTower R S A] (x : TensorProduct R Aᵐᵒᵖ Bᵐᵒᵖ) : (opAlgEquiv R S A B) x = MulOpposite.op ((_root_.TensorProduct.map ↑(MulOpposite.opLinearEquiv R).symm ↑(MulOpposite.opLinearEquiv R).symm) x)

theorem Algebra.TensorProduct.opAlgEquiv_symm_apply (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R S] [Algebra R A] [Algebra R B] [Algebra S A] [IsScalarTower R S A] (x : (TensorProduct R A B)ᵐᵒᵖ) : (opAlgEquiv R S A B).symm x = (_root_.TensorProduct.map ↑(MulOpposite.opLinearEquiv R) ↑(MulOpposite.opLinearEquiv R)) (MulOpposite.unop x)

@[simp]

theorem Algebra.TensorProduct.opAlgEquiv_tmul (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R S] [Algebra R A] [Algebra R B] [Algebra S A] [IsScalarTower R S A] (a : Aᵐᵒᵖ) (b : Bᵐᵒᵖ) : (opAlgEquiv R S A B) (a ⊗ₜ[R] b) = MulOpposite.op (MulOpposite.unop a ⊗ₜ[R] MulOpposite.unop b)

@[simp]

theorem Algebra.TensorProduct.opAlgEquiv_symm_tmul (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R S] [Algebra R A] [Algebra R B] [Algebra S A] [IsScalarTower R S A] (a : A) (b : B) : (opAlgEquiv R S A B).symm (MulOpposite.op (a ⊗ₜ[R] b)) = MulOpposite.op a ⊗ₜ[R] MulOpposite.op b