Tensor product and products

In this file we examine the behaviour of the tensor product with arbitrary and finite products.

Let S be an R-algebra, N an S-module, ι an index type and Mᵢ a family of R-modules. We then have a natural map

TensorProduct.piRightHom: N ⊗[R] (∀ i, M i) →ₗ[S] ∀ i, N ⊗[R] M i

In general, this is not an isomorphism, but if ι is finite, then it is and it is packaged as TensorProduct.piRight. Also a special case for when Mᵢ = R is given.

Notes

See Mathlib.LinearAlgebra.TensorProduct.Prod for binary products.

noncomputable def TensorProduct.piRightHom (R : Type u_1) [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (N : Type u_3) [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower R S N] {ι : Type u_4} (M : ι → Type u_5) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] : TensorProduct R N ((i : ι) → M i) →ₗ[S] (i : ι) → TensorProduct R N (M i)

For any R-module N, index type ι and family of R-modules Mᵢ, there is a natural linear map N ⊗[R] (∀ i, M i) →ₗ ∀ i, N ⊗[R] M i. This map is an isomorphism if ι is finite.

Equations

• TensorProduct.piRightHom R S N M = TensorProduct.AlgebraTensorModule.lift (TensorProduct.piRightHomBil✝ R S N M)

@[simp]

theorem TensorProduct.piRightHom_tmul (R : Type u_1) [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (N : Type u_3) [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower R S N] {ι : Type u_4} (M : ι → Type u_5) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (x : N) (f : (i : ι) → M i) : (TensorProduct.piRightHom R S N M) (x ⊗ₜ[R] f) = fun (j : ι) => x ⊗ₜ[R] f j

noncomputable def TensorProduct.piRight (R : Type u_1) [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (N : Type u_3) [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower R S N] {ι : Type u_4} (M : ι → Type u_5) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [Fintype ι] [DecidableEq ι] : TensorProduct R N ((i : ι) → M i) ≃ₗ[S] (i : ι) → TensorProduct R N (M i)

Tensor product commutes with finite products on the right.

Equations

• TensorProduct.piRight R S N M = LinearEquiv.ofLinear (TensorProduct.piRightHom R S N M) (TensorProduct.piRightInv✝ R S N M) ⋯ ⋯

@[simp]

theorem TensorProduct.piRight_apply (R : Type u_1) [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (N : Type u_3) [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower R S N] {ι : Type u_4} (M : ι → Type u_5) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [Fintype ι] [DecidableEq ι] (x : TensorProduct R N ((i : ι) → M i)) : (TensorProduct.piRight R S N M) x = (TensorProduct.piRightHom R S N M) x

@[simp]

theorem TensorProduct.piRight_symm_apply (R : Type u_1) [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (N : Type u_3) [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower R S N] {ι : Type u_4} (M : ι → Type u_5) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [Fintype ι] [DecidableEq ι] (x : N) (m : (i : ι) → M i) : ((TensorProduct.piRight R S N M).symm fun (i : ι) => x ⊗ₜ[R] m i) = x ⊗ₜ[R] m

@[simp]

theorem TensorProduct.piRight_symm_single (R : Type u_1) [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (N : Type u_3) [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower R S N] {ι : Type u_4} (M : ι → Type u_5) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [Fintype ι] [DecidableEq ι] (x : N) (i : ι) (m : M i) : (TensorProduct.piRight R S N M).symm (Pi.single i (x ⊗ₜ[R] m)) = x ⊗ₜ[R] Pi.single i m

noncomputable def TensorProduct.piScalarRightHom (R : Type u_1) [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (N : Type u_3) [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower R S N] (ι : Type u_4) : TensorProduct R N (ι → R) →ₗ[S] ι → N

For any R-module N and index type ι, there is a natural linear map N ⊗[R] (ι → R) →ₗ (ι → N). This map is an isomorphism if ι is finite.

Equations

• TensorProduct.piScalarRightHom R S N ι = TensorProduct.AlgebraTensorModule.lift (TensorProduct.piScalarRightHomBil✝ R S N ι)

@[simp]

theorem TensorProduct.piScalarRightHom_tmul (R : Type u_1) [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (N : Type u_3) [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower R S N] (ι : Type u_4) (x : N) (f : ι → R) : (TensorProduct.piScalarRightHom R S N ι) (x ⊗ₜ[R] f) = fun (j : ι) => f j • x

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

For any R-module N and finite index type ι, N ⊗[R] (ι → R) is canonically isomorphic to ι → N.

Equations

• TensorProduct.piScalarRight R S N ι = LinearEquiv.ofLinear (TensorProduct.piScalarRightHom R S N ι) (TensorProduct.piScalarRightInv✝ R S N ι) ⋯ ⋯

@[simp]

theorem TensorProduct.piScalarRight_apply (R : Type u_1) [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (N : Type u_3) [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower R S N] (ι : Type u_4) [Fintype ι] [DecidableEq ι] (x : TensorProduct R N (ι → R)) : (TensorProduct.piScalarRight R S N ι) x = (TensorProduct.piScalarRightHom R S N ι) x

@[simp]

theorem TensorProduct.piScalarRight_symm_single (R : Type u_1) [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (N : Type u_3) [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower R S N] (ι : Type u_4) [Fintype ι] [DecidableEq ι] (x : N) (i : ι) : (TensorProduct.piScalarRight R S N ι).symm (Pi.single i x) = x ⊗ₜ[R] Pi.single i 1