Research proof index

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.

Removing two pairs of entries from c in either order gives the same colour list: removing the i1-th and j1-th entries and then the (shifted) i2-th and j2-th entries matches removing the i2-th and j2-th entries first and then the (shifted) i1-th and j1-th entries, via the identity permutation. This is used for the commutation of two *cont...

Rewriting basis for the product in terms of the tensor product basis. -/ lemma basis_prod_eq {n1 n2} {c : Fin n1 → C} {c1 : Fin n2 → C} : basis (S := S) (Fin.append c c1) = (((Tensor.basis (S := S) c).tensorProduct (Tensor.basis (S := S) c1)).reindex (ComponentIdx.prod.symm)).map tensorEquivProd := by ext b simp [ComponentIdx.prod, tensorEquivProd] rw [pr...