Physlib.Mathematics.Groups.SpecialUnitary.LieAlgebra.Basic

Let $R$ be a commutative $*$-ring that is also a real $*$-algebra. `SULieAlgebra.submodule n R` is the $\mathbb{R}$-submodule of $n \times n$ matrices over $R$ consisting of matrices $A$ that are self-adjoint ($A^* = A$) and have zero trace ($\text{Tr}(A) = 0$). This is formally defined as the intersection of the submodule of self-adjoint matrices and the kernel of the trace linear map.

Let $n$ be a natural number and $R$ be a commutative $*$-ring that is also a real $*$-algebra. The type `SULieAlgebra n R` is defined as the space of $n \times n$ matrices $A$ with entries in $R$ that are self-adjoint ($A^* = A$) and have zero trace ($\text{Tr}(A) = 0$). In the case where $R = \mathbb{C}$, this corresponds to the Lie algebra $\mathfrak{su}(n)$ in the hermitian presentation.

Given an $n \times n$ matrix $A$ with entries in a commutative $*$-ring $R$, a proof $h_A$ that $A$ is self-adjoint ($A^* = A$), and a proof $h_T$ that its trace is zero ($\text{Tr}(A) = 0$), this function constructs the corresponding element in the Lie algebra $\mathfrak{su}(n)$ (represented by the type `SULieAlgebra n R`).

Let $R$ be a commutative $*$-ring that is also a real $*$-algebra. Given an $n \times n$ matrix $A$ over $R$ that is hermitian ($A^* = A$) and has zero trace ($\text{Tr}(A) = 0$), the underlying matrix of the element in the Lie algebra $\mathfrak{su}(n, R)$ constructed from $A$ using `ofMatrix` is equal to $A$.

Let $R$ be a commutative $*$-ring that is also a real $*$-algebra. For any element $x$ in the Lie algebra $\mathfrak{su}(n, R)$ (the space of traceless hermitian $n \times n$ matrices), its underlying matrix is self-adjoint (hermitian), satisfying $x^* = x$.

Let $R$ be a commutative $*$-ring that is also a real $*$-algebra. For any element $x$ in the Lie algebra of traceless hermitian $n \times n$ matrices $\mathfrak{su}(n, R)$, the trace of its underlying matrix is zero, i.e., $\text{Tr}(x) = 0$.

Let $R$ be a commutative $*$-ring that is also a real $*$-algebra. The term `SULieAlgebra.conj` defines the group representation of the unitary group $U(n, R)$ on the real Lie algebra $\mathfrak{su}(n, R)$ of traceless hermitian $n \times n$ matrices. For a unitary matrix $U \in U(n, R)$ and an element $x \in \mathfrak{su}(n, R)$, the action is given by the conjugation $x \mapsto U x U^*$, where $U^*$ denotes the adjoint (conjugate transpose) of the matrix $U$.

Let $R$ be a commutative $*$-ring that is also a real $*$-algebra. For any unitary matrix $U \in U(n, R)$ and any traceless hermitian matrix $x \in \mathfrak{su}(n, R)$, the conjugation representation action $\text{conj}(U, x)$ is given by the matrix product $U x U^*$, where $U^*$ denotes the adjoint (conjugate transpose) of $U$.

For any two elements $x$ and $y$ in the Lie algebra of traceless hermitian matrices $\mathfrak{su}(n)$ (represented by `SULieAlgebra n R`), the bracket operation $\lfloor x, y \rfloor$ is defined as $i$ times their commutator: $$\lfloor x, y \rfloor = i(xy - yx)$$ where $i$ is the imaginary unit. This definition ensures that the resulting matrix remains both hermitian and traceless.

For any elements $x$ and $y$ in the Lie algebra of traceless hermitian $n \times n$ matrices $\mathfrak{su}(n)$ (represented by `SULieAlgebra n R`), the underlying matrix of their Lie bracket $\lfloor x, y \rfloor$ is equal to $i(xy - yx)$, where $i$ is the imaginary unit and $xy - yx$ is the commutator of the matrices $x$ and $y$.

For a natural number $n$ and a commutative $*$-ring $R$ that is also a real $*$-algebra, the space of $n \times n$ traceless hermitian matrices `SULieAlgebra n R` forms a Lie ring. The Lie bracket is defined as $\lfloor x, y \rfloor = i(xy - yx)$, where $i$ is the imaginary unit. This structure ensures that the bracket operation satisfies the axioms of a Lie ring, including bilinearity, the alternating property $\lfloor x, x \rfloor = 0$, and the Jacobi identity.

For a natural number $n$ and a commutative $*$-ring $R$ that is a real $*$-algebra, the space of $n \times n$ traceless hermitian matrices $\mathfrak{su}(n, R)$ forms a Lie algebra over the real numbers $\mathbb{R}$. The Lie bracket is given by $\lfloor x, y \rfloor = i(xy - yx)$, where $i$ is the imaginary unit. This structure signifies that the Lie bracket is $\mathbb{R}$-bilinear.

