DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

docs: Minkowski Matrix

Browse source
This commit is contained in:
jstoobysmith 2024-11-26 11:58:37 +00:00
parent 6db6752077
commit 20d3dc4dca
1 changed files with 25 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

27
HepLean/Lorentz/MinkowskiMatrix.lean
View file

@ -30,6 +30,7 @@ variable {d : ℕ}
/-- Notation for `minkowskiMatrix`. -/
scoped[minkowskiMatrix] notation "η" => minkowskiMatrix
/-- The Minkowski matrix is self-inveting. -/
@[simp]
lemma sq : @minkowskiMatrix d * minkowskiMatrix = 1 := by
simp only [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, diagonal_mul_diagonal]
@ -50,20 +51,25 @@ lemma sq : @minkowskiMatrix d * minkowskiMatrix = 1 := by
simp_all only [one_apply_eq]
· simp_all only [ne_eq, Sum.inr.injEq, not_false_eq_true, one_apply_ne]
/-- The Minkowski matrix is symmetric. -/
@[simp]
lemma eq_transpose : minkowskiMatrixᵀ = @minkowskiMatrix d := by
simp only [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, diagonal_transpose]
/-- The deteminant of the Minkowski matrix is equal to `-1` to the power
of the number of spactial dimensions. -/
@[simp]
lemma det_eq_neg_one_pow_d : (@minkowskiMatrix d).det = (- 1) ^ d := by
simp [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal]
/-- Multiplying any element on the diagonal of the Minkowski matrix by itself gives `1`. -/
@[simp]
lemma η_apply_mul_η_apply_diag (μ : Fin 1 ⊕ Fin d) : η μ μ * η μ μ = 1 := by
match μ with
| Sum.inl _ => simp [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal]
| Sum.inr _ => simp [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal]
/-- The Minkowski matix as a block matrix. -/
lemma as_block : @minkowskiMatrix d =
Matrix.fromBlocks (1 : Matrix (Fin 1) (Fin 1) ℝ) 0 0 (-1 : Matrix (Fin d) (Fin d) ℝ) := by
rw [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, ← fromBlocks_diagonal]
@ -73,24 +79,29 @@ lemma as_block : @minkowskiMatrix d =
rw [← diagonal_neg]
rfl
/-- The off diagonal elements of the Minkowski matrix are zero. -/
@[simp]
lemma off_diag_zero {μ ν : Fin 1 ⊕ Fin d} (h : μ ≠ ν) : η μ ν = 0 := by
simp only [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal]
exact diagonal_apply_ne _ h
/-- The `time-time` component of the Minkowski matrix is `1`. -/
lemma inl_0_inl_0 : @minkowskiMatrix d (Sum.inl 0) (Sum.inl 0) = 1 := by
rfl
/-- The space diagonal components of the Minkowski matriz are `-1`. -/
lemma inr_i_inr_i (i : Fin d) : @minkowskiMatrix d (Sum.inr i) (Sum.inr i) = -1 := by
simp only [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal]
simp_all only [diagonal_apply_eq, Sum.elim_inr]
/-- The time components of a vector acted on by the Minkowski matrix remains unchanged. -/
@[simp]
lemma mulVec_inl_0 (v : (Fin 1 ⊕ Fin d) → ℝ) :
(η *ᵥ v) (Sum.inl 0)= v (Sum.inl 0) := by
simp only [mulVec, minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, mulVec_diagonal]
simp only [Fin.isValue, diagonal_dotProduct, Sum.elim_inl, one_mul]
/-- The space components of a vector acted on by the Minkowski matrix swaps sign. -/
@[simp]
lemma mulVec_inr_i (v : (Fin 1 ⊕ Fin d) → ℝ) (i : Fin d) :
(η *ᵥ v) (Sum.inr i)= - v (Sum.inr i) := by
@ -99,13 +110,16 @@ lemma mulVec_inr_i (v : (Fin 1 ⊕ Fin d) → ℝ) (i : Fin d) :
variable (Λ Λ' : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)
/-- The dual of a matrix with respect to the Minkowski metric. -/
/-- The dual of a matrix with respect to the Minkowski metric.
A suitable name fo this construction is the Minkowski dual. -/
def dual : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ := η * Λᵀ * η
/-- The Minkowski dual of the identity is the identity. -/
@[simp]
lemma dual_id : @dual d 1 = 1 := by
simpa only [dual, transpose_one, mul_one] using minkowskiMatrix.sq
/-- The Minkowski dual swaps multiplications (acts contrvariantly). -/
@[simp]
lemma dual_mul : dual (Λ * Λ') = dual Λ' * dual Λ := by
simp only [dual, transpose_mul]
@ -113,23 +127,28 @@ lemma dual_mul : dual (Λ * Λ') = dual Λ' * dual Λ := by
· noncomm_ring [minkowskiMatrix.sq]
· noncomm_ring
/-- The Minkowski dual is involutive (i.e. `dual (dual Λ)) = Λ`). -/
@[simp]
lemma dual_dual : dual (dual Λ) = Λ := by
lemma dual_dual : Function.Involutive (@dual d) := by
intro Λ
simp only [dual, transpose_mul, transpose_transpose, eq_transpose]
trans (η * η) * Λ * (η * η)
· noncomm_ring
· noncomm_ring [minkowskiMatrix.sq]
/-- The Minkowski dual preserves the Minkowski matrix. -/
@[simp]
lemma dual_eta : @dual d η = η := by
simp only [dual, eq_transpose]
noncomm_ring [minkowskiMatrix.sq]
/-- The Minkowski dual commutes with the transpose. -/
@[simp]
lemma dual_transpose : dual Λᵀ = (dual Λ)ᵀ := by
simp only [dual, transpose_transpose, transpose_mul, eq_transpose]
noncomm_ring
/-- The Minkowski dual preserves determinants. -/
@[simp]
lemma det_dual : (dual Λ).det = Λ.det := by
simp only [dual, det_mul, minkowskiMatrix.det_eq_neg_one_pow_d, det_transpose]
@ -137,11 +156,15 @@ lemma det_dual : (dual Λ).det = Λ.det := by
norm_cast
simp
/-- Expansion of the components of the Minkowski dual interms of the components
of the original matrix. -/
lemma dual_apply (μ ν : Fin 1 ⊕ Fin d) :
dual Λ μ ν = η μ μ * Λ ν μ * η ν ν := by
simp only [dual, minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, mul_diagonal,
diagonal_mul, transpose_apply, diagonal_apply_eq]
/-- The components of the Minkowski dual of a matrix multiplied by the Minkowski matrix
in tems of the original matrix. -/
lemma dual_apply_minkowskiMatrix (μ ν : Fin 1 ⊕ Fin d) :
dual Λ μ ν * η ν ν = η μ μ * Λ ν μ := by
rw [dual_apply, mul_assoc]