feat: Writing toDualRep in terms of contrOneTwoLeft

HepLean/Tensors/OverColor/Iso.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.Tensors.OverColor.Functors
-import HepLean.Tensors.OverColor.Lift
 import HepLean.Mathematics.Fin
 /-!
 

HepLean/Tensors/OverColor/Lift.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.Tensors.OverColor.Basic
+import HepLean.Tensors.OverColor.Iso
 import HepLean.Mathematics.PiTensorProduct
 /-!
 
@@ -821,6 +822,23 @@ lemma forgetLiftApp_hom_hom_apply_eq (c : C)
   erw [LinearEquiv.eq_symm_apply]
   rfl
 
+def forgetLiftAppCon (c : C) : (lift.obj F).obj (OverColor.mk ![c])
+    ≅ F.obj (Discrete.mk c) := ((lift.obj F).mapIso (OverColor.mkIso (by
+  funext i
+  fin_cases i
+  rfl))).trans (forgetLiftApp F c)
+
+lemma forgetLiftAppCon_inv_apply_expand (c : C) (x : F.obj (Discrete.mk c)) :
+    (forgetLiftAppCon F c).inv.hom x =
+    ((lift.obj F).map (OverColor.mkIso (by
+    funext i
+    fin_cases i
+    rfl)).hom).hom ((forgetLiftApp F c).inv.hom x):= by
+  rw [forgetLiftAppCon]
+  simp_all only [Nat.succ_eq_add_one, Nat.reduceAdd, Iso.trans_inv, Functor.mapIso_inv, Action.comp_hom,
+    ModuleCat.coe_comp, Function.comp_apply]
+  rfl
+
 informal_definition forgetLift where
   math :≈ "The natural isomorphism between `lift (C := C) ⋙ forget` and
     `Functor.id (Discrete C ⥤ Rep k G)`."

HepLean/Tensors/TensorSpecies/ContractLemmas.lean

@@ -29,13 +29,11 @@ variable {S : TensorSpecies}
 def contrOneTwoLeft {c1 c2 : S.C}
     (x : S.F.obj (OverColor.mk ![c1])) (y : S.F.obj (OverColor.mk ![S.τ c1, c2])) :
     S.F.obj (OverColor.mk ![c2]) :=
-  (S.F.map (OverColor.mkIso (by funext x; fin_cases x; rfl)).hom).hom <|
-  (OverColor.forgetLiftApp S.FD c2).inv.hom <|
+  (OverColor.forgetLiftAppCon S.FD c2).inv.hom <|
   (λ_ (S.FD.obj (Discrete.mk c2))).hom.hom <|
   ((S.contr.app (Discrete.mk c1)) ▷ (S.FD.obj (Discrete.mk (c2 )))).hom <|
   (α_ _ _ (S.FD.obj (Discrete.mk (c2 )))).inv.hom <|
-  (OverColor.forgetLiftApp S.FD c1).hom.hom ((S.F.map (OverColor.mkIso (by
-    funext x; fin_cases x; rfl)).hom).hom x) ⊗ₜ
+  (OverColor.forgetLiftAppCon S.FD c1).hom.hom (x) ⊗ₜ
   (OverColor.Discrete.pairIsoSep S.FD).inv.hom y
 
 @[simp]
@@ -72,19 +70,20 @@ lemma contrOneTwoLeft_tprod_eq {c1 c2 : S.C}
     (fy : (i : (𝟭 Type).obj (OverColor.mk ![S.τ c1, c2]).left)
       → CoeSort.coe (S.FD.obj { as := (OverColor.mk ![S.τ c1, c2]).hom i })) :
     contrOneTwoLeft (PiTensorProduct.tprod S.k fx) (PiTensorProduct.tprod S.k fy) =
