Tensors

This module sets up the tensors used for index notation in Physlib.

Physics picture:

• Choose a symmetry group G (for example, the Lorentz group).
• Give each index kind a name called a color (encoded by a type C). In Lorentzian notation, a typical choice is two colors: up and down.
• For each color, choose a representation of G.
• Fix a basis for each color. This determines which values that index can take and lets us speak about tensor components explicitly.
• Specify a dual color for each color, telling us which index pairs can contract.
• For dual pairs, provide the contraction/unit/metric data used for contraction and for raising/lowering indices.

All of this structure is packaged as a TensorSpecies.

For S : TensorSpecies and a list of index colors c : Fin n → C:

• Tensor S c is the type of tensors with those indices.
• Pure S c is the type of pure tensors, i.e. tensors of the form v₀ ⊗ₜ v₁ ⊗ₜ v₂ ….
• ComponentIdx S c is the type of allowed component labels for those indices.

From this setup we get the usual index-notation operations in a uniform way: contraction, raising/lowering, and permutation of indices.

@[reducible, inline]

noncomputable abbrev TensorSpecies.Tensor {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 → C) : Type

The tensors associated with a list of indices of a given color c : Fin n → C.

Equations

• S.Tensor c = ↑(S.F.obj (IndexNotation.OverColor.mk c))

@[reducible, inline]

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

Given a list of indices c : Fin n → C e.g. ![.up, .down], the type ComponentIdx c is the type of components indexes of a tensor with those indices e.g. ⟨0, 2⟩ corresponding to T⁰₂.

Equations

• TensorSpecies.Tensor.ComponentIdx c = ((j : Fin n) → basisIdx (c j))

theorem TensorSpecies.Tensor.ComponentIdx.congr_right {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 → C} (b : ComponentIdx c) (i j : Fin n) (h : i = j) : b i = (basisIdxCongr ⋯) (b j)

def TensorSpecies.Tensor.ComponentIdx.cast {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 m : ℕ} {c : Fin n → C} {cm : Fin m → C} (h : n = m) (hc : c = cm ∘ Fin.cast h) (b : ComponentIdx c) : ComponentIdx cm

Casting of a ComponentIdx through equivalent color maps.

Equations

• TensorSpecies.Tensor.ComponentIdx.cast h hc b j = (TensorSpecies.basisIdxCongr ⋯) (b (Fin.cast ⋯ j))

Pure tensors

@[reducible, inline]

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

The type of pure tensors associated to a list of indices c : OverColor C. A pure tensor is a tensor which can be written in the form v1 ⊗ₜ v2 ⊗ₜ v3 ….

Equations

• TensorSpecies.Tensor.Pure S c = ((i : Fin n) → ↑(S.FD.obj { as := c i }))

@[simp]

theorem TensorSpecies.Tensor.Pure.congr_right {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 → C} (p : Pure S c) (i j : Fin n) (h : i = j) : (CategoryTheory.ConcreteCategory.hom (S.FD.map (CategoryTheory.eqToHom ⋯))) (p j) = p i