Let $R$ be a commutative $*$-ring that is also a real $*$-algebra. For any natural number $n$, let $\mathfrak{su}(n, R)$ be the real Lie algebra of $n \times n$ traceless hermitian matrices over $R$, equipped with the Lie bracket $[x, y] = i(xy - yx)$, where $i$ is the imaginary unit. For any unitary matrix $U$ in the unitary group $U(n, R)$, the conjugation action $\text{conj}_U(x) = U x U^*$ (where $U^*$ denotes the adjoint or conjugate transpose) preserves the Lie bracket, meaning that for all $x, y \in \mathfrak{su}(n, R)$: $$\text{conj}_U([x, y]) = [\text{conj}_U(x), \text{conj}_U(y)]$$ This implies that the conjugation action by a unitary matrix defines a Lie algebra automorphism on $\mathfrak{su}(n, R)$.

For a natural number $n$, the complexification of the Lie algebra $\mathfrak{su}(n)$ is the complex Lie algebra defined by the tensor product $\mathbb{C} \otimes_{\mathbb{R}} \mathfrak{su}(n)$, where $\mathfrak{su}(n)$ is the real Lie algebra consisting of $n \times n$ complex matrices $A$ that are traceless ($\text{Tr}(A) = 0$) and hermitian ($A^* = A$).

The $\mathbb{C}$-linear map from the complexification of the Lie algebra $\mathfrak{su}(n)$ (denoted $\mathbb{C} \otimes_{\mathbb{R}} \mathfrak{su}(n)$) to the space of $n \times n$ complex matrices $M_n(\mathbb{C})$ that sends a tensor $z \otimes X$ to the matrix $zX$, where $z \in \mathbb{C}$ and $X$ is a traceless hermitian matrix.

Let $z \in \mathbb{C}$ and let $x \in \mathfrak{su}(n)$ be an $n \times n$ traceless hermitian matrix. The $\mathbb{C}$-linear map $\text{toMatrix}_{\mathbb{C}}$ from the complexification $\mathbb{C} \otimes_{\mathbb{R}} \mathfrak{su}(n)$ to the space of complex matrices $M_n(\mathbb{C})$ maps the elementary tensor $z \otimes x$ to the matrix $zx$.

For any element $A$ in the complexification of the Lie algebra $\mathfrak{su}(n)$ (denoted $\mathbb{C} \otimes_{\mathbb{R}} \mathfrak{su}(n)$), the trace of the corresponding $n \times n$ complex matrix $\text{toMatrixℂ}(A)$ is zero, i.e., $\text{Tr}(\text{toMatrixℂ}(A)) = 0$.

For any elements $A, B$ in the complexification of the Lie algebra $\mathfrak{su}(n)$ (denoted $\mathbb{C} \otimes_{\mathbb{R}} \mathfrak{su}(n)$), the $\mathbb{C}$-linear map $\text{toMatrix}_{\mathbb{C}}$ maps their Lie bracket $\lfloor A, B \rfloor$ to $i$ times the commutator of their corresponding matrices: $$\text{toMatrix}_{\mathbb{C}}(\lfloor A, B \rfloor) = i (\text{toMatrix}_{\mathbb{C}}(A) \text{toMatrix}_{\mathbb{C}}(B) - \text{toMatrix}_{\mathbb{C}}(B) \text{toMatrix}_{\mathbb{C}}(A))$$ where $i$ is the imaginary unit. This identity reflects the hermitian presentation of $\mathfrak{su}(n)$, where the bracket is $i$ times the standard commutator.

Given an $n \times n$ complex matrix $M$ and a proof $h_M$ that its trace is zero ($\text{Tr}(M) = 0$), this function constructs the corresponding element in the complexified Lie algebra $\mathbb{C} \otimes_{\mathbb{R}} \mathfrak{su}(n)$. The element is defined as $1 \otimes \text{Re}(M) + i \otimes \text{Im}(M)$, where $\text{Re}(M) = \frac{1}{2}(M + M^*)$ and $\text{Im}(M) = \frac{1}{2i}(M - M^*)$ are the traceless hermitian matrices that form the "real" and "imaginary" parts of $M$ in the hermitian presentation of $\mathfrak{su}(n)$.

Let $M$ be an $n \times n$ complex matrix with trace zero ($\text{Tr}(M) = 0$). Then the image of the element $\text{ofTracelessℂ}(M) \in \mathbb{C} \otimes_{\mathbb{R}} \mathfrak{su}(n)$ under the linear map $\text{toMatrixℂ}$ is equal to $M$. This identity reflects the decomposition $M = \text{Re}(M) + i \text{Im}(M)$ into its traceless hermitian parts.

For any $n \times n$ complex matrices $M$ and $N$ such that $\text{Tr}(M) = 0$ and $\text{Tr}(N) = 0$, the map $\text{ofTracelessℂ}$ (which constructs an element of the complexified Lie algebra $\mathbb{C} \otimes_{\mathbb{R}} \mathfrak{su}(n)$ from a traceless matrix) is additive. That is, $$\text{ofTracelessℂ}(M + N) = \text{ofTracelessℂ}(M) + \text{ofTracelessℂ}(N).$$

