Physlib.Relativity.Fermions.Weyl.LeftHanded

This is an equivalence (isomorphism) between the space of left-handed Weyl fermions and the complex vector space $\mathbb{C}^2$.

The space of left-handed Weyl fermions, denoted by the type $\text{Fermion.LeftHandedWeyl}$ which wraps the vector space $\mathbb{C}^2$, is equipped with the structure of an additive commutative monoid. This means that left-handed Weyl fermions can be added together, the addition is associative and commutative, and there exists a zero fermion acting as the additive identity.

The space of left-handed Weyl fermions, represented by the type `Fermion.LeftHandedWeyl` (which wraps the vector space $\mathbb{C}^2$), is endowed with the structure of an additive commutative group. This allows for the addition of left-handed Weyl fermions, the existence of a zero fermion, and the definition of additive inverses.

The type `Fermion.LeftHandedWeyl`, which represents the space of left-handed Weyl fermions (mathematically modeled as $\mathbb{C}^2$), is equipped with a module structure over the complex numbers $\mathbb{C}$. This defines the scalar multiplication and addition required for it to behave as a complex vector space.

The $\mathbb{C}$-linear equivalence (vector space isomorphism) between the space of left-handed Weyl fermions and the complex vector space $\mathbb{C}^2$.

The function maps a left-handed Weyl fermion to its representation as a vector in $\mathbb{C}^2$. Here, the type of left-handed Weyl fermions is a structure that wraps the space of complex two-component spinors to distinguish them from other types of fermions.

For any left-handed Weyl fermion $\psi$, its representation as a 2-component complex vector in $\mathbb{C}^2$, denoted by $\psi.\text{toFin2}\mathbb{C}$, is equal to its internal value $\psi.\text{val}$.

A basis for the space of left-handed Weyl fermions, which is a 2-dimensional vector space over the complex numbers $\mathbb{C}$. The basis is indexed by the set $\{0, 1\}$.

For any indices $i, j \in \{0, 1\}$, the $j$-th component of the $i$-th basis vector of the space of left-handed Weyl spinors is equal to the Kronecker delta $\delta_{ij}$, which is $1$ if $j = i$ and $0$ otherwise.

For each index $i \in \{0, 1\}$, the $i$-th basis vector of the space of left-handed Weyl spinors is the standard basis vector $e_i$, which takes the value $1$ at index $i$ and $0$ at the other index.

This definition provides the complex linear representation of the special linear group $\text{SL}(2, \mathbb{C})$ on the vector space of left-handed Weyl spinors.

Let $SL(2, \mathbb{C})$ be the special linear group of $2 \times 2$ complex matrices. For any matrix $M \in SL(2, \mathbb{C})$ and any left-handed Weyl spinor $\psi$, the representation of $M$ acting on $\psi$ is given by the matrix-vector multiplication $M \psi$.

For any matrix $M$ in the special linear group $SL(2, \mathbb{C})$ and any left-handed Weyl spinor $\psi$, the action of the representation of $M$ on $\psi$ is given by the linear combination $$\rho(M) \psi = \sum_{i} \left( \sum_{j} M_{ij} \psi_j \right) \mathbf{e}_i$$ where $M_{ij}$ are the entries of the matrix $M$, $\psi_j$ are the components of the spinor $\psi$, and $\mathbf{e}_i$ are the basis vectors of the space of left-handed Weyl spinors.

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 $\mathbf{e}_i$ of the space of left-handed Weyl spinors is given by $$\rho(M) \mathbf{e}_i = \sum_{j=0}^1 M_{ji} \mathbf{e}_j$$ where $M_{ji}$ denotes the entry of the matrix $M$ at row $j$ and column $i$.

Let $SL(2, \mathbb{C})$ be the special linear group of $2 \times 2$ complex matrices. For any $M \in SL(2, \mathbb{C})$, the matrix representing the action of $M$ on the space of left-handed Weyl fermions, with respect to the standard basis, is equal to $M$ itself.

For any matrix $M \in SL(2, \mathbb{C})$ and indices $i, j \in \{1, 2\}$, let $e_i$ be the $i$-th basis vector of the left-handed Weyl spinor space. The $j$-th coordinate of the vector obtained by applying the representation of $M$ to $e_i$ is equal to the matrix entry $M_{ji}$.