theorem TensorSpecies.Tensor.Pure.congr_mid {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 → C} (c' : C) (p : Pure S c) (i j : Fin n) (h : i = j) (hi : c i = c') (hj : c j = c') : (CategoryTheory.ConcreteCategory.hom (S.FD.map (CategoryTheory.eqToHom ⋯))) (p i) = (CategoryTheory.ConcreteCategory.hom (S.FD.map (CategoryTheory.eqToHom ⋯))) (p j)

theorem TensorSpecies.Tensor.Pure.map_mid_move_left {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 n1 : ℕ} {c : Fin n → C} {c1 : Fin n1 → C} (p : Pure S c) (p' : Pure S c1) {c' : C} (i : Fin n) (j : Fin n1) (hi : c i = c') (hj : c1 j = c') : (CategoryTheory.ConcreteCategory.hom (S.FD.map (CategoryTheory.eqToHom ⋯))) (p i) = (CategoryTheory.ConcreteCategory.hom (S.FD.map (CategoryTheory.eqToHom ⋯))) (p' j) ↔ (CategoryTheory.ConcreteCategory.hom (S.FD.map (CategoryTheory.eqToHom ⋯))) (p i) = p' j

theorem TensorSpecies.Tensor.Pure.map_map_apply {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 → C} (c1 c2 : C) (p : Pure S c) (i : Fin n) (f : { as := c i } ⟶ { as := c1 }) (g : { as := c1 } ⟶ { as := c2 }) : (CategoryTheory.ConcreteCategory.hom (S.FD.map g)) ((CategoryTheory.ConcreteCategory.hom (S.FD.map f)) (p i)) = (CategoryTheory.ConcreteCategory.hom (S.FD.map (CategoryTheory.CategoryStruct.comp f g))) (p i)

noncomputable def TensorSpecies.Tensor.Pure.toTensor {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 → C} (p : Pure S c) : S.Tensor c

The tensor corresponding to a pure tensor.

Equations

• p.toTensor = (PiTensorProduct.tprod k) p

theorem TensorSpecies.Tensor.Pure.toTensor_apply {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 → C) (p : Pure S c) : p.toTensor = (PiTensorProduct.tprod k) p

def TensorSpecies.Tensor.Pure.update {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 → C} [inst : DecidableEq (Fin n)] (p : Pure S c) (i : Fin n) (x : ↑(S.FD.obj { as := c i })) : Pure S c

Given a list of indices c of n indices, a pure tensor p, an element i : Fin n and a x in S.FD.obj (Discrete.mk (c i)) then update p i x corresponds to p where the ith part of p is replaced with x.

E.g. if n = 2 and p = v₀ ⊗ₜ v₁ then update p 0 x = x ⊗ₜ v₁.

Equations

• p.update i x = Function.update p i x

@[simp]

theorem TensorSpecies.Tensor.Pure.update_same {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 → C} [inst : DecidableEq (Fin n)] (p : Pure S c) (i : Fin n) (x : ↑(S.FD.obj { as := c i })) : p.update i x i = x

@[simp]

theorem TensorSpecies.Tensor.Pure.update_succAbove_apply {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))] (p : Pure S c) (i : Fin (n + 1)) (j : Fin n) (x : ↑(S.FD.obj { as := c (i.succAbove j) })) : p.update (i.succAbove j) x i = p i

@[simp]

theorem TensorSpecies.Tensor.Pure.toTensor_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 → C} [inst : DecidableEq (Fin n)] (p : Pure S c) (i : Fin n) (x y : ↑(S.FD.obj { as := c i })) : (p.update i (x + y)).toTensor = (p.update i x).toTensor + (p.update i y).toTensor

@[simp]

theorem TensorSpecies.Tensor.Pure.toTensor_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 → C} [inst : DecidableEq (Fin n)] (p : Pure S c) (i : Fin n) (r : k) (y : ↑(S.FD.obj { as := c i })) : (p.update i (r • y)).toTensor = r • (p.update i y).toTensor

def TensorSpecies.Tensor.Pure.drop {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} (p : Pure S c) (i : Fin (n + 1)) : Pure S (c ∘ i.succAbove)

Given a list of indices c of length n + 1, a pure tensor p and an i : Fin (n + 1), then drop p i is the tensor p with it's ith part dropped.

For example, if n = 2 and p = v₀ ⊗ₜ v₁ ⊗ₜ v₂ then drop p 1 = v₀ ⊗ₜ v₂.

Equations

• p.drop i j = p (i.succAbove j)

@[simp]

theorem TensorSpecies.Tensor.Pure.update_succAbove_drop {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))] (p : Pure S c) (i : Fin (n + 1)) (k✝ : Fin n) (x : ↑(S.FD.obj { as := c (i.succAbove k✝) })) : (p.update (i.succAbove k✝) x).drop i = (p.drop i).update k✝ x

@[simp]

theorem TensorSpecies.Tensor.Pure.update_drop_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} [inst : DecidableEq (Fin (n + 1))] (p : Pure S c) (i : Fin (n + 1)) (x : ↑(S.FD.obj { as := c i })) : (p.update i x).drop i = p.drop i

theorem TensorSpecies.Tensor.Pure.μ_toTensor_tmul_toTensor {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} {n1 n2 : ℕ} {c : Fin n1 → C} {c1 : Fin n2 → C} (t : Pure S c) (t1 : Pure S c1) : (Rep.Hom.hom (CategoryTheory.Functor.LaxMonoidal.μ S.F (IndexNotation.OverColor.mk c) (IndexNotation.OverColor.mk c1))) (t.toTensor ⊗ₜ[k] t1.toTensor) = (PiTensorProduct.tprod k) fun (x : (CategoryTheory.MonoidalCategoryStruct.tensorObj (IndexNotation.OverColor.mk c) (IndexNotation.OverColor.mk c1)).left) => match x with | Sum.inl i => t i | Sum.inr i => t1 i

