Physlib

Physlib.Relativity.Tensors.ComponentIdx.Contraction

Contractions of component indices

i. Overview

This file contains the component-index API induced by dropping a pair of contracted indices from a tensor.

The constructions here describe how component indices restrict along `Fin.succSuccAbove`, and how the fiber of this restriction is equivalent to the two component choices at the contracted positions.

ii. Key results

- `TensorSpecies.Tensor.ComponentIdx.dropPair` restricts a component index by dropping two positions. - `TensorSpecies.Tensor.ComponentIdx.DropPairSection` is the finite set of component indices mapping to a fixed restricted component index. - `TensorSpecies.Tensor.ComponentIdx.DropPairSection.ofFinEquiv` identifies a `DropPairSection` with the two basis indices at the dropped positions.

iii. Table of contents

  • A. Dropping a pair
  • B. Sections of the drop-pair map

iv. References

There are no known references for the material in this module.

A. Dropping a pair

B. Sections of the drop-pair map

2 declarations

theorem

b′∈DropPairSection(b)  ⟺  ∀m,b′(succSuccAbovei,j(m))=b(m)b' \in \text{DropPairSection}(b) \iff \forall m, b'(\text{succSuccAbove}_{i,j}(m)) = b(m)

For any natural number nn, index structure c:Fin(n+2)→Cc: \text{Fin}(n+2) \to C, and pair of indices i,j∈Fin(n+2)i, j \in \text{Fin}(n+2), let b∈ComponentIdx(c∘succSuccAbovei,j)b \in \text{ComponentIdx}(c \circ \text{succSuccAbove}_{i,j}) be a multi-index of a tensor with two positions removed, and let b′∈ComponentIdx(c)b' \in \text{ComponentIdx}(c) be a multi-index of the original tensor. Then b′b' is an element of the set DropPairSection(b)\text{DropPairSection}(b) if and only if for every m∈Fin(n)m \in \text{Fin}(n), the component of b′b' at the position succSuccAbovei,j(m)\text{succSuccAbove}_{i,j}(m) is equal to the component b(m)b(m).

theorem

ofFini,j(b,x)∈DropPairSection(b)\text{ofFin}_{i,j}(b, x) \in \text{DropPairSection}(b)

Let n∈Nn \in \mathbb{N} and c:Fin(n+2)→Cc : \text{Fin}(n+2) \to C be an index structure for a tensor of rank n+2n+2. Let i,j∈Fin(n+2)i, j \in \text{Fin}(n+2) be distinct indices (i≠ji \neq j). Given a reduced multi-index bb for the structure c∘succSuccAbovei,jc \circ \text{succSuccAbove}_{i,j} and a pair of coordinate values x=(x1,x2)x = (x_1, x_2) for the positions ii and jj (where x1∈basisIdx(ci)x_1 \in \text{basisIdx}(c_i) and x2∈basisIdx(cj)x_2 \in \text{basisIdx}(c_j)), the multi-index constructed by inserting xx into bb, denoted as ofFini,j(b,x)\text{ofFin}_{i,j}(b, x), is an element of the fiber DropPairSection(b)\text{DropPairSection}(b).