MulOpposite distributes over ⊗ #
The main result in this file is:
Algebra.TensorProduct.opAlgEquiv R S A B : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ ≃ₐ[S] (A ⊗[R] B)ᵐᵒᵖ
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] :
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.
Instances For
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ᵐᵒᵖ) :
@[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) :