refactor(Tensors): remove pre-Lorentz Contr/Co reps in favour of ContrMod.rep/CoMod.rep

Physlib/Relativity/Tensors/ComplexTensor/Vector/Pre/Basic.lean

@@ -194,7 +194,7 @@ lemma complexContrBasis_of_real (i : Fin 1 ⊕ Fin 3) :
 
 lemma inclCongrRealLorentz_ρ (M : SL(2, ℂ)) (v : ContrMod 3) :
     (ContrℂModule.SL2CRep M) (inclCongrRealLorentz v) =
-    inclCongrRealLorentz ((Contr 3).ρ (SL2C.toLorentzGroup M) v) := by
+    inclCongrRealLorentz (ContrMod.rep (SL2C.toLorentzGroup M) v) := by
   apply Lorentz.ContrℂModule.ext
   rw [complexContrBasis_ρ_val, inclCongrRealLorentz_val, inclCongrRealLorentz_val]
   rw [LorentzGroup.toComplex_mulVec_ofReal]
@@ -246,7 +246,7 @@ lemma complexCoBasis_of_real (i : Fin 1 ⊕ Fin 3) :
 
 lemma inclCoRealLorentz_ρ (M : SL(2, ℂ)) (v : CoMod 3) :
     (CoℂModule.SL2CRep M) (inclCoRealLorentz v) =
-    inclCoRealLorentz ((Co 3).ρ (SL2C.toLorentzGroup M) v) := by
+    inclCoRealLorentz (CoMod.rep (SL2C.toLorentzGroup M) v) := by
   ext i
   rw [CoℂModule.SL2CRep_val, inclCoRealLorentz_val, inclCoRealLorentz_val]
   change ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ *ᵥ

Physlib/Relativity/Tensors/RealTensor/Matrix/Pre.lean

@@ -20,7 +20,7 @@ open Matrix Module MatrixGroups Complex TensorProduct CategoryTheory.MonoidalCat
 
 namespace Lorentz
 
-/-- Equivalence of `Contr ⊗ Contr` to `(1 + d) x (1 + d)` real matrices. -/
+/-- Equivalence of `ContrMod ⊗ ContrMod` to `(1 + d) x (1 + d)` real matrices. -/
 def contrContrToMatrixRe {d : ℕ} : (ContrMod d ⊗[ℝ] ContrMod d) ≃ₗ[ℝ]
     Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ :=
   (Basis.tensorProduct (contrBasis d) (contrBasis d)).repr ≪≫ₗ
