Physlib.Relativity.Tensors.ComplexTensor.Weyl.Modules

The definition establishes a bijective equivalence between the structure `LeftHandedModule`, which represents left-handed Weyl fermions, and the complex vector space $\mathbb{C}^2$ (represented as the space of functions $\text{Fin } 2 \to \mathbb{C}$). This equivalence allows for the conversion between the wrapped fermion type and its underlying coordinate representation.

The type `LeftHandedModule`, which represents the space of left-handed Weyl fermions, is endowed with the structure of an additive commutative monoid. This structure defines a zero element $0$ and an addition operation $+$ that is both associative and commutative. The structure is inherited from the complex vector space $\mathbb{C}^2$ via the bijective equivalence $\text{LeftHandedModule} \simeq \mathbb{C}^2$.

The type `LeftHandedModule`, representing the space of left-handed Weyl fermions, is equipped with the structure of an additive commutative group (abelian group). This structure, which defines addition, a zero element $0$, and additive inverses, is inherited from the complex vector space $\mathbb{C}^2$ (represented as $\text{Fin } 2 \to \mathbb{C}$) via the bijective equivalence $\text{LeftHandedModule} \simeq \mathbb{C}^2$.

The type `LeftHandedModule`, which represents the space of left-handed Weyl fermions, is equipped with the structure of a module over the complex numbers $\mathbb{C}$. This $\mathbb{C}$-module structure (or complex vector space structure) is inherited from the standard module structure on $\mathbb{C}^2$ (represented as the space of functions $\text{Fin } 2 \to \mathbb{C}$) via the bijective equivalence $\text{LeftHandedModule} \simeq \mathbb{C}^2$.

This definition establishes a linear equivalence (an isomorphism of complex vector spaces) between the space of left-handed Weyl fermions, `LeftHandedModule`, and the standard two-dimensional complex vector space $\mathbb{C}^2$, represented as the type of functions $\text{Fin } 2 \to \mathbb{C}$. This map identifies the wrapped fermion structure with its underlying coordinate representation while preserving the addition and complex scalar multiplication operations.

For a left-handed Weyl fermion $\psi$ in the module $\text{LeftHandedModule}$, this function returns its underlying representation as a vector in $\mathbb{C}^2$ (the space of functions $\text{Fin } 2 \to \mathbb{C}$). This is achieved by applying the linear isomorphism $\text{LeftHandedModule} \cong \mathbb{C}^2$ to $\psi$.

This definition establishes an equivalence (a bijection) between the space of alternative left-handed Weyl fermions, denoted as `AltLeftHandedModule`, and the standard two-dimensional complex vector space $\mathbb{C}^2$ (represented as the type of functions $\text{Fin } 2 \to \mathbb{C}$). The mapping relates the internal structure of the fermion module to its coordinate representation in $\mathbb{C}^2$.

This definition provides the structure of an additive commutative monoid for the space of alternative left-handed Weyl fermions, denoted as $\text{AltLeftHandedModule}$. The addition operation and the zero element are induced by transporting the standard additive structure of the complex vector space $\mathbb{C}^2$ (represented as functions $\text{Fin } 2 \to \mathbb{C}$) through the established equivalence between $\text{AltLeftHandedModule}$ and $\mathbb{C}^2$.

This definition establishes an additive commutative group structure on the space of alternative left-handed Weyl fermions, denoted as $\text{AltLeftHandedModule}$. The group operations—including addition, negation, and the zero element—are induced by transporting the standard additive structure of the complex vector space $\mathbb{C}^2$ (represented as functions $\text{Fin } 2 \to \mathbb{C}$) through the equivalence $\text{AltLeftHandedModule} \simeq \mathbb{C}^2$.

This definition equips the space of alternative left-handed Weyl fermions, denoted as $\text{AltLeftHandedModule}$, with a module structure over the complex numbers $\mathbb{C}$. The scalar multiplication is induced by transporting the standard $\mathbb{C}$-module structure from the vector space $\mathbb{C}^2$ (represented as the type of functions $\text{Fin } 2 \to \mathbb{C}$) through the equivalence $\text{AltLeftHandedModule} \simeq \mathbb{C}^2$.

This definition establishes a $\mathbb{C}$-linear equivalence (isomorphism of complex vector spaces) between the space of alternative left-handed Weyl fermions, denoted as $\text{AltLeftHandedModule}$, and the standard two-dimensional complex vector space $\mathbb{C}^2$ (represented as the type of functions $\text{Fin } 2 \to \mathbb{C}$). This equivalence ensures that the vector space operations (addition and scalar multiplication) in $\text{AltLeftHandedModule}$ correspond directly to those in $\mathbb{C}^2$.

This function maps an element $\psi$ of the alternative left-handed Weyl fermion module, $\text{AltLeftHandedModule}$, to its corresponding vector in the standard complex vector space $\mathbb{C}^2$ (represented as functions $\text{Fin } 2 \to \mathbb{C}$). This is defined by applying the $\mathbb{C}$-linear equivalence between the module and $\mathbb{C}^2$.

