mathlib3 documentation

lean-ga / for_mathlib.linear_algebra.tensor_product.opposite

MulOpposite commutes with ⊗ #

The main result in this file is:

source
def algebra.tensor_product.op_alg_equiv {R : Type u_1} (S : Type u_2) {A : Type u_3} {B : Type u_4} [comm_semiring R] [comm_semiring S] [semiring A] [semiring B] [algebra R S] [algebra R A] [algebra R B] [algebra S A] [smul_comm_class R S A] [is_scalar_tower R S A] :
tensor_product R Aᵐᵒᵖ Bᵐᵒᵖ ≃ₐ[S] (tensor_product R A B)ᵐᵒᵖ

MulOpposite commutes with TensorProduct.

Equations
source
theorem algebra.tensor_product.op_alg_equiv_apply {R : Type u_1} (S : Type u_2) {A : Type u_3} {B : Type u_4} [comm_semiring R] [comm_semiring S] [semiring A] [semiring B] [algebra R S] [algebra R A] [algebra R B] [algebra S A] [smul_comm_class R S A] [is_scalar_tower R S A] (x : tensor_product R Aᵐᵒᵖ Bᵐᵒᵖ) :
⇑(algebra.tensor_product.op_alg_equiv S) x = mul_opposite.op (⇑(tensor_product.map (mul_opposite.op_linear_equiv R).symm.to_linear_map (mul_opposite.op_linear_equiv R).symm.to_linear_map) x)
source
@[simp]
theorem algebra.tensor_product.op_alg_equiv_tmul {R : Type u_1} (S : Type u_2) {A : Type u_3} {B : Type u_4} [comm_semiring R] [comm_semiring S] [semiring A] [semiring B] [algebra R S] [algebra R A] [algebra R B] [algebra S A] [smul_comm_class R S A] [is_scalar_tower R S A] (a : Aᵐᵒᵖ) (b : Bᵐᵒᵖ) :
⇑(algebra.tensor_product.op_alg_equiv S) (a ⊗ₜ[R] b) = mul_opposite.op (mul_opposite.unop a ⊗ₜ[R] mul_opposite.unop b)
source
@[simp]
theorem algebra.tensor_product.op_alg_equiv_symm_tmul {R : Type u_1} (S : Type u_2) {A : Type u_3} {B : Type u_4} [comm_semiring R] [comm_semiring S] [semiring A] [semiring B] [algebra R S] [algebra R A] [algebra R B] [algebra S A] [smul_comm_class R S A] [is_scalar_tower R S A] (a : A) (b : B) :
⇑((algebra.tensor_product.op_alg_equiv S).symm) (mul_opposite.op (a ⊗ₜ[R] b)) = mul_opposite.op a ⊗ₜ[R] mul_opposite.op b