Tensor species

• A tensor species is a structure including all of the ingredients needed to define a type of tensor.
• Examples of tensor species will include real Lorentz tensors, complex Lorentz tensors, and Einstein tensors.
• Tensor species are built upon symmetric monoidal categories.

structure TensorSpecies (k : Type) [CommRing k] (G : Type) [Group G] : Type 1

The structure TensorSpecies contains the necessary structure needed to define a system of tensors with index notation. Examples of TensorSpecies include real Lorentz tensors, complex Lorentz tensors, and ordinary Euclidean tensors.

• C : Type

  The colors of indices e.g. up or down.

• FD : CategoryTheory.Functor (CategoryTheory.Discrete self.C) (Rep k G)

  A functor from C to Rep k G giving our building block representations. Equivalently a function C → Re k G.

• repDim : self.C → ℕ

  A specification of the dimension of each color in C. This will be used for explicit evaluation of tensors.

• repDim_neZero (c : self.C) : NeZero (self.repDim c)

  repDim is not zero for any color. This allows casting of ℕ to Fin (S.repDim c).

• basis (c : self.C) : Basis (Fin (self.repDim c)) k ↑(self.FD.obj { as := c }).V

  A basis for each Module, determined by the evaluation map.

• τ : self.C → self.C

  A map from C to C. An involution.

• τ_involution : Function.Involutive self.τ

  The condition that τ is an involution.

• contr : IndexNotation.OverColor.Discrete.pairτ self.FD self.τ ⟶ 𝟙_ (CategoryTheory.Functor (CategoryTheory.Discrete self.C) (Rep k G))

  The natural transformation describing contraction.

• contr_tmul_symm (c : self.C) (x : ↑(self.FD.obj { as := c }).V) (y : ↑(self.FD.obj { as := self.τ c }).V) : (CategoryTheory.ConcreteCategory.hom (self.contr.app { as := c }).hom) (x ⊗ₜ[k] y) = (CategoryTheory.ConcreteCategory.hom (self.contr.app { as := self.τ c }).hom) (y ⊗ₜ[k] (CategoryTheory.ConcreteCategory.hom (self.FD.map (CategoryTheory.Discrete.eqToHom ⋯)).hom) x)

  Contraction is symmetric with respect to duals.

• unit : 𝟙_ (CategoryTheory.Functor (CategoryTheory.Discrete self.C) (Rep k G)) ⟶ IndexNotation.OverColor.Discrete.τPair self.FD self.τ

  The natural transformation describing the unit.

• unit_symm (c : self.C) : (CategoryTheory.ConcreteCategory.hom (self.unit.app { as := c }).hom) 1 = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (self.FD.obj { as := self.τ c }) (self.FD.map (CategoryTheory.Discrete.eqToHom ⋯))).hom) ((CategoryTheory.ConcreteCategory.hom (β_ (self.FD.obj { as := self.τ (self.τ c) }) (self.FD.obj { as := self.τ c })).hom.hom) ((CategoryTheory.ConcreteCategory.hom (self.unit.app { as := self.τ c }).hom) 1))

  The unit is symmetric. The de-categorification of this lemma is: unitTensor_eq_permT_dual.

• contr_unit (c : self.C) (x : ↑(self.FD.obj { as := c }).V) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor (self.FD.obj { as := c })).hom.hom) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight (self.contr.app { as := c }) (self.FD.obj { as := c })).hom) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator (self.FD.obj { as := c }) (((CategoryTheory.Discrete.functor (CategoryTheory.Discrete.mk ∘ self.τ)).comp self.FD).obj { as := c }) (self.FD.obj { as := c })).inv.hom) (x ⊗ₜ[k] (CategoryTheory.ConcreteCategory.hom (self.unit.app { as := c }).hom) 1))) = x

  Contraction with unit leaves invariant. The de-categorification of this lemma is: contrT_single_unitTensor.

• metric : 𝟙_ (CategoryTheory.Functor (CategoryTheory.Discrete self.C) (Rep k G)) ⟶ IndexNotation.OverColor.Discrete.pair self.FD

  The natural transformation describing the metric.

• contr_metric (c : self.C) : (CategoryTheory.ConcreteCategory.hom (β_ (self.FD.obj { as := c }) (self.FD.obj { as := self.τ c })).hom.hom) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (self.FD.obj { as := c }) (CategoryTheory.MonoidalCategoryStruct.leftUnitor (self.FD.obj { as := self.τ c })).hom).hom) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (self.FD.obj { as := c }) (CategoryTheory.MonoidalCategoryStruct.whiskerRight (self.contr.app { as := c }) (self.FD.obj { as := self.τ c }))).hom) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (self.FD.obj { as := c }) (CategoryTheory.MonoidalCategoryStruct.associator (self.FD.obj { as := c }) (self.FD.obj { as := self.τ c }) (self.FD.obj { as := self.τ c })).inv).hom) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator (self.FD.obj { as := c }) (self.FD.obj { as := c }) (CategoryTheory.MonoidalCategoryStruct.tensorObj (self.FD.obj { as := self.τ c }) (self.FD.obj { as := self.τ c }))).hom.hom) ((CategoryTheory.ConcreteCategory.hom (self.metric.app { as := c }).hom) 1 ⊗ₜ[k] (CategoryTheory.ConcreteCategory.hom (self.metric.app { as := self.τ c }).hom) 1))))) = (CategoryTheory.ConcreteCategory.hom (self.unit.app { as := c }).hom) 1

  On contracting metrics we get back the unit. The de-categorification of this lemma is: contrT_metricTensor_metricTensor.

