Tensor product and products of algebras

In this file we examine the behaviour of the tensor product with (finite) products. This is a direct application of Mathlib/LinearAlgebra/TensorProduct/Pi.lean to the algebra case.

@[simp]

theorem Algebra.TensorProduct.piRightHom_one (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommSemiring R] [CommSemiring S] [Algebra R S] [CommSemiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {ι : Type u_4} (B : ι → Type u_5) [(i : ι) → CommSemiring (B i)] [(i : ι) → Algebra R (B i)] : (_root_.TensorProduct.piRightHom R S A B) 1 = 1

@[simp]

theorem Algebra.TensorProduct.piRightHom_mul {R : Type u_1} {S : Type u_2} {A : Type u_3} [CommSemiring R] [CommSemiring S] [Algebra R S] [CommSemiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {ι : Type u_4} {B : ι → Type u_5} [(i : ι) → CommSemiring (B i)] [(i : ι) → Algebra R (B i)] (x y : TensorProduct R A ((i : ι) → B i)) : (_root_.TensorProduct.piRightHom R S A B) (x * y) = (_root_.TensorProduct.piRightHom R S A B) x * (_root_.TensorProduct.piRightHom R S A B) y

noncomputable def Algebra.TensorProduct.piRightHom (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommSemiring R] [CommSemiring S] [Algebra R S] [CommSemiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {ι : Type u_4} (B : ι → Type u_5) [(i : ι) → CommSemiring (B i)] [(i : ι) → Algebra R (B i)] : TensorProduct R A ((i : ι) → B i) →ₐ[S] (i : ι) → TensorProduct R A (B i)

The canonical map A ⊗[R] (∀ i, B i) →ₐ[S] ∀ i, A ⊗[R] B i. This is an isomorphism if ι is finite (see Algebra.TensorProduct.piRight).

Equations

• Algebra.TensorProduct.piRightHom R S A B = AlgHom.ofLinearMap (TensorProduct.piRightHom R S A B) ⋯ ⋯

noncomputable def Algebra.TensorProduct.piRight (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommSemiring R] [CommSemiring S] [Algebra R S] [CommSemiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {ι : Type u_4} (B : ι → Type u_5) [(i : ι) → CommSemiring (B i)] [(i : ι) → Algebra R (B i)] [Fintype ι] [DecidableEq ι] : TensorProduct R A ((i : ι) → B i) ≃ₐ[S] (i : ι) → TensorProduct R A (B i)

Tensor product of rings commutes with finite products on the right.

Equations

• Algebra.TensorProduct.piRight R S A B = AlgEquiv.ofLinearEquiv (TensorProduct.piRight R S A B) ⋯ ⋯

@[simp]

theorem Algebra.TensorProduct.piRight_tmul (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommSemiring R] [CommSemiring S] [Algebra R S] [CommSemiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {ι : Type u_4} (B : ι → Type u_5) [(i : ι) → CommSemiring (B i)] [(i : ι) → Algebra R (B i)] [Fintype ι] [DecidableEq ι] (x : A) (f : (i : ι) → B i) : (piRight R S A B) (x ⊗ₜ[R] f) = fun (j : ι) => x ⊗ₜ[R] f j

noncomputable def Algebra.TensorProduct.piScalarRight (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommSemiring R] [CommSemiring S] [Algebra R S] [CommSemiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] (ι : Type u_4) [Fintype ι] [DecidableEq ι] : TensorProduct R A (ι → R) ≃ₐ[S] ι → A

Variant of Algebra.TensorProduct.piRight with constant factors.

Equations

• Algebra.TensorProduct.piScalarRight R S A ι = (Algebra.TensorProduct.piRight R S A fun (x : ι) => R).trans (AlgEquiv.piCongrRight fun (x : ι) => Algebra.TensorProduct.rid R S A)

theorem Algebra.TensorProduct.piScalarRight_tmul (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommSemiring R] [CommSemiring S] [Algebra R S] [CommSemiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (x : A) (y : ι → R) : (piScalarRight R S A ι) (x ⊗ₜ[R] y) = fun (i : ι) => y i • x

@[simp]

theorem Algebra.TensorProduct.piScalarRight_tmul_apply (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommSemiring R] [CommSemiring S] [Algebra R S] [CommSemiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (x : A) (y : ι → R) (i : ι) : (piScalarRight R S A ι) (x ⊗ₜ[R] y) i = y i • x

noncomputable def Algebra.TensorProduct.prodRight (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommSemiring R] [CommSemiring S] [Algebra R S] [CommSemiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] (B : Type u_6) (C : Type u_7) [Semiring B] [Semiring C] [Algebra R B] [Algebra R C] : TensorProduct R A (B × C) ≃ₐ[S] TensorProduct R A B × TensorProduct R A C

Tensor product of rings commutes with binary products on the right.

Equations

• Algebra.TensorProduct.prodRight R S A B C = AlgEquiv.ofLinearEquiv (TensorProduct.prodRight R S A B C) ⋯ ⋯

theorem Algebra.TensorProduct.prodRight_tmul (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommSemiring R] [CommSemiring S] [Algebra R S] [CommSemiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] (B : Type u_6) (C : Type u_7) [Semiring B] [Semiring C] [Algebra R B] [Algebra R C] (a : A) (x : B × C) : (prodRight R S A B C) (a ⊗ₜ[R] x) = (a ⊗ₜ[R] x.1, a ⊗ₜ[R] x.2)

@[simp]

theorem Algebra.TensorProduct.prodRight_tmul_fst (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommSemiring R] [CommSemiring S] [Algebra R S] [CommSemiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] (B : Type u_6) (C : Type u_7) [Semiring B] [Semiring C] [Algebra R B] [Algebra R C] (a : A) (x : B × C) : ((prodRight R S A B C) (a ⊗ₜ[R] x)).1 = a ⊗ₜ[R] x.1

@[simp]

theorem Algebra.TensorProduct.prodRight_tmul_snd (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommSemiring R] [CommSemiring S] [Algebra R S] [CommSemiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] (B : Type u_6) (C : Type u_7) [Semiring B] [Semiring C] [Algebra R B] [Algebra R C] (a : A) (x : B × C) : ((prodRight R S A B C) (a ⊗ₜ[R] x)).2 = a ⊗ₜ[R] x.2

@[simp]

theorem Algebra.TensorProduct.prodRight_symm_tmul (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommSemiring R] [CommSemiring S] [Algebra R S] [CommSemiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] (B : Type u_6) (C : Type u_7) [Semiring B] [Semiring C] [Algebra R B] [Algebra R C] (a : A) (b : B) (c : C) : (prodRight R S A B C).symm (a ⊗ₜ[R] b, a ⊗ₜ[R] c) = a ⊗ₜ[R] (b, c)