Tensors and index notation

Stream: PhysLean

[Joseph Tooby-Smith]

I have been refactoring tensors and the theory around index notation to make it more friendly.

One important update is that in PR632 I have created the following instance:

class Tensorial
    {k : outParam Type} [CommRing k] {C G : outParam Type} [Group G]
    {n : outParam ℕ} (S : outParam (TensorSpecies k C G)) (c :outParam (Fin n → C)) (M : Type)
    [AddCommMonoid M] [Module k M] where
  /-- The equivalence between `M` and `S.Tensor c` in a tensorial instance. -/
  toTensor : M ≃ₗ[k] S.Tensor c

The main advantage of this is that index notation, contraction of indices etc. can be made to work on any module M carrying this instance. Previously it just worked on the modules S.Tensor c which are defined via abstract nonsense.

This has two noteworthy benefits

• The underlying definition of Lorentz.Vector and thereby SpaceTime is now Fin 1 ⊕ Fin d → ℝ rather than Tensor (realLorentzTensor) ![.up], which I hope will make it easier and more intuitive to work with. But one can still use index notation with it.
• The API around Pauli matrices has been cleaned up and now everything is defined from the actually Pauli matrices as elements of `Matrix (Fin 2) (Fin 2) ℂ, again making things hopefully more intuitive and easy to use.

Happy to hear if anyone has other suggestions to make this better (I'm more than happy to refactor things if it would improve things).