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 to the algebra case.

@[simp]

theorem 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)] : (TensorProduct.piRightHom R S A B) 1 = 1

@[simp]

theorem 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)) : (TensorProduct.piRightHom R S A B) (x * y) = (TensorProduct.piRightHom R S A B) x * (TensorProduct.piRightHom R S A B) y

noncomputable def 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

• 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) : (Algebra.TensorProduct.piRight R S A B) (x ⊗ₜ[R] f) = fun (j : ι) => x ⊗ₜ[R] f j