Components

noncomputable def TensorSpecies.Tensor.Pure.component {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 → C} (p : Pure S c) (b : ComponentIdx c) : k

Given an element b of ComponentIdx c and a pure tensor p then component p b is the element of the ring k corresponding to the component of p in the direction b.

For example, if p = v ⊗ₜ w and b = ⟨0, 1⟩ then component p b = v⁰ ⊗ₜ w¹.

Equations

• p.component b = ∏ i : Fin n, ((S.basis (c i)).repr (p i)) (b i)

theorem TensorSpecies.Tensor.Pure.component_eq {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 → C} (p : Pure S c) (b : ComponentIdx c) : p.component b = ∏ i : Fin n, ((S.basis (c i)).repr (p i)) (b i)

theorem TensorSpecies.Tensor.Pure.component_eq_drop {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} (p : Pure S c) (i : Fin (n + 1)) (b : ComponentIdx c) : p.component b = ((S.basis (c i)).repr (p i)) (b i) * (p.drop i).component fun (j : Fin n) => b (i.succAbove j)

@[simp]

theorem TensorSpecies.Tensor.Pure.component_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 : ℕ} [inst : DecidableEq (Fin n)] {c : Fin n → C} (p : Pure S c) (i : Fin n) (x y : ↑(S.FD.obj { as := c i })) (b : ComponentIdx c) : (p.update i (x + y)).component b = (p.update i x).component b + (p.update i y).component b

@[simp]

theorem TensorSpecies.Tensor.Pure.component_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 : ℕ} [inst : DecidableEq (Fin n)] {c : Fin n → C} (p : Pure S c) (i : Fin n) (x : k) (y : ↑(S.FD.obj { as := c i })) (b : ComponentIdx c) : (p.update i (x • y)).component b = x * (p.update i y).component b

noncomputable def TensorSpecies.Tensor.Pure.componentMap {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 → C) : MultilinearMap k (fun (i : Fin n) => ↑(S.FD.obj { as := c i })) (ComponentIdx c → k)

The multilinear map taking pure tensors p to a map ComponentIdx c → k which when evaluated returns the components of p.

Equations

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

@[simp]

theorem TensorSpecies.Tensor.Pure.componentMap_apply {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 → C) (p : Pure S c) : (componentMap c) p = p.component

noncomputable def TensorSpecies.Tensor.Pure.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 → C) (b : ComponentIdx c) : Pure S c

Given an component idx b in ComponentIdx c, basisVector c b is the pure tensor formed by S.basis (c i) (b i).

Equations

• TensorSpecies.Tensor.Pure.basisVector c b i = (S.basis (c i)) (b i)

@[simp]

theorem TensorSpecies.Tensor.Pure.component_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 → C) (b1 b2 : ComponentIdx c) : (basisVector c b1).component b2 = if b1 = b2 then 1 else 0

theorem TensorSpecies.Tensor.induction_on_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 → C} {P : S.Tensor c → Prop} (h : ∀ (p : Pure S c), P p.toTensor) (hsmul : ∀ (r : k) (t : S.Tensor c), P t → P (r • t)) (hadd : ∀ (t1 t2 : S.Tensor c), P t1 → P t2 → P (t1 + t2)) (t : S.Tensor c) : P t

The basis

noncomputable def TensorSpecies.Tensor.componentMap {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 → C) : S.Tensor c →ₗ[k] ComponentIdx c → k

The linear map from tensors to its components.

Equations

• TensorSpecies.Tensor.componentMap c = PiTensorProduct.lift (TensorSpecies.Tensor.Pure.componentMap c)

@[simp]

theorem TensorSpecies.Tensor.componentMap_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 → C) (p : Pure S c) : (componentMap c) p.toTensor = (Pure.componentMap c) p

noncomputable def TensorSpecies.Tensor.ofComponents {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 → C) : (ComponentIdx c → k) →ₗ[k] S.Tensor c

The tensor created from it's components.

Equations

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

@[simp]

theorem TensorSpecies.Tensor.componentMap_ofComponents {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 → C) (f : ComponentIdx c → k) : (componentMap c) ((ofComponents c) f) = f

@[simp]

theorem TensorSpecies.Tensor.ofComponents_componentMap {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 → C) (t : S.Tensor c) : (ofComponents c) ((componentMap c) t) = t

