From 6e96b558d5c0b978c30d52fa141ccdadad6501c7 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Wed, 12 Jun 2024 11:47:38 -0400 Subject: [PATCH] feat: Add properties of the Lorentz basis --- HepLean/SpaceTime/LorentzAlgebra/Basis.lean | 49 +++++++++++++++++++++ HepLean/SpaceTime/Metric.lean | 39 ++++++++++++---- 2 files changed, 79 insertions(+), 9 deletions(-) diff --git a/HepLean/SpaceTime/LorentzAlgebra/Basis.lean b/HepLean/SpaceTime/LorentzAlgebra/Basis.lean index f7143d2..40432e4 100644 --- a/HepLean/SpaceTime/LorentzAlgebra/Basis.lean +++ b/HepLean/SpaceTime/LorentzAlgebra/Basis.lean @@ -21,6 +21,55 @@ open Matrix def σMat (μ ν : Fin 4) : Matrix (Fin 4) (Fin 4) ℝ := fun ρ δ ↦ η^[ρ]_[μ] * η_[ν]_[δ] - η_[μ]_[δ] * η^[ρ]_[ν] +lemma σMat_in_lorentzAlgebra (μ ν : Fin 4) : σMat μ ν ∈ lorentzAlgebra := by + rw [mem_iff] + funext ρ δ + rw [Matrix.neg_mul, Matrix.neg_apply, η_mul, mul_η, transpose_apply] + apply Eq.trans ?_ (by ring : + - ((η^[ρ]_[μ] * η_[ρ]_[ρ]) * η_[ν]_[δ] - η_[μ]_[δ] * (η^[ρ]_[ν] * η_[ρ]_[ρ])) = + -(η_[ρ]_[ρ] * (η^[ρ]_[μ] * η_[ν]_[δ] - η_[μ]_[δ] * η^[ρ]_[ν]))) + apply Eq.trans (by ring : (η^[δ]_[μ] * η_[ν]_[ρ] - η_[μ]_[ρ] * η^[δ]_[ν]) * η_[δ]_[δ] + = ((η^[δ]_[μ] * η_[δ]_[δ]) * η_[ν]_[ρ] - η_[μ]_[ρ] * (η^[δ]_[ν] * η_[δ]_[δ]))) + rw [η_mul_self, η_mul_self, η_mul_self, η_mul_self] + ring + +/-- Elements of the Lorentz algebra which form a basis thereof. -/ +@[simps!] +def σ (μ ν : Fin 4) : lorentzAlgebra := ⟨σMat μ ν, σMat_in_lorentzAlgebra μ ν⟩ + +lemma σ_anti_symm (μ ν : Fin 4) : σ μ ν = - σ ν μ := by + refine SetCoe.ext ?_ + funext ρ δ + simp only [σ_coe, σMat, NegMemClass.coe_neg, neg_apply, neg_sub] + ring + +lemma σMat_mul (α β γ δ a b: Fin 4) : + (σMat α β * σMat γ δ) a b = + η^[a]_[α] * (η_[δ]_[b] * η_[β]_[γ] - η_[γ]_[b] * η_[β]_[δ]) + - η^[a]_[β] * (η_[δ]_[b] * η_[α]_[γ]- η_[γ]_[b] * η_[α]_[δ]) := by + rw [Matrix.mul_apply] + simp only [σMat] + trans (η^[a]_[α] * η_[δ]_[b]) * ∑ x, η^[x]_[γ] * η_[β]_[x] + - (η^[a]_[α] * η_[γ]_[b]) * ∑ x, η^[x]_[δ] * η_[β]_[x] + - (η^[a]_[β] * η_[δ]_[b]) * ∑ x, η^[x]_[γ] * η_[α]_[x] + + (η^[a]_[β] * η_[γ]_[b]) * ∑ x, η^[x]_[δ] * η_[α]_[x] + repeat rw [Fin.sum_univ_four] + ring + rw [η_contract_self', η_contract_self', η_contract_self', η_contract_self'] + ring + +lemma σ_comm (α β γ δ : Fin 4) : + ⁅σ α β , σ γ δ⁆ = + η_[α]_[δ] • σ β γ + η_[α]_[γ] • σ δ β + η_[β]_[δ] • σ γ α + η_[β]_[γ] • σ α δ := by + refine SetCoe.ext ?_ + change σMat α β * σ γ δ - σ γ δ * σ α β = _ + funext a b + simp only [σ_coe, sub_apply, AddSubmonoid.coe_add, Submodule.coe_toAddSubmonoid, + Submodule.coe_smul_of_tower, add_apply, smul_apply, σMat, smul_eq_mul] + rw [σMat_mul, σMat_mul, η_symmetric α γ, η_symmetric α δ, η_symmetric β γ, η_symmetric β δ] + ring + + end lorentzAlgebra end spaceTime diff --git a/HepLean/SpaceTime/Metric.lean b/HepLean/SpaceTime/Metric.lean index 67ce30b..fd0f2a8 100644 --- a/HepLean/SpaceTime/Metric.lean +++ b/HepLean/SpaceTime/Metric.lean @@ -32,16 +32,11 @@ def η : Matrix (Fin 4) (Fin 4) ℝ := Matrix.reindex finSumFinEquiv finSumFinEq /-- The metric with lower indices. -/ notation "η_[" μ "]_[" ν "]" => η μ ν +/-- The inverse of `η`. Used for notation. -/ +def ηInv : Matrix (Fin 4) (Fin 4) ℝ := η + /-- The metric with upper indices. -/ -notation "η^[" μ "]^[" ν "]" => η μ ν - -/-- The metric with one lower and one upper index. -/ -notation "η_[" μ "]^[" ν "]" => η_[μ]_[0] * η^[0]^[ν] + η_[μ]_[1] * η^[1]^[ν] + - η_[μ]_[2] * η^[2]^[ν] + η_[μ]_[3] * η^[3]^[ν] - -/-- The metric with one lower and one upper index. -/ -notation "η^[" μ "]_[" ν "]" => η^[μ]^[0] * η_[0]_[ν] + η^[μ]^[1] * η_[1]_[ν] - + η^[μ]^[2] * η_[2]_[ν] + η^[μ]^[3] * η_[3]_[ν] +notation "η^[" μ "]^[" ν "]" => ηInv μ ν /-- A matrix with one lower and one upper index. -/ notation "["Λ"]^[" μ "]_[" ν "]" => (Λ : Matrix (Fin 4) (Fin 4) ℝ) μ ν @@ -49,6 +44,12 @@ notation "["Λ"]^[" μ "]_[" ν "]" => (Λ : Matrix (Fin 4) (Fin 4) ℝ) μ ν /-- A matrix with both lower indices. -/ notation "["Λ"]_[" μ "]_[" ν "]" => ∑ ρ, η_[μ]_[ρ] * [Λ]^[ρ]_[ν] +/-- `η` with $η^μ_ν$ indices. This is equivalent to the identity. This is used for notation. -/ +def ηUpDown : Matrix (Fin 4) (Fin 4) ℝ := 1 + +/-- The metric with one lower and one upper index. -/ +notation "η^[" μ "]_[" ν "]" => ηUpDown μ ν + lemma η_block : η = Matrix.reindex finSumFinEquiv finSumFinEquiv ( Matrix.fromBlocks (1 : Matrix (Fin 1) (Fin 1) ℝ) 0 0 (-1 : Matrix (Fin 3) (Fin 3) ℝ)) := by @@ -129,6 +130,26 @@ lemma η_as_diagonal : η = diagonal ![1, -1, -1, -1] := by intro μ ν fin_cases μ <;> fin_cases ν <;> rfl +lemma η_mul (Λ : Matrix (Fin 4) (Fin 4) ℝ) (μ ρ : Fin 4) : + [η * Λ]^[μ]_[ρ] = [η]^[μ]_[μ] * [Λ]^[μ]_[ρ] := by + rw [η_as_diagonal, @diagonal_mul, diagonal_apply_eq ![1, -1, -1, -1] μ] + +lemma mul_η (Λ : Matrix (Fin 4) (Fin 4) ℝ) (μ ρ : Fin 4) : + [Λ * η]^[μ]_[ρ] = [Λ]^[μ]_[ρ] * [η]^[ρ]_[ρ] := by + rw [η_as_diagonal, @mul_diagonal, diagonal_apply_eq ![1, -1, -1, -1] ρ] + +lemma η_mul_self (μ ν : Fin 4) : η^[ν]_[μ] * η_[ν]_[ν] = η_[μ]_[ν] := by + fin_cases μ <;> fin_cases ν <;> simp [ηUpDown] + +lemma η_contract_self (μ ν : Fin 4) : ∑ x, (η^[x]_[μ] * η_[x]_[ν]) = η_[μ]_[ν] := by + rw [Fin.sum_univ_four] + fin_cases μ <;> fin_cases ν <;> simp [ηUpDown] + +lemma η_contract_self' (μ ν : Fin 4) : ∑ x, (η^[x]_[μ] * η_[ν]_[x]) = η_[ν]_[μ] := by + rw [Fin.sum_univ_four] + fin_cases μ <;> fin_cases ν <;> simp [ηUpDown] + + /-- Given a point in spaceTime `x` the linear map `y → x ⬝ᵥ (η *ᵥ y)`. -/ @[simps!]