@@ -39,8 +39,8 @@ lemma contrContrToMatrixRe_symm_expand_tmul (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1
     rfl
   · simp
 
-/-- Equivalence of `Co ⊗ Co` to `(1 + d) x (1 + d)` real matrices. -/
-def coCoToMatrixRe {d : ℕ} : (Co d ⊗ Co d).V ≃ₗ[ℝ]
+/-- Equivalence of `CoMod ⊗ CoMod` to `(1 + d) x (1 + d)` real matrices. -/
+def coCoToMatrixRe {d : ℕ} : (CoMod d ⊗[ℝ] CoMod d) ≃ₗ[ℝ]
     Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ :=
   (Basis.tensorProduct (coBasis d) (coBasis d)).repr ≪≫ₗ
   Finsupp.linearEquivFunOnFinite ℝ ℝ ((Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)) ≪≫ₗ
@@ -57,8 +57,8 @@ lemma coCoToMatrixRe_symm_expand_tmul (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ F
     rfl
   · simp
 
-/-- Equivalence of `Contr d ⊗ Co d` to `(1 + d) x (1 + d)` real matrices. -/
-def contrCoToMatrixRe {d : ℕ} : (Contr d ⊗ Co d).V ≃ₗ[ℝ]
+/-- Equivalence of `ContrMod d ⊗ CoMod d` to `(1 + d) x (1 + d)` real matrices. -/
+def contrCoToMatrixRe {d : ℕ} : (ContrMod d ⊗[ℝ] CoMod d) ≃ₗ[ℝ]
     Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ :=
   (Basis.tensorProduct (contrBasis d) (coBasis d)).repr ≪≫ₗ
   Finsupp.linearEquivFunOnFinite ℝ ℝ ((Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)) ≪≫ₗ
@@ -76,8 +76,8 @@ lemma contrCoToMatrixRe_symm_expand_tmul (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 
     rfl
   · simp
 
-/-- Equivalence of `Co d ⊗ Contr d` to `(1 + d) x (1 + d)` real matrices. -/
-def coContrToMatrixRe : (Co d ⊗ Contr d).V ≃ₗ[ℝ]
+/-- Equivalence of `CoMod d ⊗ ContrMod d` to `(1 + d) x (1 + d)` real matrices. -/
+def coContrToMatrixRe : (CoMod d ⊗[ℝ] ContrMod d) ≃ₗ[ℝ]
     Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ :=
   (Basis.tensorProduct (coBasis d) (contrBasis d)).repr ≪≫ₗ
   Finsupp.linearEquivFunOnFinite ℝ ℝ ((Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)) ≪≫ₗ
@@ -102,28 +102,28 @@ lemma coContrToMatrixRe_symm_expand_tmul (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 
 -/
 
 set_option backward.isDefEq.respectTransparency false in
-lemma contrContrToMatrixRe_ρ {d : ℕ} (v : (Contr d ⊗ Contr d).V) (M : LorentzGroup d) :
-    contrContrToMatrixRe (TensorProduct.map ((Contr d).ρ M) ((Contr d).ρ M) v) =
+lemma contrContrToMatrixRe_ρ {d : ℕ} (v : (ContrMod d ⊗[ℝ] ContrMod d)) (M : LorentzGroup d) :
+    contrContrToMatrixRe (TensorProduct.map (ContrMod.rep M) (ContrMod.rep M) v) =
     M.1 * contrContrToMatrixRe v * Mᵀ := by
   nth_rewrite 1 [contrContrToMatrixRe]
   simp only [LinearEquiv.trans_apply]
   trans (LinearEquiv.curry ℝ ℝ (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d)) ((LinearMap.toMatrix
       ((contrBasis d).tensorProduct (contrBasis d))
       ((contrBasis d).tensorProduct (contrBasis d))
-      (TensorProduct.map ((Contr d).ρ M) ((Contr d).ρ M)))
+      (TensorProduct.map (ContrMod.rep M) (ContrMod.rep M)))
       *ᵥ ((Finsupp.linearEquivFunOnFinite ℝ ℝ ((Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)))
       (((contrBasis d).tensorProduct (contrBasis d)).repr v)))
   · apply congrArg
     have h1 := (LinearMap.toMatrix_mulVec_repr ((contrBasis d).tensorProduct (contrBasis d))
       ((contrBasis d).tensorProduct (contrBasis d))
-      (TensorProduct.map ((Contr d).ρ M) ((Contr d).ρ M)) v)
+      (TensorProduct.map (ContrMod.rep M) (ContrMod.rep M)) v)
     erw [h1]
     rfl
   rw [TensorProduct.toMatrix_map]
   funext i j
   change ∑ k, ((kroneckerMap (fun x1 x2 => x1 * x2)
-        ((LinearMap.toMatrix (contrBasis d) (contrBasis d)) ((Contr d).ρ M))
-        ((LinearMap.toMatrix (contrBasis d) (contrBasis d)) ((Contr d).ρ M)) (i, j) k)
+        ((LinearMap.toMatrix (contrBasis d) (contrBasis d)) (ContrMod.rep M))
+        ((LinearMap.toMatrix (contrBasis d) (contrBasis d)) (ContrMod.rep M)) (i, j) k)
         * contrContrToMatrixRe v k.1 k.2) = _
   rw [Fintype.sum_prod_type]
   simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
@@ -139,28 +139,28 @@ lemma contrContrToMatrixRe_ρ {d : ℕ} (v : (Contr d ⊗ Contr d).V) (M : Loren
   ring
 
 set_option backward.isDefEq.respectTransparency false in
-lemma coCoToMatrixRe_ρ {d : ℕ} (v : ((Co d) ⊗ (Co d)).V) (M : LorentzGroup d) :
-    coCoToMatrixRe (TensorProduct.map ((Co d).ρ M) ((Co d).ρ M) v) =
+lemma coCoToMatrixRe_ρ {d : ℕ} (v : (CoMod d ⊗[ℝ] CoMod d)) (M : LorentzGroup d) :
+    coCoToMatrixRe (TensorProduct.map (CoMod.rep M) (CoMod.rep M) v) =
     M.1⁻¹ᵀ * coCoToMatrixRe v * M⁻¹ := by
   nth_rewrite 1 [coCoToMatrixRe]
   simp only [LinearEquiv.trans_apply]
   trans (LinearEquiv.curry ℝ ℝ (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d)) ((LinearMap.toMatrix
       ((coBasis d).tensorProduct (coBasis d))
       ((coBasis d).tensorProduct (coBasis d))
-      (TensorProduct.map ((Co d).ρ M) ((Co d).ρ M))
+      (TensorProduct.map (CoMod.rep M) (CoMod.rep M))
       *ᵥ ((Finsupp.linearEquivFunOnFinite ℝ ℝ ((Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)))
       (((coBasis d).tensorProduct (coBasis d)).repr v))))
   · apply congrArg
     have h1 := (LinearMap.toMatrix_mulVec_repr ((coBasis d).tensorProduct (coBasis d))
       ((coBasis d).tensorProduct (coBasis d))
-      (TensorProduct.map ((Co d).ρ M) ((Co d).ρ M)) v)
+      (TensorProduct.map (CoMod.rep M) (CoMod.rep M)) v)
     erw [h1]
     rfl
   rw [TensorProduct.toMatrix_map]
   funext i j
   change ∑ k, ((kroneckerMap (fun x1 x2 => x1 * x2)
-        ((LinearMap.toMatrix (coBasis d) (coBasis d)) ((Co d).ρ M))
-        ((LinearMap.toMatrix (coBasis d) (coBasis d)) ((Co d).ρ M)) (i, j) k)
+        ((LinearMap.toMatrix (coBasis d) (coBasis d)) (CoMod.rep M))
+        ((LinearMap.toMatrix (coBasis d) (coBasis d)) (CoMod.rep M)) (i, j) k)
         * coCoToMatrixRe v k.1 k.2) = _
   rw [Fintype.sum_prod_type]
   simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
@@ -176,28 +176,28 @@ lemma coCoToMatrixRe_ρ {d : ℕ} (v : ((Co d) ⊗ (Co d)).V) (M : LorentzGroup
   ring
 
 set_option backward.isDefEq.respectTransparency false in
-lemma contrCoToMatrixRe_ρ {d : ℕ} (v : ((Contr d) ⊗ (Co d)).V) (M : LorentzGroup d) :
-    contrCoToMatrixRe (TensorProduct.map ((Contr d).ρ M) ((Co d).ρ M) v) =
+lemma contrCoToMatrixRe_ρ {d : ℕ} (v : (ContrMod d ⊗[ℝ] CoMod d)) (M : LorentzGroup d) :
+    contrCoToMatrixRe (TensorProduct.map (ContrMod.rep M) (CoMod.rep M) v) =
     M.1 * contrCoToMatrixRe v * M.1⁻¹ := by
   nth_rewrite 1 [contrCoToMatrixRe]
   simp only [LinearEquiv.trans_apply]
   trans (LinearEquiv.curry ℝ ℝ (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d)) ((LinearMap.toMatrix
       ((contrBasis d).tensorProduct (coBasis d))
       ((contrBasis d).tensorProduct (coBasis d))
-      (TensorProduct.map ((Contr d).ρ M) ((Co d).ρ M))
+      (TensorProduct.map (ContrMod.rep M) (CoMod.rep M))
       *ᵥ ((Finsupp.linearEquivFunOnFinite ℝ ℝ ((Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)))
       (((contrBasis d).tensorProduct (coBasis d)).repr v))))
   · apply congrArg
     have h1 := (LinearMap.toMatrix_mulVec_repr ((contrBasis d).tensorProduct (coBasis d))
       ((contrBasis d).tensorProduct (coBasis d))
-      (TensorProduct.map ((Contr d).ρ M) ((Co d).ρ M)) v)
+      (TensorProduct.map (ContrMod.rep M) (CoMod.rep M)) v)
     erw [h1]
     rfl
   rw [TensorProduct.toMatrix_map]
   funext i j
   change ∑ k, ((kroneckerMap (fun x1 x2 => x1 * x2)
-        ((LinearMap.toMatrix (contrBasis d) (contrBasis d)) ((Contr d).ρ M))
-        ((LinearMap.toMatrix (coBasis d) (coBasis d)) ((Co d).ρ M)) (i, j) k)
+        ((LinearMap.toMatrix (contrBasis d) (contrBasis d)) (ContrMod.rep M))
+        ((LinearMap.toMatrix (coBasis d) (coBasis d)) (CoMod.rep M)) (i, j) k)
         * contrCoToMatrixRe v k.1 k.2) = _
   rw [Fintype.sum_prod_type]
   simp_rw [kroneckerMap_apply, Matrix.mul_apply]
