Contraction against the unit tensor

i. Overview

The unit tensor is the identity for slot contraction: contracting any slot of t against unitTensor for that slot's color returns t, the slot relabelled to the survivor tail. That is what collapses "raise then lower" to the identity, a metric contracted against its dual becoming the unit tensor and then contracting away.

crossToEnd_unitTensor is proved by decomposing t along its last slot (eq_sum_evalT) and transporting to an arbitrary slot with the transposition swap i (last). On it the round trip against a matched pair is assembled in both conventions, and a pair collapsing in both orders makes the two contractions mutually inverse, which crossToSlotEquiv bundles as a linear equivalence between the two color assignments.

Since unitTensor is RCLike-valued, this material sits over an [RCLike k] variable block, apart from the CommRing crossToEnd/crossToSlot algebra.

ii. Key results

TensorSpecies.Tensor.crossToEnd_unitTensor : the unit tensor is an identity for crossToEnd at any named slot.

TensorSpecies.Tensor.crossToEnd_round_trip_of_unit_slot : two contractions against a pair that collapses to the unit tensor return the original tensor, in result-to-end form.

TensorSpecies.Tensor.crossToSlot_raise_lower_round_trip : the round trip in result-to-slot form, every color propositional.

TensorSpecies.Tensor.crossToSlotEquiv : raising and lowering a named index against a pair that collapses in both orders, as a linear equivalence.

iii. Table of contents

A. The unit tensor as a slot-contraction identity

B. Round trips against a matched pair

C. Raising and lowering as an equivalence

iv. References

A. The unit tensor as a slot-contraction identity

Contracting a named slot against unitTensor returns the tensor unchanged, the slot carried to the survivor tail by move_last.

Cross-contracting the last slot of the product E ⊗ B (with B rank one) against the unit tensor for that slot's color returns E ⊗ B unchanged, the contracted slot carried to the end. The rank-one spectator case that seeds crossToEnd_unitTensor_slot.