From a438af453daf1e0445bc9e9a19acd5dd5a6a7912 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 30 Jul 2024 08:07:47 -0400 Subject: [PATCH] refactor: Linting --- HepLean.lean | 4 +- .../AnomalyCancellation/PureU1/ConstAbs.lean | 2 +- .../PureU1/Even/BasisLinear.lean | 2 +- .../PureU1/Odd/BasisLinear.lean | 2 +- .../PureU1/{Sort.lean => Sorts.lean} | 0 .../PureU1/VectorLike.lean | 2 +- HepLean/SpaceTime/LorentzTensor/Basic.lean | 7 +- .../{Contractions.lean => Contraction.lean} | 13 --- HepLean/SpaceTime/LorentzTensor/Fin.lean | 3 + .../LorentzTensor/MulActionTensor.lean | 6 +- .../SpaceTime/LorentzTensor/Real/Basic.lean | 104 +++++++++--------- .../SpaceTime/LorentzVector/Contraction.lean | 12 ++ .../SpaceTime/LorentzVector/Covariant.lean | 5 +- .../LorentzVector/LorentzAction.lean | 1 - 14 files changed, 87 insertions(+), 76 deletions(-) rename HepLean/AnomalyCancellation/PureU1/{Sort.lean => Sorts.lean} (100%) rename HepLean/SpaceTime/LorentzTensor/{Contractions.lean => Contraction.lean} (93%) diff --git a/HepLean.lean b/HepLean.lean index f8931b7..840ed79 100644 --- a/HepLean.lean +++ b/HepLean.lean @@ -23,7 +23,7 @@ import HepLean.AnomalyCancellation.PureU1.Odd.BasisLinear import HepLean.AnomalyCancellation.PureU1.Odd.LineInCubic import HepLean.AnomalyCancellation.PureU1.Odd.Parameterization import HepLean.AnomalyCancellation.PureU1.Permutations -import HepLean.AnomalyCancellation.PureU1.Sort +import HepLean.AnomalyCancellation.PureU1.Sorts import HepLean.AnomalyCancellation.PureU1.VectorLike import HepLean.AnomalyCancellation.SM.Basic import HepLean.AnomalyCancellation.SM.FamilyMaps @@ -71,7 +71,7 @@ import HepLean.SpaceTime.LorentzGroup.Proper import HepLean.SpaceTime.LorentzGroup.Restricted import HepLean.SpaceTime.LorentzGroup.Rotations import HepLean.SpaceTime.LorentzTensor.Basic -import HepLean.SpaceTime.LorentzTensor.Contractions +import HepLean.SpaceTime.LorentzTensor.Contraction import HepLean.SpaceTime.LorentzTensor.Fin import HepLean.SpaceTime.LorentzTensor.MulActionTensor import HepLean.SpaceTime.LorentzTensor.Notation diff --git a/HepLean/AnomalyCancellation/PureU1/ConstAbs.lean b/HepLean/AnomalyCancellation/PureU1/ConstAbs.lean index 795653a..cf6882e 100644 --- a/HepLean/AnomalyCancellation/PureU1/ConstAbs.lean +++ b/HepLean/AnomalyCancellation/PureU1/ConstAbs.lean @@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ -import HepLean.AnomalyCancellation.PureU1.Sort +import HepLean.AnomalyCancellation.PureU1.Sorts import HepLean.AnomalyCancellation.PureU1.VectorLike /-! # Charges assignments with constant abs diff --git a/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean b/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean index 06f2707..6002430 100644 --- a/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean +++ b/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean @@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ -import HepLean.AnomalyCancellation.PureU1.Sort +import HepLean.AnomalyCancellation.PureU1.Sorts import HepLean.AnomalyCancellation.PureU1.BasisLinear import HepLean.AnomalyCancellation.PureU1.VectorLike import Mathlib.Logic.Equiv.Fin diff --git a/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean b/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean index d8ef7b7..40b3b65 100644 --- a/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean +++ b/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean @@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ -import HepLean.AnomalyCancellation.PureU1.Sort +import HepLean.AnomalyCancellation.PureU1.Sorts import HepLean.AnomalyCancellation.PureU1.BasisLinear import HepLean.AnomalyCancellation.PureU1.VectorLike import Mathlib.Logic.Equiv.Fin diff --git a/HepLean/AnomalyCancellation/PureU1/Sort.lean b/HepLean/AnomalyCancellation/PureU1/Sorts.lean similarity index 100% rename from HepLean/AnomalyCancellation/PureU1/Sort.lean rename to HepLean/AnomalyCancellation/PureU1/Sorts.lean diff --git a/HepLean/AnomalyCancellation/PureU1/VectorLike.lean b/HepLean/AnomalyCancellation/PureU1/VectorLike.lean index 7452348..d7d8170 100644 --- a/HepLean/AnomalyCancellation/PureU1/VectorLike.lean +++ b/HepLean/AnomalyCancellation/PureU1/VectorLike.lean @@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ -import HepLean.AnomalyCancellation.PureU1.Sort +import HepLean.AnomalyCancellation.PureU1.Sorts import Mathlib.Logic.Equiv.Fin /-! # Vector like charges diff --git a/HepLean/SpaceTime/LorentzTensor/Basic.lean b/HepLean/SpaceTime/LorentzTensor/Basic.lean index 62d3fd5..eb592e3 100644 --- a/HepLean/SpaceTime/LorentzTensor/Basic.lean +++ b/HepLean/SpaceTime/LorentzTensor/Basic.lean @@ -34,6 +34,7 @@ open TensorProduct variable {R : Type} [CommSemiring R] +/-- An auxillary function to contract the vector space `V1` and `V2` in `V1 ⊗[R] V2 ⊗[R] V3`. -/ def contrDualLeftAux {V1 V2 V3 : Type} [AddCommMonoid V1] [AddCommMonoid V2] [AddCommMonoid V3] [Module R V1] [Module R V2] [Module R V3] (f : V1 ⊗[R] V2 →ₗ[R] R) : V1 ⊗[R] V2 ⊗[R] V3 →ₗ[R] V3 := @@ -41,9 +42,11 @@ def contrDualLeftAux {V1 V2 V3 : Type} [AddCommMonoid V1] [AddCommMonoid V2] [Ad TensorProduct.map (f) (LinearEquiv.refl R V3).toLinearMap ∘ₗ (TensorProduct.assoc R _ _ _).symm.toLinearMap +/-- An auxillary function to contract the vector space `V1` and `V2` in + `V4 ⊗[R] V1 ⊗[R] V2 ⊗[R] V3`. -/ def contrDualMidAux {V1 V2 V3 V4 : Type} [AddCommMonoid V1] [AddCommMonoid V2] [AddCommMonoid V3] - [AddCommMonoid V4] [Module R V1] [Module R V2] [Module R V3] [Module R V4] (f : V1 ⊗[R] V2 →ₗ[R] R) : - (V4 ⊗[R] V1) ⊗[R] (V2 ⊗[R] V3) →ₗ[R] V4 ⊗[R] V3 := + [AddCommMonoid V4] [Module R V1] [Module R V2] [Module R V3] [Module R V4] + (f : V1 ⊗[R] V2 →ₗ[R] R) : (V4 ⊗[R] V1) ⊗[R] (V2 ⊗[R] V3) →ₗ[R] V4 ⊗[R] V3 := (TensorProduct.map (LinearEquiv.refl R V4).toLinearMap (contrDualLeftAux f)) ∘ₗ (TensorProduct.assoc R _ _ _).toLinearMap diff --git a/HepLean/SpaceTime/LorentzTensor/Contractions.lean b/HepLean/SpaceTime/LorentzTensor/Contraction.lean similarity index 93% rename from HepLean/SpaceTime/LorentzTensor/Contractions.lean rename to HepLean/SpaceTime/LorentzTensor/Contraction.lean index fe92d54..782a131 100644 --- a/HepLean/SpaceTime/LorentzTensor/Contractions.lean +++ b/HepLean/SpaceTime/LorentzTensor/Contraction.lean @@ -51,25 +51,12 @@ variable {d : ℕ} {X Y Y' Z W : Type} [Fintype X] [DecidableEq X] [Fintype Y] [ -/ -def contrDualLeftAux {V1 V2 V3 : Type} [AddCommMonoid V1] [AddCommMonoid V2] [AddCommMonoid V3] - [Module R V1] [Module R V2] [Module R V3] (f : V1 ⊗[R] V2 →ₗ[R] R) : - V1 ⊗[R] V2 ⊗[R] V3 →ₗ[R] V3 := - (TensorProduct.lid R _).toLinearMap ∘ₗ - TensorProduct.map (f) (LinearEquiv.refl R V3).toLinearMap - ∘ₗ (TensorProduct.assoc R _ _ _).symm.toLinearMap - /-- The contraction of a vector in `𝓣.ColorModule ν` with a vector in `𝓣.ColorModule (𝓣.τ ν) ⊗[R] 𝓣.ColorModule η` to form a vector in `𝓣.ColorModule η`. -/ def contrDualLeft {ν η : 𝓣.Color} : 𝓣.ColorModule ν ⊗[R] 𝓣.ColorModule (𝓣.τ ν) ⊗[R] 𝓣.ColorModule η →ₗ[R] 𝓣.ColorModule η := contrDualLeftAux (𝓣.contrDual ν) -def contrDualMidAux {V1 V2 V3 V4 : Type} [AddCommMonoid V1] [AddCommMonoid V2] [AddCommMonoid V3] - [AddCommMonoid V4] [Module R V1] [Module R V2] [Module R V3] [Module R V4] (f : V1 ⊗[R] V2 →ₗ[R] R) : - (V4 ⊗[R] V1) ⊗[R] (V2 ⊗[R] V3) →ₗ[R] V4 ⊗[R] V3 := - (TensorProduct.map (LinearEquiv.refl R V4).toLinearMap (contrDualLeftAux f)) ∘ₗ - (TensorProduct.assoc R _ _ _).toLinearMap - /-- The contraction of a vector in `𝓣.ColorModule μ ⊗[R] 𝓣.ColorModule ν` with a vector in `𝓣.ColorModule (𝓣.τ ν) ⊗[R] 𝓣.ColorModule η` to form a vector in `𝓣.ColorModule μ ⊗[R] 𝓣.ColorModule η`. -/ diff --git a/HepLean/SpaceTime/LorentzTensor/Fin.lean b/HepLean/SpaceTime/LorentzTensor/Fin.lean index 26fe05a..745e33b 100644 --- a/HepLean/SpaceTime/LorentzTensor/Fin.lean +++ b/HepLean/SpaceTime/LorentzTensor/Fin.lean @@ -35,10 +35,13 @@ variable {d : ℕ} {X Y Y' Z W : Type} [Fintype X] [DecidableEq X] [Fintype Y] [ {cW : W → 𝓣.Color} {cY' : Y' → 𝓣.Color} {μ ν: 𝓣.Color} {cn : Fin n → 𝓣.Color} {cm : Fin m → 𝓣.Color} +/-- Casting a tensor defined on `Fin n` to `Fin m` where `n = m`. -/ @[simp] def finCast (h : n = m) (hc : cn = cm ∘ Fin.castOrderIso h) : 𝓣.Tensor cn ≃ₗ[R] 𝓣.Tensor cm := 𝓣.mapIso (Fin.castOrderIso h) hc +/-- An equivalence between `𝓣.Tensor cn ⊗[R] 𝓣.Tensor cm` indexed by `Fin n` and `Fin m`, + and `𝓣.Tensor (Sum.elim cn cm ∘ finSumFinEquiv.symm)` indexed by `Fin (n + m)`. -/ @[simp] def finSumEquiv : 𝓣.Tensor cn ⊗[R] 𝓣.Tensor cm ≃ₗ[R] 𝓣.Tensor (Sum.elim cn cm ∘ finSumFinEquiv.symm) := diff --git a/HepLean/SpaceTime/LorentzTensor/MulActionTensor.lean b/HepLean/SpaceTime/LorentzTensor/MulActionTensor.lean index c2afbb5..1589170 100644 --- a/HepLean/SpaceTime/LorentzTensor/MulActionTensor.lean +++ b/HepLean/SpaceTime/LorentzTensor/MulActionTensor.lean @@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ -import HepLean.SpaceTime.LorentzTensor.Contractions +import HepLean.SpaceTime.LorentzTensor.Contraction import Mathlib.RepresentationTheory.Basic /-! @@ -19,6 +19,8 @@ variable {R : Type} [CommSemiring R] /-! TODO: Add preservation of the unit, and the metric. -/ +/-- A multiplicative action on a tensor structure (e.g. the action of the Lorentz + group on real Lorentz tensors). -/ class MulActionTensor (G : Type) [Monoid G] (𝓣 : TensorStructure R) where /-- For each color `μ` a representation of `G` on `ColorModule μ`. -/ repColorModule : (μ : 𝓣.Color) → Representation R G (𝓣.ColorModule μ) @@ -42,12 +44,14 @@ variable {d : ℕ} {X Y Y' Z : Type} [Fintype X] [DecidableEq X] [Fintype Y] [De -/ +/-- The `MulActionTensor` defined by restriction along a group homomorphism. -/ def compHom (f : H →* G) : MulActionTensor H 𝓣 where repColorModule μ := MonoidHom.comp (repColorModule μ) f contrDual_inv μ h := by simp only [MonoidHom.coe_comp, Function.comp_apply] rw [contrDual_inv] +/-- The trivial `MulActionTensor` defined via trivial representations. -/ def trivial : MulActionTensor G 𝓣 where repColorModule μ := Representation.trivial R contrDual_inv μ g := by diff --git a/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean index 41bad45..2196328 100644 --- a/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean +++ b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean @@ -23,6 +23,8 @@ variable {d : ℕ} ## Definitions and lemmas needed to define a `LorentzTensorStructure` -/ + +/-- The type colors for real Lorentz tensors. -/ inductive ColorType | up | down @@ -34,57 +36,57 @@ open realTensor /-! TODO: Set up the notation `𝓛𝓣ℝ` or similar. -/ /-- The `LorentzTensorStructure` associated with real Lorentz tensors. -/ def realLorentzTensor (d : ℕ) : TensorStructure ℝ where - Color := ColorType - ColorModule μ := - match μ with - | .up => LorentzVector d - | .down => CovariantLorentzVector d - τ μ := - match μ with - | .up => .down - | .down => .up - τ_involutive μ := - match μ with - | .up => rfl - | .down => rfl - colorModule_addCommMonoid μ := - match μ with - | .up => instAddCommMonoidLorentzVector d - | .down => instAddCommMonoidCovariantLorentzVector d - colorModule_module μ := - match μ with - | .up => instModuleRealLorentzVector d - | .down => instModuleRealCovariantLorentzVector d - contrDual μ := - match μ with - | .up => LorentzVector.contrUpDown - | .down => LorentzVector.contrDownUp - contrDual_symm μ := - match μ with - | .up => by - intro x y - simp only [LorentzVector.contrDownUp, Equiv.cast_refl, Equiv.refl_apply, LinearMap.coe_comp, - LinearEquiv.coe_coe, Function.comp_apply, comm_tmul] - | .down => by - intro x y - simp only [LorentzVector.contrDownUp, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, - comm_tmul, Equiv.cast_refl, Equiv.refl_apply] - unit μ := - match μ with - | .up => LorentzVector.unitUp - | .down => LorentzVector.unitDown - unit_lid μ := - match μ with - | .up => LorentzVector.unitUp_lid - | .down => LorentzVector.unitDown_lid - metric μ := - match μ with - | realTensor.ColorType.up => asProdLorentzVector - | realTensor.ColorType.down => asProdCovariantLorentzVector - metric_dual μ := - match μ with - | realTensor.ColorType.up => asProdLorentzVector_contr_asCovariantProdLorentzVector - | realTensor.ColorType.down => asProdCovariantLorentzVector_contr_asProdLorentzVector + Color := ColorType + ColorModule μ := + match μ with + | .up => LorentzVector d + | .down => CovariantLorentzVector d + τ μ := + match μ with + | .up => .down + | .down => .up + τ_involutive μ := + match μ with + | .up => rfl + | .down => rfl + colorModule_addCommMonoid μ := + match μ with + | .up => instAddCommMonoidLorentzVector d + | .down => instAddCommMonoidCovariantLorentzVector d + colorModule_module μ := + match μ with + | .up => instModuleRealLorentzVector d + | .down => instModuleRealCovariantLorentzVector d + contrDual μ := + match μ with + | .up => LorentzVector.contrUpDown + | .down => LorentzVector.contrDownUp + contrDual_symm μ := + match μ with + | .up => by + intro x y + simp only [LorentzVector.contrDownUp, Equiv.cast_refl, Equiv.refl_apply, LinearMap.coe_comp, + LinearEquiv.coe_coe, Function.comp_apply, comm_tmul] + | .down => by + intro x y + simp only [LorentzVector.contrDownUp, LinearMap.coe_comp, LinearEquiv.coe_coe, + Function.comp_apply, comm_tmul, Equiv.cast_refl, Equiv.refl_apply] + unit μ := + match μ with + | .up => LorentzVector.unitUp + | .down => LorentzVector.unitDown + unit_lid μ := + match μ with + | .up => LorentzVector.unitUp_lid + | .down => LorentzVector.unitDown_lid + metric μ := + match μ with + | realTensor.ColorType.up => asProdLorentzVector + | realTensor.ColorType.down => asProdCovariantLorentzVector + metric_dual μ := + match μ with + | realTensor.ColorType.up => asProdLorentzVector_contr_asCovariantProdLorentzVector + | realTensor.ColorType.down => asProdCovariantLorentzVector_contr_asProdLorentzVector /-- The action of the Lorentz group on real Lorentz tensors. -/ instance : MulActionTensor (LorentzGroup d) (realLorentzTensor d) where diff --git a/HepLean/SpaceTime/LorentzVector/Contraction.lean b/HepLean/SpaceTime/LorentzVector/Contraction.lean index 7238c20..0e0001c 100644 --- a/HepLean/SpaceTime/LorentzVector/Contraction.lean +++ b/HepLean/SpaceTime/LorentzVector/Contraction.lean @@ -27,6 +27,8 @@ namespace LorentzVector open Matrix variable {d : ℕ} (v : LorentzVector d) +/-- The bi-linear map defining the contraction of a contravariant Lorentz vector + and a covariant Lorentz vector. -/ def contrUpDownBi : LorentzVector d →ₗ[ℝ] CovariantLorentzVector d →ₗ[ℝ] ℝ where toFun v := { toFun := fun w => ∑ i, v i * w i, @@ -57,6 +59,8 @@ def contrUpDownBi : LorentzVector d →ₗ[ℝ] CovariantLorentzVector d →ₗ[ simp only [RingHom.id, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk, id_eq] ring +/-- The linear map defining the contraction of a contravariant Lorentz vector + and a covariant Lorentz vector. -/ def contrUpDown : LorentzVector d ⊗[ℝ] CovariantLorentzVector d →ₗ[ℝ] ℝ := TensorProduct.lift contrUpDownBi @@ -93,6 +97,8 @@ lemma contrUpDown_stdBasis_right (x : CovariantLorentzVector d) (i : Fin 1 ⊕ F simp only [LinearMap.stdBasis_apply', ite_eq_right_iff, one_ne_zero, imp_false] exact Or.intro_left (x b = 0) (id (Ne.symm hbi)) +/-- The linear map defining the contraction of a covariant Lorentz vector + and a contravariant Lorentz vector. -/ def contrDownUp : CovariantLorentzVector d ⊗[ℝ] LorentzVector d →ₗ[ℝ] ℝ := contrUpDown ∘ₗ (TensorProduct.comm ℝ _ _).toLinearMap @@ -107,6 +113,8 @@ lemma contrDownUp_tmul_eq_dotProduct {x : CovariantLorentzVector d} {y : Lorentz -/ +/-- The unit of the contraction of contravariant Lorentz vector and a + covariant Lorentz vector. -/ def unitUp : LorentzVector d ⊗[ℝ] CovariantLorentzVector d := ∑ i, LorentzVector.stdBasis i ⊗ₜ[ℝ] CovariantLorentzVector.stdBasis i @@ -122,6 +130,8 @@ lemma unitUp_lid (x : LorentzVector d) : LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, comm_tmul, contrUpDown_stdBasis_left, rid_tmul, decomp_stdBasis'] +/-- The unit of the contraction of covariant Lorentz vector and a + contravariant Lorentz vector. -/ def unitDown : CovariantLorentzVector d ⊗[ℝ] LorentzVector d := ∑ i, CovariantLorentzVector.stdBasis i ⊗ₜ[ℝ] LorentzVector.stdBasis i @@ -168,9 +178,11 @@ open LorentzVector open scoped minkowskiMatrix variable {d : ℕ} +/-- The metric tensor as an element of `LorentzVector d ⊗[ℝ] LorentzVector d`. -/ def asProdLorentzVector : LorentzVector d ⊗[ℝ] LorentzVector d := ∑ μ, η μ μ • (LorentzVector.stdBasis μ ⊗ₜ[ℝ] LorentzVector.stdBasis μ) +/-- The metric tensor as an element of `CovariantLorentzVector d ⊗[ℝ] CovariantLorentzVector d`. -/ def asProdCovariantLorentzVector : CovariantLorentzVector d ⊗[ℝ] CovariantLorentzVector d := ∑ μ, η μ μ • (CovariantLorentzVector.stdBasis μ ⊗ₜ[ℝ] CovariantLorentzVector.stdBasis μ) diff --git a/HepLean/SpaceTime/LorentzVector/Covariant.lean b/HepLean/SpaceTime/LorentzVector/Covariant.lean index 1e81d32..b2e799b 100644 --- a/HepLean/SpaceTime/LorentzVector/Covariant.lean +++ b/HepLean/SpaceTime/LorentzVector/Covariant.lean @@ -61,7 +61,8 @@ lemma decomp_stdBasis (v : CovariantLorentzVector d) : ∑ i, v i • stdBasis i @[simp] lemma decomp_stdBasis' (v : CovariantLorentzVector d) : - v (Sum.inl 0) • stdBasis (Sum.inl 0) + ∑ a₂ : Fin d, v (Sum.inr a₂) • stdBasis (Sum.inr a₂) = v := by + v (Sum.inl 0) • stdBasis (Sum.inl 0) + + ∑ a₂ : Fin d, v (Sum.inr a₂) • stdBasis (Sum.inr a₂) = v := by trans ∑ i, v i • stdBasis i simp only [Fin.isValue, Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton] @@ -83,7 +84,7 @@ def rep : Representation ℝ (LorentzGroup d) (CovariantLorentzVector d) where lorentzGroupIsGroup_mul_coe, map_mul] open Matrix in -@[simp] + lemma rep_apply (g : LorentzGroup d) : rep g v = (g.1⁻¹)ᵀ *ᵥ v := by trans (LorentzGroup.transpose g⁻¹) *ᵥ v rfl diff --git a/HepLean/SpaceTime/LorentzVector/LorentzAction.lean b/HepLean/SpaceTime/LorentzVector/LorentzAction.lean index d4b0944..40ad4d1 100644 --- a/HepLean/SpaceTime/LorentzVector/LorentzAction.lean +++ b/HepLean/SpaceTime/LorentzVector/LorentzAction.lean @@ -26,7 +26,6 @@ def rep : Representation ℝ (LorentzGroup d) (LorentzVector d) where simp only [lorentzGroupIsGroup_mul_coe, map_mul] open Matrix in -@[simp] lemma rep_apply (g : LorentzGroup d) : rep g v = g *ᵥ v := rfl end LorentzVector