@@ -213,28 +213,28 @@ lemma contrCoToMatrixRe_ρ {d : ℕ} (v : ((Contr d) ⊗ (Co d)).V) (M : Lorentz
   ring
 
 set_option backward.isDefEq.respectTransparency false in
-lemma coContrToMatrixRe_ρ {d : ℕ} (v : ((Co d) ⊗ (Contr d)).V) (M : LorentzGroup d) :
-    coContrToMatrixRe (TensorProduct.map ((Co d).ρ M) ((Contr d).ρ M) v) =
+lemma coContrToMatrixRe_ρ {d : ℕ} (v : (CoMod d ⊗[ℝ] ContrMod d)) (M : LorentzGroup d) :
+    coContrToMatrixRe (TensorProduct.map (CoMod.rep M) (ContrMod.rep M) v) =
     M.1⁻¹ᵀ * coContrToMatrixRe v * M.1ᵀ := by
   nth_rewrite 1 [coContrToMatrixRe]
   simp only [LinearEquiv.trans_apply]
   trans (LinearEquiv.curry ℝ ℝ (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d)) ((LinearMap.toMatrix
       ((coBasis d).tensorProduct (contrBasis d))
       ((coBasis d).tensorProduct (contrBasis d))
-      (TensorProduct.map ((Co d).ρ M) ((Contr d).ρ M))
+      (TensorProduct.map (CoMod.rep M) (ContrMod.rep M))
       *ᵥ ((Finsupp.linearEquivFunOnFinite ℝ ℝ ((Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)))
       (((coBasis d).tensorProduct (contrBasis d)).repr v))))
   · apply congrArg
     have h1 := (LinearMap.toMatrix_mulVec_repr ((coBasis d).tensorProduct (contrBasis d))
       ((coBasis d).tensorProduct (contrBasis d))
-      (TensorProduct.map ((Co d).ρ M) ((Contr d).ρ M)) v)
+      (TensorProduct.map (CoMod.rep M) (ContrMod.rep M)) v)
     erw [h1]
     rfl
   rw [TensorProduct.toMatrix_map]
   funext i j
   change ∑ k, ((kroneckerMap (fun x1 x2 => x1 * x2)
-        ((LinearMap.toMatrix (coBasis d) (coBasis d)) ((Co d).ρ M))
-        ((LinearMap.toMatrix (contrBasis d) (contrBasis d)) ((Contr d).ρ M)) (i, j) k)
+        ((LinearMap.toMatrix (coBasis d) (coBasis d)) (CoMod.rep M))
+        ((LinearMap.toMatrix (contrBasis d) (contrBasis d)) (ContrMod.rep M)) (i, j) k)
         * coContrToMatrixRe v k.1 k.2) = _
   rw [Fintype.sum_prod_type]
   simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
