Indexed tensor products of binary tensor products

For a finite index type ι and families of modules M i and N i, the indexed tensor product of the binary tensor products is the binary tensor product of the indexed tensor products:

⨂ᵢ (Mᵢ ⊗ Nᵢ) ≃ (⨂ᵢ Mᵢ) ⊗ (⨂ᵢ Nᵢ),     ⨂ₜ (mᵢ ⊗ₜ nᵢ) ↦ (⨂ₜ mᵢ) ⊗ₜ (⨂ₜ nᵢ).

The equivalence PiTensorProduct.tensorDistribEquiv is fixed by this formula on pure tensors. Its inverse is Mathlib's PiTensorProduct.map₂ applied to the factorwise tensor maps. It commutes with factorwise linear maps and with reindexing the factors, so it is equivariant for every action built from these two operations; in particular, it shows that tensor induction of representations takes tensor products to tensor products.

Finiteness of ι is needed: over an infinite index type, a multilinear map out of ∏ᵢ (Mᵢ ⊗ Nᵢ) would have to expand infinitely many sums at once.

Main definitions

• PiTensorProduct.tensorDistribEquiv: the equivalence ⨂ᵢ (Mᵢ ⊗ Nᵢ) ≃ (⨂ᵢ Mᵢ) ⊗ (⨂ᵢ Nᵢ).

Main results

• PiTensorProduct.tensorDistribEquiv_tprod: the defining formula on pure tensors.
• PiTensorProduct.tensorDistribEquiv_symm_toLinearMap: the inverse is map₂ of the factorwise tensor maps.
• PiTensorProduct.ext_tprod_tmul: linear maps out of ⨂ᵢ (Mᵢ ⊗ Nᵢ) are determined on the tensors ⨂ₜ (mᵢ ⊗ₜ nᵢ).
• PiTensorProduct.tensorDistribEquiv_map and PiTensorProduct.tensorDistribEquiv_reindex: compatibility with factorwise linear maps and with reindexing.

noncomputable def PiTensorProduct.tensorDistribEquiv (R : Type u) [CommSemiring R] {ι : Type x} [Finite ι] (M : ι → Type v) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (N : ι → Type w) [(i : ι) → AddCommMonoid (N i)] [(i : ι) → Module R (N i)] : (PiTensorProduct R fun (i : ι) => TensorProduct R (M i) (N i)) ≃ₗ[R] TensorProduct R (PiTensorProduct R fun (i : ι) => M i) (PiTensorProduct R fun (i : ι) => N i)

An indexed tensor product of binary tensor products is the binary tensor product of the indexed tensor products: ⨂ᵢ (Mᵢ ⊗ Nᵢ) ≃ (⨂ᵢ Mᵢ) ⊗ (⨂ᵢ Nᵢ). The index type must be finite.

@[simp]

theorem PiTensorProduct.tensorDistribEquiv_tprod {R : Type u} [CommSemiring R] {ι : Type x} [Finite ι] {M : ι → Type v} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {N : ι → Type w} [(i : ι) → AddCommMonoid (N i)] [(i : ι) → Module R (N i)] (m : (i : ι) → M i) (n : (i : ι) → N i) : (tensorDistribEquiv R M N) ((tprod R) fun (i : ι) => m i ⊗ₜ[R] n i) = (tprod R) m ⊗ₜ[R] (tprod R) n

The distributivity equivalence separates the two components of every tensor factor.

@[simp]

theorem PiTensorProduct.tensorDistribEquiv_symm_tmul {R : Type u} [CommSemiring R] {ι : Type x} [Finite ι] {M : ι → Type v} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {N : ι → Type w} [(i : ι) → AddCommMonoid (N i)] [(i : ι) → Module R (N i)] (m : (i : ι) → M i) (n : (i : ι) → N i) : (tensorDistribEquiv R M N).symm ((tprod R) m ⊗ₜ[R] (tprod R) n) = (tprod R) fun (i : ι) => m i ⊗ₜ[R] n i

The inverse distributivity equivalence pairs up the factors of two pure tensors.

theorem PiTensorProduct.tensorDistribEquiv_symm_toLinearMap {R : Type u} [CommSemiring R] {ι : Type x} [Finite ι] {M : ι → Type v} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {N : ι → Type w} [(i : ι) → AddCommMonoid (N i)] [(i : ι) → Module R (N i)] : ↑(tensorDistribEquiv R M N).symm = TensorProduct.lift (map₂ fun (i : ι) => TensorProduct.mk R (M i) (N i))

The inverse distributivity equivalence is map₂ of the factorwise tensor maps.

theorem PiTensorProduct.ext_tprod_tmul {R : Type u} [CommSemiring R] {ι : Type x} [Finite ι] {M : ι → Type v} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {N : ι → Type w} [(i : ι) → AddCommMonoid (N i)] [(i : ι) → Module R (N i)] {P : Type y} [AddCommMonoid P] [Module R P] {f g : (PiTensorProduct R fun (i : ι) => TensorProduct R (M i) (N i)) →ₗ[R] P} (h : ∀ (m : (i : ι) → M i) (n : (i : ι) → N i), f ((tprod R) fun (i : ι) => m i ⊗ₜ[R] n i) = g ((tprod R) fun (i : ι) => m i ⊗ₜ[R] n i)) : f = g

Linear maps out of ⨂ᵢ (Mᵢ ⊗ Nᵢ) agree once they agree on the tensors ⨂ₜ (mᵢ ⊗ₜ nᵢ).

theorem PiTensorProduct.tensorDistribEquiv_map {R : Type u} [CommSemiring R] {ι : Type x} [Finite ι] {M : ι → Type v} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {N : ι → Type w} [(i : ι) → AddCommMonoid (N i)] [(i : ι) → Module R (N i)] {M' : ι → Type u_1} [(i : ι) → AddCommMonoid (M' i)] [(i : ι) → Module R (M' i)] {N' : ι → Type u_2} [(i : ι) → AddCommMonoid (N' i)] [(i : ι) → Module R (N' i)] (f : (i : ι) → M i →ₗ[R] M' i) (g : (i : ι) → N i →ₗ[R] N' i) (z : PiTensorProduct R fun (i : ι) => TensorProduct R (M i) (N i)) : (tensorDistribEquiv R M' N') ((map fun (i : ι) => TensorProduct.map (f i) (g i)) z) = (TensorProduct.map (map f) (map g)) ((tensorDistribEquiv R M N) z)

The distributivity equivalence commutes with applying linear maps in every factor.

theorem PiTensorProduct.tensorDistribEquiv_reindex {R : Type u} [CommSemiring R] {ι : Type x} [Finite ι] {M : ι → Type v} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {N : ι → Type w} [(i : ι) → AddCommMonoid (N i)] [(i : ι) → Module R (N i)] {ι₂ : Type u_1} [Finite ι₂] (e : ι ≃ ι₂) (z : PiTensorProduct R fun (i : ι) => TensorProduct R (M i) (N i)) : (tensorDistribEquiv R (fun (j : ι₂) => M (e.symm j)) fun (j : ι₂) => N (e.symm j)) ((reindex R (fun (i : ι) => TensorProduct R (M i) (N i)) e) z) = (TensorProduct.map ↑(reindex R M e) ↑(reindex R N e)) ((tensorDistribEquiv R M N) z)

The distributivity equivalence commutes with reindexing the tensor factors.