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),

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)),
            condition=InSet(TensorProd(A, B), W)),

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))
In [6]:
%end axioms
These axioms may now be imported from the theory package: proveit.linear_algebra.tensors