refactor: Remove category theory from Tensors

Physlib/Electromagnetism/Kinematics/EMPotential.lean

@@ -497,8 +497,8 @@ lemma tensorDeriv_eval_eq {d} {A : ElectromagneticPotential d} (hA : Differentia
   induction' t using Tensor.induction_on_basis with b a t h t1 t2 h1 h2
   · simp only [LinearEquiv.apply_symm_apply, basis_apply, evalT_pure, Pure.evalP, map_smul,
       toField_pure, smul_eq_mul, mul_one, Pure.evalPCoeff]
-    change _ * ((realLorentzTensor d).basis (Color.up)).repr
-      ((realLorentzTensor d).basis (Color.up) (b 1)) ν = _
+
+    change _ * (Lorentz.contrBasis d).repr (Lorentz.contrBasis d (b 1)) ν = _
     /- Transforming the basis -/
     let e : ComponentIdx (Fin.append ![Color.down] ![Color.up])
       ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans <|

Physlib/Relativity/Tensors/Contraction/Basic.lean

@@ -19,11 +19,13 @@ open CategoryTheory
 open MonoidalCategory
 
 namespace TensorSpecies
-open OverColor
+open OverColor Module
 
-variable {k : Type} [CommRing k] {C G : Type} [Group G]
-  {basisIdx : C → Type} [∀ c, Fintype (basisIdx c)] [∀ c, DecidableEq (basisIdx c)]
-  {S : TensorSpecies k C G basisIdx}
+variable {k : Type} [CommRing k] {C : Type} {G : Type} [Group G]
+    {V : C → Type} [∀ c, AddCommGroup (V c)] [∀ c, Module k (V c)]
+    {basisIdx : C → Type} [∀ c, Fintype (basisIdx c)] [∀ c, DecidableEq (basisIdx c)]
+    {rep : (c : C) → Representation k G (V c)} {b : (c : C) → Basis (basisIdx c) k (V c)}
+    {S : TensorSpecies k C G V basisIdx rep b}
 
 TODO "docs: The files on contractions of tensors are currently lacking documentation.
   These should be added, mirroring good examples within Physlib."
@@ -69,7 +71,6 @@ lemma contrT_pure {n : ℕ} {c : Fin (n + 1 + 1) → C} (i j : Fin (n + 1 + 1))
   simp only [contrT, Pure.toTensor]
   change _ = Pure.contrPMultilinear i j hij p
   conv_rhs => rw [← PiTensorProduct.lift.tprod]
-  rfl
 
 @[simp]
 lemma contrT_equivariant {n : ℕ} {c : Fin (n + 1 + 1) → C}
@@ -88,7 +89,7 @@ lemma contrT_equivariant {n : ℕ} {c : Fin (n + 1 + 1) → C}
   · intro p q hp
     simp [P, hp]
   · intro p r hr hp
-    simp [P, hp, hr, Tensor.actionT_add]
+    simp [P, hp, hr]
 
 lemma contrT_permT {n n1 : ℕ} {c : Fin (n + 1 + 1) → C}
     {c1 : Fin (n1 + 1 + 1) → C}

Physlib/Relativity/Tensors/Contraction/Basis.lean

@@ -19,9 +19,11 @@ open IndexNotation CategoryTheory MonoidalCategory Module
 namespace TensorSpecies
 open OverColor
 
-variable {k : Type} [CommRing k] {C G : Type} [Group G]
-  {basisIdx : C → Type} [∀ c, Fintype (basisIdx c)] [∀ c, DecidableEq (basisIdx c)]
-  {S : TensorSpecies k C G basisIdx}
+variable {k : Type} [CommRing k] {C : Type} {G : Type} [Group G]
+    {V : C → Type} [∀ c, AddCommGroup (V c)] [∀ c, Module k (V c)]
+    {basisIdx : C → Type} [∀ c, Fintype (basisIdx c)] [∀ c, DecidableEq (basisIdx c)]
+    {rep : (c : C) → Representation k G (V c)} {b : (c : C) → Module.Basis (basisIdx c) k (V c)}
+    {S : TensorSpecies k C G V basisIdx rep b}
 
 namespace Tensor
 
@@ -156,31 +158,34 @@ lemma Pure.dropPair_basisVector {n : ℕ} {c : Fin (n + 1 + 1) → C}
   funext l
   simp [dropPair, basisVector]
 
+attribute [-simp] LinearEquiv.cast_apply
 set_option backward.isDefEq.respectTransparency false in
 lemma contrT_basis_repr_apply {n : ℕ} {c : Fin (n + 1 + 1) → C} {i j : Fin (n + 1 + 1)}
     (h : i ≠ j ∧ S.τ (c i) = c j) (t : Tensor S c)
-    (b : ComponentIdx (c ∘ Fin.succSuccAbove i j)) :
-    (basis (c ∘ Fin.succSuccAbove i j)).repr (contrT n i j h t) b =
-    ∑ (b' : DropPairSection b), (basis c).repr t b'.1 *
-    S.castToField ((S.contr.app (Discrete.mk (c i))).hom
-    (S.basis (c i) (b'.1 i) ⊗ₜ[k] S.basis (S.τ (c i)) (basisIdxCongr (by rw [h.2]) (b'.1 j)))) := by
+    (φ : ComponentIdx (c ∘ Fin.succSuccAbove i j)) :
+    (basis (c ∘ Fin.succSuccAbove i j)).repr (contrT n i j h t) φ =
+    ∑ (b' : DropPairSection φ), (basis c).repr t b'.1 *
+     (S.contr (c i) (b (c i) (b'.1 i) ⊗ₜ[k] b (S.τ (c i)) (basisIdxCongr (by rw [h.2]) (b'.1 j)))) := by
   apply induction_on_basis _ _ _ _ t
   · intro b'
     conv_lhs =>
       rw [basis_apply, contrT_pure]
       simp [Pure.contrP, Pure.dropPair_basisVector]
-      change if b'.dropPair i j = b then _ else 0
+      change if b'.dropPair i j = φ then _ else 0
     split_ifs
     · rename_i h
       subst h
       rw [Finset.sum_eq_single ⟨b', by simp⟩]
-      · simp [Pure.contrPCoeff, castToField]
+      · simp [Pure.contrPCoeff]
         simp [Pure.basisVector]
-        rw [S.basis_congr (h.2 : S.τ (c i) = c j)]
-        simp
+        congr 2
+        generalize_proofs h1 h2
+        generalize b' j = bj
+        generalize c j = cj at *
+        subst h2
+        rfl
       · intro b'' _ hb
-        simp only [Basis.repr_self, Monoidal.tensorUnit_obj, Functor.comp_obj,
-          Discrete.functor_obj_eq_as, Function.comp_apply]
+        simp only [Basis.repr_self]
         apply mul_eq_zero_of_left
         rw [@MonoidAlgebra.single_apply]
         rw [if_neg]
@@ -216,13 +221,13 @@ lemma contrT_basis_repr_apply {n : ℕ} {c : Fin (n + 1 + 1) → C} {i j : Fin (
 set_option backward.isDefEq.respectTransparency false in
 lemma contrT_basis_repr_apply_eq_sum_fin {n : ℕ} {c : Fin (n + 1 + 1) → C} {i j : Fin (n + 1 + 1)}
     (h : i ≠ j ∧ S.τ (c i) = c j) (t : Tensor S c)
-    (b : ComponentIdx (c ∘ Fin.succSuccAbove i j)) :
-    (basis (c ∘ Fin.succSuccAbove i j)).repr (contrT n i j h t) b =
+    (φ  : ComponentIdx (c ∘ Fin.succSuccAbove i j)) :
+    (basis (c ∘ Fin.succSuccAbove i j)).repr (contrT n i j h t) φ =
     ∑ (x1 : basisIdx (c i)), ∑ (x2 : basisIdx (c j)),
-    (basis c).repr t (DropPairSection.ofFinEquiv h.1 b (x1, x2)).1 *
-    S.castToField ((S.contr.app (Discrete.mk (c i))).hom
-    (S.basis (c i) x1 ⊗ₜ[k] S.basis (S.τ (c i)) (basisIdxCongr (by rw [h.2]) x2))) := by
-  rw [contrT_basis_repr_apply h t b, ← (DropPairSection.ofFinEquiv h.1 b).sum_comp,
+    (basis c).repr t (DropPairSection.ofFinEquiv h.1 φ (x1, x2)).1 *
+    ((S.contr (c i))
+    (b (c i) x1 ⊗ₜ[k] b (S.τ (c i)) (basisIdxCongr (by rw [h.2]) x2))) := by
+  rw [contrT_basis_repr_apply h t φ, ← (DropPairSection.ofFinEquiv h.1 φ).sum_comp,
     Fintype.sum_prod_type]
   simp
 

Physlib/Relativity/Tensors/Contraction/Products.lean

@@ -22,9 +22,12 @@ open MonoidalCategory
 namespace TensorSpecies
 open OverColor
 
-variable {k : Type} [CommRing k] {C G : Type} [Group G]
-  {basisIdx : C → Type} [∀ c, Fintype (basisIdx c)] [∀ c, DecidableEq (basisIdx c)]
-  {S : TensorSpecies k C G basisIdx}
+variable {k : Type} [CommRing k] {C : Type} {G : Type} [Group G]
+    {V : C → Type} [∀ c, AddCommGroup (V c)] [∀ c, Module k (V c)]
+    {basisIdx : C → Type} [∀ c, Fintype (basisIdx c)] [∀ c, DecidableEq (basisIdx c)]
+    {rep : (c : C) → Representation k G (V c)} {b : (c : C) → Module.Basis (basisIdx c) k (V c)}
+    {S : TensorSpecies k C G V basisIdx rep b}
+attribute [-simp] LinearEquiv.cast_apply
 
 namespace Tensor
 
@@ -34,45 +37,37 @@ namespace Tensor
 
 -/
 
-set_option backward.isDefEq.respectTransparency false in
 lemma Pure.contrPCoeff_natAdd {n n1 : ℕ} {c : Fin (n + 1 + 1) → C}
     {c1 : Fin n1 → C}
     (i j : Fin (n + 1 + 1)) (hij : i ≠ j ∧ S.τ (c i) = c j)
     (p : Pure S c) (p1 : Pure S c1) :
     contrPCoeff (Fin.natAdd n1 i) (Fin.natAdd n1 j)
-    (by simp_all [Fin.ext_iff]) (p1.prodP p)
-    = contrPCoeff i j hij p := by
-  simp only [contrPCoeff, Monoidal.tensorUnit_obj, Functor.comp_obj, Discrete.functor_obj_eq_as,
-    Function.comp_apply, prodP_apply_natAdd]
-  conv_lhs => erw [S.contr_congr _ ((c i)) (by simp)]
-  apply congrArg
-  congr 1
-  · change (ConcreteCategory.hom (S.FD.map (Discrete.eqToHom _)))
-      ((ConcreteCategory.hom (S.FD.map (eqToHom _))) (p i)) = _
-    simp [map_map_apply]
-  · change (ConcreteCategory.hom (S.FD.map (Discrete.eqToHom _)))
-      ((ConcreteCategory.hom (S.FD.map (eqToHom _))) _) = _
-    simp [map_map_apply]
+    (by simp_all [Fin.ext_iff]) (p1.prodP p) = contrPCoeff i j hij p := by
+  simp only [contrPCoeff, prodP_apply_natAdd]
+  generalize_proofs ha hb hc hd he
+  generalize p i = pi at *
+  generalize p j = pj at *
+  generalize c i = ci at *
+  generalize c j = cj at *
+  subst he
+  subst hb
+  simp [LinearEquiv.cast_apply]
 
-set_option backward.isDefEq.respectTransparency false in
 lemma Pure.contrPCoeff_castAdd {n n1 : ℕ} {c : Fin (n + 1 + 1) → C}
     {c1 : Fin n1 → C}
     (i j : Fin (n + 1 + 1)) (hij : i ≠ j ∧ S.τ (c i) = c j)
     (p : Pure S c) (p1 : Pure S c1) :
     contrPCoeff (Fin.castAdd n1 i) (Fin.castAdd n1 j)
-    (by simp_all [Fin.ext_iff]) (p.prodP p1)
-    = contrPCoeff i j hij p := by
-  simp only [contrPCoeff, Monoidal.tensorUnit_obj, Functor.comp_obj, Discrete.functor_obj_eq_as,
-    Function.comp_apply, prodP_apply_castAdd]
-  conv_lhs => erw [S.contr_congr _ ((c i)) (by simp)]
-  apply congrArg
-  congr 1
-  · change (ConcreteCategory.hom (S.FD.map (Discrete.eqToHom _)))
-      ((ConcreteCategory.hom (S.FD.map (eqToHom _))) (p i)) = _
-    simp [map_map_apply]
-  · change (ConcreteCategory.hom (S.FD.map (Discrete.eqToHom _)))
-      ((ConcreteCategory.hom (S.FD.map (eqToHom _))) _) = _
-    simp [map_map_apply]
+    (by simp_all [Fin.ext_iff]) (p.prodP p1) = contrPCoeff i j hij p := by
+  simp only [contrPCoeff, prodP_apply_castAdd]
+  generalize_proofs ha hb hc hd he
+  generalize p i = pi at *
+  generalize p j = pj at *
+  generalize c i = ci at *
+  generalize c j = cj at *
+  subst he
+  subst hb
+  simp [LinearEquiv.cast_apply]
 
 set_option backward.isDefEq.respectTransparency false in
 lemma Pure.prodP_dropPair {n n1 : ℕ} {c : Fin (n + 1 + 1) → C}
@@ -92,12 +87,12 @@ lemma Pure.prodP_dropPair {n n1 : ℕ} {c : Fin (n + 1 + 1) → C}
     simp only [finSumFinEquiv_apply_left]
     rw [← congr_right (p1.prodP p) _ (Fin.castAdd (n + 1 + 1) x)
       (by rw [Fin.succSuccAbove_natAdd_apply_castAdd i j])]
-    simp [map_map_apply]
+    simp [LinearEquiv.cast_apply]
   | Sum.inr m =>
     simp only [finSumFinEquiv_apply_right]
     rw [← congr_right (p1.prodP p) _ (Fin.natAdd n1 (i.succSuccAbove j m))
       (by rw [Fin.succSuccAbove_comm_natAdd i j])]
-    simp [map_map_apply]
+    simp [LinearEquiv.cast_apply]
 
 set_option backward.isDefEq.respectTransparency false in
 lemma Pure.prodP_contrP_snd {n n1 : ℕ} {c : Fin (n + 1 + 1) → C}
@@ -106,17 +101,16 @@ lemma Pure.prodP_contrP_snd {n n1 : ℕ} {c : Fin (n + 1 + 1) → C}
     (p : Pure S c) (p1 : Pure S c1) :
     prodT p1.toTensor (contrP i j hij p) =
     ((permT id (PermCond.append_right_succSuccAbove i j)) <|
-    contrP
-      (finSumFinEquiv (m := n1) (Sum.inr i))
-      (finSumFinEquiv (m := n1) (Sum.inr j))
-      (by simpa using hij) <|
+    contrP (Fin.natAdd n1 i) (Fin.natAdd n1 j) (by simpa using hij) <|
     prodP p1 p) := by
   simp only [contrP, map_smul, Nat.add_eq, finSumFinEquiv_apply_right]
   rw [contrPCoeff_natAdd i j hij]
-  congr 1
-  rw [prodT_pure, permT_pure]
-  congr
+  rw [prodT_pure]
   rw [prodP_dropPair _ _ hij]
+  generalize_proofs ha hb hc hd
+  erw [map_smul]
+  congr
+  erw [permT_pure]
 
 set_option backward.isDefEq.respectTransparency false in
 lemma prodT_contrT_snd {n n1 : ℕ} {c : Fin (n + 1 + 1) → C}
@@ -126,6 +120,7 @@ lemma prodT_contrT_snd {n n1 : ℕ} {c : Fin (n + 1 + 1) → C}
     prodT t1 (contrT n i j hij t) =
     ((permT id (PermCond.append_right_succSuccAbove i j)) <|
     contrT _
+
       (finSumFinEquiv (m := n1) (Sum.inr i))
       (finSumFinEquiv (m := n1) (Sum.inr j))
       (by simpa using hij) <|