For any element $A$ in the complexification of the Lie algebra $\mathfrak{su}(n)$ (denoted $\mathbb{C} \otimes_{\mathbb{R}} \mathfrak{su}(n)$), applying the construction map $\text{ofTraceless}_{\mathbb{C}}$ to its matrix representation $\text{toMatrix}_{\mathbb{C}}(A)$ recovers the original element $A$. That is, $$\text{ofTraceless}_{\mathbb{C}}(\text{toMatrix}_{\mathbb{C}}(A)) = A.$$ Here, $\text{toMatrix}_{\mathbb{C}}$ is the $\mathbb{C}$-linear map that sends a tensor $z \otimes X$ to the matrix $zX$, and $\text{ofTraceless}_{\mathbb{C}}$ is the map that takes a traceless $n \times n$ matrix $M$ and returns the element $1 \otimes \text{Re}(M) + i \otimes \text{Im}(M)$ in the complexification.

Let $\mathfrak{su}(n)$ be the real Lie algebra of $n \times n$ traceless hermitian matrices. The $\mathbb{C}$-linear map $\text{toMatrix}_{\mathbb{C}} : \mathbb{C} \otimes_{\mathbb{R}} \mathfrak{su}(n) \to M_n(\mathbb{C})$, which sends the tensor $z \otimes X$ to the matrix $zX$ for $z \in \mathbb{C}$ and $X \in \mathfrak{su}(n)$, is injective. This implies that an element of the complexification is uniquely determined by its matrix.

Let $\mathfrak{su}(n)$ be the real Lie algebra of $n \times n$ traceless hermitian matrices and let $\mathbb{C} \otimes_{\mathbb{R}} \mathfrak{su}(n)$ be its complexification. Let $\Phi: \mathbb{C} \otimes_{\mathbb{R}} \mathfrak{su}(n) \to M_n(\mathbb{C})$ be the $\mathbb{C}$-linear map that sends a tensor $z \otimes X$ to the matrix $zX$, where $z \in \mathbb{C}$ and $X \in \mathfrak{su}(n)$. The range of $\Phi$ is equal to the kernel of the trace linear map $\text{Tr}: M_n(\mathbb{C}) \to \mathbb{C}$, which consists of all $n \times n$ complex matrices $A$ such that $\text{Tr}(A) = 0$.

Let $n$ be a natural number and let $M$ be an $n \times n$ complex matrix. If $M$ commutes with every matrix $x$ in the Lie algebra $\mathfrak{su}(n)$ (the space of $n \times n$ traceless hermitian matrices over $\mathbb{C}$), then $M$ commutes with every $n \times n$ complex matrix $N$.

For a natural number $n$, let $\mathfrak{su}(n)$ be the real Lie algebra of $n \times n$ complex matrices that are traceless ($\text{Tr}(M) = 0$) and hermitian ($M^* = M$). This definition provides a $\mathbb{C}$-linear equivalence between the complexification of this Lie algebra, $\mathbb{C} \otimes_{\mathbb{R}} \mathfrak{su}(n)$, and the subspace of $n \times n$ complex matrices $M \in M_n(\mathbb{C})$ with zero trace. The map sends an element of the complexification to its corresponding matrix representation.

For any element $A$ in the complexification of the Lie algebra $\mathfrak{su}(n)$ (denoted $\mathbb{C} \otimes_{\mathbb{R}} \mathfrak{su}(n)$), the underlying matrix of its image under the $\mathbb{C}$-linear equivalence $\text{equivTraceKer}$ is equal to its matrix representation $\text{toMatrix}_{\mathbb{C}}(A)$.

Let $n$ be a natural number and $M$ be an $n \times n$ complex matrix with zero trace ($\text{Tr}(M) = 0$). Let $\text{equivTraceKer}^{-1}$ be the inverse of the $\mathbb{C}$-linear equivalence between the complexification of the Lie algebra $\mathfrak{su}(n)$ (denoted $\mathbb{C} \otimes_{\mathbb{R}} \mathfrak{su}(n)$) and the subspace of traceless matrices. Let $\text{toMatrix}_{\mathbb{C}}$ be the linear map that sends an element of the complexification to its matrix representation in $M_n(\mathbb{C})$. Then, $\text{toMatrix}_{\mathbb{C}}(\text{equivTraceKer}^{-1}(M)) = M$.

Let $\mathfrak{su}(n)$ be the real Lie algebra of $n \times n$ complex matrices that are traceless and hermitian. The dimension of the complexification $\mathbb{C} \otimes_{\mathbb{R}} \mathfrak{su}(n)$ as a vector space over the complex numbers $\mathbb{C}$ is $n^2 - 1$.

Let $\mathfrak{su}(n)$ be the Lie algebra of $n \times n$ complex matrices that are traceless and hermitian (satisfying $A^* = A$ and $\operatorname{Tr}(A) = 0$). The dimension of $\mathfrak{su}(n)$ as a vector space over the real numbers $\mathbb{R}$ is $n^2 - 1$.