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

feat: Basis properties of covariant Lorentz vec

Browse source
This commit is contained in:
jstoobysmith 2024-11-08 08:11:21 +00:00
parent 87aae0f879
commit 4192af777e
2 changed files with 36 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

30
HepLean/SpaceTime/LorentzVector/Real/Modules.lean
View file

@ -67,7 +67,6 @@ lemma val_add (ψ ψ' : ContrMod d) : (ψ + ψ').val = ψ.val + ψ'.val := rfl
lemma val_smul (r : ℝ) (ψ : ContrMod d) : (r • ψ).val = r • ψ.val := rfl
/-- The linear equivalence between `ContrℝModule` and `(Fin 1 ⊕ Fin d → ℝ)`. -/
@[simps!]
def toFin1dℝEquiv : ContrMod d ≃ₗ[ℝ] (Fin 1 ⊕ Fin d → ℝ) :=
Equiv.linearEquiv ℝ toFin1dℝFun
@ -117,7 +116,6 @@ instance : AddCommGroup (CoMod d) := Equiv.addCommGroup toFin1dℝFun
instance : Module ℝ (CoMod d) := Equiv.module ℝ toFin1dℝFun
/-- The linear equivalence between `CoℝModule` and `(Fin 1 ⊕ Fin d → ℝ)`. -/
@[simps!]
def toFin1dℝEquiv : CoMod d ≃ₗ[ℝ] (Fin 1 ⊕ Fin d → ℝ) :=
Equiv.linearEquiv ℝ toFin1dℝFun
@ -129,6 +127,34 @@ abbrev toFin1dℝ (ψ : CoMod d) := toFin1dℝEquiv ψ
@[simps!]
def stdBasis : Basis (Fin 1 ⊕ Fin d) ℝ (CoMod d) := Basis.ofEquivFun toFin1dℝEquiv
@[simp]
lemma stdBasis_toFin1dℝEquiv_apply_self (μ : Fin 1 ⊕ Fin d) :
toFin1dℝEquiv (stdBasis μ) μ = 1 := by
simp only [stdBasis, Basis.ofEquivFun, Basis.coe_ofRepr, LinearEquiv.trans_symm,
LinearEquiv.symm_symm, LinearEquiv.trans_apply, Finsupp.linearEquivFunOnFinite_single]
rw [@LinearEquiv.apply_symm_apply]
exact Pi.single_eq_same μ 1
lemma stdBasis_toFin1dℝEquiv_apply_ne {μ ν : Fin 1 ⊕ Fin d} (h : μ ≠ ν) :
toFin1dℝEquiv (stdBasis μ) ν = 0 := by
simp only [stdBasis, Basis.ofEquivFun, Basis.coe_ofRepr, LinearEquiv.trans_symm,
LinearEquiv.symm_symm, LinearEquiv.trans_apply, Finsupp.linearEquivFunOnFinite_single]
rw [@LinearEquiv.apply_symm_apply]
exact Pi.single_eq_of_ne' h 1
/-- Decomposition of a covariant Lorentz vector into the standard basis. -/
lemma stdBasis_decomp (v : CoMod d) : v = ∑ i, v.toFin1dℝ i • stdBasis i := by
apply toFin1dℝEquiv.injective
simp only [map_sum, _root_.map_smul]
funext μ
rw [Fintype.sum_apply μ fun c => toFin1dℝEquiv v c • toFin1dℝEquiv (stdBasis c)]
change _ = ∑ x : Fin 1 ⊕ Fin d, toFin1dℝEquiv v x • (toFin1dℝEquiv (stdBasis x) μ)
rw [Finset.sum_eq_single_of_mem μ (Finset.mem_univ μ)]
· simp only [stdBasis_toFin1dℝEquiv_apply_self, smul_eq_mul, mul_one]
· intro b _ hbμ
rw [stdBasis_toFin1dℝEquiv_apply_ne hbμ]
simp only [smul_eq_mul, mul_zero]
/-- The representation of the Lorentz group acting on `CoℝModule d`. -/
def rep : Representation ℝ (LorentzGroup d) (CoMod d) where
toFun g := Matrix.toLinAlgEquiv stdBasis (LorentzGroup.transpose g⁻¹)

12
HepLean/SpaceTime/PauliMatrices/Basic.lean
View file

@ -18,16 +18,20 @@ namespace PauliMatrix
open Complex
open Matrix
/-- The zeroth Pauli-matrix as a `2 x 2` complex matrix. -/
/-- The zeroth Pauli-matrix as a `2 x 2` complex matrix.
That is the matrix `!![1, 0; 0, 1]`. -/
def σ0 : Matrix (Fin 2) (Fin 2) ℂ := !![1, 0; 0, 1]
/-- The first Pauli-matrix as a `2 x 2` complex matrix. -/
/-- The first Pauli-matrix as a `2 x 2` complex matrix.
That is, the matrix `!![0, 1; 1, 0]`. -/
def σ1 : Matrix (Fin 2) (Fin 2) ℂ := !![0, 1; 1, 0]
/-- The second Pauli-matrix as a `2 x 2` complex matrix. -/
/-- The second Pauli-matrix as a `2 x 2` complex matrix.
That is, the matrix `!![0, -I; I, 0]`. -/
def σ2 : Matrix (Fin 2) (Fin 2) ℂ := !![0, -I; I, 0]
/-- The third Pauli-matrix as a `2 x 2` complex matrix. -/
/-- The third Pauli-matrix as a `2 x 2` complex matrix.
That is, the matrix `!![1, 0; 0, -1]`. -/
def σ3 : Matrix (Fin 2) (Fin 2) ℂ := !![1, 0; 0, -1]
@[simp]