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 : 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.

• k : Type

  The commutative ring over which we want to consider the tensors to live in, usually ℝ or ℂ.

• k_commRing : CommRing self.k

  An instance of k as a commutative ring.

• G : Type

  The symmetry group acting on these tensor e.g. the Lorentz group or SL(2,ℂ).

• G_group : Group self.G

  An instance of G as a group.

• C : Type

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

• FD : CategoryTheory.Functor (CategoryTheory.Discrete self.C) (Rep self.k self.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)) self.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 self.k self.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 ⊗ₜ[self.k] y) = (CategoryTheory.ConcreteCategory.hom (self.contr.app { as := self.τ c }).hom) (y ⊗ₜ[self.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 self.k self.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.

• 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 ⊗ₜ[self.k] (CategoryTheory.ConcreteCategory.hom (self.unit.app { as := c }).hom) 1))) = x

  Contraction with unit leaves invariant.

• metric : 𝟙_ (CategoryTheory.Functor (CategoryTheory.Discrete self.C) (Rep self.k self.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 ⊗ₜ[self.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.

instance TensorSpecies.instCommRingK (S : TensorSpecies) : CommRing S.k

The field k of a TensorSpecies has the instance of a commutative ring.

Equations

• S.instCommRingK = S.k_commRing

instance TensorSpecies.instGroupG (S : TensorSpecies) : Group S.G

The field G of a TensorSpecies has the instance of a group.

Equations

• S.instGroupG = S.G_group

instance TensorSpecies.instNeZeroNatRepDim (S : TensorSpecies) (c : S.C) : NeZero (S.repDim c)

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

theorem TensorSpecies.FD_map_basis (S : TensorSpecies) {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 (S : TensorSpecies) : CategoryTheory.Functor (IndexNotation.OverColor S.C) (Rep S.k S.G)

The lift of the functor S.F to functor.

Equations

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

theorem TensorSpecies.F_def (S : TensorSpecies) : S.F = (IndexNotation.OverColor.lift.obj S.FD).toFunctor

instance TensorSpecies.F_monoidal (S : TensorSpecies) : S.F.Monoidal

The functor F is monoidal.

Equations

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

instance TensorSpecies.F_laxBraided (S : TensorSpecies) : S.F.LaxBraided

The functor F is lax-braided.

Equations

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

instance TensorSpecies.F_braided (S : TensorSpecies) : S.F.Braided

The functor F is braided.

Equations

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

theorem TensorSpecies.perm_contr_cond (S : TensorSpecies) {n : ℕ} {c c1 : Fin n.succ.succ → S.C} {i : Fin n.succ.succ} {j : Fin n.succ} (h : c1 (i.succAbove j) = S.τ (c1 i)) (σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c1) : c (Fin.succAbove ((IndexNotation.OverColor.Hom.toEquiv σ).symm i) ((IndexNotation.OverColor.Hom.toEquiv (IndexNotation.OverColor.extractOne i σ)).symm j)) = S.τ (c ((IndexNotation.OverColor.Hom.toEquiv σ).symm i))

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

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

Equations

• S.castToField v = v

def TensorSpecies.castFin0ToField (S : TensorSpecies) {c : Fin 0 → S.C} : ↑(S.F.obj (IndexNotation.OverColor.mk c)).V →ₗ[S.k] S.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 (S : TensorSpecies) {c : Fin 0 → S.C} (x : (i : Fin 0) → ↑(S.FD.obj { as := c i }).V) : S.castFin0ToField ((PiTensorProduct.tprod S.k) x) = 1

Evalutation of indices.

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

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

Equations

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

theorem TensorSpecies.evalIso_tprod (S : TensorSpecies) {n : ℕ} {c : Fin n.succ → S.C} (i : Fin n.succ) (x : (i : Fin n.succ) → ↑(S.FD.obj { as := c i }).V) : (CategoryTheory.ConcreteCategory.hom (S.evalIso c i).hom.hom) ((PiTensorProduct.tprod S.k) x) = x i ⊗ₜ[S.k] (PiTensorProduct.tprod S.k) fun (k : Fin n) => x (i.succAbove k)

def TensorSpecies.evalLinearMap (S : TensorSpecies) {n : ℕ} {c : Fin n.succ → S.C} (i : Fin n.succ) (e : Fin (S.repDim (c i))) : ↑(S.FD.obj { as := c i }).V →ₗ[S.k] S.k

The linear map giving the coordinate of a vector with respect to the given basis. Important Note: This is not a morphism in the category of representations. In general, it cannot be lifted thereto.

Equations

• S.evalLinearMap i e = { toFun := fun (v : ↑(S.FD.obj { as := c i }).V) => ((S.basis (c i)).repr v) e, map_add' := ⋯, map_smul' := ⋯ }

def TensorSpecies.evalMap (S : TensorSpecies) {n : ℕ} {c : Fin n.succ → S.C} (i : Fin n.succ) (e : Fin (S.repDim (c i))) : (S.F.obj (IndexNotation.OverColor.mk c)).V ⟶ (S.F.obj (IndexNotation.OverColor.mk (c ∘ i.succAbove))).V

The evaluation map, used to evaluate indices of tensors. Important Note: The evaluation map is in general, not equivariant with respect to group actions. It is a morphism in the underlying module category, not the category of representations.

Equations

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

theorem TensorSpecies.evalMap_tprod (S : TensorSpecies) {n : ℕ} {c : Fin n.succ → S.C} (i : Fin n.succ) (e : Fin (S.repDim (c i))) (x : (i : Fin n.succ) → ↑(S.FD.obj { as := c i }).V) : (CategoryTheory.ConcreteCategory.hom (S.evalMap i e)) ((PiTensorProduct.tprod S.k) x) = ((S.basis (c i)).repr (x i)) e • (PiTensorProduct.tprod S.k) fun (k : (CategoryTheory.Functor.id Type).obj (IndexNotation.OverColor.mk (c ∘ i.succAbove)).left) => x (i.succAbove k)

The equivalence turning vecs into tensors

def TensorSpecies.tensorToVec (S : TensorSpecies) (c : S.C) : S.F.obj (IndexNotation.OverColor.mk ![c]) ≅ S.FD.obj { as := c }

The equivalence between tensors based on ![c] and vectors in S.FD.obj (Discrete.mk c).

Equations

• S.tensorToVec c = IndexNotation.OverColor.forgetLiftAppCon S.FD c

theorem TensorSpecies.tensorToVec_inv_apply_expand (S : TensorSpecies) (c : S.C) (x : ↑(S.FD.obj { as := c }).V) : (CategoryTheory.ConcreteCategory.hom (S.tensorToVec c).inv.hom) x = (CategoryTheory.ConcreteCategory.hom ((IndexNotation.OverColor.lift.obj S.FD).map (IndexNotation.OverColor.mkIso ⋯).hom).hom) ((CategoryTheory.ConcreteCategory.hom (IndexNotation.OverColor.forgetLiftApp S.FD c).inv.hom) x)

theorem TensorSpecies.tensorToVec_naturality_eqToHom (S : TensorSpecies) (c c1 : S.C) (h : c = c1) : CategoryTheory.CategoryStruct.comp (S.tensorToVec c).hom (S.FD.map (CategoryTheory.Discrete.eqToHom h)) = CategoryTheory.CategoryStruct.comp (S.F.map (IndexNotation.OverColor.mkIso ⋯).hom) (S.tensorToVec c1).hom

theorem TensorSpecies.tensorToVec_naturality_eqToHom_apply (S : TensorSpecies) (c c1 : S.C) (h : c = c1) (x : ↑(S.F.obj (IndexNotation.OverColor.mk ![c])).V) : (CategoryTheory.ConcreteCategory.hom (S.FD.map (CategoryTheory.Discrete.eqToHom h)).hom) ((CategoryTheory.ConcreteCategory.hom (S.tensorToVec c).hom.hom) x) = (CategoryTheory.ConcreteCategory.hom (S.tensorToVec c1).hom.hom) ((CategoryTheory.ConcreteCategory.hom (S.F.map (IndexNotation.OverColor.mkIso ⋯).hom).hom) x)

Lift

def TensorSpecies.liftTensor (S : TensorSpecies) {n : ℕ} {c : Fin n → S.C} {E : Type} [AddCommMonoid E] [Module S.k E] : MultilinearMap S.k (fun (i : Fin n) => ↑(S.FD.obj { as := c i }).V) E ≃ₗ[S.k] ↑(S.F.obj (IndexNotation.OverColor.mk c)).V →ₗ[S.k] E

The lift of a linear map (S.F.obj (OverColor.mk c) →ₗ[S.k] E) to a multi-linear map from fun i => S.FD.obj (Discrete.mk (c i)) (i.e. pure tensors) to E.

Equations

• S.liftTensor = PiTensorProduct.lift

def TensorSpecies.numIndices {S : TensorSpecies} {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