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] (C G : Type) [Group G] (basisIdx : C → Type) [(c : C) → Fintype (basisIdx c)] [(c : C) → DecidableEq (basisIdx c)] : 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.

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

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

• basis (c : C) : Module.Basis (basisIdx c) k ↑(self.FD.obj { as := c })

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

• τ : C → 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.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G))

  The natural transformation describing contraction.

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

  Contraction is symmetric with respect to duals.

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

  The natural transformation describing the unit.

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

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

• contr_unit (c : C) (x : ↑(self.FD.obj { as := c })) : (Rep.Hom.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor (self.FD.obj { as := c })).hom) ((Rep.Hom.hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight (self.contr.app { as := c }) (self.FD.obj { as := c }))) ((Rep.Hom.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) (x ⊗ₜ[k] (Rep.Hom.hom (self.unit.app { as := c })) 1))) = x

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

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

  The natural transformation describing the metric.

• contr_metric (c : C) : (Rep.Hom.hom (β_ (self.FD.obj { as := c }) (self.FD.obj { as := self.τ c })).hom) ((Rep.Hom.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (self.FD.obj { as := c }) (CategoryTheory.MonoidalCategoryStruct.leftUnitor (self.FD.obj { as := self.τ c })).hom)) ((Rep.Hom.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (self.FD.obj { as := c }) (CategoryTheory.MonoidalCategoryStruct.whiskerRight (self.contr.app { as := c }) (self.FD.obj { as := self.τ c })))) ((Rep.Hom.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)) ((Rep.Hom.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) ((Rep.Hom.hom (self.metric.app { as := c })) 1 ⊗ₜ[k] (Rep.Hom.hom (self.metric.app { as := self.τ c })) 1))))) = (Rep.Hom.hom (self.unit.app { as := c })) 1

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

Non-categorial constructor

noncomputable def TensorSpecies.ofFunctions {G k : Type} [CommRing k] {C : Type} [Group G] {basisIdx : C → Type} [(c : C) → Fintype (basisIdx c)] [(c : C) → DecidableEq (basisIdx c)] (V : C → Type) [(c : C) → AddCommGroup (V c)] [(c : C) → Module k (V c)] (rep : (c : C) → Representation k G (V c)) (basis : (c : C) → Module.Basis (basisIdx c) k (V c)) (τ : C → C) (τ_involution : Function.Involutive τ) (contr : (c : C) → ((rep c).tprod (rep (τ c))).IntertwiningMap (Representation.trivial k G k)) (unit : (c : C) → (Representation.trivial k G k).IntertwiningMap ((rep (τ c)).tprod (rep c))) (metric : (c : C) → (Representation.trivial k G k).IntertwiningMap ((rep c).tprod (rep c))) (contr_tmul_symm : ∀ (c : C) (x : V c) (y : V (τ c)), (contr c) (x ⊗ₜ[k] y) = (contr (τ c)) (y ⊗ₜ[k] (Equiv.cast ⋯) x)) (unit_symm : ∀ (c : C), (unit c) 1 = (LinearMap.lTensor (V (τ c)) ↑(LinearEquiv.cast ⋯)) ((TensorProduct.comm k (V (τ (τ c))) (V (τ c))) ((unit (τ c)) 1))) (contr_unit : ∀ (c : C) (x : V c), (TensorProduct.lid k (V c)) ((LinearMap.rTensor (V c) (contr c).toLinearMap) ((TensorProduct.assoc k (V c) (V (τ c)) (V c)).symm (x ⊗ₜ[k] (unit c) 1))) = x) (contr_metric : ∀ (c : C), (TensorProduct.comm k (V c) (V (τ c))) ((LinearEquiv.lTensor (V c) (TensorProduct.lid k (V (τ c)))) ((LinearMap.lTensor (V c) (LinearMap.rTensor (V (τ c)) (contr c).toLinearMap)) ((LinearMap.lTensor (V c) ↑(TensorProduct.assoc k (V c) (V (τ c)) (V (τ c))).symm) ((TensorProduct.assoc k (V c) (V c) (TensorProduct k (V (τ c)) (V (τ c)))) ((metric c) 1 ⊗ₜ[k] (metric (τ c)) 1))))) = (unit c) 1) : TensorSpecies k C G basisIdx

The creation of an element of TensorSpecies from functions rather than categorical objects.

Equations

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

Properties of TensorSpecies

def TensorSpecies.basisIdxCongr {C : Type} {basisIdx : C → Type} {c c1 : C} (h : c = c1) : basisIdx c ≃ basisIdx c1

The casting between basisIdx c and basisIdx c1.

Equations

• TensorSpecies.basisIdxCongr h = Equiv.cast ⋯

@[simp]

theorem TensorSpecies.basisIdxCongr_rfl {C : Type} {basisIdx : C → Type} (c : C) (i : basisIdx c) : (basisIdxCongr ⋯) i = i

@[simp]

theorem TensorSpecies.basisIdxCongr_apply_apply {C : Type} {basisIdx : C → Type} {c c1 c2 : C} (h1 : c = c1) (h2 : c1 = c2) (i : basisIdx c) : (basisIdxCongr h2) ((basisIdxCongr h1) i) = (basisIdxCongr ⋯) i

@[simp]

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