noncomputable def TensorSpecies.Tensor.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 → C) : Module.Basis (ComponentIdx c) k (S.Tensor c)

The basis of tensors.

Equations

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

theorem TensorSpecies.Tensor.basis_congr {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} {c1 c2 : C} (h : c1 = c2) (x : basisIdx c1) (y : basisIdx c2) (hxy : y = (basisIdxCongr ⋯) x) : (CategoryTheory.ConcreteCategory.hom (S.FD.map (CategoryTheory.eqToHom ⋯))) ((S.basis c1) x) = (S.basis c2) y

theorem TensorSpecies.Tensor.basis_apply {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 → C) (b : ComponentIdx c) : (basis c) b = (Pure.basisVector c b).toTensor

@[simp]

theorem TensorSpecies.Tensor.basis_repr_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 → C) (p : Pure S c) : ⇑((basis c).repr p.toTensor) = p.component

theorem TensorSpecies.Tensor.induction_on_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 → C} {P : S.Tensor c → Prop} (h : ∀ (b : ComponentIdx c), P ((basis c) b)) (hzero : P 0) (hsmul : ∀ (r : k) (t : S.Tensor c), P t → P (r • t)) (hadd : ∀ (t1 t2 : S.Tensor c), P t1 → P t2 → P (t1 + t2)) (t : S.Tensor c) : P t

The rank

instance TensorSpecies.Tensor.instFiniteDimensional {n : ℕ} {k : Type} [Field 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) {c : Fin n → C} : FiniteDimensional k (S.Tensor c)

@[implicit_reducible]

noncomputable instance TensorSpecies.Tensor.instTopologicalSpace {n : ℕ} {k : Type} [RCLike 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) {c : Fin n → C} : TopologicalSpace (S.Tensor c)

Equations

• TensorSpecies.Tensor.instTopologicalSpace S = moduleTopology k (S.Tensor c)

instance TensorSpecies.Tensor.instIsTopologicalAddGroup {n : ℕ} {k : Type} [RCLike 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) {c : Fin n → C} : IsTopologicalAddGroup (S.Tensor c)

The action

@[implicit_reducible]

noncomputable instance TensorSpecies.Tensor.Pure.actionP {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 → C} : MulAction G (Pure S c)

Equations

• TensorSpecies.Tensor.Pure.actionP = { smul := fun (g : G) (p : TensorSpecies.Tensor.Pure S c) (i : Fin n) => ((S.FD.obj { as := c i }).ρ g) (p i), mul_smul := ⋯, one_smul := ⋯ }

@[implicit_reducible]

noncomputable instance TensorSpecies.Tensor.Pure.instSMul {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 → C} : SMul G (Pure S c)

Equations

• TensorSpecies.Tensor.Pure.instSMul = TensorSpecies.Tensor.Pure.actionP.toSMul

theorem TensorSpecies.Tensor.Pure.actionP_eq {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 → C} {g : G} {p : Pure S c} : g • p = fun (i : Fin n) => ((S.FD.obj { as := c i }).ρ g) (p i)

@[simp]

theorem TensorSpecies.Tensor.Pure.drop_actionP {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)} {p : Pure S c} (g : G) : (g • p).drop i = g • p.drop i

The action on tensors

@[implicit_reducible]

noncomputable instance TensorSpecies.Tensor.actionT {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 → C} : MulAction G (S.Tensor c)

Equations

• TensorSpecies.Tensor.actionT = { smul := fun (g : G) (t : S.Tensor c) => ((S.F.obj (IndexNotation.OverColor.mk c)).ρ g) t, mul_smul := ⋯, one_smul := ⋯ }

theorem TensorSpecies.Tensor.actionT_eq {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 → C} {g : G} {t : S.Tensor c} : g • t = ((S.F.obj (IndexNotation.OverColor.mk c)).ρ g) t

theorem TensorSpecies.Tensor.actionT_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 → C} {g : G} {p : Pure S c} : g • p.toTensor = (g • p).toTensor

theorem TensorSpecies.Tensor.actionT_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 → C} {g : G} {t1 t2 : S.Tensor c} : g • (t1 + t2) = g • t1 + g • t2

@[simp]

theorem TensorSpecies.Tensor.actionT_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 → C} {g : G} {r : k} {t : S.Tensor c} : g • r • t = r • g • t

