Basis for tensors in a tensor species

@[reducible, inline]

abbrev TensorSpecies.Tensor.TensorInt {k : Type} [CommRing k] {G : Type} [Group G] (S : TensorSpecies k G) {n : ℕ} (c : Fin n → S.C) : Type

A tensor with integer components with respect to the basis.

Equations

• TensorSpecies.Tensor.TensorInt S c = (TensorSpecies.Tensor.ComponentIdx c → ℤ)

noncomputable def TensorSpecies.Tensor.TensorInt.toTensor {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {n : ℕ} {c : Fin n → S.C} (f : TensorInt S c) : S.Tensor c

The element of S.Tensor c created from a tensor TensorInt S c.

Equations

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

theorem TensorSpecies.Tensor.TensorInt.basis_repr_apply {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {n : ℕ} {c : Fin n → S.C} (f : TensorInt S c) (b : ComponentIdx c) : ((basis c).repr f.toTensor) b = ↑(f b)

theorem TensorSpecies.Tensor.basis_eq_tensorInt {k : Type} [CommRing k] {G : Type} [Group G] (S : TensorSpecies k G) {n : ℕ} {c : Fin n → S.C} (b : ComponentIdx c) : (basis c) b = TensorInt.toTensor fun (b' : ComponentIdx c) => if b = b' then 1 else 0