Physlib

Physlib.Relativity.SL2C.SelfAdjoint

Extra lemmas regarding `Lorentz.SL2C.toSelfAdjointMap`

This file redefines `Lorentz.SL2C.toSelfAdjointMap` by dropping the special linear condition for its first argument `M`. Then, `Lorentz.SL2C.toSelfAdjointMap_det_one` is proved for `M` being upper triangular.

Main definitions

- `Lorentz.SL2C.toSelfAdjointMap'`: definitionally equal to `Lorentz.SL2C.toSelfAdjointMap` but `M` is not required to be special linear. - `Lorentz.SL2C.toSelfAdjointMap_det_one'`: proves `Lorentz.SL2C.toSelfAdjointMap_det_one` with the additional requirement that `M` be upper triangular. The general case is reduced to this special case via `Matrix.schur_triangulation` in `Lorentz.SL2C.toSelfAdjointMap_det_one`.

Showing `Lorentz.SL2C.toSelfAdjointMap` has determinant 1

Since `Lorentz.ℍ₂` as a real vector space has the 4 Pauli matrices as basis, we know that its vector representation consists of 4 real components. This makes the matrix representation of `toSelfAdjointMap M` a 4-by-4 real matrix `F`. To make the computation of `F.det` manageable, the following basis is used instead of the Pauli matrices to induce as many zeros as possible in `F`: E0=[1000],E1=[0001],E2=σ1=[0110],E3=−σ2=[0i−i0], E_0 = \begin{bmatrix} 1 & 0 \\ 0 & 0 \end{bmatrix}, E_1 = \begin{bmatrix} 0 & 0 \\ 0 & 1 \end{bmatrix}, E_2 = \sigma_1 = \begin{bmatrix} 0 & 1 \\ 1 & 0 \end{bmatrix}, E_3 = -\sigma_2 = \begin{bmatrix} 0 & i \\ -i & 0 \end{bmatrix}, Suppose that M=[x□0y]M = \begin{bmatrix} x & □ \\ 0 & y \end{bmatrix} is upper triangular, the basis {Ek}k=03\{E_k\}_{k=0}^3 induces the matrix representation F=[∣x∣2□□□0∣y∣2000□Re⁡(xyˉ)−Im⁡(xyˉ)0□Im⁡(xyˉ)Re⁡(xyˉ)]. F = \begin{bmatrix} \lvert x\rvert^2 & □ & □ & □ \\ 0 & \lvert y\rvert^2 & 0 & 0 \\ 0 & □ & \operatorname{Re}(x\bar{y}) & -\operatorname{Im}(x\bar{y}) \\ 0 & □ & \operatorname{Im}(x\bar{y}) & \operatorname{Re}(x\bar{y}) \\ \end{bmatrix}. If xy=1xy = 1, the Schur complement formula `Matrix.det_fromBlocks₂₂` yields det⁡F=∣Re⁡(xyˉ)−Im⁡(xyˉ)Im⁡(xyˉ)Re⁡(xyˉ)∣det⁡([∣x∣2□0∣y∣2]−[□□00][□□□□][0□0□])=∣xyˉ∣2∣x∣2∣y∣2=∣xy∣4=1.\begin{align} \det F &= \begin{vmatrix} \operatorname{Re}(x\bar{y}) & -\operatorname{Im}(x\bar{y}) \\ \operatorname{Im}(x\bar{y}) & \operatorname{Re}(x\bar{y}) \end{vmatrix} \det\left(\begin{bmatrix} \lvert x\rvert^2 & □ \\ 0 & \lvert y\rvert^2 \end{bmatrix} - \begin{bmatrix} □ & □ \\ 0 & 0 \end{bmatrix} \begin{bmatrix} □ & □ \\ □ & □ \end{bmatrix} \begin{bmatrix} 0 & □ \\ 0 & □ \end{bmatrix} \right) \\ &= \lvert x\bar{y}\rvert^2 \lvert x\rvert^2 \lvert y\rvert^2 = \lvert xy\rvert^4 = 1. \end{align} This concludes `Lorentz.SL2C.toSelfAdjointMap_det_one'`. To get `Lorentz.SL2C.toSelfAdjointMap_det_one`, triangulate the special linear matrix using `Matrix.schur_triangulation`, and observe that `Matrix.schurTriangulation` preserves the determinant which is 1.

7 declarations

definition

Complex 2×22 \times 2 matrices C2×2\mathbb{C}^{2 \times 2}