instance TensorSpecies.instNeZeroNatRepDim {k : Type} [CommRing k] {G : Type} [Group G] (S : TensorSpecies k G) (c : S.C) : NeZero (S.repDim c)

The field repDim of a TensorSpecies is non-zero for all colors.

@[simp]

theorem TensorSpecies.τ_τ_apply {k : Type} [CommRing k] {G : Type} [Group G] (S : TensorSpecies k G) (c : S.C) : S.τ (S.τ c) = c

theorem TensorSpecies.basis_congr {k : Type} [CommRing k] {G : Type} [Group G] (S : TensorSpecies k G) {c c1 : S.C} (h : c = c1) (i : Fin (S.repDim c)) : (S.basis c) i = (CategoryTheory.ConcreteCategory.hom (S.FD.map (CategoryTheory.eqToHom ⋯))) ((S.basis c1) (Fin.cast ⋯ i))

theorem TensorSpecies.basis_congr_repr {k : Type} [CommRing k] {G : Type} [Group G] (S : TensorSpecies k G) {c c1 : S.C} (h : c = c1) (i : Fin (S.repDim c)) (t : ↑(S.FD.obj { as := c }).V) : ((S.basis c).repr t) i = ((S.basis c1).repr ((CategoryTheory.ConcreteCategory.hom (S.FD.map (CategoryTheory.eqToHom ⋯))) t)) (Fin.cast ⋯ i)

theorem TensorSpecies.FD_map_basis {k : Type} [CommRing k] {G : Type} [Group G] (S : TensorSpecies k G) {c c1 : S.C} (h : c = c1) (i : Fin (S.repDim c)) : (ModuleCat.Hom.hom (S.FD.map (CategoryTheory.Discrete.eqToHom h)).hom) ((S.basis c) i) = (S.basis c1) (Fin.cast ⋯ i)

def TensorSpecies.F {k : Type} [CommRing k] {G : Type} [Group G] (S : TensorSpecies k G) : CategoryTheory.Functor (IndexNotation.OverColor S.C) (Rep k G)

The lift of the functor S.F to functor.

Equations

• S.F = (IndexNotation.OverColor.lift.obj S.FD).toFunctor

theorem TensorSpecies.F_def {k : Type} [CommRing k] {G : Type} [Group G] (S : TensorSpecies k G) : S.F = (IndexNotation.OverColor.lift.obj S.FD).toFunctor

instance TensorSpecies.F_monoidal {k : Type} [CommRing k] {G : Type} [Group G] (S : TensorSpecies k G) : S.F.Monoidal

The functor F is monoidal.

Equations

• S.F_monoidal = IndexNotation.OverColor.lift.instMonoidalRepObjFunctorDiscreteLaxBraidedFunctor S.FD

instance TensorSpecies.F_laxBraided {k : Type} [CommRing k] {G : Type} [Group G] (S : TensorSpecies k G) : S.F.LaxBraided

The functor F is lax-braided.

Equations

• S.F_laxBraided = IndexNotation.OverColor.lift.instLaxBraidedRepObjFunctorDiscreteLaxBraidedFunctor S.FD

instance TensorSpecies.F_braided {k : Type} [CommRing k] {G : Type} [Group G] (S : TensorSpecies k G) : S.F.Braided

The functor F is braided.

Equations

• S.F_braided = CategoryTheory.Functor.Braided.mk ⋯

def TensorSpecies.castToField {k : Type} [CommRing k] {G : Type} [Group G] (S : TensorSpecies k G) {c : S.C} (v : ↑((𝟙_ (CategoryTheory.Functor (CategoryTheory.Discrete S.C) (Rep k G))).obj { as := c }).V) : k

Casts an element of the monoidal unit of Rep k G to the field k.

Equations

• S.castToField v = v

def TensorSpecies.castFin0ToField {k : Type} [CommRing k] {G : Type} [Group G] (S : TensorSpecies k G) {c : Fin 0 → S.C} : ↑(S.F.obj (IndexNotation.OverColor.mk c)).V →ₗ[k] k

Casts an element of (S.F.obj (OverColor.mk c)).V for c a map from Fin 0 to an element of the field.

Equations

• S.castFin0ToField = ↑(PiTensorProduct.isEmptyEquiv (Fin 0))

theorem TensorSpecies.castFin0ToField_tprod {k : Type} [CommRing k] {G : Type} [Group G] (S : TensorSpecies k G) {c : Fin 0 → S.C} (x : (i : Fin 0) → ↑(S.FD.obj { as := c i }).V) : S.castFin0ToField ((PiTensorProduct.tprod k) x) = 1

Some properties of contractions

theorem TensorSpecies.contr_congr {k : Type} [CommRing k] {G : Type} [Group G] (S : TensorSpecies k G) (c c' : S.C) (h : c = c') (x : ↑(S.FD.obj { as := c }).V) (y : ↑(S.FD.obj { as := S.τ c }).V) : (CategoryTheory.ConcreteCategory.hom (S.contr.app { as := c }).hom) (x ⊗ₜ[k] y) = (CategoryTheory.ConcreteCategory.hom (S.contr.app { as := c' }).hom) ((CategoryTheory.ConcreteCategory.hom (S.FD.map (CategoryTheory.Discrete.eqToHom ⋯)).hom) x ⊗ₜ[k] (CategoryTheory.ConcreteCategory.hom (S.FD.map (CategoryTheory.Discrete.eqToHom ⋯)).hom) y)

def TensorSpecies.numIndices {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {n : ℕ} {c : Fin n → S.C} : ↑(S.F.obj (IndexNotation.OverColor.mk c)).V → ℕ

The number of indices n from a tensor.

Equations

• TensorSpecies.numIndices x✝ = n