theorem TensorSpecies.basis_congr {G k : Type} [CommRing k] {C : Type} [Group G] {basisIdx : C → Type} [(c : C) → Fintype (basisIdx c)] [(c : C) → DecidableEq (basisIdx c)] (S : TensorSpecies k C G basisIdx) {c c1 : C} (h : c = c1) (i : basisIdx c) : (S.basis c) i = (CategoryTheory.ConcreteCategory.hom (S.FD.map (CategoryTheory.eqToHom ⋯))) ((S.basis c1) ((basisIdxCongr h) i))

theorem TensorSpecies.map_basis_eq {G k : Type} [CommRing k] {C : Type} [Group G] {basisIdx : C → Type} [(c : C) → Fintype (basisIdx c)] [(c : C) → DecidableEq (basisIdx c)] (S : TensorSpecies k C G basisIdx) {c c1 : C} (h : c = c1) (i : basisIdx c) : (Rep.Hom.hom (S.FD.map (CategoryTheory.Discrete.eqToHom h))) ((S.basis c) i) = (S.basis c1) ((basisIdxCongr h) i)

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

theorem TensorSpecies.FD_map_basis {G k : Type} [CommRing k] {C : Type} [Group G] {basisIdx : C → Type} [(c : C) → Fintype (basisIdx c)] [(c : C) → DecidableEq (basisIdx c)] (S : TensorSpecies k C G basisIdx) {c c1 : C} (h : c = c1) (i : basisIdx c) : (Rep.Hom.hom (S.FD.map (CategoryTheory.Discrete.eqToHom h))) ((S.basis c) i) = (S.basis c1) ((basisIdxCongr ⋯) i)

theorem TensorSpecies.repr_ρ_basis_FDTransport {G k : Type} [CommRing k] {C : Type} [Group G] {basisIdx : C → Type} [(c : C) → Fintype (basisIdx c)] [(c : C) → DecidableEq (basisIdx c)] (S : TensorSpecies k C G basisIdx) {c c₁ : C} (h : c = c₁) (g : G) (i b : basisIdx c) : ((S.basis c).repr (((S.FD.obj { as := c }).ρ g) ((S.basis c) b))) i = ((S.basis c₁).repr (((S.FD.obj { as := c₁ }).ρ g) ((S.basis c₁) ((basisIdxCongr ⋯) b)))) ((basisIdxCongr ⋯) i)

Categorical bookkeeping: relate basis.repr of ρ g on a basis vector before and after identifying slot colors c and c₁ via Discrete.eqToHom (basis_congr_repr, Rep.hom_comm_apply, FD_map_basis chained). Not a physical statement; use for component calculations.

noncomputable def TensorSpecies.F {G k : Type} [CommRing k] {C : Type} [Group G] {basisIdx : C → Type} [(c : C) → Fintype (basisIdx c)] [(c : C) → DecidableEq (basisIdx c)] (S : TensorSpecies k C G basisIdx) : CategoryTheory.Functor (IndexNotation.OverColor 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 {G k : Type} [CommRing k] {C : Type} [Group G] {basisIdx : C → Type} [(c : C) → Fintype (basisIdx c)] [(c : C) → DecidableEq (basisIdx c)] (S : TensorSpecies k C G basisIdx) : S.F = (IndexNotation.OverColor.lift.obj S.FD).toFunctor

@[implicit_reducible]

noncomputable instance TensorSpecies.F_monoidal {G k : Type} [CommRing k] {C : Type} [Group G] {basisIdx : C → Type} [(c : C) → Fintype (basisIdx c)] [(c : C) → DecidableEq (basisIdx c)] (S : TensorSpecies k C G basisIdx) : S.F.Monoidal

The functor F is monoidal.

Equations

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

@[implicit_reducible]

noncomputable instance TensorSpecies.F_laxBraided {G k : Type} [CommRing k] {C : Type} [Group G] {basisIdx : C → Type} [(c : C) → Fintype (basisIdx c)] [(c : C) → DecidableEq (basisIdx c)] (S : TensorSpecies k C G basisIdx) : S.F.LaxBraided

The functor F is lax-braided.

Equations

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

@[implicit_reducible]

noncomputable instance TensorSpecies.F_braided {G k : Type} [CommRing k] {C : Type} [Group G] {basisIdx : C → Type} [(c : C) → Fintype (basisIdx c)] [(c : C) → DecidableEq (basisIdx c)] (S : TensorSpecies k C G basisIdx) : S.F.Braided

The functor F is braided.

Equations

• S.F_braided = { toMonoidal := S.F_monoidal, braided := ⋯ }

def TensorSpecies.castToField {G k : Type} [CommRing k] {C : Type} [Group G] {basisIdx : C → Type} [(c : C) → Fintype (basisIdx c)] [(c : C) → DecidableEq (basisIdx c)] {c : C} {S : TensorSpecies k C G basisIdx} (v : ↑((CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G))).obj { as := c })) : k

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

Equations

• TensorSpecies.castToField v = v

theorem TensorSpecies.castToField_eq_self {G k : Type} [CommRing k] {C : Type} [Group G] {basisIdx : C → Type} [(c : C) → Fintype (basisIdx c)] [(c : C) → DecidableEq (basisIdx c)] {S : TensorSpecies k C G basisIdx} {c : C} (v : ↑((CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G))).obj { as := c })) : castToField v = v

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

Some properties of contractions

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

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

The number of indices n from a tensor.

Equations

• TensorSpecies.numIndices x✝ = n