From 9ec574645117ed5adaa4751b6fa537089304c0c4 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Thu, 24 Oct 2024 16:47:32 +0000 Subject: [PATCH] refactor: Lint --- HepLean/SpaceTime/LorentzVector/AsSelfAdjointMatrix.lean | 8 ++++---- HepLean/SpaceTime/LorentzVector/Complex/Basic.lean | 2 -- HepLean/SpaceTime/PauliMatrices/AsTensor.lean | 4 ---- HepLean/SpaceTime/WeylFermion/Basic.lean | 4 ---- HepLean/SpaceTime/WeylFermion/Unit.lean | 1 - 5 files changed, 4 insertions(+), 15 deletions(-) diff --git a/HepLean/SpaceTime/LorentzVector/AsSelfAdjointMatrix.lean b/HepLean/SpaceTime/LorentzVector/AsSelfAdjointMatrix.lean index 82bec94..62fa0a4 100644 --- a/HepLean/SpaceTime/LorentzVector/AsSelfAdjointMatrix.lean +++ b/HepLean/SpaceTime/LorentzVector/AsSelfAdjointMatrix.lean @@ -52,7 +52,7 @@ lemma toSelfAdjointMatrix_apply_coe (x : LorentzVector 3) : (toSelfAdjointMatrix - x (Sum.inr 1) • PauliMatrix.σ2 - x (Sum.inr 2) • PauliMatrix.σ3 := by rw [toSelfAdjointMatrix_apply] - simp only [Fin.isValue, AddSubgroupClass.coe_sub, selfAdjoint.val_smul] + rfl lemma toSelfAdjointMatrix_stdBasis (i : Fin 1 ⊕ Fin 3) : toSelfAdjointMatrix (LorentzVector.stdBasis i) = PauliMatrix.σSAL i := by @@ -68,21 +68,21 @@ lemma toSelfAdjointMatrix_stdBasis (i : Fin 1 ⊕ Fin 3) : simp only [Fin.isValue, ne_eq, reduceCtorEq, not_false_eq_true, Pi.single_eq_of_ne, zero_smul, Pi.single_eq_same, one_smul, zero_sub, Sum.inr.injEq, one_ne_zero, sub_zero, Fin.reduceEq, PauliMatrix.σSAL, Basis.coe_mk, PauliMatrix.σSAL'] - refine Eq.symm (PauliMatrix.selfAdjoint_ext rfl rfl rfl rfl) + rfl | Sum.inr 1 => simp only [LorentzVector.stdBasis, Fin.isValue] erw [Pi.basisFun_apply] simp only [Fin.isValue, ne_eq, reduceCtorEq, not_false_eq_true, Pi.single_eq_of_ne, zero_smul, Sum.inr.injEq, zero_ne_one, sub_self, Pi.single_eq_same, one_smul, zero_sub, Fin.reduceEq, sub_zero, PauliMatrix.σSAL, Basis.coe_mk, PauliMatrix.σSAL'] - refine Eq.symm (PauliMatrix.selfAdjoint_ext rfl rfl rfl rfl) + rfl | Sum.inr 2 => simp only [LorentzVector.stdBasis, Fin.isValue] erw [Pi.basisFun_apply] simp only [Fin.isValue, ne_eq, reduceCtorEq, not_false_eq_true, Pi.single_eq_of_ne, zero_smul, Sum.inr.injEq, Fin.reduceEq, sub_self, Pi.single_eq_same, one_smul, zero_sub, PauliMatrix.σSAL, Basis.coe_mk, PauliMatrix.σSAL'] - refine Eq.symm (PauliMatrix.selfAdjoint_ext rfl rfl rfl rfl) + rfl @[simp] lemma toSelfAdjointMatrix_symm_basis (i : Fin 1 ⊕ Fin 3) : diff --git a/HepLean/SpaceTime/LorentzVector/Complex/Basic.lean b/HepLean/SpaceTime/LorentzVector/Complex/Basic.lean index b59a393..aeed668 100644 --- a/HepLean/SpaceTime/LorentzVector/Complex/Basic.lean +++ b/HepLean/SpaceTime/LorentzVector/Complex/Basic.lean @@ -44,7 +44,6 @@ def complexContrBasis : Basis (Fin 1 ⊕ Fin 3) ℂ complexContr := Basis.ofEqui lemma complexContrBasis_toFin13ℂ (i :Fin 1 ⊕ Fin 3) : (complexContrBasis i).toFin13ℂ = Pi.single i 1 := by simp only [complexContrBasis, Basis.coe_ofEquivFun] - rw [Lorentz.ContrℂModule.toFin13ℂ] rfl @[simp] @@ -72,7 +71,6 @@ def complexCoBasis : Basis (Fin 1 ⊕ Fin 3) ℂ complexCo := Basis.ofEquivFun @[simp] lemma complexCoBasis_toFin13ℂ (i :Fin 1 ⊕ Fin 3) : (complexCoBasis i).toFin13ℂ = Pi.single i 1 := by simp only [complexCoBasis, Basis.coe_ofEquivFun] - rw [Lorentz.CoℂModule.toFin13ℂ] rfl @[simp] diff --git a/HepLean/SpaceTime/PauliMatrices/AsTensor.lean b/HepLean/SpaceTime/PauliMatrices/AsTensor.lean index 5c3da9e..8532ea9 100644 --- a/HepLean/SpaceTime/PauliMatrices/AsTensor.lean +++ b/HepLean/SpaceTime/PauliMatrices/AsTensor.lean @@ -41,10 +41,6 @@ lemma asTensor_expand_complexContrBasis : asTensor = + complexContrBasis (Sum.inr 0) ⊗ₜ leftRightToMatrix.symm (σSA (Sum.inr 0)) + complexContrBasis (Sum.inr 1) ⊗ₜ leftRightToMatrix.symm (σSA (Sum.inr 1)) + complexContrBasis (Sum.inr 2) ⊗ₜ leftRightToMatrix.symm (σSA (Sum.inr 2)) := by - simp only [Action.instMonoidalCategory_tensorObj_V, asTensor, - CategoryTheory.Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor, - Action.FunctorCategoryEquivalence.functor_obj_obj, Fintype.sum_sum_type, Finset.univ_unique, - Fin.default_eq_zero, Fin.isValue, Finset.sum_singleton, Fin.sum_univ_three] rfl /-- The expansion of the pauli matrix `σ₀` in terms of a basis of tensor product vectors. -/ diff --git a/HepLean/SpaceTime/WeylFermion/Basic.lean b/HepLean/SpaceTime/WeylFermion/Basic.lean index d8d6487..3d5e3cb 100644 --- a/HepLean/SpaceTime/WeylFermion/Basic.lean +++ b/HepLean/SpaceTime/WeylFermion/Basic.lean @@ -61,7 +61,6 @@ lemma leftBasis_ρ_apply (M : SL(2,ℂ)) (i j : Fin 2) : @[simp] lemma leftBasis_toFin2ℂ (i : Fin 2) : (leftBasis i).toFin2ℂ = Pi.single i 1 := by simp only [leftBasis, Basis.coe_ofEquivFun] - rw [LeftHandedModule.toFin2ℂ] rfl /-- The vector space ℂ^2 carrying the representation of SL(2,C) given by @@ -94,7 +93,6 @@ def altLeftBasis : Basis (Fin 2) ℂ altLeftHanded := Basis.ofEquivFun @[simp] lemma altLeftBasis_toFin2ℂ (i : Fin 2) : (altLeftBasis i).toFin2ℂ = Pi.single i 1 := by simp only [altLeftBasis, Basis.coe_ofEquivFun] - rw [AltLeftHandedModule.toFin2ℂ] rfl @[simp] @@ -132,7 +130,6 @@ def rightBasis : Basis (Fin 2) ℂ rightHanded := Basis.ofEquivFun @[simp] lemma rightBasis_toFin2ℂ (i : Fin 2) : (rightBasis i).toFin2ℂ = Pi.single i 1 := by simp only [rightBasis, Basis.coe_ofEquivFun] - rw [RightHandedModule.toFin2ℂ] rfl @[simp] @@ -174,7 +171,6 @@ def altRightBasis : Basis (Fin 2) ℂ altRightHanded := Basis.ofEquivFun @[simp] lemma altRightBasis_toFin2ℂ (i : Fin 2) : (altRightBasis i).toFin2ℂ = Pi.single i 1 := by simp only [altRightBasis, Basis.coe_ofEquivFun] - rw [AltRightHandedModule.toFin2ℂ] rfl @[simp] diff --git a/HepLean/SpaceTime/WeylFermion/Unit.lean b/HepLean/SpaceTime/WeylFermion/Unit.lean index accba8a..e9df80d 100644 --- a/HepLean/SpaceTime/WeylFermion/Unit.lean +++ b/HepLean/SpaceTime/WeylFermion/Unit.lean @@ -7,7 +7,6 @@ import HepLean.SpaceTime.WeylFermion.Basic import HepLean.SpaceTime.WeylFermion.Contraction import Mathlib.LinearAlgebra.TensorProduct.Matrix import HepLean.SpaceTime.WeylFermion.Two -import LLMLean /-! # Units of Weyl fermions