Axioms for the theory of proveit.linear_algebra.tensors

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

%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.

unary_tensor_prod_def = Forall(
        K, Forall(V, Forall(A, Equals(TensorProd(A), A), domain=V),
                  domain=VecSpaces(K)))

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

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

tensor_prod_in_vec_space_only_if_valid:

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

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)

multi_tensor_prod_def:

%end axioms

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