theorem TensorSpecies.Tensor.actionT_zero {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 → C} {g : G} : g • 0 = 0

theorem TensorSpecies.Tensor.actionT_neg {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 → C} {g : G} {t : S.Tensor c} : g • -t = -(g • t)

Permutations

And their interactions with

• actions

def TensorSpecies.Tensor.PermCond {C : Type} {n m : ℕ} (c : Fin n → C) (c1 : Fin m → C) (σ : Fin m → Fin n) : Prop

Given two lists of indices c : Fin n → C and c1 : Fin m → C a map σ : Fin m → Fin n satisfies the condition PermCond c c1 σ if it is:

• A bijection
• Forms a commutative triangle with c and c1.

Equations

• TensorSpecies.Tensor.PermCond c c1 σ = (Function.Bijective σ ∧ ∀ (i : Fin m), c (σ i) = c1 i)

theorem TensorSpecies.Tensor.PermCond.auto {C : Type} {n m : ℕ} {c : Fin n → C} {c1 : Fin m → C} {σ : Fin m → Fin n} (h : PermCond c c1 σ := by { simp [PermCond]; try decide }) : PermCond c c1 σ

@[simp]

theorem TensorSpecies.Tensor.PermCond.on_id {C : Type} {n : ℕ} {c c1 : Fin n → C} : PermCond c c1 id ↔ ∀ (i : Fin n), c i = c1 i

theorem TensorSpecies.Tensor.PermCond.on_id_symm {C : Type} {n : ℕ} {c c1 : Fin n → C} (h : PermCond c1 c id) : PermCond c c1 id

def TensorSpecies.Tensor.PermCond.inv {C : Type} {n m : ℕ} {c : Fin n → C} {c1 : Fin m → C} (σ : Fin m → Fin n) (h : PermCond c c1 σ) : Fin n → Fin m

For a map σ satisfying PermCond c c1 σ, the inverse of that map.

Equations

• TensorSpecies.Tensor.PermCond.inv σ h = Fintype.bijInv ⋯

def TensorSpecies.Tensor.PermCond.toEquiv {C : Type} {n m : ℕ} {c : Fin n → C} {c1 : Fin m → C} {σ : Fin m → Fin n} (h : PermCond c c1 σ) : Fin n ≃ Fin m

For a map σ : Fin m → Fin n satisfying PermCond c c1 σ, that map lifted to an equivalence between Fin n and Fin m.

Equations

• h.toEquiv = { toFun := TensorSpecies.Tensor.PermCond.inv σ h, invFun := σ, left_inv := ⋯, right_inv := ⋯ }

theorem TensorSpecies.Tensor.PermCond.apply_inv_apply {C : Type} {n m : ℕ} {c : Fin n → C} {c1 : Fin m → C} (σ : Fin m → Fin n) (h : PermCond c c1 σ) (x : Fin m) : inv σ h (σ x) = x

theorem TensorSpecies.Tensor.PermCond.inv_apply_apply {C : Type} {n m : ℕ} {c : Fin n → C} {c1 : Fin m → C} (σ : Fin m → Fin n) (h : PermCond c c1 σ) (x : Fin n) : σ (inv σ h x) = x

theorem TensorSpecies.Tensor.PermCond.preserve_color {C : Type} {n m : ℕ} {c : Fin n → C} {c1 : Fin m → C} {σ : Fin m → Fin n} (h : PermCond c c1 σ) (x : Fin m) : c1 x = (c ∘ σ) x

@[simp]

theorem TensorSpecies.Tensor.PermCond.inv_perserve_color {C : Type} {n m : ℕ} {c : Fin n → C} {c1 : Fin m → C} {σ : Fin m → Fin n} (h : PermCond c c1 σ) (x : Fin n) : c1 (inv σ h x) = c x

theorem TensorSpecies.Tensor.PermCond.symm {C : Type} {n m : ℕ} {c : Fin n → C} {c1 : Fin m → C} {σ : Fin m → Fin n} (h : PermCond c c1 σ) : PermCond c1 c (inv σ h)

def TensorSpecies.Tensor.PermCond.toHom {C : Type} {n m : ℕ} {c : Fin n → C} {c1 : Fin m → C} {σ : Fin m → Fin n} (h : PermCond c c1 σ) : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c1

For a map σ : Fin m → Fin n satisfying PermCond c c1 σ, that map lifted to a morphism in the OverColor C category.

Equations

