PhyslibSearch

Physlib.Relativity.Tensors.Contraction.Basis

14 declarations

definition

Dropping indices ii and jj from a multi-index bb

#dropPair

Given a multi-index bComponentIdx(c)b \in \text{ComponentIdx}(c) for a tensor with n+2n+2 indices (where c:{0,,n+1}Cc: \{0, \dots, n+1\} \to C defines the index structure), and two specific index positions i,j{0,,n+1}i, j \in \{0, \dots, n+1\}, the function `dropPair` constructs a reduced multi-index of length nn. This resulting multi-index belongs to the index structure cdropPairEmbi,jc \circ \text{dropPairEmb}_{i,j}, which corresponds to the original structure with the ii-th and jj-th entries removed. For each m{0,,n1}m \in \{0, \dots, n-1\}, the value of the new multi-index is b(dropPairEmbi,j(m))b(\text{dropPairEmb}_{i,j}(m)), effectively extracting the components of bb at all positions except for ii and jj.

definition

Fiber of the multi-index projection dropPairi,j\text{dropPair}_{i,j}

#DropPairSection

Given a multi-index bComponentIdx(cdropPairEmbi,j)b \in \text{ComponentIdx}(c \circ \text{dropPairEmb}_{i,j}) for a tensor with nn indices (where the index structure cc has had two positions i,j{0,,n+1}i, j \in \{0, \dots, n+1\} removed), the function `DropPairSection` defines the finite set of all multi-indices bComponentIdx(c)b' \in \text{ComponentIdx}(c) that map to bb under the `dropPair` operation. Mathematically, it is the fiber of the projection map: \[ \text{DropPairSection}(b) = \{ b' \in \text{ComponentIdx}(c) \mid \text{dropPair}_{i,j}(b') = b \}. \] This set consists of all multi-indices of length n+2n+2 that match bb at all positions other than ii and jj.

theorem

bDropPairSection(b)b' \in \text{DropPairSection}(b) iff bb' and bb match at all non-dropped indices

#mem_iff_apply_dropPairEmb_eq

Let nn be a natural number and c:{0,,n+1}Cc: \{0, \dots, n+1\} \to C define the index structure of a tensor with n+2n+2 indices. For any two index positions i,j{0,,n+1}i, j \in \{0, \dots, n+1\}, let bb' be a multi-index for the structure cc, and bb be a reduced multi-index for the structure cdropPairEmbi,jc \circ \text{dropPairEmb}_{i,j} (where positions ii and jj are skipped). Then bb' belongs to the fiber DropPairSection(b)\text{DropPairSection}(b) if and only if for all m{0,,n1}m \in \{0, \dots, n-1\}, the component of bb' at the position dropPairEmbi,j(m)\text{dropPairEmb}_{i,j}(m) is equal to the component of bb at position mm. \[ b' \in \text{DropPairSection}(b) \iff \forall m \in \{0, \dots, n-1\}, b'(\text{dropPairEmb}_{i,j}(m)) = b(m) \]

theorem

bDropPairSection(dropPairi,j(b))b \in \text{DropPairSection}(\text{dropPair}_{i,j}(b))

#mem_self_of_dropPair

Let nn be a natural number and c:{0,,n+1}Cc: \{0, \dots, n+1\} \to C define the index structure of a tensor with n+2n+2 indices. For any multi-index bComponentIdx(c)b \in \text{ComponentIdx}(c) and any two index positions i,j{0,,n+1}i, j \in \{0, \dots, n+1\}, let dropPairi,j(b)\text{dropPair}_{i,j}(b) denote the reduced multi-index of length nn obtained by skipping the components at positions ii and jj. Then bb belongs to the fiber DropPairSection(dropPairi,j(b))\text{DropPairSection}(\text{dropPair}_{i,j}(b)), which consists of all multi-indices bb' that satisfy dropPairi,j(b)=dropPairi,j(b)\text{dropPair}_{i,j}(b') = \text{dropPair}_{i,j}(b).

definition

Multi-index construction by inserting values at ii and jj

#ofFin

Given a sequence of index types c:{0,,n+1}Cc : \{0, \dots, n+1\} \to C and two distinct indices i,j{0,,n+1}i, j \in \{0, \dots, n+1\}, let bb be a multi-index (of type `ComponentIdx`) corresponding to the indices of cc after positions ii and jj have been removed (via `dropPairEmb`). Given a pair x=(x1,x2)x = (x_1, x_2) representing the specific coordinate values for the ii-th and jj-th indices, where x1{0,,di1}x_1 \in \{0, \dots, d_i - 1\} and x2{0,,dj1}x_2 \in \{0, \dots, d_j - 1\}, this function constructs a full multi-index BComponentIdx(c)B \in \text{ComponentIdx}(c). The components of the resulting multi-index are defined as: \[ B_m = \begin{cases} x_1 & \text{if } m = i \\ x_2 & \text{if } m = j \\ b_{f(i, j, m)} & \text{otherwise} \end{cases} \] where f(i,j,m)f(i, j, m) is the preimage of mm under the embedding that skips ii and jj, effectively mapping the mm-th position in the full sequence to its corresponding position in the reduced sequence bb.

theorem

The ii-th component of the multi-index constructed by `ofFin` equals x1x_1

#ofFin_apply_fst

Let nn be a natural number and let c:{0,,n+1}Cc: \{0, \dots, n+1\} \to C define a sequence of index types for a tensor. For any two distinct indices i,j{0,,n+1}i, j \in \{0, \dots, n+1\}, let bb be a multi-index of type `ComponentIdx` corresponding to the structure cc after indices ii and jj have been removed. Given a pair of coordinate values x=(x1,x2)x = (x_1, x_2) where x1{0,,di1}x_1 \in \{0, \dots, d_i-1\} and x2{0,,dj1}x_2 \in \{0, \dots, d_j-1\} (with dkd_k being the dimension of the kk-th representation space), the function `ofFin` constructs a full multi-index BComponentIdx(c)B \in \text{ComponentIdx}(c) by inserting x1x_1 at position ii, x2x_2 at position jj, and the elements of bb at the remaining positions. This theorem states that the ii-th component of the resulting multi-index BB is equal to x1x_1.

theorem

The jj-th component of the multi-index constructed by `ofFin` equals x2x_2

#ofFin_apply_snd

Let nn be a natural number and let c:{0,,n+1}Cc: \{0, \dots, n+1\} \to C define a sequence of index types for a tensor. For any two distinct indices i,j{0,,n+1}i, j \in \{0, \dots, n+1\}, let bb be a multi-index of type `ComponentIdx` corresponding to the structure cc after indices ii and jj have been removed. Given a pair of coordinate values x=(x1,x2)x = (x_1, x_2) where x1{0,,di1}x_1 \in \{0, \dots, d_i-1\} and x2{0,,dj1}x_2 \in \{0, \dots, d_j-1\} (with dkd_k being the dimension of the kk-th representation space), the function `ofFin` constructs a full multi-index BComponentIdx(c)B \in \text{ComponentIdx}(c) by inserting x1x_1 at position ii, x2x_2 at position jj, and the elements of bb at the remaining positions. This theorem states that the jj-th component of the resulting multi-index BB is equal to x2x_2.

theorem

ofFin(b,x)DropPairSection(b)\text{ofFin}(b, x) \in \text{DropPairSection}(b)

#ofFin_mem_dropPairEmbSection

Let nNn \in \mathbb{N} and let c:{0,,n+1}Cc: \{0, \dots, n+1\} \to C define the index structure of a tensor. For any two distinct indices i,j{0,,n+1}i, j \in \{0, \dots, n+1\}, let bb be a reduced multi-index corresponding to the structure cc after indices ii and jj have been removed. Given a pair of coordinate values x=(x1,x2)x = (x_1, x_2) (where x1x_1 and x2x_2 are valid coordinates for the ii-th and jj-th index types, respectively), let B=ofFin(i,j,b,x)B = \text{ofFin}(i, j, b, x) be the full multi-index constructed by inserting x1x_1 at position ii, x2x_2 at position jj, and the components of bb at all other positions. This theorem states that BB is an element of DropPairSection(b)\text{DropPairSection}(b), which is the set of all multi-indices bb' such that dropping the ii-th and jj-th components of bb' results in bb.

definition

Equivalence between index pairs (xi,xj)(x_i, x_j) and DropPairSection(b)\text{DropPairSection}(b)

#ofFinEquiv

