refactor: Adjust Minkowski metric

HepLean/SpaceTime/LorentzGroup/Basic.lean

@@ -3,8 +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.MinkowskiMetric
-import HepLean.SpaceTime.LorentzVector.NormOne
+import HepLean.SpaceTime.MinkowskiMatrix
 /-!
 # The Lorentz Group
 
@@ -32,17 +31,16 @@ These matrices form the Lorentz group, which we will define in the next section
 -/
 variable {d : ℕ}
 
-open minkowskiMetric in
-/-- The Lorentz group is the subset of matrices which preserve the minkowski metric. -/
+open minkowskiMatrix in
+/-- The Lorentz group is the subset of matrices for which
+  `Λ * dual Λ = 1`. -/
 def LorentzGroup (d : ℕ) : Set (Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :=
-    {Λ : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ |
-    ∀ (x y : LorentzVector d), ⟪Λ *ᵥ x, Λ *ᵥ y⟫ₘ = ⟪x, y⟫ₘ}
+    {Λ : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ | Λ * dual Λ = 1}
 
 namespace LorentzGroup
 /-- Notation for the Lorentz group. -/
 scoped[LorentzGroup] notation (name := lorentzGroup_notation) "𝓛" => LorentzGroup
 
-open minkowskiMetric
 open minkowskiMatrix
 variable {Λ Λ' : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ}
 
@@ -52,32 +50,11 @@ variable {Λ Λ' : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ}
 
 -/
 
-lemma mem_iff_norm : Λ ∈ LorentzGroup d ↔
-    ∀ (x : LorentzVector d), ⟪Λ *ᵥ x, Λ *ᵥ x⟫ₘ = ⟪x, x⟫ₘ := by
-  refine Iff.intro (fun h x => h x x) (fun h x y => ?_)
-  have hp := h (x + y)
-  have hn := h (x - y)
-  rw [mulVec_add] at hp
-  rw [mulVec_sub] at hn
-  simp only [map_add, LinearMap.add_apply, map_sub, LinearMap.sub_apply] at hp hn
-  rw [symm (Λ *ᵥ y) (Λ *ᵥ x), symm y x] at hp hn
-  linear_combination hp / 4 + -1 * hn / 4
-
-lemma mem_iff_on_right : Λ ∈ LorentzGroup d ↔
-    ∀ (x y : LorentzVector d), ⟪x, (dual Λ * Λ) *ᵥ y⟫ₘ = ⟪x, y⟫ₘ := by
-  refine Iff.intro (fun h x y ↦ ?_) (fun h x y ↦ ?_)
-  · have h1 := h x y
-    rw [← dual_mulVec_right, mulVec_mulVec] at h1
-    exact h1
-  · rw [← dual_mulVec_right, mulVec_mulVec]
-    exact h x y
+lemma mem_iff_self_mul_dual : Λ ∈ LorentzGroup d ↔ Λ * dual Λ = 1 := by
+  rfl
 
 lemma mem_iff_dual_mul_self : Λ ∈ LorentzGroup d ↔ dual Λ * Λ = 1 := by
-  rw [mem_iff_on_right, matrix_eq_id_iff]
-  exact forall_comm
-
-lemma mem_iff_self_mul_dual : Λ ∈ LorentzGroup d ↔ Λ * dual Λ = 1 := by
-  rw [mem_iff_dual_mul_self]
+  rw [mem_iff_self_mul_dual]
   exact mul_eq_one_comm
 
 lemma mem_iff_transpose : Λ ∈ LorentzGroup d ↔ Λᵀ ∈ LorentzGroup d := by
@@ -108,6 +85,29 @@ lemma dual_mem (h : Λ ∈ LorentzGroup d) : dual Λ ∈ LorentzGroup d := by
   rw [mem_iff_dual_mul_self, dual_dual]
   exact mem_iff_self_mul_dual.mp h
 
+/-
+lemma mem_iff_norm : Λ ∈ LorentzGroup d ↔
+    ∀ (x : LorentzVector d), ⟪Λ *ᵥ x, Λ *ᵥ x⟫ₘ = ⟪x, x⟫ₘ := by
+  refine Iff.intro (fun h x => h x x) (fun h x y => ?_)
+  have hp := h (x + y)
+  have hn := h (x - y)
+  rw [mulVec_add] at hp
+  rw [mulVec_sub] at hn
+  simp only [map_add, LinearMap.add_apply, map_sub, LinearMap.sub_apply] at hp hn
+  rw [symm (Λ *ᵥ y) (Λ *ᵥ x), symm y x] at hp hn
+  linear_combination hp / 4 + -1 * hn / 4
+
+lemma mem_iff_on_right : Λ ∈ LorentzGroup d ↔
+    ∀ (x y : LorentzVector d), ⟪x, (dual Λ * Λ) *ᵥ y⟫ₘ = ⟪x, y⟫ₘ := by
+  refine Iff.intro (fun h x y ↦ ?_) (fun h x y ↦ ?_)
+  · have h1 := h x y
+    rw [← dual_mulVec_right, mulVec_mulVec] at h1
+    exact h1
+  · rw [← dual_mulVec_right, mulVec_mulVec]
+    exact h x y
+
+-/
+
 end LorentzGroup
 
 /-!
@@ -131,7 +131,6 @@ instance : TopologicalSpace (LorentzGroup d) := instTopologicalSpaceSubtype
 
 namespace LorentzGroup
 
-open minkowskiMetric
 open minkowskiMatrix
 
 variable {Λ Λ' : LorentzGroup d}
@@ -285,43 +284,6 @@ lemma toGL_embedding : IsEmbedding (@toGL d).toFun where
 instance : TopologicalGroup (LorentzGroup d) :=
   IsInducing.topologicalGroup toGL toGL_embedding.toIsInducing
 
-section
-open LorentzVector
-/-!
-
-# To a norm one Lorentz vector
-
--/
-
-/-- The first column of a Lorentz matrix as a `NormOneLorentzVector`. -/
-@[simps!]
-def toNormOneLorentzVector (Λ : LorentzGroup d) : NormOneLorentzVector d :=
-  ⟨Λ.1 *ᵥ timeVec, by rw [NormOneLorentzVector.mem_iff, Λ.2, minkowskiMetric.on_timeVec]⟩
-
-/-!
-
-# The time like element
-
--/
-
-/-- The time like element of a Lorentz matrix. -/
-@[simp]
-def timeComp (Λ : LorentzGroup d) : ℝ := Λ.1 (Sum.inl 0) (Sum.inl 0)
-
-lemma timeComp_eq_toNormOneLorentzVector : timeComp Λ = (toNormOneLorentzVector Λ).1.time := by
-  simp only [time, toNormOneLorentzVector, timeVec, Fin.isValue, timeComp]
-  erw [Pi.basisFun_apply, Matrix.mulVec_single_one]
-  rfl
-
-lemma timeComp_mul (Λ Λ' : LorentzGroup d) : timeComp (Λ * Λ') =
-    ⟪toNormOneLorentzVector (transpose Λ), (toNormOneLorentzVector Λ').1.spaceReflection⟫ₘ := by
-  simp only [timeComp, Fin.isValue, lorentzGroupIsGroup_mul_coe, mul_apply, Fintype.sum_sum_type,
-    Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton, toNormOneLorentzVector,
-    transpose, timeVec, right_spaceReflection, time, space, PiLp.inner_apply, Function.comp_apply,
-    RCLike.inner_apply, conj_trivial]
-  erw [Pi.basisFun_apply, Matrix.mulVec_single_one]
-  simp
-
 /-!
 
 ## To Complex matrices
@@ -387,6 +349,46 @@ lemma toComplex_mulVec_ofReal (v : Fin 1 ⊕ Fin d → ℝ) (Λ : LorentzGroup d
   funext i
   rw [← RingHom.map_mulVec]
   rfl
+  /-!
+/-!
+
+# To a norm one Lorentz vector
+
+-/
+
+/-- The first column of a Lorentz matrix as a `NormOneLorentzVector`. -/
+@[simps!]
+def toNormOneLorentzVector (Λ : LorentzGroup d) : NormOneLorentzVector d :=
+  ⟨Λ.1 *ᵥ timeVec, by rw [NormOneLorentzVector.mem_iff, Λ.2, minkowskiMetric.on_timeVec]⟩
+
+/-!
+
+# The time like element
+
+-/
+
+/-- The time like element of a Lorentz matrix. -/
+@[simp]
+def timeComp (Λ : LorentzGroup d) : ℝ := Λ.1 (Sum.inl 0) (Sum.inl 0)
+
+lemma timeComp_eq_toNormOneLorentzVector : timeComp Λ = (toNormOneLorentzVector Λ).1.time := by
+  simp only [time, toNormOneLorentzVector, timeVec, Fin.isValue, timeComp]
+  erw [Pi.basisFun_apply, Matrix.mulVec_single_one]
+  rfl
+
+lemma timeComp_mul (Λ Λ' : LorentzGroup d) : timeComp (Λ * Λ') =
+    ⟪toNormOneLorentzVector (transpose Λ), (toNormOneLorentzVector Λ').1.spaceReflection⟫ₘ := by
+  simp only [timeComp, Fin.isValue, lorentzGroupIsGroup_mul_coe, mul_apply, Fintype.sum_sum_type,
+    Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton, toNormOneLorentzVector,
+    transpose, timeVec, right_spaceReflection, time, space, PiLp.inner_apply, Function.comp_apply,
+    RCLike.inner_apply, conj_trivial]
+  erw [Pi.basisFun_apply, Matrix.mulVec_single_one]
+  simp
+-/
+
+/-- The parity transformation. -/
+def parity : LorentzGroup d := ⟨minkowskiMatrix, by
+  rw [mem_iff_dual_mul_self]
+  simp only [dual_eta, minkowskiMatrix.sq]⟩
 
-end
 end LorentzGroup

HepLean/SpaceTime/LorentzGroup/Proper.lean

@@ -21,7 +21,6 @@ open ComplexConjugate
 
 namespace LorentzGroup
 
-open minkowskiMetric
 open minkowskiMatrix
 
 variable {d : ℕ}

HepLean/SpaceTime/LorentzGroup/Rotations.lean

@@ -43,8 +43,8 @@ lemma SO3ToMatrix_injective : Function.Injective SO3ToMatrix := by
 space-time rotation. -/
 def SO3ToLorentz : SO(3) →* LorentzGroup 3 where
   toFun A := ⟨SO3ToMatrix A, SO3ToMatrix_in_LorentzGroup A⟩
-  map_one' := Subtype.eq <|
-    (minkowskiMetric.matrix_eq_iff_eq_forall _ ↑1).mpr fun w => congrFun rfl
+  map_one' := Subtype.eq <| by
+    simp only [SO3ToMatrix, SO3Group_one_coe, Matrix.fromBlocks_one, lorentzGroupIsGroup_one_coe]
   map_mul' A B := Subtype.eq <| by
     simp only [SO3ToMatrix, SO3Group_mul_coe, lorentzGroupIsGroup_mul_coe,
       Matrix.fromBlocks_multiply, mul_one, Matrix.mul_zero, add_zero, Matrix.zero_mul,

HepLean/SpaceTime/LorentzVector/Real/Basic.lean

@@ -5,8 +5,7 @@ Authors: Joseph Tooby-Smith
 -/
 import Mathlib.Data.Complex.Exponential
 import Mathlib.Analysis.InnerProductSpace.PiL2
-import HepLean.SpaceTime.SL2C.Basic
-import HepLean.SpaceTime.LorentzVector.Complex.Modules
+import HepLean.SpaceTime.LorentzGroup.Basic
 import HepLean.Meta.Informal
 import Mathlib.RepresentationTheory.Rep
 import HepLean.SpaceTime.LorentzVector.Real.Modules
@@ -24,10 +23,8 @@ open Matrix
 open MatrixGroups
 open Complex
 open TensorProduct
-open SpaceTime
 
 namespace Lorentz
-open minkowskiMetric
 open minkowskiMatrix
 /-- The representation of `LorentzGroup d` on real vectors corresponding to contravariant
   Lorentz vectors. In index notation these have an up index `ψⁱ`. -/

HepLean/SpaceTime/LorentzVector/Real/Contraction.lean

@@ -16,7 +16,6 @@ open Matrix
 open MatrixGroups
 open Complex
 open TensorProduct
-open SpaceTime
 open CategoryTheory.MonoidalCategory
 open minkowskiMatrix
 namespace Lorentz
@@ -183,7 +182,6 @@ We derive the lemmas in main for `contrContrContract`.
 namespace contrContrContract
 
 variable (x y : Contr d)
-open minkowskiMetric
 
 lemma as_sum : ⟪x, y⟫ₘ = x.val (Sum.inl 0) * y.val (Sum.inl 0) -
       ∑ i, x.val (Sum.inr i) * y.val (Sum.inr i)  := by
@@ -210,6 +208,114 @@ lemma dual_mulVec_right : ⟪x, dual Λ *ᵥ y⟫ₘ = ⟪Λ *ᵥ x, y⟫ₘ :=
 lemma dual_mulVec_left : ⟪dual Λ *ᵥ x, y⟫ₘ = ⟪x, Λ *ᵥ y⟫ₘ := by
   rw [symm, dual_mulVec_right, symm]
 
+lemma right_parity : ⟪x, (Contr d).ρ LorentzGroup.parity y⟫ₘ =  ∑ i, x.val i * y.val i := by
+  rw [as_sum]
+  simp only [Action.instMonoidalCategory_tensorUnit_V, Fin.isValue, Fintype.sum_sum_type,
+    Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton]
+  trans x.val (Sum.inl 0) * (((Contr d).ρ LorentzGroup.parity) y).val (Sum.inl 0) +
+    ∑ i : Fin d, - (x.val (Sum.inr i) * (((Contr d).ρ LorentzGroup.parity) y).val (Sum.inr i))
+  · simp only [Fin.isValue, Finset.sum_neg_distrib]
+    rfl
+  congr 1
+  · change x.val (Sum.inl 0) * (η *ᵥ y.toFin1dℝ) (Sum.inl 0) = _
+    simp only [Fin.isValue, mulVec_inl_0, mul_eq_mul_left_iff]
+    exact mul_eq_mul_left_iff.mp rfl
+  · congr
+    funext i
+    change - (x.val (Sum.inr i) * ((η *ᵥ y.toFin1dℝ) (Sum.inr i)))  = _
+    simp only [mulVec_inr_i, mul_neg, neg_neg, mul_eq_mul_left_iff]
+    exact mul_eq_mul_left_iff.mp rfl
+
+lemma self_parity_eq_zero_iff : ⟪y, (Contr d).ρ LorentzGroup.parity y⟫ₘ = 0 ↔ y = 0 := by
+  refine Iff.intro (fun h => ?_) (fun h => ?_)
+  · rw [right_parity] at h
+    have hn := Fintype.sum_eq_zero_iff_of_nonneg (f := fun i => y.val i * y.val i) (fun i => by
+      simpa using mul_self_nonneg (y.val i))
+    rw [h] at hn
+    simp at hn
+    apply ContrMod.ext
+    funext i
+    simpa using congrFun hn i
+  · rw [h]
+    simp only [Action.instMonoidalCategory_tensorUnit_V, Action.instMonoidalCategory_tensorObj_V,
+      Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
+      Action.FunctorCategoryEquivalence.functor_obj_obj, map_zero, tmul_zero]
+
+/-- The metric tensor is non-degenerate. -/
+lemma nondegenerate : (∀ (x : Contr d), ⟪x, y⟫ₘ = 0) ↔ y = 0 := by
+  refine Iff.intro (fun h => ?_) (fun h => ?_)
+  · exact (self_parity_eq_zero_iff _).mp ((symm _ _).trans $ h _)
+  · simp [h]
+
+lemma matrix_apply_eq_iff_sub : ⟪x, Λ *ᵥ y⟫ₘ = ⟪x, Λ' *ᵥ y⟫ₘ ↔ ⟪x, (Λ - Λ') *ᵥ y⟫ₘ = 0 := by
+  rw [← sub_eq_zero, ← LinearMap.map_sub, ← tmul_sub, ← ContrMod.sub_mulVec Λ Λ' y]
+
+lemma matrix_eq_iff_eq_forall' : (∀ (v : Contr d), (Λ *ᵥ v) = Λ' *ᵥ v) ↔
+    ∀ (w v : Contr d), ⟪v, Λ *ᵥ w⟫ₘ = ⟪v, Λ' *ᵥ w⟫ₘ := by
+  refine Iff.intro (fun h ↦ fun w v ↦ ?_) (fun h ↦ fun v ↦ ?_)
+  · rw [h w]
+  · simp only [matrix_apply_eq_iff_sub] at h
+    refine sub_eq_zero.1 ?_
+    have h1 := h v
+    rw [nondegenerate] at h1
+    simp only [ContrMod.sub_mulVec] at h1
+    exact h1
+
+lemma matrix_eq_iff_eq_forall : Λ = Λ' ↔ ∀ (w v : Contr d), ⟪v, Λ *ᵥ w⟫ₘ = ⟪v, Λ' *ᵥ w⟫ₘ := by
+  rw [← matrix_eq_iff_eq_forall']
+  refine Iff.intro (fun h => ?_) (fun h => ?_)
+  · subst h
+    exact fun v => rfl
+  · rw [← (LinearMap.toMatrix ContrMod.stdBasis ContrMod.stdBasis).toEquiv.symm.apply_eq_iff_eq]
+    ext1 v
+    exact h v
+
+lemma matrix_eq_id_iff : Λ = 1 ↔ ∀ (w v : Contr d), ⟪v, Λ *ᵥ w⟫ₘ = ⟪v, w⟫ₘ := by
+  rw [matrix_eq_iff_eq_forall]
+  simp only [Action.instMonoidalCategory_tensorUnit_V, Action.instMonoidalCategory_tensorObj_V,
+    Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
+    Action.FunctorCategoryEquivalence.functor_obj_obj, ContrMod.one_mulVec]
+
+lemma _root_.LorentzGroup.mem_iff_invariant : Λ ∈ LorentzGroup d ↔
+    ∀ (w v : Contr d), ⟪Λ *ᵥ v, Λ *ᵥ w⟫ₘ = ⟪v, w⟫ₘ := by
+  refine Iff.intro (fun h => ?_) (fun h => ?_)
+  · intro x y
+    rw [← dual_mulVec_right, ContrMod.mulVec_mulVec]
+    have h1 := LorentzGroup.mem_iff_dual_mul_self.mp h
+    rw [h1]
+    simp only [Action.instMonoidalCategory_tensorUnit_V, Action.instMonoidalCategory_tensorObj_V,
+      Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
+      Action.FunctorCategoryEquivalence.functor_obj_obj, ContrMod.one_mulVec]
+  · conv at h =>
+      intro x y
+      rw [← dual_mulVec_right, ContrMod.mulVec_mulVec]
+    rw [← matrix_eq_id_iff] at h
+    exact LorentzGroup.mem_iff_dual_mul_self.mpr h
+
+lemma _root_.LorentzGroup.mem_iff_norm : Λ ∈ LorentzGroup d ↔
+    ∀ (w : Contr d), ⟪Λ *ᵥ w, Λ *ᵥ w⟫ₘ = ⟪w, w⟫ₘ := by
+  rw [LorentzGroup.mem_iff_invariant]
+  refine Iff.intro (fun h x => h x x) (fun h x y => ?_)
+  have hp := h (x + y)
+  have hn := h (x - y)
+  rw [ContrMod.mulVec_add, tmul_add, add_tmul, add_tmul, tmul_add, add_tmul, add_tmul] at hp
+  rw [ContrMod.mulVec_sub, tmul_sub, sub_tmul, sub_tmul, tmul_sub, sub_tmul, sub_tmul] at hn
+  simp only [map_add, LinearMap.add_apply, map_sub, LinearMap.sub_apply] at hp hn
+  rw [symm (Λ *ᵥ y) (Λ *ᵥ x), symm y x] at hp hn
+  let e :  𝟙_ (Rep ℝ ↑(LorentzGroup d)) ≃ₗ[ℝ] ℝ :=
+    LinearEquiv.refl ℝ (CoeSort.coe (𝟙_ (Rep ℝ ↑(LorentzGroup d))))
+  apply e.injective
+  have hp' := e.injective.eq_iff.mpr hp
+  have hn' := e.injective.eq_iff.mpr hn
+  simp only [Action.instMonoidalCategory_tensorUnit_V, Action.instMonoidalCategory_tensorObj_V,
+    Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
+    Action.FunctorCategoryEquivalence.functor_obj_obj, map_add, map_sub] at hp' hn'
+  linear_combination  (norm := ring_nf) (1 / 4) * hp' + (-1/ 4) * hn'
+  rw [symm (Λ *ᵥ y) (Λ *ᵥ x), symm y x]
+  simp only [Action.instMonoidalCategory_tensorUnit_V, Action.instMonoidalCategory_tensorObj_V,
+    Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
+    Action.FunctorCategoryEquivalence.functor_obj_obj, add_sub_cancel, neg_add_cancel, e]
+
 end contrContrContract
 
 end Lorentz

HepLean/SpaceTime/LorentzVector/Real/Modules.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.Meta.Informal
-import HepLean.SpaceTime.SL2C.Basic
+import HepLean.SpaceTime.LorentzGroup.Basic
 import Mathlib.RepresentationTheory.Rep
 import Mathlib.Logic.Equiv.TransferInstance
 /-!
@@ -34,6 +34,13 @@ namespace ContrMod
 
 variable {d : ℕ}
 
+@[ext]
+lemma ext {ψ ψ' : ContrMod d} (h : ψ.val = ψ'.val) : ψ = ψ' := by
+  cases ψ
+  cases ψ'
+  subst h
+  rfl
+
 /-- The equivalence between `ContrℝModule` and `Fin 1 ⊕ Fin d → ℂ`. -/
 def toFin1dℝFun : ContrMod d ≃ (Fin 1 ⊕ Fin d → ℝ) where
   toFun v := v.val
@@ -53,13 +60,6 @@ instance : AddCommGroup (ContrMod d) := Equiv.addCommGroup toFin1dℝFun
   with `Fin 1 ⊕ Fin d → ℝ`. -/
 instance : Module ℝ (ContrMod d) := Equiv.module ℝ toFin1dℝFun
 
-@[ext]
-lemma ext (ψ ψ' : ContrMod d) (h : ψ.val = ψ'.val) : ψ = ψ' := by
-  cases ψ
-  cases ψ'
-  subst h
-  rfl
-
 @[simp]
 lemma val_add (ψ ψ' : ContrMod d) : (ψ + ψ').val = ψ.val + ψ'.val := rfl
 
@@ -122,13 +122,33 @@ lemma stdBasis_decomp (v : ContrMod d) : v = ∑ i, v.toFin1dℝ i • stdBasis
 abbrev mulVec (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v : ContrMod d) :
     ContrMod d := Matrix.toLinAlgEquiv stdBasis M v
 
-scoped[Lorentz] notation M " *ᵥ " v => ContrMod.mulVec M v
+scoped[Lorentz] infixr:73 " *ᵥ " => ContrMod.mulVec
 
 @[simp]
 lemma mulVec_toFin1dℝ (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v : ContrMod d) :
     (M *ᵥ v).toFin1dℝ = M *ᵥ v.toFin1dℝ := by
   rfl
 
+lemma mulVec_sub (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v w : ContrMod d) :
+    M *ᵥ (v - w) = M *ᵥ v - M *ᵥ w := by
+  simp only [mulVec, LinearMap.map_sub]
+
+lemma sub_mulVec (M N : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v : ContrMod d) :
+    (M - N) *ᵥ v = M *ᵥ v - N *ᵥ v := by
+  simp only [mulVec, map_sub, LinearMap.sub_apply]
+
+lemma mulVec_add (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v w : ContrMod d) :
+    M *ᵥ (v + w) = M *ᵥ v + M *ᵥ w := by
+  simp only [mulVec, LinearMap.map_add]
+
+@[simp]
+lemma one_mulVec (v : ContrMod d) : (1 : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) *ᵥ v = v := by
+  simp only [mulVec, _root_.map_one, LinearMap.one_apply]
+
+lemma mulVec_mulVec (M N : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v : ContrMod d) :
+    M *ᵥ (N *ᵥ v) = (M * N) *ᵥ v := by
+  simp only [mulVec, _root_.map_mul, LinearMap.mul_apply]
+
 /-!
 
 ## The representation.
@@ -158,6 +178,13 @@ namespace CoMod
 
 variable {d : ℕ}
 
+@[ext]
+lemma ext {ψ ψ' : CoMod d} (h : ψ.val = ψ'.val) : ψ = ψ' := by
+  cases ψ
+  cases ψ'
+  subst h
+  rfl
+
 /-- The equivalence between `CoℝModule` and `Fin 1 ⊕ Fin d → ℝ`. -/
 def toFin1dℝFun : CoMod d ≃ (Fin 1 ⊕ Fin d → ℝ) where
   toFun v := v.val
@@ -232,7 +259,7 @@ lemma stdBasis_decomp (v : CoMod d) : v = ∑ i, v.toFin1dℝ i • stdBasis i :
 abbrev mulVec (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v : CoMod d) :
     CoMod d := Matrix.toLinAlgEquiv stdBasis M v
 
-scoped[Lorentz] notation M " *ᵥ " v => CoMod.mulVec M v
+scoped[Lorentz] infixr:73 " *ᵥ " => CoMod.mulVec
 
 @[simp]
 lemma mulVec_toFin1dℝ (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v : CoMod d) :

HepLean/SpaceTime/MinkowskiMatrix.lean

@@ -85,6 +85,18 @@ lemma inr_i_inr_i (i : Fin d) : @minkowskiMatrix d (Sum.inr i) (Sum.inr i) = -1
   simp only [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal]
   simp_all only [diagonal_apply_eq, Sum.elim_inr]
 
+@[simp]
+lemma mulVec_inl_0 (v : (Fin 1 ⊕ Fin d) → ℝ) :
+    (η *ᵥ v) (Sum.inl 0)= v (Sum.inl 0) := by
+  simp only [mulVec, minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, mulVec_diagonal]
+  simp only [Fin.isValue, diagonal_dotProduct, Sum.elim_inl, one_mul]
+
+@[simp]
+lemma mulVec_inr_i (v : (Fin 1 ⊕ Fin d) → ℝ) (i : Fin d) :
+    (η *ᵥ v) (Sum.inr i)= - v (Sum.inr i) := by
+  simp only [mulVec, minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, mulVec_diagonal]
+  simp only [diagonal_dotProduct, Sum.elim_inr, neg_mul, one_mul]
+
 
 variable (Λ Λ' : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)