The notation C2×2\mathbb{C}^{2 \times 2} denotes the type of 2×22 \times 2 matrices whose entries are complex numbers C\mathbb{C}.

abbrev

Space of 2×22 \times 2 Hermitian matrices H2\mathbb{H}_2

The space H2\mathbb{H}_2 is defined as the set of 2×22 \times 2 complex matrices that are self-adjoint (Hermitian). That is, H2={M∈C2×2∣M=M†}\mathbb{H}_2 = \{ M \in \mathbb{C}^{2 \times 2} \mid M = M^\dagger \}, where M†M^\dagger denotes the conjugate transpose.

definition

The R\mathbb{R}-linear map A↦MAM†A \mapsto M A M^\dagger on H2\mathbb{H}_2

Given a complex 2×22 \times 2 matrix M∈C2×2M \in \mathbb{C}^{2 \times 2}, this defines the R\mathbb{R}-linear map from the space of 2×22 \times 2 Hermitian matrices H2\mathbb{H}_2 to itself that sends a matrix AA to MAM†M A M^\dagger, where M†M^\dagger denotes the conjugate transpose of MM. This map is a generalization of the Lorentz transformation on Hermitian matrices where MM is not required to be in SL(2,C)SL(2, \mathbb{C}).

theorem

The determinant of A↦MAM†A \mapsto M A M^\dagger is 1 for upper triangular M∈SL(2,C)M \in SL(2, \mathbb{C})

Let MM be a 2×22 \times 2 complex matrix that is upper triangular and has determinant det⁡M=1\det M = 1. Let H2\mathbb{H}_2 be the real vector space of 2×22 \times 2 Hermitian matrices, defined as H2={A∈C2×2∣A=A†}\mathbb{H}_2 = \{ A \in \mathbb{C}^{2 \times 2} \mid A = A^\dagger \}, where A†A^\dagger denotes the conjugate transpose. Consider the R\mathbb{R}-linear map ΦM:H2→H2\Phi_M: \mathbb{H}_2 \to \mathbb{H}_2 given by ΦM(A)=MAM†\Phi_M(A) = M A M^\dagger. Then, the determinant of the linear operator ΦM\Phi_M is equal to 11.

definition

R\mathbb{R}-linear equivalence A↦MAM†A \mapsto M A M^\dagger on H2\mathbb{H}_2

Given an invertible 2×22 \times 2 complex matrix M∈GL(2,C)M \in \text{GL}(2, \mathbb{C}), this defines the R\mathbb{R}-linear equivalence from the space of 2×22 \times 2 Hermitian matrices H2\mathbb{H}_2 to itself. The linear map is defined by A↦MAM†A \mapsto M A M^\dagger, and its inverse is the map A↦M−1A(M−1)†A \mapsto M^{-1} A (M^{-1})^\dagger, where M†M^\dagger denotes the conjugate transpose of MM.

theorem

ΦMN=ΦM∘ΦN\Phi_{MN} = \Phi_M \circ \Phi_N for the map ΦM(A)=MAM†\Phi_M(A) = MAM^\dagger

For any 2×22 \times 2 complex matrices MM and NN, let ΦX:H2→H2\Phi_X: \mathbb{H}_2 \to \mathbb{H}_2 be the R\mathbb{R}-linear map on the space of 2×22 \times 2 Hermitian matrices defined by ΦX(A)=XAX†\Phi_X(A) = XAX^\dagger, where X†X^\dagger denotes the conjugate transpose of XX. Then the map associated with the product MNMN satisfies ΦMN=ΦM∘ΦN\Phi_{MN} = \Phi_M \circ \Phi_N.

theorem

det⁡(ΦMNM−1)=det⁡(ΦN)\det(\Phi_{MNM^{-1}}) = \det(\Phi_N) for the map ΦX(A)=XAX†\Phi_X(A) = XAX^\dagger

Let H2\mathbb{H}_2 be the real vector space of 2×22 \times 2 Hermitian matrices. For any complex 2×22 \times 2 matrix XX, let ΦX:H2→H2\Phi_X: \mathbb{H}_2 \to \mathbb{H}_2 be the R\mathbb{R}-linear map defined by ΦX(A)=XAX†\Phi_X(A) = XAX^\dagger, where X†X^\dagger is the conjugate transpose of XX. For any 2×22 \times 2 complex matrices MM and NN such that MM is invertible, the determinant of the linear map ΦMNM−1\Phi_{MNM^{-1}} is equal to the determinant of the linear map ΦN\Phi_N.