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.

def Lorentz.«termℂ²ˣ²» : Lean.ParserDescr

A notation for the type of complex 2-by-2 matrices. It would have been better to make it an abbreviation if it wasn't for Lean's inability to recognize ℂ²ˣ² as an identifier.

Equations

• Lorentz.«termℂ²ˣ²» = Lean.ParserDescr.node `Lorentz.«termℂ²ˣ²» 1024 (Lean.ParserDescr.symbol "ℂ²ˣ²")

@[reducible, inline]

noncomputable abbrev Lorentz.ℍ₂ : AddSubgroup (Matrix (Fin 2) (Fin 2) ℂ)

A convenient abbreviation for the type of self-adjoint complex 2-by-2 matrices.

Equations

• Lorentz.ℍ₂ = selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)

noncomputable def Lorentz.SL2C.toSelfAdjointMap' (M : Matrix (Fin 2) (Fin 2) ℂ) : ↥ℍ₂ →ₗ[ℝ] ↥ℍ₂

Definitionally equal to Lorentz.SL2C.toSelfAdjointMap but dropping the requirement that M be special linear.

Equations

• Lorentz.SL2C.toSelfAdjointMap' M = { toFun := fun (x : ↥Lorentz.ℍ₂) => match x with | ⟨A, hA⟩ => ⟨M * A * M.conjTranspose, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

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: $$ 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 = \begin{bmatrix} x & □ \\ 0 & y \end{bmatrix}$ is upper triangular, the basis $\{E_k\}_{k=0}^3$ induces the matrix representation $$ 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 = 1$, the Schur complement formula Matrix.det_fromBlocks₂₂ yields $$\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.

theorem Lorentz.SL2C.toSelfAdjointMap_det_one' {M : Matrix (Fin 2) (Fin 2) ℂ} (hM : M.IsUpperTriangular) (detM : M.det = 1) : LinearMap.det (toSelfAdjointMap' M) = 1

noncomputable def Lorentz.SL2C.toSelfAdjointEquiv (M : Matrix (Fin 2) (Fin 2) ℂ) [Invertible M] : ↥ℍ₂ ≃ₗ[ℝ] ↥ℍ₂

This promotes Lorentz.SL2C.toSelfAdjointMap M and its definitional equivalence, Lorentz.SL2C.toSelfAdjointMap' M, to a linear equivalence by recognizing the linear inverse to be Lorentz.SL2C.toSelfAdjointMap M⁻¹, i.e., Lorentz.SL2C.toSelfAdjointMap' M⁻¹.

Equations

• Lorentz.SL2C.toSelfAdjointEquiv M = { toLinearMap := Lorentz.SL2C.toSelfAdjointMap' M, invFun := ⇑(Lorentz.SL2C.toSelfAdjointMap' M⁻¹), left_inv := ⋯, right_inv := ⋯ }

theorem Lorentz.SL2C.toSelfAdjointMap_mul (M N : Matrix (Fin 2) (Fin 2) ℂ) : toSelfAdjointMap' (M * N) = toSelfAdjointMap' M ∘ₗ toSelfAdjointMap' N

theorem Lorentz.SL2C.toSelfAdjointMap_similar_det (M N : Matrix (Fin 2) (Fin 2) ℂ) [Invertible M] : LinearMap.det (toSelfAdjointMap' (M * N * M⁻¹)) = LinearMap.det (toSelfAdjointMap' N)