API: Tensor components

[jstoobysmith]

Details

Key data structure

The components of tensor, for example a 2-tensor $T^\mu_\nu$, the components would contain all specifications of the index.

• is defined as ComponentIdx

Need

This is used to manipulate tensors and extract their components. It is also used with basis of tensors.

What needs doing

• The data structure ComponentIdx and results related there to are currently spread throughout the Tensors directory. They should be moved into their own file system.

Requirements

• The API shall contain the combination of components based on taking the product of tensors.
• The API shall contain the restriction of components based on contraction of indices.

Corresponding file system

Currently these sit in the file system:

https://github.com/lean-phys-community/PhysLean/tree/master/PhysLean/Relativity/Tensors