Tensor product of an indexed family of modules over commutative semirings #
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 FreeAddMonoid (R × ∀ i, s i)
quotiented by the appropriate equivalence relation. The treatment follows very closely that of the
binary tensor product in LinearAlgebra/TensorProduct.lean
.
Main definitions #
PiTensorProduct R s
withR
a commutative semiring ands : ι → Type*
is the tensor product of all thes i
's. This is denoted by⨂[R] i, s i
.tprod R f
withf : ∀ i, s i
is the tensor product of the vectorsf i
over alli : ι
. This is bundled as a multilinear map from∀ i, s i
to⨂[R] i, s i
.liftAddHom
constructs anAddMonoidHom
from(⨂[R] i, s i)
to some spaceF
from a functionφ : (R × ∀ i, s i) → F
with the appropriate properties.lift φ
withφ : MultilinearMap R s E
is the corresponding linear map(⨂[R] i, s i) →ₗ[R] E
. This is bundled as a linear equivalence.PiTensorProduct.reindex e
re-indexes the components of⨂[R] i : ι, M
alonge : ι ≃ ι₂
.PiTensorProduct.tmulEquiv
equivalence between aTensorProduct
ofPiTensorProduct
s and a singlePiTensorProduct
.
Notations #
⨂[R] i, s i
is defined as localized notation in localeTensorProduct
.⨂ₜ[R] i, f i
withf : ∀ i, f i
is defined globally as the tensor product of all thef i
's.
Implementation notes #
- We define it via
FreeAddMonoid (R × ∀ i, s i)
with theR
representing a "hidden" tensor factor, rather thanFreeAddMonoid (∀ i, s i)
to ensure that, ifι
is an empty type, the space is isomorphic to the base ringR
. - We have not restricted the index type
ι
to be aFintype
, 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
DecidableEq ι
as an argument toPiTensorProduct
itself, we include it as an argument in the constructors of the relation. A decidability instance still has to come from somewhere due to the use ofFunction.update
, but this hides it from the downstream user. See the implementation notes forMultilinearMap
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
- of_zero: ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)] [inst_2 : (i : ι) → Module R (s i)] (r : R) (f : (i : ι) → s i) (i : ι), f i = 0 → PiTensorProduct.Eqv R s (FreeAddMonoid.of (r, f)) 0
- of_zero_scalar: ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)] [inst_2 : (i : ι) → Module R (s i)] (f : (i : ι) → s i), PiTensorProduct.Eqv R s (FreeAddMonoid.of (0, f)) 0
- of_add: ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)] [inst_2 : (i : ι) → Module R (s i)] (x : DecidableEq ι) (r : R) (f : (i : ι) → s i) (i : ι) (m₁ m₂ : s i), PiTensorProduct.Eqv R s (FreeAddMonoid.of (r, Function.update f i m₁) + FreeAddMonoid.of (r, Function.update f i m₂)) (FreeAddMonoid.of (r, Function.update f i (m₁ + m₂)))
- of_add_scalar: ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)] [inst_2 : (i : ι) → Module R (s i)] (r r' : R) (f : (i : ι) → s i), PiTensorProduct.Eqv R s (FreeAddMonoid.of (r, f) + FreeAddMonoid.of (r', f)) (FreeAddMonoid.of (r + r', f))
- of_smul: ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)] [inst_2 : (i : ι) → Module R (s i)] (x : DecidableEq ι) (r : R) (f : (i : ι) → s i) (i : ι) (r' : R), PiTensorProduct.Eqv R s (FreeAddMonoid.of (r, Function.update f i (r' • f i))) (FreeAddMonoid.of (r' * r, f))
- add_comm: ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)] [inst_2 : (i : ι) → Module R (s i)] (x y : FreeAddMonoid (R × ((i : ι) → s i))), PiTensorProduct.Eqv R s (x + y) (y + x)
The relation on FreeAddMonoid (R × ∀ i, s i)
that generates a congruence whose quotient is
the tensor product.
Instances For
PiTensorProduct 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
.
Instances For
notation for tensor product over some indexed type
Instances For
tprodCoeff R r f
with r : R
and f : ∀ i, s i
is the tensor product of the vectors f i
over all i : ι
, multiplied by the coefficient r
. Note that this is meant as an auxiliary
definition for this file alone, and that one should use tprod
defined below for most purposes.
Instances For
Construct an AddMonoidHom
from (⨂[R] i, s i)
to some space F
from a function
φ : (R × ∀ i, s i) → F
with the appropriate properties.
Instances For
The canonical MultilinearMap R s (⨂[R] i, s i)
.
Instances For
pure tensor in tensor product over some index type
Instances For
Auxiliary function to constructing a linear map (⨂[R] i, s i) → E
given a
MultilinearMap R s E
with the property that its composition with the canonical
MultilinearMap R s (⨂[R] i, s i)
is the given multilinear map.
Instances For
Constructing a linear map (⨂[R] i, s i) → E
given a MultilinearMap R s E
with the
property that its composition with the canonical MultilinearMap R s E
is
the given multilinear map φ
.
Instances For
Re-index the components of the tensor power by e
.
For simplicity, this is defined only for homogeneously- (rather than dependently-) typed components.
Instances For
The tensor product over an empty index type ι
is isomorphic to the base ring.
Instances For
Tensor product of M
over a singleton set is equivalent to M
Instances For
Equivalence between a TensorProduct
of PiTensorProduct
s and a single
PiTensorProduct
indexed by a Sum
type.
For simplicity, this is defined only for homogeneously- (rather than dependently-) typed components.