Let nNn \in \mathbb{N} and let c:{0,,n+1}Cc: \{0, \dots, n+1\} \to C define the index structure of a tensor. For any two distinct indices i,j{0,,n+1}i, j \in \{0, \dots, n+1\}, let bb be a reduced multi-index (an element of `ComponentIdx`) corresponding to the structure cc after the positions ii and jj have been removed. This definition provides an equivalence (bijection): \[ \{0, \dots, d_i - 1\} \times \{0, \dots, d_j - 1\} \simeq \text{DropPairSection}(b) \] where dk=S.repDim(ck)d_k = \text{S.repDim}(c_k) is the dimension of the representation space associated with the kk-th index, and DropPairSection(b)\text{DropPairSection}(b) is the set of all full multi-indices BComponentIdx(c)B \in \text{ComponentIdx}(c) that reduce to bb when the ii-th and jj-th components are removed. The bijection is defined such that a pair (x1,x2)(x_1, x_2) is mapped to the multi-index BB formed by inserting x1x_1 at position ii, x2x_2 at position jj, and the components of bb in the remaining nn positions. The inverse map extracts the values at positions ii and jj from a given multi-index in the section.

theorem

The ii-th component of the multi-index reconstructed by `ofFinEquiv` equals x1x_1

#ofFinEquiv_apply_fst

Let nNn \in \mathbb{N} and let c:{0,,n+1}Cc: \{0, \dots, n+1\} \to C define the sequence of index types for a tensor. For any two distinct indices i,j{0,,n+1}i, j \in \{0, \dots, n+1\}, let bb be a reduced multi-index corresponding to the structure cc after the positions ii and jj have been removed. Given a pair of index values x=(x1,x2)x = (x_1, x_2), where x1{0,,di1}x_1 \in \{0, \dots, d_i-1\} and x2{0,,dj1}x_2 \in \{0, \dots, d_j-1\} (with dkd_k being the dimension of the kk-th representation space), the equivalence `ofFinEquiv` constructs a full multi-index BB by inserting x1x_1 at position ii, x2x_2 at position jj, and the elements of bb at the remaining positions. This theorem states that the ii-th component of the resulting multi-index BB is equal to x1x_1.

theorem

The jj-th component of the multi-index reconstructed by `ofFinEquiv` is x2x_2

#ofFinEquiv_apply_snd

Let nNn \in \mathbb{N} and let c:{0,,n+1}Cc: \{0, \dots, n+1\} \to C define the index structure of a tensor. For any two distinct indices i,j{0,,n+1}i, j \in \{0, \dots, n+1\}, let bb be a reduced multi-index (an element of `ComponentIdx`) corresponding to the structure cc after the positions ii and jj have been removed. Given a pair of index values x=(x1,x2)x = (x_1, x_2) with x1{0,,di1}x_1 \in \{0, \dots, d_i - 1\} and x2{0,,dj1}x_2 \in \{0, \dots, d_j - 1\} (where dkd_k is the dimension of the kk-th representation space), the equivalence `ofFinEquiv` reconstructs a full multi-index BB by inserting x1x_1 at position ii, x2x_2 at position jj, and the components of bb in the remaining positions. This theorem states that the jj-th component of the resulting multi-index BB is equal to x2x_2.

theorem

dropPair\text{dropPair} of a basis vector ebe_b is the basis vector of the reduced multi-index bb

#dropPair_basisVector

Let SS be a tensor species and c:{0,,n+1}Cc: \{0, \dots, n+1\} \to C be a sequence of index types. Let b=(b0,,bn+1)b = (b_0, \dots, b_{n+1}) be a multi-index in ComponentIdx(c)\text{ComponentIdx}(c), and let eb=eb0(c0)ebn+1(cn+1)e_b = e_{b_0}^{(c_0)} \otimes \dots \otimes e_{b_{n+1}}^{(c_{n+1})} be the corresponding pure basis vector. For any two distinct indices i,j{0,,n+1}i, j \in \{0, \dots, n+1\}, let dropPairi,j(eb)\text{dropPair}_{i,j}(e_b) be the pure tensor obtained by removing the ii-th and jj-th components of ebe_b. Then dropPairi,j(eb)=ebϕ \text{dropPair}_{i,j}(e_b) = e_{b \circ \phi} where ϕ:{0,,n1}{0,,n+1}\phi: \{0, \dots, n-1\} \to \{0, \dots, n+1\} is the embedding (defined by `dropPairEmb`) that skips the indices ii and jj, and ebϕe_{b \circ \phi} is the basis vector in the reduced tensor product space associated with the multi-index restricted to the remaining nn positions.