The canonical equivalence (bijection) between the space of right-handed Weyl fermions, `RightHandedModule`, and the standard vector space $\mathbb{C}^2$ (represented as the type of functions $\text{Fin } 2 \to \mathbb{C}$). This map identifies a right-handed fermion with its underlying pair of complex coordinates.

The space of right-handed Weyl fermions, `RightHandedModule`, is endowed with the structure of an additive commutative monoid. This structure is inherited from the standard additive commutative monoid structure on $\mathbb{C}^2$ (represented as the type of functions $\text{Fin } 2 \to \mathbb{C}$) via the canonical equivalence between `RightHandedModule` and $\mathbb{C}^2$.

The space of right-handed Weyl fermions, `RightHandedModule`, is endowed with the structure of an additive abelian group. This group structure is inherited from the standard additive abelian group structure on $\mathbb{C}^2$ (represented as the type of functions $\text{Fin } 2 \to \mathbb{C}$) via the canonical equivalence between `RightHandedModule` and $\mathbb{C}^2$.

The space of right-handed Weyl fermions, `RightHandedModule`, is endowed with the structure of a module over the complex numbers $\mathbb{C}$ (a complex vector space). This structure is inherited from the standard $\mathbb{C}$-module structure on $\mathbb{C}^2$ (represented as the type of functions $\text{Fin } 2 \to \mathbb{C}$) via the canonical equivalence between `RightHandedModule` and $\mathbb{C}^2$.

This definition establishes a linear equivalence (an isomorphism of complex vector spaces) between the space of right-handed Weyl fermions, `RightHandedModule`, and the standard coordinate space $\mathbb{C}^2$ (represented as the type of functions $\text{Fin } 2 \to \mathbb{C}$). It identifies a right-handed fermion with its underlying pair of complex coordinates while preserving both the addition and complex scalar multiplication operations.

This function maps a right-handed Weyl fermion $\psi \in \text{RightHandedModule}$ to its underlying representation as a vector in $\mathbb{C}^2$ (modeled as functions $\text{Fin } 2 \to \mathbb{C}$). The mapping is defined by applying the linear equivalence between the space of right-handed Weyl fermions and the standard coordinate space $\mathbb{C}^2$.

This definition provides a bijection (equivalence) between the module of alternative right-handed Weyl fermions, $\text{AltRightHandedModule}$, and the vector space $\mathbb{C}^2$ (represented as the type of functions $\text{Fin } 2 \to \mathbb{C}$). It maps a fermion $v$ to its underlying vector in $\mathbb{C}^2$ and vice versa.

The space of alternative right-handed Weyl fermions, denoted as $\text{AltRightHandedModule}$, is equipped with the structure of an additive commutative monoid. This structure is induced by transporting the standard addition and the zero element from the vector space $\mathbb{C}^2$ (modeled as functions $\text{Fin } 2 \to \mathbb{C}$) via the equivalence $\text{AltRightHandedModule} \simeq \mathbb{C}^2$.

The space of alternative right-handed Weyl fermions, denoted as $\text{AltRightHandedModule}$, is equipped with the structure of an additive abelian group. This group structure is induced by transporting the standard addition and negation operations from the vector space $\mathbb{C}^2$ (modeled as the type of functions $\text{Fin } 2 \to \mathbb{C}$) via the equivalence $\text{AltRightHandedModule} \simeq \mathbb{C}^2$.

The space of alternative right-handed Weyl fermions, denoted as $\text{AltRightHandedModule}$, is equipped with the structure of a module (vector space) over the complex numbers $\mathbb{C}$. This structure is induced by transporting the scalar multiplication from the standard vector space $\mathbb{C}^2$ (represented as functions $\text{Fin } 2 \to \mathbb{C}$) to $\text{AltRightHandedModule}$ via the equivalence $\text{AltRightHandedModule} \simeq \mathbb{C}^2$.

This definition establishes a $\mathbb{C}$-linear equivalence (an isomorphism of complex modules) between the space of alternative right-handed Weyl fermions, denoted as $\text{AltRightHandedModule}$, and the standard complex vector space $\mathbb{C}^2$ (represented by the type of functions $\text{Fin } 2 \to \mathbb{C}$). This equivalence identifies elements of the fermion module with their underlying two-component complex vectors while preserving the operations of addition and scalar multiplication.

Given an element $\psi$ of the module $\text{AltRightHandedModule}$ (the space of alternative right-handed Weyl fermions), this function returns its underlying representation as a two-component complex vector in $\mathbb{C}^2$ (modeled as $\text{Fin } 2 \to \mathbb{C}$) by applying the linear equivalence $\text{AltRightHandedModule} \cong \mathbb{C}^2$.