Documentation

Mathlib.LinearAlgebra.TensorProduct.Pi

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 and ι an index type. We then have a natural map

TensorProduct.piScalarRightHom: N ⊗[R] (ι → R) →ₗ[S] (ι → N)

In general, this is not an isomorphism, but if ι is finite, then it is and it is packaged as TensorProduct.piScalarRight.

Notes #

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

source
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
Instances For
    source
    @[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
    source
    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
    Instances For
      source
      @[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
      source
      @[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