@@ -257,14 +257,14 @@ lemma coContrToMatrixRe_ρ {d : ℕ} (v : ((Co d) ⊗ (Contr d)).V) (M : Lorentz
 
 lemma contrContrToMatrixRe_ρ_symm {d : ℕ} (v : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)
     (M : LorentzGroup d) :
-    TensorProduct.map ((Contr d).ρ M) ((Contr d).ρ M) (contrContrToMatrixRe.symm v) =
+    TensorProduct.map (ContrMod.rep M) (ContrMod.rep M) (contrContrToMatrixRe.symm v) =
     contrContrToMatrixRe.symm (M.1 * v * M.1ᵀ) := by
   refine contrContrToMatrixRe.injective ?_
   simp [contrContrToMatrixRe_ρ]
 
 lemma coCoToMatrixRe_ρ_symm {d : ℕ} (v : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)
     (M : LorentzGroup d) :
-    TensorProduct.map ((Co d).ρ M) ((Co d).ρ M) (coCoToMatrixRe.symm v) =
+    TensorProduct.map (CoMod.rep M) (CoMod.rep M) (coCoToMatrixRe.symm v) =
     coCoToMatrixRe.symm (M.1⁻¹ᵀ * v * M.1⁻¹) := by
   have h1 := coCoToMatrixRe_ρ (coCoToMatrixRe.symm v) M
   simp only [LinearEquiv.apply_symm_apply, ← LorentzGroup.coe_inv] at h1
@@ -274,15 +274,15 @@ lemma coCoToMatrixRe_ρ_symm {d : ℕ} (v : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕
 
 lemma contrCoToMatrixRe_ρ_symm {d : ℕ} (v : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)
     (M : LorentzGroup d) :
-    TensorProduct.map ((Contr d).ρ M) ((Co d).ρ M) (contrCoToMatrixRe.symm v) =
+    TensorProduct.map (ContrMod.rep M) (CoMod.rep M) (contrCoToMatrixRe.symm v) =
     contrCoToMatrixRe.symm (M.1 * v * M.1⁻¹) := by
   have h1 := contrCoToMatrixRe_ρ (contrCoToMatrixRe.symm v) M
   simp only [LinearEquiv.apply_symm_apply] at h1
   rw [← h1, LinearEquiv.symm_apply_apply]
 
 lemma coContrToMatrixRe_ρ_symm {d : ℕ} (v : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)
     (M : LorentzGroup d) :
-    TensorProduct.map ((Co d).ρ M) ((Contr d).ρ M) (coContrToMatrixRe.symm v) =
+    TensorProduct.map (CoMod.rep M) (ContrMod.rep M) (coContrToMatrixRe.symm v) =
     coContrToMatrixRe.symm (M.1⁻¹ᵀ * v * M.1ᵀ) := by
   have h1 := coContrToMatrixRe_ρ (coContrToMatrixRe.symm v) M
   simp only [LinearEquiv.apply_symm_apply] at h1

Physlib/Relativity/Tensors/RealTensor/Metrics/Pre.lean

@@ -20,7 +20,7 @@ open Module Matrix MatrixGroups Complex TensorProduct CategoryTheory.MonoidalCat
 namespace Lorentz
 open scoped TensorProduct
 
-/-- The metric `ηᵃᵃ` as an element of `(Contr d ⊗ Contr d).V`. -/
+/-- The metric `ηᵃᵃ` as an element of `(ContrMod d ⊗[ℝ] ContrMod d)`. -/
 def preContrMetricVal (d : ℕ := 3) : ContrMod d ⊗[ℝ] ContrMod d :=
   contrContrToMatrixRe.symm ((@minkowskiMatrix d))
 
@@ -39,7 +39,7 @@ lemma preContrMetricVal_expand_tmul {d : ℕ} : preContrMetricVal d =
     sub_eq_add_neg]
 
 set_option backward.isDefEq.respectTransparency false in
-/-- The metric `ηᵃᵃ` as a morphism `𝟙_ (Rep ℝ (LorentzGroup d)) ⟶ Contr d ⊗ Contr d`,
+/-- The metric `ηᵃᵃ` as a morphism `𝟙_ (Rep ℝ (LorentzGroup d)) ⟶ ContrMod.rep ⊗ ContrMod.rep`,
   making its invariance under the action of `LorentzGroup d`. -/
 def preContrMetric (d : ℕ := 3) :
     (Representation.trivial ℝ (LorentzGroup d) ℝ).IntertwiningMap
@@ -51,7 +51,7 @@ def preContrMetric (d : ℕ := 3) :
     refine LinearMap.ext fun x : ℝ => ?_
     simp only [LinearMap.coe_comp, Function.comp_apply]
     change x • (preContrMetricVal d) =
-      (TensorProduct.map ((Contr d).ρ M) ((Contr d).ρ M)) (x • (preContrMetricVal d))
+      (TensorProduct.map (ContrMod.rep M) (ContrMod.rep M)) (x • (preContrMetricVal d))
     simp only [map_smul]
     apply congrArg
     simp only [preContrMetricVal]
@@ -63,8 +63,8 @@ def preContrMetric (d : ℕ := 3) :
 lemma preContrMetric_apply_one {d : ℕ} : (preContrMetric d) (1 : ℝ) = preContrMetricVal d :=
   one_smul ℝ _
 
-/-- The metric `ηᵢᵢ` as an element of `(Co d ⊗ Co d).V`. -/
-def preCoMetricVal (d : ℕ := 3) : (Co d ⊗ Co d).V :=
+/-- The metric `ηᵢᵢ` as an element of `(CoMod d ⊗[ℝ] CoMod d)`. -/
+def preCoMetricVal (d : ℕ := 3) : CoMod d ⊗[ℝ] CoMod d :=
   coCoToMatrixRe.symm ((@minkowskiMatrix d))
 
 lemma preCoMetricVal_expand_tmul_minkowskiMatrix {d : ℕ} : preCoMetricVal d =
@@ -82,7 +82,7 @@ lemma preCoMetricVal_expand_tmul {d : ℕ} : preCoMetricVal d =
     sub_eq_add_neg]
 
 set_option backward.isDefEq.respectTransparency false in
