Tensors

This module sets up the tensors used for index notation in Physlib.

Physics picture:

Choose a symmetry group G (for example, the Lorentz group).

Give each index kind a name called a color (encoded by a type C). In Lorentzian notation, a typical choice is two colors: up and down.

For each color, choose a representation of G.

Fix a basis for each color. This determines which values that index can take and lets us speak about tensor components explicitly.

Specify a dual color for each color, telling us which index pairs can contract.

For dual pairs, provide the contraction/unit/metric data used for contraction and for raising/lowering indices.

All of this structure is packaged as a TensorSpecies.

For S : TensorSpecies and a list of index colors c : Fin n → C:

Tensor S c is the type of tensors with those indices.

Pure S c is the type of pure tensors, i.e. tensors of the form v₀ ⊗ₜ v₁ ⊗ₜ v₂ ….

ComponentIdx S c is the type of allowed component labels for those indices.

This file realizes Tensor S c as a PiTensorProduct, relates pure tensors to their components, constructs the component basis, and supplies the inherited finite-dimensional and module-topology instances. It also defines the natural action of G on pure tensors and tensors, the associated permutation maps, and the map from rank-zero tensors to the base field.

From this setup we get the usual index-notation operations in a uniform way: contraction, raising/lowering, and permutation of indices.

The tensors associated with a list of indices of a given color c : Fin n → C.

Components of tensors

Pure tensors

The type of pure tensors associated to a list of indices c : OverColor C. A pure tensor is a tensor which can be written in the form v1 ⊗ₜ v2 ⊗ₜ v3 ….