lemma: Contract with unitTensor

HepLean/Tensors/OverColor/Discrete.lean

@@ -276,6 +276,26 @@ lemma rep_iso_hom_inv_apply (x y : Rep k G) (f : x ≅ y) (i : y) :
   change (f.inv ≫ f.hom).hom i = i
   simp
 
+lemma rep_iso_apply_iff (x y : Rep k G) (f : x ≅ y) (i : x) (j : y) :
+    f.hom.hom i = j ↔ i = f.inv.hom j := by
+  apply Iff.intro
+  · intro a
+    subst a
+    simp_all only [rep_iso_inv_hom_apply]
+  · intro a
+    subst a
+    exact rep_iso_hom_inv_apply x y f j
+
+lemma rep_iso_inv_apply_iff (x y : Rep k G) (f : x ≅ y) (i : y) (j : x) :
+    f.inv.hom i = j ↔ i = f.hom.hom j := by
+  apply Iff.intro
+  · intro a
+    subst a
+    simp_all only [rep_iso_hom_inv_apply]
+  · intro a
+    subst a
+    simp_all only [rep_iso_inv_hom_apply]
+
 end
 end Discrete
 end OverColor

HepLean/Tensors/TensorSpecies/ContractLemmas.lean

@@ -3,7 +3,9 @@ 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.Tensors.TensorSpecies.UnitTensor
+import HepLean.Tensors.Tree.Elab
+import HepLean.Tensors.Tree.NodeIdentities.Basic
+import HepLean.Tensors.Tree.NodeIdentities.Congr
 /-!
 
 ## Contraction of specific tensor types
@@ -23,6 +25,165 @@ open TensorTree
 
 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 <|
