The contraction map

def TensorSpecies.contrFin1Fin1 (S : TensorSpecies) {n : ℕ} (c : Fin n.succ.succ → S.C) (i : Fin n.succ.succ) (j : Fin n.succ) (h : c (i.succAbove j) = S.τ (c i)) : S.F.obj (IndexNotation.OverColor.mk ((c ∘ ⇑(PhysLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)) ≅ (IndexNotation.OverColor.Discrete.pairτ S.FD S.τ).obj { as := c i }

The isomorphism between the image of a map Fin 1 ⊕ Fin 1 → S.C constructed by finExtractTwo under S.F.obj, and an object in the image of OverColor.Discrete.pairτ S.FD.

Equations

• One or more equations did not get rendered due to their size.

theorem TensorSpecies.contrFin1Fin1_inv_tmul (S : TensorSpecies) {n : ℕ} (c : Fin n.succ.succ → S.C) (i : Fin n.succ.succ) (j : Fin n.succ) (h : c (i.succAbove j) = S.τ (c i)) (x : ↑(S.FD.obj { as := c i }).V) (y : ↑(S.FD.obj { as := S.τ (c i) }).V) : (CategoryTheory.ConcreteCategory.hom (S.contrFin1Fin1 c i j h).inv.hom) (x ⊗ₜ[S.k] y) = (PiTensorProduct.tprod S.k) fun (k : (CategoryTheory.Functor.id Type).obj (IndexNotation.OverColor.mk ((c ∘ ⇑(PhysLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)).left) => match k with | Sum.inl 0 => x | Sum.inr 0 => (CategoryTheory.ConcreteCategory.hom (S.FD.map (CategoryTheory.eqToHom ⋯)).hom) y

theorem TensorSpecies.contrFin1Fin1_hom_hom_tprod (S : TensorSpecies) {n : ℕ} (c : Fin n.succ.succ → S.C) (i : Fin n.succ.succ) (j : Fin n.succ) (h : c (i.succAbove j) = S.τ (c i)) (x : (k : Fin 1 ⊕ Fin 1) → ↑(S.FD.obj { as := (IndexNotation.OverColor.mk ((c ∘ ⇑(PhysLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)).hom k }).V) : (CategoryTheory.ConcreteCategory.hom (S.contrFin1Fin1 c i j h).hom.hom) ((PiTensorProduct.tprod S.k) x) = x (Sum.inl 0) ⊗ₜ[S.k] (CategoryTheory.ConcreteCategory.hom (S.FD.map (CategoryTheory.eqToHom ⋯)).hom) (x (Sum.inr 0))

def TensorSpecies.contrIso (S : TensorSpecies) {n : ℕ} (c : Fin n.succ.succ → S.C) (i : Fin n.succ.succ) (j : Fin n.succ) (h : c (i.succAbove j) = S.τ (c i)) : S.F.obj (IndexNotation.OverColor.mk c) ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj ((IndexNotation.OverColor.Discrete.pairτ S.FD S.τ).obj { as := c i }) ((IndexNotation.OverColor.lift.obj S.FD).obj (IndexNotation.OverColor.mk (c ∘ i.succAbove ∘ j.succAbove)))

The isomorphism of objects in Rep S.k S.G given an i in Fin n.succ.succ and a j in Fin n.succ allowing us to undertake contraction.

Equations

• One or more equations did not get rendered due to their size.

theorem TensorSpecies.contrIso_hom_hom (S : TensorSpecies) {n : ℕ} {c1 : Fin n.succ.succ → S.C} {i : Fin n.succ.succ} {j : Fin n.succ} {h : c1 (i.succAbove j) = S.τ (c1 i)} : (S.contrIso c1 i j h).hom.hom = CategoryTheory.CategoryStruct.comp (S.F.map (IndexNotation.OverColor.equivToIso (PhysLean.Fin.finExtractTwo i j)).hom).hom (CategoryTheory.CategoryStruct.comp (S.F.map (IndexNotation.OverColor.mkSum (c1 ∘ ⇑(PhysLean.Fin.finExtractTwo i j).symm)).hom).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.Monoidal.μIso S.F (IndexNotation.OverColor.mk ((c1 ∘ ⇑(PhysLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)) (IndexNotation.OverColor.mk ((c1 ∘ ⇑(PhysLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv.hom (CategoryTheory.MonoidalCategoryStruct.tensorHom (S.contrFin1Fin1 c1 i j h).hom.hom (S.F.map (IndexNotation.OverColor.mkIso ⋯).hom).hom)))

def TensorSpecies.contrMap (S : TensorSpecies) {n : ℕ} (c : Fin n.succ.succ → S.C) (i : Fin n.succ.succ) (j : Fin n.succ) (h : c (i.succAbove j) = S.τ (c i)) : S.F.obj (IndexNotation.OverColor.mk c) ⟶ S.F.obj (IndexNotation.OverColor.mk (c ∘ i.succAbove ∘ j.succAbove))

contrMap is a function that takes a natural number n, a function c from Fin n.succ.succ to S.C, an index i of type Fin n.succ.succ, an index j of type Fin n.succ, and a proof h that c (i.succAbove j) = S.τ (c i). It returns a morphism corresponding to the contraction of the ith index with the i.succAbove j index.

Equations

• One or more equations did not get rendered due to their size.

theorem TensorSpecies.contrMap_tprod (S : TensorSpecies) {n : ℕ} (c : Fin n.succ.succ → S.C) (i : Fin n.succ.succ) (j : Fin n.succ) (h : c (i.succAbove j) = S.τ (c i)) (x : (i : Fin n.succ.succ) → ↑(S.FD.obj { as := c i }).V) : (CategoryTheory.ConcreteCategory.hom (S.contrMap c i j h).hom) ((PiTensorProduct.tprod S.k) x) = S.castToField ((CategoryTheory.ConcreteCategory.hom (S.contr.app { as := c i }).hom) (x i ⊗ₜ[S.k] (CategoryTheory.ConcreteCategory.hom (S.FD.map (CategoryTheory.Discrete.eqToHom h)).hom) (x (i.succAbove j)))) • (PiTensorProduct.tprod S.k) fun (k : (CategoryTheory.Functor.id Type).obj (IndexNotation.OverColor.mk (c ∘ i.succAbove ∘ j.succAbove)).left) => x (i.succAbove (j.succAbove k))

Acting with contrMap on a tprod gives a tprod multiplied by a scalar.