# Axioms for the theory of proveit.linear_algebra.tensors¶

In [1]:
import proveit
# Prepare this notebook for defining the axioms of a theory:
%axioms_notebook # Keep this at the top following 'import proveit'.

from proveit import m, A, B, K, U, V, W
from proveit.core_expr_types import A_1_to_m
from proveit.logic import And, Forall, Exists, Equals, InSet
from proveit.numbers import Natural
from proveit.linear_algebra import VecSpaces, TensorProd

In [2]:
%begin axioms

Defining axioms for theory 'proveit.linear_algebra.tensors'
Subsequent end-of-cell assignments will define axioms
%end_axioms will finalize the definitions


A unary tensor product of a vector (over any field) is just the vector itself.

In [3]:
unary_tensor_prod_def = Forall(
K, Forall(V, Forall(A, Equals(TensorProd(A), A), domain=V),
domain=VecSpaces(K)))

Out[3]:
unary_tensor_prod_def:

Need binary_tensor_prod_def to really define tensor products

By the following axiom, we can know that a TensorProd only results in an element of a vector space over a field if the operands are also in vector spaces over that field (otherwise, if no such field or vector spaces exists, the TensorProd is not defined unless it is a tensor product of vector spaces themselves):

In [4]:
tensor_prod_in_vec_space_only_if_valid = Forall(
K, Forall(
W, Forall(
(A, B), Exists((U, V),
And(InSet(A, U), InSet(B, V)),
domain=VecSpaces(K)),
condition=InSet(TensorProd(A, B), W)),
domain=VecSpaces(K)))

Out[4]:
tensor_prod_in_vec_space_only_if_valid:

We define multiple tensor products as successive tensor products without any constraints for simplicity.

In [5]:
multi_tensor_prod_def = \
Forall(m, Forall((A_1_to_m, B),
Equals(TensorProd(A_1_to_m, B),
TensorProd(TensorProd(A_1_to_m), B))
.with_wrap_after_operator()),
domain=Natural)

Out[5]:
multi_tensor_prod_def:
In [6]:
%end axioms

These axioms may now be imported from the theory package: proveit.linear_algebra.tensors