-/-- The metric `ηᵢᵢ` as a morphism `𝟙_ (Rep ℂ (LorentzGroup d))) ⟶ Co d ⊗ Co d`,
+/-- The metric `ηᵢᵢ` as a morphism `𝟙_ (Rep ℂ (LorentzGroup d))) ⟶ CoMod.rep ⊗ CoMod.rep`,
   making its invariance under the action of `LorentzGroup d`. -/
 def preCoMetric (d : ℕ := 3) : (Representation.trivial ℝ (LorentzGroup d) ℝ).IntertwiningMap
     ((CoMod.rep).tprod (CoMod.rep)) where
@@ -93,7 +93,7 @@ def preCoMetric (d : ℕ := 3) : (Representation.trivial ℝ (LorentzGroup d) 
     refine LinearMap.ext fun x : ℝ => ?_
     simp only [LinearMap.coe_comp, Function.comp_apply]
     change x • preCoMetricVal d =
-      (TensorProduct.map ((Co d).ρ M) ((Co d).ρ M)) (x • preCoMetricVal d)
+      (TensorProduct.map (CoMod.rep M) (CoMod.rep M)) (x • preCoMetricVal d)
     simp only [_root_.map_smul]
     apply congrArg
     simp only [preCoMetricVal]

Physlib/Relativity/Tensors/RealTensor/ToComplex.lean

@@ -472,7 +472,7 @@ lemma actionP_toComplexPure {n : ℕ} (c : Fin n → Color) (p : Pure realLorent
           = (Lorentz.ContrℂModule.SL2CRep Λ) (Lorentz.inclCongrRealLorentz p) := by
             exact congrArg (Lorentz.ContrℂModule.SL2CRep Λ)
               (toComplexVector_up_eq_inclCongrRealLorentz p)
-      _ = Lorentz.inclCongrRealLorentz ((Lorentz.Contr 3).ρ (toLorentzGroup Λ) p) := by
+      _ = Lorentz.inclCongrRealLorentz (Lorentz.ContrMod.rep (toLorentzGroup Λ) p) := by
         rw [Lorentz.inclCongrRealLorentz_ρ]
       _ = (toComplexVector Color.up) ((Lorentz.ContrMod.rep (toLorentzGroup Λ)) p) := by
         exact (toComplexVector_up_eq_inclCongrRealLorentz
@@ -483,7 +483,7 @@ lemma actionP_toComplexPure {n : ℕ} (c : Fin n → Color) (p : Pure realLorent
           = (Lorentz.CoℂModule.SL2CRep Λ) (Lorentz.inclCoRealLorentz p) := by
             exact congrArg (Lorentz.CoℂModule.SL2CRep Λ)
               (toComplexVector_down_eq_inclCoRealLorentz p)
-      _ = Lorentz.inclCoRealLorentz ((Lorentz.Co 3).ρ (toLorentzGroup Λ) p) := by
+      _ = Lorentz.inclCoRealLorentz (Lorentz.CoMod.rep (toLorentzGroup Λ) p) := by
         rw [Lorentz.inclCoRealLorentz_ρ]
       _ = (toComplexVector Color.down) ((Lorentz.CoMod.rep (toLorentzGroup Λ)) p) := by
         exact (toComplexVector_down_eq_inclCoRealLorentz

Physlib/Relativity/Tensors/RealTensor/Units/Pre.lean

@@ -21,7 +21,7 @@ open Module Matrix MatrixGroups Complex TensorProduct CategoryTheory.MonoidalCat
 namespace Lorentz
 
 /-- The contra-co unit for complex lorentz vectors. Usually denoted `δⁱᵢ`. -/
-def preContrCoUnitVal (d : ℕ := 3) : (Contr d ⊗ Co d).V :=
+def preContrCoUnitVal (d : ℕ := 3) : ContrMod d ⊗[ℝ] CoMod d :=
   contrCoToMatrixRe.symm 1
 
 /-- Expansion of `preContrCoUnitVal` into basis. -/
@@ -60,7 +60,7 @@ def preContrCoUnit (d : ℕ := 3) :
     refine LinearMap.ext fun x : ℝ => ?_
     simp only [LinearMap.coe_comp, Function.comp_apply]
     change x • preContrCoUnitVal d =
-      (TensorProduct.map ((Contr d).ρ M) ((Co d).ρ M)) (x • preContrCoUnitVal d)
+      (TensorProduct.map (ContrMod.rep M) (CoMod.rep M)) (x • preContrCoUnitVal d)
     simp only [map_smul]
     apply congrArg
     simp only [preContrCoUnitVal]
@@ -73,7 +73,7 @@ lemma preContrCoUnit_apply_one {d : ℕ} : (preContrCoUnit d) (1 : ℝ) = preCon
   rw [one_smul]
 
 /-- The co-contra unit for complex lorentz vectors. Usually denoted `δᵢⁱ`. -/
-def preCoContrUnitVal (d : ℕ := 3) : (Co d ⊗ Contr d).V :=
+def preCoContrUnitVal (d : ℕ := 3) : CoMod d ⊗[ℝ] ContrMod d :=
   coContrToMatrixRe.symm 1
 
 /-- Expansion of `preCoContrUnitVal` into basis. -/
@@ -97,7 +97,7 @@ lemma preCoContrUnitVal_expand_tmul {d : ℕ} : preCoContrUnitVal d =
 
 set_option backward.isDefEq.respectTransparency false in
 /-- The co-contra unit for complex lorentz vectors as a morphism
-  `𝟙_ (Rep ℝ (LorentzGroup d)) ⟶ Co d ⊗ Contr d`, manifesting the invariance under
+  `𝟙_ (Rep ℝ (LorentzGroup d)) ⟶ CoMod.rep ⊗ ContrMod.rep`, manifesting the invariance under
   the `LorentzGroup d` action. -/
 def preCoContrUnit (d : ℕ) : (Representation.trivial ℝ (LorentzGroup d) ℝ).IntertwiningMap
     ((CoMod.rep).tprod (ContrMod.rep)) where
@@ -111,7 +111,7 @@ def preCoContrUnit (d : ℕ) : (Representation.trivial ℝ (LorentzGroup d) ℝ)
     refine LinearMap.ext fun x : ℝ => ?_
     simp only [LinearMap.coe_comp, Function.comp_apply]
     change x • preCoContrUnitVal d =
-      (TensorProduct.map ((Co d).ρ M) ((Contr d).ρ M)) (x • preCoContrUnitVal d)
+      (TensorProduct.map (CoMod.rep M) (ContrMod.rep M)) (x • preCoContrUnitVal d)
     simp only [map_smul]
     apply congrArg
     simp only [preCoContrUnitVal]