Documentation

Mathlib.LinearAlgebra.TensorProduct.Opposite

MulOpposite distributes over ⊗ #

The main result in this file is:

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