-      (S.F.map (OverColor.mkIso (by funext x; fin_cases x; rfl)).hom).hom
-      ((OverColor.forgetLiftApp S.FD c2).inv.hom (
+      ((OverColor.forgetLiftAppCon S.FD c2).inv.hom (
      ((S.contr.app (Discrete.mk c1)).hom (fx (0 : Fin 1) ⊗ₜ fy (0 : Fin 2)) •
       fy (1 : Fin 2)))) := by
   rw [contrOneTwoLeft]
   apply congrArg
-  apply congrArg
-  rw [Discrete.pairIsoSep_inv_tprod S.FD fy]
+  rw [Discrete.pairIsoSep_inv_tprod S.FD fy, OverColor.forgetLiftAppCon]
   change (S.contr.app { as := c1 }).hom (_ ⊗ₜ[S.k] fy (0 : Fin 2)) • fy (1 : Fin 2) = _
   congr
-  simp
+  simp only [Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
+    Action.FunctorCategoryEquivalence.functor_obj_obj, Nat.succ_eq_add_one, Nat.reduceAdd,
+    Iso.trans_hom, Functor.mapIso_hom, Action.comp_hom, mk_left, Functor.id_obj, mk_hom,
+    ModuleCat.coe_comp, Function.comp_apply, LinearMap.id_coe, id_eq, Fin.isValue]
   rw [forgetLiftApp_hom_hom_apply_eq]
-  simp [S.F_def]
+  simp only [mk_left, Functor.id_obj, Fin.isValue]
   erw [OverColor.lift.map_tprod]
   congr
   funext x
@@ -107,6 +106,7 @@ lemma contr_one_two_left_eq_contrOneTwoLeft_tprod {c1 c2 : S.C} (x : S.F.obj (Ov
   subst hy
   conv_rhs =>
     rw [contrOneTwoLeft_tprod_eq]
+    rw [OverColor.forgetLiftAppCon_inv_apply_expand]
   simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, Fin.succAbove_zero, mk_left,
     Functor.id_obj, mk_hom, contr_tensor, prod_tensor, Action.instMonoidalCategory_tensorObj_V,
     Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
@@ -184,7 +184,6 @@ lemma contr_one_two_left_eq_contrOneTwoLeft {c1 c2 : S.C} (x : S.F.obj (OverColo
   simpa using contr_one_two_left_eq_contrOneTwoLeft_tprod (PiTensorProduct.tprod S.k fx)
     (PiTensorProduct.tprod S.k fy) fx fy
 
-
 /-- Expands the inner contraction of two 2-tensors which are
   tprods in terms of basic categorical
   constructions and fields of the tensor species. -/

HepLean/Tensors/TensorSpecies/RepIso.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.Tensors.TensorSpecies.Basic
+import HepLean.Tensors.TensorSpecies.MetricTensor
 /-!
 
 # Isomorphism between rep of color `c` and rep of dual color.
@@ -40,6 +41,24 @@ lemma toDualRep_congr {c c' : S.C} (h : c = c') : S.toDualRep c = S.FD.map (Disc
 def fromDualRep (c : S.C) : S.FD.obj (Discrete.mk (S.τ c)) ⟶ S.FD.obj (Discrete.mk c) :=
   S.toDualRep (S.τ c) ≫ S.FD.map (Discrete.eqToHom (S.τ_involution c))
 
+/-- The rewriting of `toDualRep` in terms of `contrOneTwoLeft`. -/
+lemma toDualRep_apply_eq_contrOneTwoLeft (c : S.C) (x : S.FD.obj (Discrete.mk c)) :
+    (S.toDualRep c).hom x = (OverColor.forgetLiftAppCon S.FD (S.τ c)).hom.hom
+    (contrOneTwoLeft (((OverColor.forgetLiftAppCon S.FD c).inv.hom x))
+    (S.metricTensor (S.τ c))) := by
+  simp only [toDualRep, Monoidal.tensorUnit_obj, Action.comp_hom,
+    Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
+    Action.instMonoidalCategory_rightUnitor_inv_hom, Action.instMonoidalCategory_whiskerLeft_hom,
+    Action.instMonoidalCategory_associator_inv_hom, Action.instMonoidalCategory_whiskerRight_hom,
+    Action.instMonoidalCategory_leftUnitor_hom_hom, ModuleCat.coe_comp, Function.comp_apply,
+    ModuleCat.MonoidalCategory.rightUnitor_inv_apply, ModuleCat.MonoidalCategory.whiskerLeft_apply,
+    Nat.succ_eq_add_one, Nat.reduceAdd, contrOneTwoLeft, Functor.comp_obj,
+    Discrete.functor_obj_eq_as, Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
+    Action.FunctorCategoryEquivalence.functor_obj_obj, OverColor.Discrete.rep_iso_hom_inv_apply]
+  repeat apply congrArg
+  erw [pairIsoSep_inv_metricTensor]
+  rfl
+
 end TensorSpecies
 
 end

HepLean/Tensors/TensorSpecies/UnitTensor.lean

@@ -120,7 +120,8 @@ lemma contrOneTwoLeft_unitTensor  {c1 : S.C} (x : S.F.obj (OverColor.mk ![c1]))
     Action.instMonoidalCategory_leftUnitor_hom_hom, Monoidal.tensorUnit_obj,
     Action.instMonoidalCategory_whiskerRight_hom, Functor.comp_obj, Discrete.functor_obj_eq_as,
     Function.comp_apply, Action.instMonoidalCategory_associator_inv_hom, Equivalence.symm_inverse,
-    Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj]
+    Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
+    forgetLiftAppCon_inv_apply_expand]
   erw [pairIsoSep_inv_unitTensor (S := S) (c := c1)]
   change (S.F.mapIso (mkIso _)).hom.hom _ = _
   rw [Discrete.rep_iso_apply_iff, Discrete.rep_iso_inv_apply_iff]