+  (λ_ (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.Discrete.pairIsoSep S.FD).inv.hom y
+
+@[simp]
+lemma contrOneTwoLeft_smul_left {c1 c2 : S.C} (x : S.F.obj (OverColor.mk ![c1]))
+    (y : S.F.obj (OverColor.mk ![S.τ c1, c2])) (r : S.k) :
+    contrOneTwoLeft (r • x) y = r • contrOneTwoLeft x y := by
+  simp only [contrOneTwoLeft]
+  simp [map_smul, smul_tmul]
+
+@[simp]
+lemma contrOneTwoLeft_smul_right {c1 c2 : S.C} (x : S.F.obj (OverColor.mk ![c1]))
+    (y : S.F.obj (OverColor.mk ![S.τ c1, c2])) (r : S.k) :
+    contrOneTwoLeft x (r • y) = r • contrOneTwoLeft x y := by
+  simp only [contrOneTwoLeft]
+  simp [map_smul, smul_tmul]
+
+@[simp]
+lemma contrOneTwoLeft_add_left {c1 c2 : S.C} (x y : S.F.obj (OverColor.mk ![c1]))
+    (z : S.F.obj (OverColor.mk ![S.τ c1, c2])) :
+    contrOneTwoLeft (x + y) z = contrOneTwoLeft x z + contrOneTwoLeft y z := by
+  simp only [contrOneTwoLeft]
+  simp [map_add, add_tmul]
+
+@[simp]
+lemma contrOneTwoLeft_add_right {c1 c2 : S.C} (x : S.F.obj (OverColor.mk ![c1]))
+    (y z : S.F.obj (OverColor.mk ![S.τ c1, c2])) :
+    contrOneTwoLeft x (y + z) = contrOneTwoLeft x y + contrOneTwoLeft x z := by
+  simp only [contrOneTwoLeft]
+  simp [map_add, add_tmul, tmul_add]
+
+lemma contrOneTwoLeft_tprod_eq {c1 c2 : S.C}
+    (fx : (i : (𝟭 Type).obj (OverColor.mk ![c1]).left) →
+      CoeSort.coe (S.FD.obj { as := (OverColor.mk ![c1]).hom i }))
+    (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 (
+     ((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]
+  change (S.contr.app { as := c1 }).hom (_ ⊗ₜ[S.k] fy (0 : Fin 2)) • fy (1 : Fin 2) = _
+  congr
+  simp
+  rw [forgetLiftApp_hom_hom_apply_eq]
+  simp [S.F_def]
+  erw [OverColor.lift.map_tprod]
+  congr
+  funext x
+  match x with
+  | (0 : Fin 1) =>
+    simp [lift.discreteFunctorMapEqIso]
+    rfl
+
+lemma contr_one_two_left_eq_contrOneTwoLeft_tprod {c1 c2 : S.C} (x : S.F.obj (OverColor.mk ![c1]))
+    (y : S.F.obj (OverColor.mk ![S.τ c1, c2]))
+    (fx : (i : (𝟭 Type).obj (OverColor.mk ![c1]).left) →
+      CoeSort.coe (S.FD.obj { as := (OverColor.mk ![c1]).hom i }))
+    (fy : (i : (𝟭 Type).obj (OverColor.mk ![S.τ c1, c2]).left)
+      → CoeSort.coe (S.FD.obj { as := (OverColor.mk ![S.τ c1, c2]).hom i }))
+    (hx : x = PiTensorProduct.tprod S.k fx)
+    (hy : y = PiTensorProduct.tprod S.k fy) :
+     {x | μ ⊗ y | μ ν}ᵀ.tensor = (S.F.mapIso (OverColor.mkIso (by funext x; fin_cases x; rfl))).hom.hom
+    (contrOneTwoLeft x y) := by
+  subst hx
+  subst hy
+  conv_rhs =>
+    rw [contrOneTwoLeft_tprod_eq]
+  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,
+    Action.FunctorCategoryEquivalence.functor_obj_obj, tensorNode_tensor, Monoidal.tensorUnit_obj,
+    Action.instMonoidalCategory_tensorUnit_V, Matrix.cons_val_one, Matrix.head_cons,
+    Functor.comp_obj, Discrete.functor_obj_eq_as, Function.comp_apply, map_smul]
+  conv_lhs =>
+    erw [OverColor.lift.μ_tmul_tprod S.FD]
+    simp only [S.F_def]
+    erw [OverColor.lift.map_tprod]
+    erw [contrMap_tprod]
+  simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, Fin.succAbove_zero, mk_left,
+    Functor.id_obj, mk_hom, Function.comp_apply, Monoidal.tensorUnit_obj,
+    Action.instMonoidalCategory_tensorUnit_V, Equivalence.symm_inverse,
+    Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
+    Functor.comp_obj, Discrete.functor_obj_eq_as, equivToIso_homToEquiv,
+    instMonoidalCategoryStruct_tensorObj_hom, Fin.zero_succAbove, Fin.succ_zero_eq_one,
+    eqToHom_refl, Discrete.functor_map_id, Action.id_hom]
+  congr 1
+   /- The contraction. -/
+  · congr
+    · simp only [Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor, Fin.isValue,
+      Function.comp_apply, Action.FunctorCategoryEquivalence.functor_obj_obj, mk_hom,
+      equivToIso_homToEquiv, lift.discreteFunctorMapEqIso, eqToIso_refl, Functor.mapIso_refl,
+      Iso.refl_hom, Action.id_hom, Iso.refl_inv, Functor.id_obj,
+      instMonoidalCategoryStruct_tensorObj_hom, LinearEquiv.ofLinear_apply]
+      rfl
+    · simp only [Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor, Fin.isValue,
+      Function.comp_apply, Functor.comp_obj, Discrete.functor_obj_eq_as,
+      Action.FunctorCategoryEquivalence.functor_obj_obj, Nat.reduceAdd, eqToHom_refl,
+      Discrete.functor_map_id, Action.id_hom, mk_hom, equivToIso_homToEquiv,
+      lift.discreteFunctorMapEqIso, eqToIso_refl, Functor.mapIso_refl, Iso.refl_hom, Iso.refl_inv,
+      Functor.id_obj, instMonoidalCategoryStruct_tensorObj_hom, LinearEquiv.ofLinear_apply]
+      rfl
+  /- The tensor. -/
+  · symm
+    rw [OverColor.Discrete.rep_iso_apply_iff]
+    erw [OverColor.lift.map_tprod]
+    erw [OverColor.lift.map_tprod]
+    apply congrArg
+    funext x
+    match x with
+    | (0 : Fin 1) =>
+      simp only [mk_left, Fin.zero_eta, List.pmap.eq_1, Matrix.cons_val_zero, equivToIso_mkIso_hom,
+        Equiv.refl_symm, Equiv.refl_apply, lift.discreteFunctorMapEqIso, eqToIso_refl,
+        Functor.mapIso_refl, Iso.refl_inv, LinearEquiv.ofLinear_apply,
+        Function.comp_apply, equivToIso_mkIso_inv, Fin.succ_zero_eq_one, Fin.succ_one_eq_two]
+      rfl
+
+lemma contr_one_two_left_eq_contrOneTwoLeft {c1 c2 : S.C} (x : S.F.obj (OverColor.mk ![c1]))
+    (y : S.F.obj (OverColor.mk ![S.τ c1, c2])) :
+     {x | μ ⊗ y | μ ν}ᵀ.tensor = (S.F.map (OverColor.mkIso (by funext x; fin_cases x; rfl)).hom).hom
+    (contrOneTwoLeft x y) := by
+  simp [contr_tensor, prod_tensor]
+  refine PiTensorProduct.induction_on' x ?_ (by
+    intro a b hx hy
+    rw [contrOneTwoLeft_add_left, map_add, ← hx, ← hy]
+    simp only [Fin.isValue, Nat.succ_eq_add_one, Nat.reduceAdd, mk_left, Functor.id_obj, mk_hom,
+      add_tmul, map_add]
+    )
+  intro rx fx
+  refine PiTensorProduct.induction_on' y ?_ (by
+    intro a b hx hy
+    rw [contrOneTwoLeft_add_right, map_add, ← hx, ← hy]
+    simp only [Fin.isValue, Nat.succ_eq_add_one, Nat.reduceAdd, mk_left, Functor.id_obj, mk_hom,
+      PiTensorProduct.tprodCoeff_eq_smul_tprod, tmul_add, map_add])
+  intro ry fy
+  simp only [PiTensorProduct.tprodCoeff_eq_smul_tprod, tmul_smul, LinearMapClass.map_smul]
+  rw [ contrOneTwoLeft_smul_right]
+  simp
+  apply congrArg
+  rw [ contrOneTwoLeft_smul_left]
+  simp only [smul_tmul, tmul_smul, LinearMapClass.map_smul]
+  apply congrArg
+  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/UnitTensor.lean

