Evaluation of tensor indices

## The evaluation coefficent.

def TensorSpecies.Tensor.Pure.evalPCoeff {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {n : ℕ} {c : Fin (n + 1) → S.C} (i : Fin (n + 1)) (b : Fin (S.repDim (c i))) (p : Pure S c) : k

Given a i : Fin (n + 1), a b : Fin (S.repDim (c i)) and a pure tensor p : Pure S c, evalPCoeff i b p is the bth component of p i.

Equations

• TensorSpecies.Tensor.Pure.evalPCoeff i b p = ((S.basis (c i)).repr (p i)) b

@[simp]

theorem TensorSpecies.Tensor.Pure.evalPCoeff_update_self {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {n : ℕ} {c : Fin (n + 1) → S.C} (i : Fin (n + 1)) [inst : DecidableEq (Fin (n + 1))] (b : Fin (S.repDim (c i))) (p : Pure S c) (x : ↑(S.FD.obj { as := c i }).V) : evalPCoeff i b (p.update i x) = ((S.basis (c i)).repr x) b

@[simp]

theorem TensorSpecies.Tensor.Pure.evalPCoeff_update_succAbove {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {n : ℕ} {c : Fin (n + 1) → S.C} (i : Fin (n + 1)) [inst : DecidableEq (Fin (n + 1))] (j : Fin n) (b : Fin (S.repDim (c i))) (p : Pure S c) (x : ↑(S.FD.obj { as := c (i.succAbove j) }).V) : evalPCoeff i b (p.update (i.succAbove j) x) = evalPCoeff i b p

Evaluation for a pure tensor.

noncomputable def TensorSpecies.Tensor.Pure.evalP {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {n : ℕ} {c : Fin (n + 1) → S.C} (i : Fin (n + 1)) (b : Fin (S.repDim (c i))) (p : Pure S c) : S.Tensor (c ∘ i.succAbove)

Given a i : Fin (n + 1), a b : Fin (S.repDim (c i)) and a pure tensor p : Pure S c, evalP i b p is the tensor formed by evaluating the ith index of p at b.

Equations

• TensorSpecies.Tensor.Pure.evalP i b p = TensorSpecies.Tensor.Pure.evalPCoeff i b p • (p.drop i).toTensor

@[simp]

theorem TensorSpecies.Tensor.Pure.evalP_update_add {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {n : ℕ} {c : Fin (n + 1) → S.C} [inst : DecidableEq (Fin (n + 1))] (i j : Fin (n + 1)) (b : Fin (S.repDim (c i))) (p : Pure S c) (x y : ↑(S.FD.obj { as := c j }).V) : evalP i b (p.update j (x + y)) = evalP i b (p.update j x) + evalP i b (p.update j y)

@[simp]

theorem TensorSpecies.Tensor.Pure.evalP_update_smul {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {n : ℕ} {c : Fin (n + 1) → S.C} [inst : DecidableEq (Fin (n + 1))] (i j : Fin (n + 1)) (b : Fin (S.repDim (c i))) (p : Pure S c) (r : k) (x : ↑(S.FD.obj { as := c j }).V) : evalP i b (p.update j (r • x)) = r • evalP i b (p.update j x)

Evaluation for a pure tensor as multilinear map.

noncomputable def TensorSpecies.Tensor.Pure.evalPMultilinear {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {n : ℕ} {c : Fin (n + 1) → S.C} (i : Fin (n + 1)) (b : Fin (S.repDim (c i))) : MultilinearMap k (fun (i : Fin (n + 1)) => ↑(S.FD.obj { as := c i }).V) (S.Tensor (c ∘ i.succAbove))

The multi-linear map formed by evaluation of an index of pure tensors.

Equations

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

noncomputable def TensorSpecies.Tensor.evalT {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {n : ℕ} {c : Fin (n + 1) → S.C} (i : Fin (n + 1)) (b : Fin (S.repDim (c i))) : S.Tensor c →ₗ[k] S.Tensor (c ∘ i.succAbove)

Given a i : Fin (n + 1), a b : Fin (S.repDim (c i)) and a tensor t : Tensor S c, evalT i b t is the tensor formed by evaluating the ith index of t at b.

Equations

• TensorSpecies.Tensor.evalT i b = PiTensorProduct.lift (TensorSpecies.Tensor.Pure.evalPMultilinear i b)