• h.toHom = IndexNotation.OverColor.equivToHomEq h.toEquiv ⋯

theorem TensorSpecies.Tensor.PermCond.ofHom {C : Type} {n m : ℕ} {c : Fin n → C} {c1 : Fin m → C} (σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c1) : PermCond c c1 ⇑(IndexNotation.OverColor.Hom.toEquiv σ).symm

Given a morphism in the OverColor C between c and c1 category the corresponding morphism (Hom.toEquiv σ).symm satisfies the PermCond.

theorem TensorSpecies.Tensor.PermCond.comp {C : Type} {n n1 n2 : ℕ} {c : Fin n → C} {c1 : Fin n1 → C} {c2 : Fin n2 → C} {σ : Fin n1 → Fin n} {σ2 : Fin n2 → Fin n1} (h : PermCond c c1 σ) (h2 : PermCond c1 c2 σ2) : PermCond c c2 (σ ∘ σ2)

The composition of two maps satisfying PermCond also satisfies the PermCond.

theorem TensorSpecies.Tensor.fin_cast_permCond {C : Type} (n n1 : ℕ) {c : Fin n → C} (h : n1 = n) : PermCond c (c ∘ Fin.cast h) (Fin.cast h)

Permutations

def TensorSpecies.Tensor.Pure.permP {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 m : ℕ} {c : Fin n → C} {c1 : Fin m → C} (σ : Fin m → Fin n) (h : PermCond c c1 σ) (p : Pure S c) : Pure S c1

Given a permutation σ : Fin m → Fin n of indices satisfying PermCond through h, and a pure tensor p, permP σ h p is the pure tensor permuted according to σ.

For example if m = n = 2 and σ = ![1, 0], and p = v ⊗ₜ w then permP σ _ p = w ⊗ₜ v.

Equations

• TensorSpecies.Tensor.Pure.permP σ h p i = (CategoryTheory.ConcreteCategory.hom (S.FD.map (CategoryTheory.eqToHom ⋯))) (p (σ i))

@[simp]

theorem TensorSpecies.Tensor.Pure.permP_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 m : ℕ} {c : Fin n → C} {c1 : Fin m → C} (σ : Fin m → Fin n) (h : PermCond c c1 σ) (b : ComponentIdx c) : permP σ h (basisVector c b) = basisVector c1 fun (i : Fin m) => (basisIdxCongr ⋯) (b (σ i))

noncomputable def TensorSpecies.Tensor.permT {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 m : ℕ} {c : Fin n → C} {c1 : Fin m → C} (σ : Fin m → Fin n) (h : PermCond c c1 σ) : S.Tensor c →ₗ[k] S.Tensor c1

Given a permutation σ : Fin m → Fin n of indices satisfying PermCond through h, and a tensor t, permT σ h t is the tensor tensor permuted according to σ.

Equations

• TensorSpecies.Tensor.permT σ h = { toFun := fun (t : S.Tensor c) => (Rep.Hom.hom (S.F.map h.toHom)) t, map_add' := ⋯, map_smul' := ⋯ }

theorem TensorSpecies.Tensor.permT_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 m : ℕ} {c : Fin n → C} {c1 : Fin m → C} {σ : Fin m → Fin n} (h : PermCond c c1 σ) (p : Pure S c) : (permT σ h) p.toTensor = (Pure.permP σ h p).toTensor

@[simp]

theorem TensorSpecies.Tensor.Pure.permP_id_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 → C} (p : Pure S c) : permP id ⋯ p = p

@[simp]

theorem TensorSpecies.Tensor.permT_id_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 → C} (t : S.Tensor c) : (permT id ⋯) t = t

theorem TensorSpecies.Tensor.permT_congr_eq_id {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 → C} (t : S.Tensor c) (σ : Fin n → Fin n) (hσ : PermCond c c σ) (h : σ = id) : (permT σ hσ) t = t

theorem TensorSpecies.Tensor.permT_congr_eq_id' {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 → C} (t t1 : S.Tensor c) (σ : Fin n → Fin n) (hσ : PermCond c c σ) (h : σ = id) (ht : t = t1) : (permT σ hσ) t = t1

@[simp]

theorem TensorSpecies.Tensor.permT_equivariant {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 m : ℕ} {c : Fin n → C} {c1 : Fin m → C} {σ : Fin m → Fin n} (h : PermCond c c1 σ) (g : G) (t : S.Tensor c) : (permT σ h) (g • t) = g • (permT σ h) t

