Isomorphism between rep of color c and rep of dual color.

def TensorSpecies.toDualRep (S : TensorSpecies) (c : S.C) : S.FD.obj { as := c } ⟶ S.FD.obj { as := S.τ c }

The morphism from S.FD.obj (Discrete.mk c) to S.FD.obj (Discrete.mk (S.τ c)) defined by contracting with the metric.

Equations

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

theorem TensorSpecies.toDualRep_congr (S : TensorSpecies) {c c' : S.C} (h : c = c') : S.toDualRep c = CategoryTheory.CategoryStruct.comp (S.FD.map (CategoryTheory.Discrete.eqToHom h)) (CategoryTheory.CategoryStruct.comp (S.toDualRep c') (S.FD.map (CategoryTheory.Discrete.eqToHom ⋯)))

The toDualRep for equal colors is the same, up-to conjugation by a trivial equivalence.

def TensorSpecies.fromDualRep (S : TensorSpecies) (c : S.C) : S.FD.obj { as := S.τ c } ⟶ S.FD.obj { as := c }

The morphism from S.FD.obj (Discrete.mk (S.τ c)) to S.FD.obj (Discrete.mk c) defined by contracting with the metric.

Equations

• S.fromDualRep c = CategoryTheory.CategoryStruct.comp (S.toDualRep (S.τ c)) (S.FD.map (CategoryTheory.Discrete.eqToHom ⋯))

theorem TensorSpecies.toDualRep_apply_eq_contrOneTwoLeft (S : TensorSpecies) (c : S.C) (x : ↑(S.FD.obj { as := c }).V) : (CategoryTheory.ConcreteCategory.hom (S.toDualRep c).hom) x = (CategoryTheory.ConcreteCategory.hom (S.tensorToVec (S.τ c)).hom.hom) (contrOneTwoLeft ((CategoryTheory.ConcreteCategory.hom (S.tensorToVec c).inv.hom) x) (S.metricTensor (S.τ c)))

The rewriting of toDualRep in terms of contrOneTwoLeft.

theorem TensorSpecies.toDualRep_tensorTree (S : TensorSpecies) (c : S.C) (x : ↑(S.FD.obj { as := c }).V) : let y := (CategoryTheory.ConcreteCategory.hom (S.tensorToVec c).inv.hom) x; (CategoryTheory.ConcreteCategory.hom (S.toDualRep c).hom) x = (CategoryTheory.ConcreteCategory.hom (S.tensorToVec (S.τ c)).hom.hom) (TensorTree.perm (IndexNotation.OverColor.equivToHomEq (Equiv.refl (Fin 1)) ⋯) (TensorTree.contr 0 0 ⋯ ((TensorTree.tensorNode y).prod (TensorTree.tensorNode (S.metricTensor (S.τ c)))))).tensor

Expansion of toDualRep is (S.tensorToVec c).inv.hom x | μ ⊗ S.metricTensor (S.τ c) | μ ν.

theorem TensorSpecies.fromDualRep_tensorTree (S : TensorSpecies) (c : S.C) (x : ↑(S.FD.obj { as := S.τ c }).V) : let y := (CategoryTheory.ConcreteCategory.hom (S.tensorToVec (S.τ c)).inv.hom) x; (ModuleCat.Hom.hom (S.fromDualRep c).hom) x = (CategoryTheory.ConcreteCategory.hom (S.tensorToVec c).hom.hom) (TensorTree.perm (IndexNotation.OverColor.equivToHomEq (Equiv.refl (Fin 1)) ⋯) (TensorTree.contr 0 0 ⋯ ((TensorTree.tensorNode y).prod (TensorTree.tensorNode (S.metricTensor (S.τ (S.τ c))))))).tensor

theorem TensorSpecies.toDualRep_fromDualRep_tensorTree_metrics (S : TensorSpecies) (c : S.C) (x : ↑(S.FD.obj { as := c }).V) : let y := (CategoryTheory.ConcreteCategory.hom (S.tensorToVec c).inv.hom) x; (CategoryTheory.ConcreteCategory.hom (S.fromDualRep c).hom) ((CategoryTheory.ConcreteCategory.hom (S.toDualRep c).hom) x) = (CategoryTheory.ConcreteCategory.hom (S.tensorToVec c).hom.hom) (TensorTree.perm (IndexNotation.OverColor.equivToHomEq (Equiv.refl (Fin 1)) ⋯) (TensorTree.contr 0 0 ⋯ ((TensorTree.contr 0 0 ⋯ ((TensorTree.tensorNode y).prod (TensorTree.tensorNode (S.metricTensor (S.τ c))))).prod (TensorTree.tensorNode (S.metricTensor (S.τ (S.τ c))))))).tensor

Applying toDualRep followed by fromDualRep is equivalent to contracting with two metric tensors on the right.

theorem TensorSpecies.toDualRep_fromDualRep_tensorTree_unitTensor (S : TensorSpecies) (c : S.C) (x : ↑(S.FD.obj { as := c }).V) : let y := (CategoryTheory.ConcreteCategory.hom (S.tensorToVec c).inv.hom) x; (CategoryTheory.ConcreteCategory.hom (S.fromDualRep c).hom) ((CategoryTheory.ConcreteCategory.hom (S.toDualRep c).hom) x) = (CategoryTheory.ConcreteCategory.hom (S.tensorToVec c).hom.hom) (TensorTree.perm (IndexNotation.OverColor.equivToHomEq (Equiv.refl (Fin 1)) ⋯) (TensorTree.contr 0 0 ⋯ ((TensorTree.tensorNode y).prod (TensorTree.tensorNode (S.unitTensor c))))).tensor

Applying toDualRep followed by fromDualRep is equivalent to contracting with a unit tensors on the right.

theorem TensorSpecies.toDualRep_fromDualRep_tensorTree (S : TensorSpecies) (c : S.C) (x : ↑(S.FD.obj { as := c }).V) : let y := (CategoryTheory.ConcreteCategory.hom (S.tensorToVec c).inv.hom) x; (CategoryTheory.ConcreteCategory.hom (S.fromDualRep c).hom) ((CategoryTheory.ConcreteCategory.hom (S.toDualRep c).hom) x) = (CategoryTheory.ConcreteCategory.hom (S.tensorToVec c).hom.hom) (TensorTree.tensorNode y).tensor

theorem TensorSpecies.toDualRep_fromDualRep_eq_self (S : TensorSpecies) (c : S.C) (x : ↑(S.FD.obj { as := c }).V) : (CategoryTheory.ConcreteCategory.hom (S.fromDualRep c).hom) ((CategoryTheory.ConcreteCategory.hom (S.toDualRep c).hom) x) = x

theorem TensorSpecies.fromDualRep_toDualRep_eq_self (S : TensorSpecies) (c : S.C) (x : ↑(S.FD.obj { as := S.τ c }).V) : (CategoryTheory.ConcreteCategory.hom (S.toDualRep c).hom) ((CategoryTheory.ConcreteCategory.hom (S.fromDualRep c).hom) x) = x

def TensorSpecies.dualRepIsoDiscrete (S : TensorSpecies) (c : S.C) : S.FD.obj { as := c } ≅ S.FD.obj { as := S.τ c }

The isomorphism between the representation associated with a color, and that associated with its dual.

Equations

• S.dualRepIsoDiscrete c = { hom := S.toDualRep c, inv := S.fromDualRep c, hom_inv_id := ⋯, inv_hom_id := ⋯ }

def TensorSpecies.dualRepIso : InformalDefinition

Given a i : Fin n the isomorphism between S.F.obj (OverColor.mk c) and S.F.obj (OverColor.mk (Function.update c i (S.τ (c i)))) induced by dualRepIsoDiscrete acting on the i-th component of the color.

Equations

• TensorSpecies.dualRepIso = { deps := [`TensorSpecies.dualRepIsoDiscrete] }

def TensorSpecies.dualRepIso_unitTensor_fst : InformalLemma

Acting with dualRepIso on the fst component of a unitTensor returns a metric.

Equations

• TensorSpecies.dualRepIso_unitTensor_fst = { deps := [`TensorSpecies.dualRepIso, `TensorSpecies.unitTensor, `TensorSpecies.metricTensor] }

def TensorSpecies.dualRepIso_unitTensor_snd : InformalLemma

Acting with dualRepIso on the snd component of a unitTensor returns a metric.

Equations

• TensorSpecies.dualRepIso_unitTensor_snd = { deps := [`TensorSpecies.dualRepIso, `TensorSpecies.unitTensor, `TensorSpecies.metricTensor] }

def TensorSpecies.dualRepIso_metricTensor_fst : InformalLemma

Acting with dualRepIso on the fst component of a metricTensor returns a unitTensor.

Equations

• TensorSpecies.dualRepIso_metricTensor_fst = { deps := [`TensorSpecies.dualRepIso, `TensorSpecies.unitTensor, `TensorSpecies.metricTensor] }

def TensorSpecies.dualRepIso_metricTensor_snd : InformalLemma

Acting with dualRepIso on the snd component of a metricTensor returns a unitTensor.

Equations

• TensorSpecies.dualRepIso_metricTensor_snd = { deps := [`TensorSpecies.dualRepIso, `TensorSpecies.unitTensor, `TensorSpecies.metricTensor] }