PhysLean Documentation

PhysLean.Relativity.Tensors.Tree.NodeIdentities.PermProd

Swapping permutations and contractions #

The results here follow from the properties of Monoidal categories and monoidal functors.

source
def TensorTree.permProdLeft {S : TensorSpecies} {n n' n2 : ℕ} {c : Fin n → S.C} {c' : Fin n' → S.C} (c2 : Fin n2 → S.C) (σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c') :
IndexNotation.OverColor.mk (Sum.elim (IndexNotation.OverColor.mk c).hom (IndexNotation.OverColor.mk c2).hom ∘ ⇑finSumFinEquiv.symm) ⟶ IndexNotation.OverColor.mk (Sum.elim (IndexNotation.OverColor.mk c').hom (IndexNotation.OverColor.mk c2).hom ∘ ⇑finSumFinEquiv.symm)

The permutation that arises when moving a perm node in the left entry through a prod node. This permutation is defined using right-whiskering and composition with finSumFinEquiv based-isomorphisms.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TensorTree.permProdLeft_toEquiv {S : TensorSpecies} {n n' n2 : ℕ} {c : Fin n → S.C} {c' : Fin n' → S.C} (c2 : Fin n2 → S.C) (σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c') :
    IndexNotation.OverColor.Hom.toEquiv (permProdLeft c2 σ) = finSumFinEquiv.symm.trans (((IndexNotation.OverColor.Hom.toEquiv σ).sumCongr (Equiv.refl (Fin n2))).trans finSumFinEquiv)
    source
    def TensorTree.permProdRight {S : TensorSpecies} {n n' n2 : ℕ} {c : Fin n → S.C} {c' : Fin n' → S.C} (c2 : Fin n2 → S.C) (σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c') :
    IndexNotation.OverColor.mk (Sum.elim (IndexNotation.OverColor.mk c2).hom (IndexNotation.OverColor.mk c).hom ∘ ⇑finSumFinEquiv.symm) ⟶ IndexNotation.OverColor.mk (Sum.elim (IndexNotation.OverColor.mk c2).hom (IndexNotation.OverColor.mk c').hom ∘ ⇑finSumFinEquiv.symm)

    The permutation that arises when moving a perm node in the right entry through a prod node. This permutation is defined using left-whiskering and composition with finSumFinEquiv based-isomorphisms.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TensorTree.permProdRight_toEquiv {S : TensorSpecies} {n n' n2 : ℕ} {c : Fin n → S.C} {c' : Fin n' → S.C} (c2 : Fin n2 → S.C) (σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c') :
      IndexNotation.OverColor.Hom.toEquiv (permProdRight c2 σ) = finSumFinEquiv.symm.trans (((Equiv.refl (Fin n2)).sumCongr (IndexNotation.OverColor.Hom.toEquiv σ)).trans finSumFinEquiv)
      source
      theorem TensorTree.prod_perm_left {S : TensorSpecies} {n n' n2 : ℕ} {c : Fin n → S.C} {c' : Fin n' → S.C} (c2 : Fin n2 → S.C) (σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c') (t : TensorTree S c) (t2 : TensorTree S c2) :
      ((perm σ t).prod t2).tensor = (perm (permProdLeft c2 σ) (t.prod t2)).tensor

      When a prod acts on a perm node in the left entry, the perm node can be moved through the prod node via right-whiskering.

      source
      theorem TensorTree.prod_perm_right {S : TensorSpecies} {n n' n2 : ℕ} {c : Fin n → S.C} {c' : Fin n' → S.C} (c2 : Fin n2 → S.C) (σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c') (t2 : TensorTree S c2) (t : TensorTree S c) :
      (t2.prod (perm σ t)).tensor = (perm (permProdRight c2 σ) (t2.prod t)).tensor

      When a prod acts on a perm node in the right entry, the perm node can be moved through the prod node via left-whiskering.