Basis for tensors in a tensor species

noncomputable def TensorSpecies.tensorOfInt {k : Type} [CommRing k] (S : TensorSpecies k) {n : ℕ} {c : Fin n → S.C} (f : ((j : Fin n) → Fin (S.repDim (c j))) → ℤ) : ↑(S.F.obj (IndexNotation.OverColor.mk c)).V

A tensor from a (Π j, Fin (S.repDim (c j))) → ℤ. All tensors which have integer coefficents with respect to tensorBasis are of this form.

Equations

• S.tensorOfInt f = (S.tensorBasis c).repr.symm ((Finsupp.linearEquivFunOnFinite k k ((j : Fin n) → Fin (S.repDim (c j)))).symm fun (j : (j : Fin n) → Fin (S.repDim (c j))) => ↑(f j))

@[simp]

theorem TensorSpecies.tensorOfInt_tensorBasis_repr_apply {k : Type} [CommRing k] (S : TensorSpecies k) {n : ℕ} {c : Fin n → S.C} (f : ((j : Fin n) → Fin (S.repDim (c j))) → ℤ) (b : (j : Fin n) → Fin (S.repDim (c j))) : ((S.tensorBasis c).repr (S.tensorOfInt f)) b = ↑(f b)

theorem TensorSpecies.tensorBasis_eq_ofInt {k : Type} [CommRing k] (S : TensorSpecies k) {n : ℕ} {c : Fin n → S.C} (b : (j : Fin n) → Fin (S.repDim (c j))) : (S.tensorBasis c) b = S.tensorOfInt fun (b' : (j : Fin n) → Fin (S.repDim (c j))) => if b = b' then 1 else 0