Tensor product of an indexed family of modules over commutative semirings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We define the tensor product of an indexed family s : ι → Type* of modules over commutative semirings. We denote this space by ⨂[R] i, s i and define it as free_add_monoid (R × Π i, s i) quotiented by the appropriate equivalence relation. The treatment follows very closely that of the binary tensor product in linear_algebra/tensor_product.lean.

Main definitions #

• pi_tensor_product R s with R a commutative semiring and s : ι → Type* is the tensor product of all the s i's. This is denoted by ⨂[R] i, s i.
• tprod R f with f : Π i, s i is the tensor product of the vectors f i over all i : ι. This is bundled as a multilinear map from Π i, s i to ⨂[R] i, s i.
• lift_add_hom constructs an add_monoid_hom from (⨂[R] i, s i) to some space F from a function φ : (R × Π i, s i) → F with the appropriate properties.
• lift φ with φ : multilinear_map R s E is the corresponding linear map (⨂[R] i, s i) →ₗ[R] E. This is bundled as a linear equivalence.
• pi_tensor_product.reindex e re-indexes the components of ⨂[R] i : ι, M along e : ι ≃ ι₂.
• pi_tensor_product.tmul_equiv equivalence between a tensor_product of pi_tensor_products and a single pi_tensor_product.

Notations #

• ⨂[R] i, s i is defined as localized notation in locale tensor_product
• ⨂ₜ[R] i, f i with f : Π i, f i is defined globally as the tensor product of all the f i's.

Implementation notes #

• We define it via free_add_monoid (R × Π i, s i) with the R representing a "hidden" tensor factor, rather than free_add_monoid (Π i, s i) to ensure that, if ι is an empty type, the space is isomorphic to the base ring R.
• We have not restricted the index type ι to be a fintype, as nothing we do here strictly requires it. However, problems may arise in the case where ι is infinite; use at your own caution.
• Instead of requiring decidable_eq ι as an argument to pi_tensor_product itself, we include it as an argument in the constructors of the relation. A decidability isntance still has to come from somewhere due to the use of function.update, but this hides it from the downstream user. See the implementation notes for multilinear_map for an extended discussion of this choice.

TODO #

• Define tensor powers, symmetric subspace, etc.
• API for the various ways ι can be split into subsets; connect this with the binary tensor product.
• Include connection with holors.
• Port more of the API from the binary tensor product over to this case.

Tags #

multilinear, tensor, tensor product