@@ -6,6 +6,7 @@ Authors: Joseph Tooby-Smith
 import HepLean.Tensors.Tree.Elab
 import HepLean.Tensors.Tree.NodeIdentities.Basic
 import HepLean.Tensors.Tree.NodeIdentities.Congr
+import HepLean.Tensors.TensorSpecies.ContractLemmas
 /-!
 
 ## Units as tensors
@@ -37,6 +38,13 @@ lemma unitTensor_congr {c c' : S.C} (h : c = c') : {S.unitTensor c | μ ν}ᵀ.t
   change _ = (S.F.map (𝟙 _)).hom (S.unitTensor c)
   simp
 
+lemma pairIsoSep_inv_unitTensor (c : S.C) :
+    (Discrete.pairIsoSep S.FD).inv.hom (S.unitTensor c) =
+    (S.unit.app (Discrete.mk c)).hom (1 : S.k) := by
+  simp only [Action.instMonoidalCategory_tensorObj_V, Nat.succ_eq_add_one, Nat.reduceAdd,
+    unitTensor, Monoidal.tensorUnit_obj, Action.instMonoidalCategory_tensorUnit_V]
+  erw [Discrete.rep_iso_inv_hom_apply]
+
 lemma unitTensor_eq_dual_perm_eq (c : S.C) : ∀ (x : Fin (Nat.succ 0).succ),
     ![S.τ c, c] x = (![S.τ (S.τ c), S.τ c] ∘ ⇑(finMapToEquiv ![1, 0] ![1, 0]).symm) x := fun x => by
   fin_cases x
@@ -105,6 +113,27 @@ lemma dual_unitTensor_eq_perm (c : S.C) : {S.unitTensor (S.τ c) | ν μ}ᵀ.ten
   simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue]
   rfl
 
+lemma contrOneTwoLeft_unitTensor  {c1 : S.C}
+    (x : S.F.obj (OverColor.mk ![c1])) :
+    contrOneTwoLeft x (S.unitTensor c1) = x := by
+  simp only [Nat.succ_eq_add_one, Nat.reduceAdd, contrOneTwoLeft,
+    Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
+    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]
+  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]
+  simpa using  S.contr_unit c1 ((OverColor.forgetLiftApp S.FD c1).hom.hom ((S.F.map (OverColor.mkIso (by
+    funext x; fin_cases x; rfl)).hom).hom x))
+
+lemma one_contr_unitTensor_eq_self {c1 : S.C} (x : S.F.obj (OverColor.mk ![c1])) :
+    {x | μ ⊗ S.unitTensor c1 | μ ν}ᵀ.tensor = ({x | ν}ᵀ |>
+    perm (OverColor.equivToHomEq (Equiv.refl _) (fun x => by fin_cases x; rfl ))).tensor  := by
+  rw [contr_one_two_left_eq_contrOneTwoLeft, contrOneTwoLeft_unitTensor]
+  rfl
+
 end TensorSpecies
 
 end