theorem

Component Formula for Tensor Contraction contrTi,j(t)\text{contrT}_{i,j}(t)

#contrT_basis_repr_apply

Let SS be a tensor species over a field kk and c:{0,,n+1}Cc: \{0, \dots, n+1\} \to C be a sequence of index colors. Let tS.Tensor(c)t \in S.\text{Tensor}(c) be a tensor of rank n+2n+2. Suppose i,j{0,,n+1}i, j \in \{0, \dots, n+1\} are distinct indices such that the color at jj is the dual of the color at ii, i.e., c(j)=τ(c(i))c(j) = \tau(c(i)). Let contrTi,j(t)\text{contrT}_{i,j}(t) be the tensor of rank nn obtained by contracting tt at indices ii and jj. For any multi-index bb for the contracted tensor space, the bb-th component of the contracted tensor is given by: [contrTi,j(t)]b=bDropPairSection(b)tbcontr(ebi(ci)ebj(cj)) [\text{contrT}_{i,j}(t)]_b = \sum_{b' \in \text{DropPairSection}(b)} t_{b'} \cdot \text{contr}(e_{b'_i}^{(c_i)} \otimes e_{b'_j}^{(c_j)}) where: - tbt_{b'} is the component of the original tensor tt at the multi-index bb'. - DropPairSection(b)\text{DropPairSection}(b) is the set of all multi-indices bb' of length n+2n+2 that reduce to bb when the ii-th and jj-th indices are removed. - ebi(ci)e_{b'_i}^{(c_i)} and ebj(cj)e_{b'_j}^{(c_j)} are the basis vectors of the representation spaces corresponding to colors c(i)c(i) and c(j)c(j) at the specific indices specified by bb'. - contr\text{contr} is the natural pairing (contraction morphism) VVkV \otimes V^* \to k associated with the tensor species.

theorem

Summation Formula for the Components of Tensor Contraction contrTi,j(t)\text{contrT}_{i,j}(t)

#contrT_basis_repr_apply_eq_sum_fin

Let SS be a tensor species over a field kk and c:{0,,n+1}Cc: \{0, \dots, n+1\} \to C be a sequence of index colors. Let tS.Tensor(c)t \in S.\text{Tensor}(c) be a tensor of rank n+2n+2. Suppose i,j{0,,n+1}i, j \in \{0, \dots, n+1\} are distinct indices such that the color at jj is the dual of the color at ii, i.e., c(j)=τ(c(i))c(j) = \tau(c(i)). Let contrTi,j(t)\text{contrT}_{i,j}(t) be the tensor of rank nn obtained by contracting tt at indices ii and jj. For any multi-index bb of the contracted tensor space, the bb-th component of the contracted tensor is given by the double sum over the basis indices of the representation spaces at ii and jj: [contrTi,j(t)]b=x1=0di1x2=0dj1tB(b,x1,x2)contr(ex1(ci)ex2(cj)) [\text{contrT}_{i,j}(t)]_b = \sum_{x_1=0}^{d_i-1} \sum_{x_2=0}^{d_j-1} t_{B(b, x_1, x_2)} \cdot \text{contr}(e_{x_1}^{(c_i)} \otimes e_{x_2}^{(c_j)}) where: - did_i and djd_j are the dimensions of the representation spaces VciV_{c_i} and VcjV_{c_j} respectively. - B(b,x1,x2)B(b, x_1, x_2) is the multi-index of length n+2n+2 formed by inserting the index x1x_1 at position ii, the index x2x_2 at position jj, and the indices of bb at the remaining nn positions. - tB(b,x1,x2)t_{B(b, x_1, x_2)} is the component of the original tensor tt at multi-index BB. - ex1(ci)e_{x_1}^{(c_i)} and ex2(cj)e_{x_2}^{(c_j)} are the x1x_1-th and x2x_2-th basis vectors of the spaces VciV_{c_i} and VcjV_{c_j}. - contr:VciVcjk\text{contr}: V_{c_i} \otimes V_{c_j} \to k is the contraction morphism (pairing) defined for the tensor species.