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.
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ᵐᵒᵖ)
:
(Algebra.TensorProduct.opAlgEquiv R S A B) x = MulOpposite.op
((TensorProduct.map ↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R))
↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)))
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)ᵐᵒᵖ)
:
(AlgEquiv.symm (Algebra.TensorProduct.opAlgEquiv R S A B)) x = (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ᵐᵒᵖ)
:
(Algebra.TensorProduct.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)
:
(AlgEquiv.symm (Algebra.TensorProduct.opAlgEquiv R S A B)) (MulOpposite.op (a ⊗ₜ[R] b)) = MulOpposite.op a ⊗ₜ[R] MulOpposite.op b