Physlib.Relativity.PauliMatrices.ToTensor
Pauli matrices as a tensor
Tensorial structure
The tensorial structure on the type `Fin 1 ⊕ Fin 3 → Matrix (Fin 2) (Fin 2) ℂ` and properties thereof.
Pauli matrices as a tensor
Variations of the pauli tensor
Different forms
Group actions
28 declarations
Index equivalence for tensors of type
This definition provides an equivalence between the component indices of a tensor with the index configuration —consisting of one Lorentz vector index, one left-handed spinor index, and one right-handed spinor index—and the product type . Specifically, the 4-dimensional Lorentz index is decomposed into a temporal component () and three spatial components (), while the spinor indices remain in . This correspondence aligns the abstract tensor indices with the physical representation of Pauli matrices .
Tensorial isomorphism for the Pauli matrices
This definition establishes a tensorial structure for the Pauli matrices by providing a linear isomorphism between the abstract tensor space in the `complexLorentzTensor` species with indices of colors (representing a contravariant Lorentz vector index, a left-handed spinor index, and a right-handed spinor index) and the concrete space of matrix-valued functions . The isomorphism maps an abstract tensor to its components , identifying the 4-dimensional Lorentz index (decomposed into temporal and spatial parts) with the function's domain and the spinor indices with the matrix indices.
The component representation of a Pauli tensor is its curried basis representation via `indexEquiv`
Let be a tensor in the complex Lorentz tensor space , which has one contravariant Lorentz vector index and two spinor indices. The inverse of the tensorial isomorphism, , maps this abstract tensor to its concrete representation as a matrix-valued function . This theorem states that this function is obtained by: 1. Taking the coefficients of with respect to the canonical tensor basis. 2. Reindexing these components using the equivalence `indexEquiv`, which maps the abstract multi-indices to the physical product space . 3. Currying the resulting indices so that the Lorentz index selects a matrix indexed by the spinor components.
Components of the basis tensor for Pauli matrices are Kronecker deltas
Let be a multi-index belonging to the component index set for the color sequence , and let be the corresponding basis tensor in the complex Lorentz tensor space . This theorem states that the component representation of as a matrix-valued function , evaluated at Lorentz index and spinor indices , is 1 if the indices match the components of and 0 otherwise. Specifically: where the match for and is defined by the equivalence between the abstract four-dimensional index and the decomposed temporal/spatial index .
The Pauli tensor
The notation (denoted as `σ^^^`) represents the Pauli matrices, including the identity, as a tensor in the complex tensor space . This tensor is defined by applying the `toTensor` mapping to the standard Pauli matrices `pauliMatrix`, where corresponds to the Lorentz vector index (type `up`) and correspond to the spinor indices (types `upL` and `upR`).
Basis Expansion of the Pauli Tensor
Let be the Pauli tensor. Let denote the canonical basis elements of the tensor space indexed by the multi-index , where is the contravariant Lorentz index and are the left-handed and right-handed spinor indices, respectively. The Pauli tensor is expressed as the following linear combination of basis elements: where is the imaginary unit.
The Pauli Tensor Equals the Tensor Derived from the Invariant Morphism `asConsTensor`
Let be the Pauli tensor within the `complexLorentzTensor` species, associated with the sequence of index colors (representing a contravariant Lorentz vector index, a left-handed spinor index, and a right-handed spinor index, respectively). Let be the -invariant morphism of representations that defines the Pauli matrices. This theorem states that the Pauli tensor is equal to the rank-3 tensor constructed from this invariant morphism via the `fromConstTriple` mapping.
Equals its `ofRat` Component-wise Definition
The Pauli tensor is equal to the tensor constructed via the `ofRat` mapping from the following component function of the multi-index : - if and ; - if and ; - if and ; - if and ; - if and ; - if and ; - otherwise. Here, denotes the imaginary unit, and the components are represented as rational complex numbers .
for
For any element , the action of on the Pauli matrices leaves them invariant: Here, is the collection of Pauli matrices (for ), considered as a tensor with one contravariant Lorentz vector index and two spinor indices (one left-handed and one right-handed conjugate). The group action is defined via the tensorial isomorphism between the space of matrix-valued functions and the abstract Lorentz tensor space.
$\Lambda \cdot \sigma^{\text{^^^}} = \sigma^{\text{^^^}}$ for
For any transformation , the Pauli tensor $\sigma^{\text{^^^}}$ (representing the Pauli matrices with one contravariant Lorentz vector index and two spinor indices) is invariant under the group action, such that $\Lambda \cdot \sigma^{\text{^^^}} = \sigma^{\text{^^^}}$.
Covariant Pauli tensor
The definition `pauliCo` represents the covariant version of the Pauli tensor, denoted by . It is an element of the complex Lorentz tensor space with three indices: a covariant Lorentz vector index (color `.down`), a left-handed spinor index (color `.upL`), and a right-handed spinor index (color `.upR`). Mathematically, this tensor is defined by contracting the covariant Minkowski metric with the contravariant Pauli tensor : where the index is the internal index over which the contraction occurs, is the resulting covariant vector index, and are the spinor indices.
Notation for the Pauli tensor $\sigma_{\text{^^}}$
The notation `σ_^^` represents the Pauli matrix tensor , which is formally defined as `PauliMatrix.pauliCo`. This tensor maps spacetime indices to their corresponding complex Pauli matrices within a tensorial framework.
The dualized Lorentz Pauli tensor equals the tensor constructed from `pauliContrDownComponent` components
The complex Lorentz tensor , obtained by dualizing the contravariant Lorentz index of the Pauli tensor , is equal to the tensor constructed from the rational-complex components defined by the function `pauliContrDownComponent`. Specifically, the tensor with index colors is given by the image of `pauliContrDownComponent` under the `ofRat` map.
Rational components of the Pauli tensor
The complex Lorentz tensor obtained by dualizing the Lorentz index and the left-handed Weyl index of the contravariant Pauli tensor has components given by the formula: where represent the components of the Pauli tensor with a lowered Lorentz index, and is the two-dimensional Levi-Civita tensor (spinor metric) defined such that and .
Covariant Pauli tensor
The definition `pauliCoDown` represents the Pauli matrices as a complex Lorentz tensor with three covariant (lower) indices, denoted as . It is an element of the complex Lorentz tensor space with indices corresponding to: 1. A covariant Lorentz vector index (color `.down`), represented by . 2. A covariant right-handed (dotted) spinor index (color `.downR`), represented by . 3. A covariant left-handed (undotted) spinor index (color `.downL`), represented by . Mathematically, this tensor is constructed by lowering the indices of the contravariant Pauli tensor using the covariant Minkowski metric and the covariant spinor metrics and : where is the metric for Lorentz vectors and denotes the invariant metrics for the respective spinor representations.
Notation `σ___` for the Pauli tensor with three lower indices
The notation `σ___` represents the Pauli matrices as a tensor with three covariant (lower) indices, typically denoted in physics as . This notation is defined to refer to the formal term `PauliMatrix.pauliCoDown`.
Pauli tensor
The Pauli tensor is a complex Lorentz tensor of type defined over the species `complexLorentzTensor`. It possesses: - A contravariant Lorentz vector index (corresponding to the color `.up`). - A covariant right-handed (dotted) Weyl spinor index (corresponding to the color `.downR`). - A covariant left-handed (undotted) Weyl spinor index (corresponding to the color `.downL`). The tensor is constructed by taking the product of the contravariant Pauli matrices with the right-handed and left-handed spinor metrics ( and ) and performing the appropriate contractions to lower the spinor indices.
Notation for the Pauli tensor
The notation represents the Pauli tensor `PauliMatrix.pauliContrDown`, which is a complex tensor with one contravariant index (typically corresponding to Minkowski space) and two covariant indices (representing the spinor row and column indices). This notation provides a shorthand for the tensorial representation of the Pauli matrices .
Equals its Rational Component Representation
The covariant Pauli tensor is equal to the tensor constructed via the `ofRat` mapping from the component function of the multi-index defined as: - if and ; - if and ; - if and ; - if and ; - if and ; - if and ; - otherwise. Here, denotes the imaginary unit, and the components are represented as rational complex numbers where corresponds to the covariant Lorentz index (color `.down`), to the left-handed spinor index (color `.upL`), and to the right-handed spinor index (color `.upR`).
Equals its Rational Component Representation
The covariant Pauli tensor is equal to the tensor constructed via the `ofRat` mapping from the component function of the multi-index defined as: - if and ; - if and ; - if and ; - if and ; - if and ; - if and ; - otherwise. Here, denotes the imaginary unit, and the components are represented as rational complex numbers where corresponds to the covariant Lorentz index (color `.down`), to the covariant right-handed spinor index (color `.downR`), and to the covariant left-handed spinor index (color `.downL`).
Equals its `ofRat` Component-wise Definition
The Pauli tensor is equal to the tensor constructed via the `ofRat` mapping from the following component function of the multi-index , where is the Lorentz vector index, is the right-handed (dotted) spinor index, and is the left-handed (undotted) spinor index: - if and ; - if and ; - if and ; - if and ; - if and ; - if and ; - otherwise. Here, denotes the imaginary unit, and the components are represented as rational complex numbers via the `ofRat` map.
Invariance of the Covariant Pauli Tensor under
For any transformation , the covariant Pauli tensor (represented by `pauliCo`) is invariant under the group action, such that .
Invariance of the Covariant Pauli Tensor under
For any transformation , the covariant Pauli tensor (represented by `pauliCoDown`) is invariant under the group action, such that . Here, the tensor consists of a covariant Lorentz vector index , a covariant right-handed spinor index , and a covariant left-handed spinor index .
-Invariance of the Pauli Tensor
For any transformation in the group , the Pauli tensor (representing the Pauli matrices with one contravariant Lorentz vector index , one covariant dotted spinor index , and one covariant undotted spinor index ) is invariant under the group action, such that .
Dualizing Weyl indices of results in
Dualizing (lowering) both Weyl (spinor) indices of the contravariant Pauli tensor results in the Pauli tensor , which possesses one contravariant Lorentz vector index and two covariant spinor indices.
Dualizing all indices of equals
Dualizing all three indices of the contravariant Pauli tensor —the Lorentz vector index , the left-handed spinor index , and the right-handed spinor index —results in the covariant Pauli tensor . This dualization corresponds to lowering the indices using the Minkowski metric and the invariant spinor metrics and , such that: where the indices on the right-hand side follow the covariant ordering (Lorentz vector, right-handed spinor, left-handed spinor).
Lowering the Lorentz index of yields
Let be the contravariant Pauli tensor, where is a contravariant Lorentz vector index, is a left-handed spinor index, and is a right-handed spinor index. Let be the covariant Pauli tensor. The theorem states that applying the duality map to the Lorentz index of (which corresponds to lowering the index via the Minkowski metric ) results in the covariant Pauli tensor .
Lowering the contravariant Lorentz index of the Pauli tensor (where and are covariant spinor indices) results in the covariant Pauli tensor . This operation uses the metric transformation (associated with the Minkowski metric ) to map the index from the contravariant representation to the covariant representation, such that .
