Physlib.Relativity.LorentzAlgebra.Basic

Imports

/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Physlib.Relativity.MinkowskiMatrix
public import Mathlib.Algebra.Lie.SerreConstruction

The Lorentz Algebra

We define

Define lorentzAlgebra via LieAlgebra.Orthogonal.so' as a subalgebra of Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ.

In mem_iff prove that a matrix is in the Lorentz algebra if and only if it satisfies the condition Aᵀ * η = - η * A.

@[expose] public sectionattribute [local instance 100] LieRing.ofAssociativeRing

The Lorentz algebra as a subalgebra of Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ.

def lorentzAlgebra : LieSubalgebra ℝ (Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ) :=
  (LieAlgebra.Orthogonal.so' (Fin 1) (Fin 3) ℝ)

              lemma transpose_eta (A : lorentzAlgebra) : A.1ᵀ * η = - η * A.1 := byA:↥lorentzAlgebra⊢ (↑A)ᵀ * η = -η * ↑A
  have h : A.1 ∈ skewAdjointMatricesSubmodule η := A.2A:↥lorentzAlgebrah:↑A ∈ skewAdjointMatricesSubmodule η⊢ (↑A)ᵀ * η = -η * ↑A
  simpa only [mem_skewAdjointMatricesSubmodule, Matrix.IsSkewAdjoint, IsAdjointPair, ← neg_mul_comm]
    using hAll goals completed! 🐙lemma mem_of_transpose_eta_eq_eta_mul_self {A : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ}
    (h : Aᵀ * η = - η * A) : A ∈ lorentzAlgebra := byA:Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝh:Aᵀ * η = -η * A⊢ A ∈ lorentzAlgebra
  simp_all only [neg_mul, lorentzAlgebra, LieAlgebra.Orthogonal.so',
    mem_skewAdjointMatricesLieSubalgebra, mem_skewAdjointMatricesSubmodule, Matrix.IsSkewAdjoint,
    IsAdjointPair, mul_neg]A:Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝh:Aᵀ * η = -(η * A)⊢ Aᵀ * LieAlgebra.Orthogonal.indefiniteDiagonal (Fin 1) (Fin 3) ℝ =
  -(LieAlgebra.Orthogonal.indefiniteDiagonal (Fin 1) (Fin 3) ℝ * A)
  exact hAll goals completed! 🐙lemma mem_iff {A : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ} :
    A ∈ lorentzAlgebra ↔ Aᵀ * η = - η * A :=
  Iff.intro (fun h => transpose_eta ⟨A, h⟩) (fun h => mem_of_transpose_eta_eq_eta_mul_self h)

lemma mem_iff' (A : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ) :
    A ∈ lorentzAlgebra ↔ A = - η * Aᵀ * η := byA:Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ⊢ A ∈ lorentzAlgebra ↔ A = -η * Aᵀ * η
  rw [mem_iffA:Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ⊢ Aᵀ * η = -η * A ↔ A = -η * Aᵀ * ηA:Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ⊢ Aᵀ * η = -η * A ↔ A = -η * Aᵀ * η]A:Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ⊢ Aᵀ * η = -η * A ↔ A = -η * Aᵀ * η
  constructormpA:Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ⊢ Aᵀ * η = -η * A → A = -η * Aᵀ * ηmprA:Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ⊢ A = -η * Aᵀ * η → Aᵀ * η = -η * A
  ·mpA:Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ⊢ Aᵀ * η = -η * A → A = -η * Aᵀ * η intro hmpA:Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝh:Aᵀ * η = -η * A⊢ A = -η * Aᵀ * η
    rw [mul_assoc,mpA:Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝh:Aᵀ * η = -η * A⊢ A = -η * (Aᵀ * η)All goals completed! 🐙 h,mpA:Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝh:Aᵀ * η = -η * A⊢ A = -η * (-η * A)All goals completed! 🐙 ← mul_assoc,mpA:Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝh:Aᵀ * η = -η * A⊢ A = -η * -η * AAll goals completed! 🐙 neg_mul_neg,mpA:Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝh:Aᵀ * η = -η * A⊢ A = η * η * AAll goals completed! 🐙 minkowskiMatrix.sq,mpA:Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝh:Aᵀ * η = -η * A⊢ A = 1 * AAll goals completed! 🐙 one_mulmpA:Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝh:Aᵀ * η = -η * A⊢ A = AAll goals completed! 🐙]All goals completed! 🐙
  ·mprA:Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ⊢ A = -η * Aᵀ * η → Aᵀ * η = -η * A intro hmprA:Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝh:A = -η * Aᵀ * η⊢ Aᵀ * η = -η * A
    nth_rewrite 2 [h]mprA:Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝh:A = -η * Aᵀ * η⊢ Aᵀ * η = -η * (-η * Aᵀ * η)
    rw [← mul_assoc,mprA:Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝh:A = -η * Aᵀ * η⊢ Aᵀ * η = -η * (-η * Aᵀ) * ηAll goals completed! 🐙 ← mul_assoc,mprA:Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝh:A = -η * Aᵀ * η⊢ Aᵀ * η = -η * -η * Aᵀ * ηAll goals completed! 🐙 neg_mul_neg,mprA:Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝh:A = -η * Aᵀ * η⊢ Aᵀ * η = η * η * Aᵀ * ηAll goals completed! 🐙 minkowskiMatrix.sq,mprA:Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝh:A = -η * Aᵀ * η⊢ Aᵀ * η = 1 * Aᵀ * ηAll goals completed! 🐙 one_mulmprA:Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝh:A = -η * Aᵀ * η⊢ Aᵀ * η = Aᵀ * ηAll goals completed! 🐙]All goals completed! 🐙lemma diag_comp (Λ : lorentzAlgebra) (μ : Fin 1 ⊕ Fin 3) : Λ.1 μ μ = 0 := byΛ:↥lorentzAlgebraμ:Fin 1 ⊕ Fin 3⊢ ↑Λ μ μ = 0
  have h := congrArg (fun M ↦ M μ μ) $ transpose_eta ΛΛ:↥lorentzAlgebraμ:Fin 1 ⊕ Fin 3h:((↑Λ)ᵀ * η) μ μ = (-η * ↑Λ) μ μ⊢ ↑Λ μ μ = 0
  simp only [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, mul_diagonal,
    transpose_apply, diagonal_neg, diagonal_mul, neg_mul] at hΛ:↥lorentzAlgebraμ:Fin 1 ⊕ Fin 3h:↑Λ μ μ * Sum.elim (fun x => 1) (fun x => -1) μ = -(Sum.elim (fun x => 1) (fun x => -1) μ * ↑Λ μ μ)⊢ ↑Λ μ μ = 0
  rcases μ with μ | μinlΛ:↥lorentzAlgebraμ:Fin 1h:↑Λ (Sum.inl μ) (Sum.inl μ) * Sum.elim (fun x => 1) (fun x => -1) (Sum.inl μ) =
  -(Sum.elim (fun x => 1) (fun x => -1) (Sum.inl μ) * ↑Λ (Sum.inl μ) (Sum.inl μ))⊢ ↑Λ (Sum.inl μ) (Sum.inl μ) = 0inrΛ:↥lorentzAlgebraμ:Fin 3h:↑Λ (Sum.inr μ) (Sum.inr μ) * Sum.elim (fun x => 1) (fun x => -1) (Sum.inr μ) =
  -(Sum.elim (fun x => 1) (fun x => -1) (Sum.inr μ) * ↑Λ (Sum.inr μ) (Sum.inr μ))⊢ ↑Λ (Sum.inr μ) (Sum.inr μ) = 0 <;>inlΛ:↥lorentzAlgebraμ:Fin 1h:↑Λ (Sum.inl μ) (Sum.inl μ) * Sum.elim (fun x => 1) (fun x => -1) (Sum.inl μ) =
  -(Sum.elim (fun x => 1) (fun x => -1) (Sum.inl μ) * ↑Λ (Sum.inl μ) (Sum.inl μ))⊢ ↑Λ (Sum.inl μ) (Sum.inl μ) = 0inrΛ:↥lorentzAlgebraμ:Fin 3h:↑Λ (Sum.inr μ) (Sum.inr μ) * Sum.elim (fun x => 1) (fun x => -1) (Sum.inr μ) =
  -(Sum.elim (fun x => 1) (fun x => -1) (Sum.inr μ) * ↑Λ (Sum.inr μ) (Sum.inr μ))⊢ ↑Λ (Sum.inr μ) (Sum.inr μ) = 0
    simp only [Sum.elim_inl, Sum.elim_inr, mul_one, one_mul, mul_neg, neg_mul, neg_neg] at hinrΛ:↥lorentzAlgebraμ:Fin 3h:-↑Λ (Sum.inr μ) (Sum.inr μ) = ↑Λ (Sum.inr μ) (Sum.inr μ)⊢ ↑Λ (Sum.inr μ) (Sum.inr μ) = 0 <;>inlΛ:↥lorentzAlgebraμ:Fin 1h:↑Λ (Sum.inl μ) (Sum.inl μ) = -↑Λ (Sum.inl μ) (Sum.inl μ)⊢ ↑Λ (Sum.inl μ) (Sum.inl μ) = 0inrΛ:↥lorentzAlgebraμ:Fin 3h:-↑Λ (Sum.inr μ) (Sum.inr μ) = ↑Λ (Sum.inr μ) (Sum.inr μ)⊢ ↑Λ (Sum.inr μ) (Sum.inr μ) = 0
    linarithAll goals completed! 🐙lemma time_comps (Λ : lorentzAlgebra) (i : Fin 3) :
    Λ.1 (Sum.inr i) (Sum.inl 0) = Λ.1 (Sum.inl 0) (Sum.inr i) := byΛ:↥lorentzAlgebrai:Fin 3⊢ ↑Λ (Sum.inr i) (Sum.inl 0) = ↑Λ (Sum.inl 0) (Sum.inr i)
  simpa only [Fin.isValue, minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, mul_diagonal,
    transpose_apply, Sum.elim_inr, mul_neg, mul_one, diagonal_neg, diagonal_mul, Sum.elim_inl,
    neg_mul, one_mul, neg_inj] using congrArg (fun M ↦ M (Sum.inl 0) (Sum.inr i)) $ transpose_eta ΛAll goals completed! 🐙lemma space_comps (Λ : lorentzAlgebra) (i j : Fin 3) :
    Λ.1 (Sum.inr i) (Sum.inr j) = - Λ.1 (Sum.inr j) (Sum.inr i) := byΛ:↥lorentzAlgebrai:Fin 3j:Fin 3⊢ ↑Λ (Sum.inr i) (Sum.inr j) = -↑Λ (Sum.inr j) (Sum.inr i)
  simpa only [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, diagonal_neg, diagonal_mul,
    Sum.elim_inr, neg_neg, one_mul, mul_diagonal, transpose_apply, mul_neg, mul_one] using
    (congrArg (fun M ↦ M (Sum.inr i) (Sum.inr j)) $ transpose_eta Λ).symmAll goals completed! 🐙