theorem TensorSpecies.Tensor.Pure.permP_congr {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 m : ℕ} {c : Fin n → C} {c1 : Fin m → C} {σ σ1 : Fin m → Fin n} {h : PermCond c c1 σ} {h1 : PermCond c c1 σ1} {p p1 : Pure S c} (hmap : σ = σ1) (hpure : p = p1) : permP σ h p = permP σ1 h1 p1

theorem TensorSpecies.Tensor.permT_congr {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 m : ℕ} {c : Fin n → C} {c1 : Fin m → C} {σ σ1 : Fin m → Fin n} {h : PermCond c c1 σ} {h1 : PermCond c c1 σ1} (hmap : σ = σ1) {t t1 : S.Tensor c} (htensor : t = t1) : (permT σ h) t = (permT σ1 h1) t1

@[simp]

theorem TensorSpecies.Tensor.Pure.permP_permP {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 m1 m2 : ℕ} {c : Fin n → C} {c1 : Fin m1 → C} {c2 : Fin m2 → C} {σ : Fin m1 → Fin n} {σ2 : Fin m2 → Fin m1} (h : PermCond c c1 σ) (h2 : PermCond c1 c2 σ2) (p : Pure S c) : permP σ2 h2 (permP σ h p) = permP (σ ∘ σ2) ⋯ p

@[simp]

theorem TensorSpecies.Tensor.permT_permT {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 m1 m2 : ℕ} {c : Fin n → C} {c1 : Fin m1 → C} {c2 : Fin m2 → C} {σ : Fin m1 → Fin n} {σ2 : Fin m2 → Fin m1} (h : PermCond c c1 σ) (h2 : PermCond c1 c2 σ2) (t : S.Tensor c) : (permT σ2 h2) ((permT σ h) t) = (permT (σ ∘ σ2) ⋯) t

theorem TensorSpecies.Tensor.permT_basis_repr_symm_apply {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 m : ℕ} {c : Fin n → C} {c1 : Fin m → C} {σ : Fin m → Fin n} (h : PermCond c c1 σ) (t : S.Tensor c) (b : ComponentIdx c1) : ((basis c1).repr ((permT σ h) t)) b = ((basis c).repr t) fun (i : Fin n) => (basisIdxCongr ⋯) (b (PermCond.inv σ h i))

theorem TensorSpecies.Tensor.permT_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 m : ℕ} {c : Fin n → C} {c1 : Fin m → C} {σ : Fin m → Fin n} (h : PermCond c c1 σ) (b : ComponentIdx c) : (permT σ h) ((basis c) b) = (basis c1) fun (i : Fin m) => (basisIdxCongr ⋯) (b (σ i))

theorem TensorSpecies.Tensor.permT_eq_zero_iff {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 m : ℕ} {c : Fin n → C} {c1 : Fin m → C} {σ : Fin m → Fin n} (h : PermCond c c1 σ) (t : S.Tensor c) : (permT σ h) t = 0 ↔ t = 0

field

noncomputable def TensorSpecies.Tensor.toField {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} {c : Fin 0 → C} : S.Tensor c →ₗ[k] k

The linear map between tensors with zero indices and the underlying field k.

Equations

• TensorSpecies.Tensor.toField = ↑(PiTensorProduct.isEmptyEquiv (Fin 0))

theorem TensorSpecies.Tensor.toField_default {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} {c : Fin 0 → C} : toField default.toTensor = 1

@[simp]

theorem TensorSpecies.Tensor.toField_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} {c : Fin 0 → C} (p : Pure S c) : toField p.toTensor = 1

theorem TensorSpecies.Tensor.toField_permT {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} {c c1 : Fin 0 → C} (σ : Fin 0 → Fin 0) (h : PermCond c c1 σ) (t : S.Tensor c) : toField ((permT σ h) t) = toField t

@[simp]

theorem TensorSpecies.Tensor.toField_basis_default {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} {c : Fin 0 → C} : toField ((basis c) default) = 1

theorem TensorSpecies.Tensor.toField_eq_repr {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} {c : Fin 0 → C} (t : S.Tensor c) : toField t = ((basis c).repr t) fun (j : Fin 0) => j.elim0

@[simp]

theorem TensorSpecies.Tensor.toField_equivariant {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} {c : Fin 0 → C} (g : G) (t : S.Tensor c) : toField (g • t) = toField t