PhyslibSearch

Physlib.Relativity.Tensors.UnitTensor

9 declarations

definition

Unit Tensor

#unitTensor

The unit tensor associated with a color cCc \in C. It defines a tensor of shape (τ(c),c)(\tau(c), c) in a tensor species SS, where τ\tau denotes the duality map on the set of colors CC.

theorem

c=c1    unitTensor(c)=unitTensor(c1)c = c_1 \implies \text{unitTensor}(c) = \text{unitTensor}(c_1)

#unitTensor_congr

Let SS be a tensor species and CC be the set of colors. For any colors c,c1Cc, c_1 \in C, if c=c1c = c_1, then the unit tensor associated with cc is equal to the unit tensor associated with c1c_1 under the identity permutation of its indices. Formally, if c=c1c = c_1, then unitTensor(c)=permT(id,unitTensor(c1))\text{unitTensor}(c) = \text{permT}(\text{id}, \text{unitTensor}(c_1)), where permT\text{permT} denotes the permutation of tensor indices and id\text{id} is the identity permutation.

theorem

Unit Application Equals Dual Unit Application with Braiding

#unit_app_eq_dual_unit_app

For any cCc \in C, the application of the unit of SS at cc is equal to the application of the unit at S.τ(c)S.\tau(c) composed with the braiding and the isomorphism induced by S.τ(S.τ(c))=cS.\tau(S.\tau(c)) = c. Expressed as a formula: S.unitc=S.unitS.τ(c)βS.FD(S.τ2(c)),S.FD(S.τ(c))(S.FD(S.τ(c))S.FD(S.τ2(c)c)) S.\text{unit}_c = S.\text{unit}_{S.\tau(c)} \gg \beta_{S.FD(S.\tau^2(c)), S.FD(S.\tau(c))} \gg (S.FD(S.\tau(c)) \triangleleft S.FD(S.\tau^2(c) \to c)) where \gg denotes diagrammatic categorical composition, β\beta is the braiding, \triangleleft is the left whiskering, S.FDS.FD is the functor mapping colors to objects, and S.τS.\tau is the duality map on CC.

theorem

S.unitTensor(c)=permT[1,0](S.unitTensor(τ(c)))S.\text{unitTensor}(c) = \text{permT}_{[1, 0]}(S.\text{unitTensor}(\tau(c)))

#unitTensor_eq_permT_dual

For any color cCc \in C in a tensor species SS, the unit tensor associated with cc is equal to the permutation of indices (1,0)(1, 0) applied to the unit tensor associated with the dual color τ(c)\tau(c). Mathematically: S.unitTensor(c)=permT[1,0](S.unitTensor(τ(c))) S.\text{unitTensor}(c) = \text{permT}_{[1, 0]}(S.\text{unitTensor}(\tau(c))) where S.unitTensor(c)S.\text{unitTensor}(c) is a tensor of shape (τ(c),c)(\tau(c), c), τ\tau is the duality map on the set of colors CC, and permT[1,0]\text{permT}_{[1, 0]} denotes the operation that swaps the first and second indices of the tensor.

theorem

S.unitTensor(τ(c))=permT[1,0](S.unitTensor(c))S.\text{unitTensor}(\tau(c)) = \text{permT}_{[1, 0]}(S.\text{unitTensor}(c))

#dual_unitTensor_eq_permT_unitTensor

Let SS be a tensor species with a set of colors CC and a duality map τ:CC\tau: C \to C. For any color cCc \in C, the unit tensor associated with the dual color τ(c)\tau(c) is equal to the unit tensor associated with cc after swapping its first and second indices. Mathematically: S.unitTensor(τ(c))=permT[1,0](S.unitTensor(c)) S.\text{unitTensor}(\tau(c)) = \text{permT}_{[1, 0]}(S.\text{unitTensor}(c)) where S.unitTensor(c)S.\text{unitTensor}(c) is a tensor of shape (τ(c),c)(\tau(c), c) and permT[1,0]\text{permT}_{[1, 0]} denotes the permutation operation that swaps the two indices of the tensor.

theorem

Contraction with Unit Tensor Yields Single Tensor

#unit_fromSingleTContrFromPairT_eq_fromSingleT

For any cCc \in C and xS.FD(Discrete.mk(c))x \in S.FD(\text{Discrete.mk}(c)), the contraction of xx with the unit morphism of SS at cc evaluated at 1k1 \in k is equal to `fromSingleT x`. That is, fromSingleTContrFromPairT(x,(S.unit.app(Discrete.mk(c))).hom(1))=fromSingleT(x). \text{fromSingleTContrFromPairT}(x, (S.\text{unit.app}(\text{Discrete.mk}(c))).\text{hom}(1)) = \text{fromSingleT}(x).

theorem

Contraction with Unit Tensor equals the original Tensor

#contrT_single_unitTensor

Let SS be a tensor species with a set of colors CC and a duality map τ:CC\tau: C \to C. For any color cCc \in C and any rank-1 tensor xx of shape (c)(c), the contraction of the tensor product of xx and the unit tensor unitTensor(c)\text{unitTensor}(c) (which has shape (τ(c),c)(\tau(c), c)) over the index of xx and the first index of the unit tensor is equal to xx. That is, contrT1,0,1(xunitTensor(c))=x \text{contrT}_{1, 0, 1}(x \otimes \text{unitTensor}(c)) = x where the contraction is performed on the 00-th and 11-st indices of the product tensor.

theorem

Contraction of Unit Tensor with Dual Tensor equals the original Tensor

#contrT_unitTensor_dual_single

Let SS be a tensor species with a set of colors CC and a duality map τ:CC\tau: C \to C. For any color cCc \in C and any rank-1 tensor xx of shape (τ(c))(\tau(c)), the contraction of the tensor product of the unit tensor unitTensor(c)\text{unitTensor}(c) (which has shape (τ(c),c)(\tau(c), c)) and xx over the second index of the unit tensor and the index of xx is equal to xx. That is, contrT1,1,2(unitTensor(c)x)=x \text{contrT}_{1, 1, 2}(\text{unitTensor}(c) \otimes x) = x where the contraction is performed on the 11-st and 22-nd indices of the product tensor.

theorem

gS.unitTensor c=S.unitTensor cg \bullet S.\text{unitTensor } c = S.\text{unitTensor } c

#unitTensor_invariant

Let SS be a tensor species defined over a set of colors CC, and let GG be a group acting on the tensors of SS. For any color cCc \in C and any group element gGg \in G, the unit tensor S.unitTensor cS.\text{unitTensor } c (which is a tensor of shape (τ(c),c)(\tau(c), c)) is invariant under the action of gg, such that gS.unitTensor c=S.unitTensor cg \bullet S.\text{unitTensor } c = S.\text{unitTensor } c.