Physlib.Relativity.Fermions.Weyl.DualLeftHanded

The equivalence (isomorphism) between the type representing dual left-handed Weyl fermions and the complex vector space $\mathbb{C}^2$, which is modeled as the space of functions $\text{Fin } 2 \to \mathbb{C}$.

The space of dual left-handed Weyl spinors, $\text{Fermion.DualLeftHandedWeyl}$, is equipped with an additive commutative monoid structure, providing a zero element and a commutative addition operation.

The type `Fermion.DualLeftHandedWeyl`, which represents the dual space of left-handed Weyl fermions (modeled as $\mathbb{C}^2$), is equipped with the structure of an additive commutative group.

The type representing dual left-handed Weyl fermions is a module (vector space) over the complex numbers $\mathbb{C}$.

This definition establishes a $\mathbb{C}$-linear equivalence between the module of dual left-handed Weyl fermions, denoted as `DualLeftHandedWeyl`, and the complex vector space $\mathbb{C}^2$ (represented as the type of functions from a two-element set to $\mathbb{C}$).

This function maps a dual left-handed Weyl fermion, represented by the structure `Fermion.DualLeftHandedWeyl`, to its underlying representation in the complex vector space $\mathbb{C}^2$ (modeled as the type `Fin 2 → ℂ`).

For any dual left-handed Weyl fermion $\psi$, its representation as a vector in $\mathbb{C}^2$ (denoted as $\psi.\text{toFin2ℂ}$) is equal to its underlying value $\psi.\text{val}$. Here, $\mathbb{C}^2$ is represented by the type of functions from a two-element set to the complex numbers, i.e., $\text{Fin } 2 \to \mathbb{C}$.

This definition provides a basis for the space of dual left-handed Weyl spinors $\text{DualLeftHandedWeyl}$, which is a 2-dimensional vector space over the complex numbers $\mathbb{C}$, indexed by the set $\{0, 1\}$.

Let $(e_i)_{i \in \{0, 1\}}$ be the standard basis for the vector space of dual left-handed Weyl spinors. For any indices $i, j \in \{0, 1\}$, the $j$-th component of the $i$-th basis vector $e_i$ is equal to $1$ if $i = j$ and $0$ otherwise (i.e., $(e_i)_j = \delta_{ij}$).

For the dual left-handed Weyl fermion vector space, the $i$-th element of its basis, where $i \in \{0, 1\}$, is equal to the standard basis vector $\delta_{ij}$ (represented by a function that returns $1$ when the index matches $i$ and $0$ otherwise).

This definition characterizes the group representation of the special linear group $SL(2, \mathbb{C})$ (the group of $2 \times 2$ complex matrices with determinant 1) on the complex vector space of dual left-handed Weyl spinors.

For any matrix $M$ in the special linear group $SL(2, \mathbb{C})$ and any dual left-handed Weyl spinor $\psi$, the action of the representation of $M$ on $\psi$ is given by: $$\text{rep}(M)\psi = \sum_{i} \left( \sum_{j} (M^{-1})_{ji} \psi_j \right) \mathbf{e}_i$$ where $\mathbf{e}_i$ are the basis vectors of the dual left-handed Weyl spinor space, $\psi_j$ are the components of $\psi$ in that basis, and $(M^{-1})_{ji}$ denotes the entry in the $j$-th row and $i$-th column of the inverse matrix of $M$.

For any matrix $M$ in the special linear group $SL(2, \mathbb{C})$ and any index $i \in \{0, 1\}$, the representation of $M$ acting on the $i$-th basis vector $e_i$ of the dual left-handed Weyl spinor space is given by the sum $$\rho(M) e_i = \sum_{j} (M^{-1})_{ij} e_j$$ where $(M^{-1})_{ij}$ denotes the $(i, j)$-th entry of the inverse matrix of $M$.

Let $SL(2, \mathbb{C})$ be the group of $2 \times 2$ complex matrices with determinant $1$. For any $M \in SL(2, \mathbb{C})$, the matrix representation of the group action (representation) of $M$ on the space of dual left-handed Weyl fermions, with respect to the standard basis, is given by the transpose of the inverse of $M$, denoted $(M^{-1})^T$.

For any matrix $M$ in the special linear group $SL(2, \mathbb{C})$ and any indices $i, j \in \{1, 2\}$, the $j$-th component of the representation of $M$ acting on the $i$-th basis vector of the dual left-handed Weyl spinor space is equal to the $(i, j)$-th entry of the inverse matrix $M^{-1}$.