Research proof index

Reconstruction of a tensor from the evaluations of its first index: every t : Tensor S c is the sum over basis indices i of the basis covector basis ![c 0] (single.symm i) tensored with the evaluation evalT 0 i t, with the prepended index permuted back into the first slot. This is the first-index analogue of eq_sum_evalT.

Commuting evaluation with permutations.

Evaluating an index in the right factor of a tensor product commutes with forming the product, up to the identity reindexing which identifies the two ways of removing that index from the appended color list.

Contracting the i-th index of a tensor with the first index of an appended metric tensor is, up to a cycle permutation, a reindexing to the color list where the i-th index is replaced by its dual.

Given a reindexing of c by c1 via σ for which the index i is sent to 0, removing the i-th entry of c1 and the first entry of c yields a reindexing of c ∘ Fin.succ by c1 ∘ i.succAbove via the map sending j to the predecessor of σ (i.succAbove j).

Given a reindexing of c by c1 via σ for which the index i is not sent to 0, removing the i-th entry of c1 and the (σ i)-th entry of c yields a reindexing of c ∘ (σ i).succAbove by c1 ∘ i.succAbove via the map (σ i).pred.predAbove ∘ σ ∘ i.succAbove.