refactor: Lint
This commit is contained in:
jstoobysmith
parent
255ea5ffd7
commit
a60ade65f0
5 changed files with 21 additions and 19 deletions
|
|
@ -82,6 +82,11 @@ import HepLean.SpaceTime.LorentzTensor.Real.Basic
|
|||
import HepLean.SpaceTime.LorentzTensor.Real.IndexNotation
|
||||
import HepLean.SpaceTime.LorentzVector.AsSelfAdjointMatrix
|
||||
import HepLean.SpaceTime.LorentzVector.Basic
|
||||
import HepLean.SpaceTime.LorentzVector.Complex.Basic
|
||||
import HepLean.SpaceTime.LorentzVector.Complex.Contraction
|
||||
import HepLean.SpaceTime.LorentzVector.Complex.Metric
|
||||
import HepLean.SpaceTime.LorentzVector.Complex.Two
|
||||
import HepLean.SpaceTime.LorentzVector.Complex.Unit
|
||||
import HepLean.SpaceTime.LorentzVector.Contraction
|
||||
import HepLean.SpaceTime.LorentzVector.Covariant
|
||||
import HepLean.SpaceTime.LorentzVector.LorentzAction
|
||||
|
|
|
|||
|
|
@ -5,7 +5,6 @@ Authors: Joseph Tooby-Smith
|
|||
-/
|
||||
import HepLean.SpaceTime.MinkowskiMetric
|
||||
import HepLean.SpaceTime.LorentzVector.NormOne
|
||||
import LLMLean
|
||||
/-!
|
||||
# The Lorentz Group
|
||||
|
||||
|
|
@ -298,18 +297,18 @@ def toComplex : LorentzGroup d →* Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d)
|
|||
toFun Λ := Λ.1.map ofReal
|
||||
map_one' := by
|
||||
ext i j
|
||||
simp
|
||||
simp only [lorentzGroupIsGroup_one_coe, map_apply, ofReal_eq_coe]
|
||||
simp only [Matrix.one_apply, ofReal_one, ofReal_zero]
|
||||
split_ifs
|
||||
· rfl
|
||||
· rfl
|
||||
map_mul' Λ Λ' := by
|
||||
ext i j
|
||||
simp
|
||||
simp only [lorentzGroupIsGroup_mul_coe, map_apply, ofReal_eq_coe]
|
||||
simp only [← Matrix.map_mul, RingHom.map_matrix_mul]
|
||||
rfl
|
||||
|
||||
instance (M : LorentzGroup d ) : Invertible (toComplex M) where
|
||||
instance (M : LorentzGroup d) : Invertible (toComplex M) where
|
||||
invOf := toComplex M⁻¹
|
||||
invOf_mul_self := by
|
||||
rw [← toComplex.map_mul, Group.inv_mul_cancel]
|
||||
|
|
@ -319,7 +318,7 @@ instance (M : LorentzGroup d ) : Invertible (toComplex M) where
|
|||
rw [@mul_inv_cancel]
|
||||
simp
|
||||
|
||||
lemma toComplex_inv (Λ : LorentzGroup d) : (toComplex Λ)⁻¹ = toComplex Λ⁻¹ := by
|
||||
lemma toComplex_inv (Λ : LorentzGroup d) : (toComplex Λ)⁻¹ = toComplex Λ⁻¹ := by
|
||||
refine inv_eq_right_inv ?h
|
||||
rw [← toComplex.map_mul, mul_inv_cancel]
|
||||
simp
|
||||
|
|
@ -340,7 +339,7 @@ lemma toComplex_transpose_mul_minkowskiMatrix_mul_self (Λ : LorentzGroup d) :
|
|||
simp [toComplex]
|
||||
have h1 : ((Λ.1).map ⇑ofReal)ᵀ = (Λ.1ᵀ).map ofReal := rfl
|
||||
rw [h1]
|
||||
trans (Λ.1ᵀ * minkowskiMatrix * Λ.1).map ofReal
|
||||
trans (Λ.1ᵀ * minkowskiMatrix * Λ.1).map ofReal
|
||||
· simp only [Matrix.map_mul]
|
||||
simp only [transpose_mul_minkowskiMatrix_mul_self]
|
||||
|
||||
|
|
|
|||
|
|
@ -8,7 +8,6 @@ import HepLean.SpaceTime.LorentzVector.Complex.Basic
|
|||
|
||||
# Contraction of Lorentz vectors
|
||||
|
||||
|
||||
-/
|
||||
|
||||
noncomputable section
|
||||
|
|
@ -91,7 +90,7 @@ def contrCoContraction : complexContr ⊗ complexCo ⟶ 𝟙_ (Rep ℂ SL(2,ℂ)
|
|||
def coContrContraction : complexCo ⊗ complexContr ⟶ 𝟙_ (Rep ℂ SL(2,ℂ)) where
|
||||
hom := TensorProduct.lift contrContrCoBi
|
||||
comm M := TensorProduct.ext' fun φ ψ => by
|
||||
change ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ *ᵥ φ.toFin13ℂ) ⬝ᵥ
|
||||
change ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ *ᵥ φ.toFin13ℂ) ⬝ᵥ
|
||||
((LorentzGroup.toComplex (SL2C.toLorentzGroup M)) *ᵥ ψ.toFin13ℂ) = φ.toFin13ℂ ⬝ᵥ ψ.toFin13ℂ
|
||||
rw [dotProduct_mulVec, mulVec_transpose, vecMul_vecMul]
|
||||
rw [inv_mul_of_invertible (LorentzGroup.toComplex (SL2C.toLorentzGroup M))]
|
||||
|
|
|
|||
|
|
@ -80,9 +80,9 @@ lemma contrContrToMatrix_ρ (v : (complexContr ⊗ complexContr).V) (M : SL(2,
|
|||
* contrContrToMatrix v k.1 k.2) = _
|
||||
erw [Finset.sum_product]
|
||||
simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
|
||||
have h1 : ∑ x, (∑ x1 , LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 *
|
||||
have h1 : ∑ x, (∑ x1, LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 *
|
||||
contrContrToMatrix v x1 x) * LorentzGroup.toComplex (SL2C.toLorentzGroup M) j x
|
||||
= ∑ x , ∑ x1 , (LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1
|
||||
= ∑ x, ∑ x1, (LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1
|
||||
* contrContrToMatrix v x1 x) * LorentzGroup.toComplex (SL2C.toLorentzGroup M) j x := by
|
||||
congr
|
||||
funext x
|
||||
|
|
@ -122,9 +122,9 @@ lemma coCoToMatrix_ρ (v : (complexCo ⊗ complexCo).V) (M : SL(2,ℂ)) :
|
|||
* coCoToMatrix v k.1 k.2) = _
|
||||
erw [Finset.sum_product]
|
||||
simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
|
||||
have h1 : ∑ x, (∑ x1 , (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i *
|
||||
have h1 : ∑ x, (∑ x1, (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i *
|
||||
coCoToMatrix v x1 x) * (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x j
|
||||
= ∑ x , ∑ x1 , ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i
|
||||
= ∑ x, ∑ x1, ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i
|
||||
* coCoToMatrix v x1 x) * (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x j := by
|
||||
congr
|
||||
funext x
|
||||
|
|
@ -164,9 +164,9 @@ lemma contrCoToMatrix_ρ (v : (complexContr ⊗ complexCo).V) (M : SL(2,ℂ)) :
|
|||
* contrCoToMatrix v k.1 k.2) = _
|
||||
erw [Finset.sum_product]
|
||||
simp_rw [kroneckerMap_apply, Matrix.mul_apply]
|
||||
have h1 : ∑ x, (∑ x1 , LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 *
|
||||
have h1 : ∑ x, (∑ x1, LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 *
|
||||
contrCoToMatrix v x1 x) * (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x j
|
||||
= ∑ x , ∑ x1 , (LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1
|
||||
= ∑ x, ∑ x1, (LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1
|
||||
* contrCoToMatrix v x1 x) * (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x j := by
|
||||
congr
|
||||
funext x
|
||||
|
|
@ -207,9 +207,9 @@ lemma coContrToMatrix_ρ (v : (complexCo ⊗ complexContr).V) (M : SL(2,ℂ)) :
|
|||
* coContrToMatrix v k.1 k.2) = _
|
||||
erw [Finset.sum_product]
|
||||
simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
|
||||
have h1 : ∑ x, (∑ x1 , (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i *
|
||||
have h1 : ∑ x, (∑ x1, (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i *
|
||||
coContrToMatrix v x1 x) * (LorentzGroup.toComplex (SL2C.toLorentzGroup M)) j x
|
||||
= ∑ x , ∑ x1 , ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i
|
||||
= ∑ x, ∑ x1, ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i
|
||||
* coContrToMatrix v x1 x) * (LorentzGroup.toComplex (SL2C.toLorentzGroup M)) j x := by
|
||||
congr
|
||||
funext x
|
||||
|
|
@ -228,7 +228,6 @@ lemma coContrToMatrix_ρ (v : (complexCo ⊗ complexContr).V) (M : SL(2,ℂ)) :
|
|||
|
||||
## The symm version of the group actions.
|
||||
|
||||
|
||||
-/
|
||||
|
||||
lemma contrContrToMatrix_ρ_symm (v : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ) (M : SL(2,ℂ)) :
|
||||
|
|
|
|||
|
|
@ -26,7 +26,7 @@ def contrCoUnitVal : (complexContr ⊗ complexCo).V :=
|
|||
/-- The contra-co unit for complex lorentz vectors as a morphism
|
||||
`𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexContr ⊗ complexCo`, manifesting the invaraince under
|
||||
the `SL(2, ℂ)` action. -/
|
||||
def contrCoUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexContr ⊗ complexCo where
|
||||
def contrCoUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexContr ⊗ complexCo where
|
||||
hom := {
|
||||
toFun := fun a =>
|
||||
let a' : ℂ := a
|
||||
|
|
@ -58,7 +58,7 @@ def coContrUnitVal : (complexCo ⊗ complexContr).V :=
|
|||
/-- The co-contra unit for complex lorentz vectors as a morphism
|
||||
`𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexCo ⊗ complexContr`, manifesting the invaraince under
|
||||
the `SL(2, ℂ)` action. -/
|
||||
def coContrUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexCo ⊗ complexContr where
|
||||
def coContrUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexCo ⊗ complexContr where
|
||||
hom := {
|
||||
toFun := fun a =>
|
||||
let a' : ℂ := a
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue