Evaluation of tensor indices

## The evaluation coefficient.

noncomputable def TensorSpecies.Tensor.Pure.evalPCoeff {k : Type} [CommRing k] {C G : 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 + 1) → C} (i : Fin (n + 1)) (b : basisIdx (c i)) (p : Pure S c) : k

Given a i : Fin (n + 1), a b : basisIdx (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] {C G : 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 + 1) → C} (i : Fin (n + 1)) [inst : DecidableEq (Fin (n + 1))] (b : basisIdx (c i)) (p : Pure S c) (x : ↑(S.FD.obj { as := c i })) : 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] {C G : 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 + 1) → C} (i : Fin (n + 1)) [inst : DecidableEq (Fin (n + 1))] (j : Fin n) (b : basisIdx (c i)) (p : Pure S c) (x : ↑(S.FD.obj { as := c (i.succAbove j) })) : evalPCoeff i b (p.update (i.succAbove j) x) = evalPCoeff i b p

theorem TensorSpecies.Tensor.Pure.evalPCoeff_basisVector {k : Type} [CommRing k] {C G : 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 + 1) → C} (i : Fin (n + 1)) (b : basisIdx (c i)) (b' : ComponentIdx c) : evalPCoeff i b (basisVector c b') = if b' i = b then 1 else 0

Evaluation for a pure tensor.

noncomputable def TensorSpecies.Tensor.Pure.evalP {k : Type} [CommRing k] {C G : 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 + 1) → C} (i : Fin (n + 1)) (b : basisIdx (c i)) (p : Pure S c) : S.Tensor (c ∘ i.succAbove)

Given a i : Fin (n + 1), a b : basisIdx (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] {C G : 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 + 1) → C} [inst : DecidableEq (Fin (n + 1))] (i j : Fin (n + 1)) (b : basisIdx (c i)) (p : Pure S c) (x y : ↑(S.FD.obj { as := c j })) : 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] {C G : 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 + 1) → C} [inst : DecidableEq (Fin (n + 1))] (i j : Fin (n + 1)) (b : basisIdx (c i)) (p : Pure S c) (r : k) (x : ↑(S.FD.obj { as := c j })) : 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] {C G : 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 + 1) → C} (i : Fin (n + 1)) (b : basisIdx (c i)) : MultilinearMap k (fun (i : Fin (n + 1)) => ↑(S.FD.obj { as := c i })) (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] {C G : 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 + 1) → C} (i : Fin (n + 1)) (b : basisIdx (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)

@[simp]

theorem TensorSpecies.Tensor.evalT_pure {k : Type} [CommRing k] {C G : 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 + 1) → C} (i : Fin (n + 1)) (b : basisIdx (c i)) (p : Pure S c) : (evalT i b) p.toTensor = Pure.evalP i b p

theorem TensorSpecies.Tensor.evalT_basis {k : Type} [CommRing k] {C G : 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 + 1) → C} (i : Fin (n + 1)) (b : ComponentIdx c) (x : basisIdx (c i)) : (evalT i x) ((basis c) b) = if b i = x then (basis (c ∘ i.succAbove)) fun (j : Fin n) => b (i.succAbove j) else 0