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

feat: Add lorentz algebra results

Browse source
This commit is contained in:
jstoobysmith 2024-05-29 16:42:04 -04:00
parent a52d8ea452
commit 20dd51d897
2 changed files with 11 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

14
HepLean/SpaceTime/LorentzAlgebra/Basic.lean
View file

@ -68,7 +68,7 @@ lemma mem_of_transpose_eta_eq_eta_mul_self {A : Matrix (Fin 4) (Fin 4) ℝ}
simpa using h1 simpa using h1
lemma mem_iff (A : Matrix (Fin 4) (Fin 4) ℝ) : A ∈ lorentzAlgebra ↔ lemma mem_iff {A : Matrix (Fin 4) (Fin 4) ℝ} : A ∈ lorentzAlgebra ↔
Aᵀ * η = - η * A := by Aᵀ * η = - η * A := by
apply Iff.intro apply Iff.intro
· intro h · intro h
@ -76,7 +76,15 @@ lemma mem_iff (A : Matrix (Fin 4) (Fin 4) ℝ) : A ∈ lorentzAlgebra ↔
· intro h · intro h
exact mem_of_transpose_eta_eq_eta_mul_self h exact mem_of_transpose_eta_eq_eta_mul_self h
lemma mem_iff' (A : Matrix (Fin 4) (Fin 4) ℝ) : A ∈ lorentzAlgebra ↔ A = - η * Aᵀ * η := by
apply Iff.intro
intro h
rw [mul_assoc, mem_iff.mp h]
simp only [neg_mul, mul_neg, ← mul_assoc, η_sq, one_mul, neg_neg]
intro h
rw [mem_iff]
nth_rewrite 2 [h]
simp [← mul_assoc, η_sq]
end lorentzAlgebra end lorentzAlgebra
@ -87,7 +95,7 @@ instance spaceTimeAsLieRingModule : LieRingModule lorentzAlgebra spaceTime where
add_lie Λ1 Λ2 x := by add_lie Λ1 Λ2 x := by
simp [add_mulVec] simp [add_mulVec]
lie_add Λ x1 x2 := by lie_add Λ x1 x2 := by
simp simp only
exact mulVec_add _ _ _ exact mulVec_add _ _ _
leibniz_lie Λ1 Λ2 x := by leibniz_lie Λ1 Λ2 x := by
simp [mulVec_add, Bracket.bracket, sub_mulVec] simp [mulVec_add, Bracket.bracket, sub_mulVec]

3
HepLean/SpaceTime/Metric.lean
View file

@ -248,9 +248,6 @@ lemma ηLin_matrix_eq_identity_iff (Λ : Matrix (Fin 4) (Fin 4) ℝ) :
/-- The metric as a quadratic form on `spaceTime`. -/ /-- The metric as a quadratic form on `spaceTime`. -/
def quadraticForm : QuadraticForm ℝ spaceTime := ηLin.toQuadraticForm def quadraticForm : QuadraticForm ℝ spaceTime := ηLin.toQuadraticForm
@[simps!]
def ηTensor : (spaceTime ⊗[ℝ] spaceTime) →ₗ[ℝ] ℝ :=
TensorProduct.lift ηLin