feat: toLorentzGroup_det_one
This commit is contained in:
kuotsanhsu
parent
5baa184092
commit
0297f0e288
2 changed files with 155 additions and 3 deletions
|
|
@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Joseph Tooby-Smith
|
||||
-/
|
||||
import HepLean.Lorentz.Group.Restricted
|
||||
import HepLean.Lorentz.SL2C.SelfAdjoint
|
||||
import Mathlib.Analysis.Complex.Polynomial.Basic -- Complex.isAlgClosed
|
||||
/-!
|
||||
# The group SL(2, ℂ) and it's relation to the Lorentz group
|
||||
|
||||
|
|
@ -282,9 +284,28 @@ In this section we will define this homomorphism.
|
|||
|
||||
-/
|
||||
|
||||
informal_lemma toLorentzGroup_det_one where
|
||||
math :≈ "The determinant of the image of `SL(2, ℂ)` in the Lorentz group is one."
|
||||
deps :≈ [``toLorentzGroup]
|
||||
/-- The determinant of the image of `SL(2, ℂ)` in the Lorentz group is one. -/
|
||||
lemma toLorentzGroup_det_one (M : SL(2, ℂ)) : det (toLorentzGroup M).val = 1 :=
|
||||
let U := M.val.schurTriangulationUnitary
|
||||
let N := M.val.schurTriangulation.val
|
||||
have h : M.val = U * N * star U := M.val.schur_triangulation
|
||||
haveI : Invertible U.val := ⟨star U.val, U.property.left, U.property.right⟩
|
||||
calc det (toLorentzGroup M).val
|
||||
_ = LinearMap.det (toSelfAdjointMap' M) := LinearMap.det_toMatrix ..
|
||||
_ = LinearMap.det (toSelfAdjointMap' (U * N * U.val⁻¹)) :=
|
||||
suffices star U = U.val⁻¹ by rw [h, this]
|
||||
calc star U.val
|
||||
_ = star U.val * (U.val * U.val⁻¹) := by simp
|
||||
_ = star U.val * U.val * U.val⁻¹ := by noncomm_ring
|
||||
_ = U.val⁻¹ := by simp
|
||||
_ = LinearMap.det (toSelfAdjointMap' N) := toSelfAdjointMap_similar_det U N
|
||||
_ = 1 :=
|
||||
suffices N.det = 1 from toSelfAdjointMap_det_one' M.val.schurTriangulation.property this
|
||||
calc N.det
|
||||
_ = det ((U * star U).val * N) := by simp
|
||||
_ = det (U.val * N * star U.val) := det_mul_right_comm ..
|
||||
_ = M.val.det := congrArg det h.symm
|
||||
_ = 1 := M.property
|
||||
|
||||
informal_lemma toRestrictedLorentzGroup where
|
||||
math :≈ "The homomorphism from `SL(2, ℂ)` to the restricted Lorentz group."
|
||||
|
|
|
|||
131
HepLean/Lorentz/SL2C/SelfAdjoint.lean
Normal file
131
HepLean/Lorentz/SL2C/SelfAdjoint.lean
Normal file
|
|
@ -0,0 +1,131 @@
|
|||
import Mathlib.LinearAlgebra.Matrix.SchurComplement
|
||||
import HepLean.Mathematics.SchurTriangulation
|
||||
|
||||
namespace Lorentz
|
||||
|
||||
open scoped Matrix
|
||||
open scoped ComplexConjugate
|
||||
|
||||
notation "ℂ²ˣ²" => Matrix (Fin 2) (Fin 2) ℂ
|
||||
noncomputable abbrev ℍ₂ := selfAdjoint ℂ²ˣ²
|
||||
|
||||
namespace SL2C
|
||||
|
||||
noncomputable def toSelfAdjointMap' (M : ℂ²ˣ²) : ℍ₂ →ₗ[ℝ] ℍ₂ where
|
||||
toFun | ⟨A, hA⟩ => ⟨M * A * Mᴴ, hA.conjugate M⟩
|
||||
map_add' | ⟨A, _⟩, ⟨B, _⟩ => Subtype.ext <|
|
||||
show M * (A + B) * Mᴴ = M * A * Mᴴ + M * B * Mᴴ by noncomm_ring
|
||||
map_smul' | r, ⟨A, _⟩ => Subtype.ext <| by simp
|
||||
|
||||
open Complex (I normSq) in
|
||||
theorem toSelfAdjointMap_det_one' {M : ℂ²ˣ²} (hM : M.IsUpperTriangular) (detM : M.det = 1)
|
||||
: LinearMap.det (toSelfAdjointMap' M) = 1 :=
|
||||
let b : Basis (Fin 2 ⊕ Fin 2) ℝ ℍ₂ := Basis.ofEquivFun {
|
||||
toFun := fun ⟨A, _⟩ => ![(A 0 0).re, (A 1 1).re] ⊕ᵥ ![(A 0 1).re, (A 0 1).im]
|
||||
map_add' := fun _ _ => funext fun | .inl 0 | .inl 1 | .inr 0 | .inr 1 => rfl
|
||||
map_smul' := fun _ _ => funext fun | .inl 0 | .inl 1 | .inr 0 | .inr 1 => by simp
|
||||
invFun := fun p => {
|
||||
val := let z : ℂ := ⟨p (.inr 0), p (.inr 1)⟩ ; !![p (.inl 0), z; conj z, p (.inl 1)]
|
||||
property := Matrix.ext fun | 0, 0 | 0, 1 | 1, 0 | 1, 1 => by simp
|
||||
}
|
||||
left_inv := fun ⟨A, hA⟩ => Subtype.ext <| Matrix.ext fun
|
||||
| 0, 1 => rfl
|
||||
| 1, 0 => show conj (A 0 1) = A 1 0 from congrFun₂ hA 1 0
|
||||
| 0, 0 => show (A 0 0).re = A 0 0 from Complex.conj_eq_iff_re.mp (congrFun₂ hA 0 0)
|
||||
| 1, 1 => show (A 1 1).re = A 1 1 from Complex.conj_eq_iff_re.mp (congrFun₂ hA 1 1)
|
||||
right_inv := fun _ => funext fun | .inl 0 | .inl 1 | .inr 0 | .inr 1 => rfl
|
||||
}
|
||||
let E₀ : ℂ²ˣ² := !![1, 0; conj 0, 0] -- b (.inl 0)
|
||||
let E₁ : ℂ²ˣ² := !![0, 0; conj 0, 1] -- b (.inl 1)
|
||||
let E₂ : ℂ²ˣ² := !![0, 1; conj 1, 0] -- b (.inr 0)
|
||||
let E₃ : ℂ²ˣ² := !![0, I; conj I, 0] -- b (.inr 1)
|
||||
let F : Matrix (Fin 2 ⊕ Fin 2) (Fin 2 ⊕ Fin 2) ℝ := LinearMap.toMatrix b b (toSelfAdjointMap' M)
|
||||
let A := F.toBlocks₁₁ ; let B := F.toBlocks₁₂ ; let C := F.toBlocks₂₁ ; let D := F.toBlocks₂₂
|
||||
let x := M 0 0 ; let y := M 1 1 ; have hM10 : M 1 0 = 0 := hM <| show 0 < 1 by decide
|
||||
have he : M = !![x, _; 0, y] := Matrix.ext fun | 0, 0 | 0, 1 | 1, 1 => rfl | 1, 0 => hM10
|
||||
have he' : Mᴴ = !![conj x, 0; _, conj y] :=
|
||||
Matrix.ext fun | 0, 0 | 1, 0 | 1, 1 => rfl | 0, 1 => by simp [hM10]
|
||||
|
||||
have detA_one : normSq x * normSq y = 1 := congrArg Complex.re <|
|
||||
calc ↑(normSq x * normSq y)
|
||||
_ = x * conj x * (y * conj y) := by simp [Complex.mul_conj]
|
||||
_ = x * y * (conj y * conj x) := by ring
|
||||
_ = x * y * conj (x * y) := congrArg _ (star_mul ..).symm
|
||||
_ = 1 := suffices x * y = 1 by simp [this]
|
||||
calc x * y
|
||||
_ = !![x, _; 0, y].det := by simp
|
||||
_ = M.det := congrArg _ he.symm
|
||||
_ = 1 := detM
|
||||
have detD_one : D.det = 1 :=
|
||||
let z := x * conj y
|
||||
have k₀ : (M * E₂ * Mᴴ) 0 1 = z := by rw [he', he] ; simp [E₂]
|
||||
have k₁ : (M * E₃ * Mᴴ) 0 1 = ⟨-z.im, z.re⟩ :=
|
||||
calc
|
||||
_ = x * I * conj y := by rw [he', he] ; simp [E₃]
|
||||
_ = Complex.I * z := by ring
|
||||
_ = ⟨-z.im, z.re⟩ := z.I_mul
|
||||
have hD : D = !![z.re, -z.im; z.im, z.re] := Matrix.ext fun
|
||||
| 0, 0 => congrArg Complex.re k₀ | 1, 0 => congrArg Complex.im k₀
|
||||
| 0, 1 => congrArg Complex.re k₁ | 1, 1 => congrArg Complex.im k₁
|
||||
calc D.det
|
||||
_ = normSq z := by simp [hD, z.normSq_apply]
|
||||
_ = normSq x * normSq y := by simp [x.normSq_mul]
|
||||
_ = 1 := detA_one
|
||||
|
||||
letI : Invertible D.det := detD_one ▸ invertibleOne
|
||||
letI : Invertible D := D.invertibleOfDetInvertible
|
||||
have hE : A - B * ⅟D * C = !![normSq x, _; 0, normSq y] :=
|
||||
have k : (M * E₀ * Mᴴ) 0 1 = 0 := by rw [he', he] ; simp [E₀]
|
||||
have hC00 : C 0 0 = 0 := congrArg Complex.re k
|
||||
have hC10 : C 1 0 = 0 := congrArg Complex.im k
|
||||
Matrix.ext fun
|
||||
| 0, 1 => rfl
|
||||
| 1, 0 =>
|
||||
have hA10 : A 1 0 = 0 := congrArg Complex.re <|
|
||||
show (M * E₀ * Mᴴ) 1 1 = 0 by rw [he', he] ; simp [E₀]
|
||||
show A 1 0 - (B * ⅟D) 1 ⬝ᵥ (C · 0) = 0 by simp [hC00, hC10, hA10]
|
||||
| 0, 0 =>
|
||||
have hA00 : A 0 0 = normSq x := congrArg Complex.re <|
|
||||
show (M * E₀ * Mᴴ) 0 0 = normSq x by rw [he', he] ; simp [E₀, x.mul_conj]
|
||||
show A 0 0 - (B * ⅟D) 0 ⬝ᵥ (C · 0) = normSq x by simp [hC00, hC10, hA00]
|
||||
| 1, 1 =>
|
||||
have hA11 : A 1 1 = normSq y := congrArg Complex.re <|
|
||||
show (M * E₁ * Mᴴ) 1 1 = normSq y by rw [he', he] ; simp [E₁, y.mul_conj]
|
||||
have hB10 : B 1 0 = 0 := congrArg Complex.re <|
|
||||
show (M * E₂ * Mᴴ) 1 1 = 0 by rw [he', he] ; simp [E₂]
|
||||
have hB11 : B 1 1 = 0 := congrArg Complex.re <|
|
||||
show (M * E₃ * Mᴴ) 1 1 = 0 by rw [he', he] ; simp [E₃]
|
||||
calc A 1 1 - (B * ⅟D * C) 1 1
|
||||
_ = A 1 1 - B 1 ⬝ᵥ ((⅟D * C) · 1) := by noncomm_ring
|
||||
_ = normSq y := by simp [hB10, hB11, hA11]
|
||||
calc LinearMap.det (toSelfAdjointMap' M)
|
||||
_ = F.det := (LinearMap.det_toMatrix ..).symm
|
||||
_ = D.det * (A - B * ⅟D * C).det := F.fromBlocks_toBlocks ▸ Matrix.det_fromBlocks₂₂ ..
|
||||
_ = 1 := by rw [hE] ; simp [detD_one, detA_one]
|
||||
|
||||
noncomputable def toSelfAdjointEquiv (M : ℂ²ˣ²) [Invertible M] : ℍ₂ ≃ₗ[ℝ] ℍ₂ where
|
||||
toLinearMap := toSelfAdjointMap' M
|
||||
invFun := toSelfAdjointMap' M⁻¹
|
||||
left_inv | ⟨A, _⟩ => Subtype.ext <|
|
||||
calc M⁻¹ * (M * A * Mᴴ) * M⁻¹ᴴ
|
||||
_ = M⁻¹ * ↑M * A * (M⁻¹ * M)ᴴ := by noncomm_ring [Matrix.conjTranspose_mul]
|
||||
_ = A := by simp
|
||||
right_inv | ⟨A, _⟩ => Subtype.ext <|
|
||||
calc M * (M⁻¹ * A * M⁻¹ᴴ) * Mᴴ
|
||||
_ = M * M⁻¹ * A * (M * M⁻¹)ᴴ := by noncomm_ring [Matrix.conjTranspose_mul]
|
||||
_ = A := by simp
|
||||
|
||||
theorem toSelfAdjointMap_mul (M N : ℂ²ˣ²)
|
||||
: toSelfAdjointMap' (M * N) = toSelfAdjointMap' M ∘ₗ toSelfAdjointMap' N :=
|
||||
LinearMap.ext fun A => Subtype.ext <|
|
||||
show M * N * A * (M * N)ᴴ = M * (N * A * Nᴴ) * Mᴴ by noncomm_ring [Matrix.conjTranspose_mul]
|
||||
|
||||
theorem toSelfAdjointMap_similar_det (M N : ℂ²ˣ²) [Invertible M]
|
||||
: LinearMap.det (toSelfAdjointMap' (M * N * M⁻¹)) = LinearMap.det (toSelfAdjointMap' N) :=
|
||||
let e := toSelfAdjointEquiv M
|
||||
let f := toSelfAdjointMap' N
|
||||
suffices toSelfAdjointMap' (M * N * M⁻¹) = e ∘ₗ f ∘ₗ e.symm from this ▸ f.det_conj e
|
||||
by rw [toSelfAdjointMap_mul, toSelfAdjointMap_mul] ; rfl
|
||||
|
||||
end SL2C
|
||||
end Lorentz
|
||||
Loading…
Add table
Add a link
Reference in a new issue