The product of tensors

i. Overview

In this module we define the tensor product of

• index components of tensors,
• pure tensors, and
• tensors. We prove a number of properties about these products, for example, permutation of the factors, equivariance, and associativity.

ii. Key results

• Pure.prodP : The tensor product of two pure tensors.
• prodT : The tensor product of two tensors.

The following results exist for both prodP and prodT :

• prodT_swap : Swapping the order of the product of two tensors.
• prodT_permT_left : Permuting the indices of the left tensor commute with the product.
• prodT_permT_right : Permuting the indices of the right tensor commute with the product.
• prodT_equivariant : The product of two tensors is equivariant.
• prodT_assoc : The product of three tensors is associative.
• prodT_assoc' : The product of three tensors is associative in the other direction.

iii. Table of contents

• A. Products of index components
  • A.1. The product of component indices as an equivalence
• B. Products of pure tensors
  • B.1. Indexing pure tensors by Fin n1 ⊕ Fin n2 rather than Fin (n1 + n2)
  • B.2. The product of two pure tensors
  • B.3. The vectors making up product of two pure tensors
  • B.4. The product of two pure basis vectors
  • B.5. The basis components of the product of two pure tensors
  • B.6. Equivariance of the product of two pure tensors
  • B.7. Product with a tensor with no indices on the right
  • B.8. Swapping the order of the product of two pure tensors
  • B.9. Permuting the indices of the left tensor in a product
  • B.10. Permuting the indices of the right tensor in a product
  • B.11. Associativity of the product of three pure tensors in one direction
  • B.12. Associativity of the product of three pure tensors in the other direction
• C. Products of tensors
  • C.1. Indexing tensors by Fin n1 ⊕ Fin n2 rather than Fin (n1 + n2)
  • C.2. The product of two tensors
  • C.3. The product of two pure tensors as a tensor
  • C.4. The product of basis vectors
  • C.5. The product as an equivalence
  • C.6. Rewriting the basis for the product in terms of the tensor product basis
  • C.7. Equivariance of the product of two tensors
  • C.8. The product with the default tensor with no indices on the right
  • C.9. Swapping the order of the product of two tensors
  • C.10. Permuting the indices of the left tensor in a product
  • C.11. Permuting the indices of the right tensor in a product
  • C.12. Associativity of the product of three tensors in one direction
  • C.13. Associativity of the product of three tensors in the other direction

iv. References

• arXiv:2411.07667

A. Products of index components

A.1 The product of component indices as an equivalence

def TensorSpecies.Tensor.ComponentIdx.prod {k C G : Type} [CommRing k] [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} : ComponentIdx (Fin.append c c1) ≃ ComponentIdx c × ComponentIdx c1

The equivalence between ComponentIdx (Fin.append c c1) and ComponentIdx c × ComponentIdx c1 formed by products.

Equations

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

B. Products of pure tensors

B.1. Indexing pure tensors by Fin n1 ⊕ Fin n2 rather than Fin (n1 + n2)

def TensorSpecies.Tensor.Pure.prodIndexEquiv {k C G : Type} [CommRing k] [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} : Pure S (Fin.append c c1) ≃ ((i : Fin n1 ⊕ Fin n2) → ↑(S.FD.obj { as := Sum.elim c c1 i }))

The equivalence between pure tensors based on a product of lists of indices, and the type Π (i : Fin n1 ⊕ Fin n2), S.FD.obj (Discrete.mk ((Sum.elim c c1) i)).

Equations

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

B.2. The product of two pure tensors

def TensorSpecies.Tensor.Pure.prodP {k C G : Type} [CommRing k] [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} (p1 : Pure S c) (p2 : Pure S c1) : Pure S (Fin.append c c1)

Given two pure tensors p1 : Pure S c and p2 : Pure S c, prodP p p2 is the tensor product of those tensors returning an element in Pure S (Sum.elim c c1 ∘ ⇑finSumFinEquiv.symm).

Equations

• p1.prodP p2 = TensorSpecies.Tensor.Pure.prodIndexEquiv.symm fun (x : Fin n1 ⊕ Fin n2) => match x with | Sum.inl i => p1 i | Sum.inr i => p2 i

B.3. The vectors making up product of two pure tensors

theorem TensorSpecies.Tensor.Pure.prodP_apply_finSumFinEquiv {k C G : Type} [CommRing k] [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} (p1 : Pure S c) (p2 : Pure S c1) (i : Fin n1 ⊕ Fin n2) : p1.prodP p2 (finSumFinEquiv i) = match i with | Sum.inl i => (CategoryTheory.ConcreteCategory.hom (S.FD.map (CategoryTheory.eqToHom ⋯))) (p1 i) | Sum.inr i => (CategoryTheory.ConcreteCategory.hom (S.FD.map (CategoryTheory.eqToHom ⋯))) (p2 i)

@[simp]

theorem TensorSpecies.Tensor.Pure.prodP_apply_castAdd {k C G : Type} [CommRing k] [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} (p1 : Pure S c) (p2 : Pure S c1) (i : Fin n1) : p1.prodP p2 (Fin.castAdd n2 i) = (CategoryTheory.ConcreteCategory.hom (S.FD.map (CategoryTheory.eqToHom ⋯))) (p1 i)

@[simp]

theorem TensorSpecies.Tensor.Pure.prodP_apply_natAdd {k C G : Type} [CommRing k] [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} (p1 : Pure S c) (p2 : Pure S c1) (i : Fin n2) : p1.prodP p2 (Fin.natAdd n1 i) = (CategoryTheory.ConcreteCategory.hom (S.FD.map (CategoryTheory.eqToHom ⋯))) (p2 i)

B.4. The product of two pure basis vectors

theorem TensorSpecies.Tensor.Pure.prodP_basisVector {k C G : Type} [CommRing k] [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} (b : ComponentIdx c) (b1 : ComponentIdx c1) : (basisVector c b).prodP (basisVector c1 b1) = basisVector (Fin.append c c1) (ComponentIdx.prod.symm (b, b1))

B.5. The basis components of the product of two pure tensors

theorem TensorSpecies.Tensor.Pure.prodP_component {k C G : Type} [CommRing k] [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} (p : Pure S c) (p1 : Pure S c1) (b : ComponentIdx (Fin.append c c1)) : (p.prodP p1).component b = p.component (ComponentIdx.prod b).1 * p1.component (ComponentIdx.prod b).2

B.6. Equivariance of the product of two pure tensors

@[simp]

theorem TensorSpecies.Tensor.Pure.prodP_equivariant {k C G : Type} [CommRing k] [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} (g : G) (p : Pure S c) (p1 : Pure S c1) : (g • p).prodP (g • p1) = g • p.prodP p1

B.7. Product with a tensor with no indices on the right

theorem TensorSpecies.Tensor.Pure.prodP_zero_right_permCond {C : Type} {n : ℕ} {c : Fin n → C} {c1 : Fin 0 → C} : PermCond c (Fin.append c c1) id

theorem TensorSpecies.Tensor.Pure.prodP_zero_right {k C G : Type} [CommRing k] [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 : Fin 0 → C} (p : Pure S c) (p0 : Pure S c1) : p.prodP p0 = permP id ⋯ p

B.8. Swapping the order of the product of two pure tensors

def TensorSpecies.Tensor.prodSwapMap (n1 n2 : ℕ) : Fin (n1 + n2) → Fin (n2 + n1)

The map between Fin (n1 + n2) and Fin (n2 + n1) formed by swapping elements.

Equations

• TensorSpecies.Tensor.prodSwapMap n1 n2 = ⇑finSumFinEquiv ∘ Sum.swap ∘ ⇑finSumFinEquiv.symm

@[simp]

theorem TensorSpecies.Tensor.prodSwapMap_permCond {C : Type} {n1 n2 : ℕ} {c : Fin n1 → C} {c2 : Fin n2 → C} : PermCond (Fin.append c c2) (Fin.append c2 c) (prodSwapMap n2 n1)

theorem TensorSpecies.Tensor.Pure.prodP_swap {k C G : Type} [CommRing k] [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) (p1 : Pure S c1) : p.prodP p1 = permP (prodSwapMap n n1) ⋯ (p1.prodP p)

B.9. Permuting the indices of the left tensor in a product

def TensorSpecies.Tensor.prodLeftMap {n n' : ℕ} (n2 : ℕ) (σ : Fin n → Fin n') : Fin (n + n2) → Fin (n' + n2)

Given a map σ : Fin n → Fin n', the induced map Fin (n + n2) → Fin (n' + n2).

Equations

• TensorSpecies.Tensor.prodLeftMap n2 σ = ⇑finSumFinEquiv ∘ Sum.map σ id ∘ ⇑finSumFinEquiv.symm

@[simp]

theorem TensorSpecies.Tensor.prodLeftMap_id {n2 n : ℕ} : prodLeftMap n2 id = id

@[simp]

theorem TensorSpecies.Tensor.prodLeftMap_permCond {C : Type} {n n' n2 : ℕ} {c : Fin n → C} {c' : Fin n' → C} {σ : Fin n' → Fin n} (c2 : Fin n2 → C) (h : PermCond c c' σ) : PermCond (Fin.append c c2) (Fin.append c' c2) (prodLeftMap n2 σ)

@[simp]

theorem TensorSpecies.Tensor.Pure.prodP_permP_left {k C G : Type} [CommRing k] [Group G] {basisIdx : C → Type} [(c : C) → Fintype (basisIdx c)] [(c : C) → DecidableEq (basisIdx c)] {S : TensorSpecies k C G basisIdx} {n2 : ℕ} {c2 : Fin n2 → C} {n n' : ℕ} {c : Fin n → C} {c' : Fin n' → C} (σ : Fin n' → Fin n) (h : PermCond c c' σ) (p : Pure S c) (p2 : Pure S c2) : (permP σ h p).prodP p2 = permP (prodLeftMap n2 σ) ⋯ (p.prodP p2)

B.10. Permuting the indices of the right tensor in a product

def TensorSpecies.Tensor.prodRightMap {n n' : ℕ} (n2 : ℕ) (σ : Fin n → Fin n') : Fin (n2 + n) → Fin (n2 + n')

Given a map σ : Fin n → Fin n', the induced map Fin (n2 + n) → Fin (n2 + n').

Equations

• TensorSpecies.Tensor.prodRightMap n2 σ = ⇑finSumFinEquiv ∘ Sum.map id σ ∘ ⇑finSumFinEquiv.symm

@[simp]

theorem TensorSpecies.Tensor.prodRightMap_id {n2 n : ℕ} : prodRightMap n2 id = id

@[simp]

theorem TensorSpecies.Tensor.prodRightMap_permCond {C : Type} {n n' n2 : ℕ} {c : Fin n → C} {c' : Fin n' → C} {σ : Fin n' → Fin n} (c2 : Fin n2 → C) (h : PermCond c c' σ) : PermCond (Fin.append c2 c) (Fin.append c2 c') (prodRightMap n2 σ)

@[simp]

theorem TensorSpecies.Tensor.Pure.prodP_permP_right {k C G : Type} [CommRing k] [Group G] {basisIdx : C → Type} [(c : C) → Fintype (basisIdx c)] [(c : C) → DecidableEq (basisIdx c)] {S : TensorSpecies k C G basisIdx} {n2 : ℕ} {c2 : Fin n2 → C} {n n' : ℕ} {c : Fin n → C} {c' : Fin n' → C} (σ : Fin n' → Fin n) (h : PermCond c c' σ) (p : Pure S c) (p2 : Pure S c2) : p2.prodP (permP σ h p) = permP (prodRightMap n2 σ) ⋯ (p2.prodP p)

B.11. Associativity of the product of three pure tensors in one direction

def TensorSpecies.Tensor.prodAssocMap (n1 n2 n3 : ℕ) : Fin (n1 + n2 + n3) → Fin (n1 + (n2 + n3))

The map between Fin (n1 + n2 + n3) and Fin (n1 + (n2 + n3)) formed by casting.

Equations

• TensorSpecies.Tensor.prodAssocMap n1 n2 n3 = Fin.cast ⋯

@[simp]

theorem TensorSpecies.Tensor.prodAssocMap_castAdd_castAdd {n1 n2 n3 : ℕ} (i : Fin n1) : prodAssocMap n1 n2 n3 (Fin.castAdd n3 (Fin.castAdd n2 i)) = finSumFinEquiv (Sum.inl i)

@[simp]

theorem TensorSpecies.Tensor.prodAssocMap_castAdd_natAdd {n1 n2 n3 : ℕ} (i : Fin n2) : prodAssocMap n1 n2 n3 (Fin.castAdd n3 (Fin.natAdd n1 i)) = finSumFinEquiv (Sum.inr (finSumFinEquiv (Sum.inl i)))

@[simp]

theorem TensorSpecies.Tensor.prodAssocMap_natAdd {n1 n2 n3 : ℕ} (i : Fin n3) : prodAssocMap n1 n2 n3 (Fin.natAdd (n1 + n2) i) = finSumFinEquiv (Sum.inr (finSumFinEquiv (Sum.inr i)))

@[simp]

theorem TensorSpecies.Tensor.prodAssocMap_permCond {C : Type} {n1 n2 n3 : ℕ} {c : Fin n1 → C} {c2 : Fin n2 → C} {c3 : Fin n3 → C} : PermCond (Fin.append c (Fin.append c2 c3)) (Fin.append (Fin.append c c2) c3) (prodAssocMap n1 n2 n3)

theorem TensorSpecies.Tensor.Pure.prodP_assoc {k C G : Type} [CommRing k] [Group G] {basisIdx : C → Type} [(c : C) → Fintype (basisIdx c)] [(c : C) → DecidableEq (basisIdx c)] {S : TensorSpecies k C G basisIdx} {n n1 n2 : ℕ} {c : Fin n → C} {c1 : Fin n1 → C} {c2 : Fin n2 → C} (p : Pure S c) (p1 : Pure S c1) (p2 : Pure S c2) : (p.prodP p1).prodP p2 = permP (prodAssocMap n n1 n2) ⋯ (p.prodP (p1.prodP p2))

B.12. Associativity of the product of three pure tensors in the other direction

def TensorSpecies.Tensor.prodAssocMap' (n1 n2 n3 : ℕ) : Fin (n1 + (n2 + n3)) → Fin (n1 + n2 + n3)

The map between Fin (n1 + (n2 + n3)) and Fin (n1 + n2 + n3) formed by casting.

Equations

• TensorSpecies.Tensor.prodAssocMap' n1 n2 n3 = Fin.cast ⋯

@[simp]

theorem TensorSpecies.Tensor.prodAssocMap'_castAdd {n1 n2 n3 : ℕ} (i : Fin n1) : prodAssocMap' n1 n2 n3 (Fin.castAdd (n2 + n3) i) = finSumFinEquiv (Sum.inl (finSumFinEquiv (Sum.inl i)))

@[simp]

theorem TensorSpecies.Tensor.prodAssocMap'_natAdd_castAdd {n1 n2 n3 : ℕ} (i : Fin n2) : prodAssocMap' n1 n2 n3 (Fin.natAdd n1 (Fin.castAdd n3 i)) = finSumFinEquiv (Sum.inl (finSumFinEquiv (Sum.inr i)))

@[simp]

theorem TensorSpecies.Tensor.prodAssocMap'_natAdd_natAdd {n1 n2 n3 : ℕ} (i : Fin n3) : prodAssocMap' n1 n2 n3 (Fin.natAdd n1 (Fin.natAdd n2 i)) = finSumFinEquiv (Sum.inr i)

@[simp]

theorem TensorSpecies.Tensor.prodAssocMap'_permCond {C : Type} {n1 n2 n3 : ℕ} {c : Fin n1 → C} {c2 : Fin n2 → C} {c3 : Fin n3 → C} : PermCond (Fin.append (Fin.append c c2) c3) (Fin.append c (Fin.append c2 c3)) (prodAssocMap' n1 n2 n3)

theorem TensorSpecies.Tensor.Pure.prodP_assoc' {k C G : Type} [CommRing k] [Group G] {basisIdx : C → Type} [(c : C) → Fintype (basisIdx c)] [(c : C) → DecidableEq (basisIdx c)] {S : TensorSpecies k C G basisIdx} {n n1 n2 : ℕ} {c : Fin n → C} {c1 : Fin n1 → C} {c2 : Fin n2 → C} (p : Pure S c) (p1 : Pure S c1) (p2 : Pure S c2) : p.prodP (p1.prodP p2) = permP (prodAssocMap' n n1 n2) ⋯ ((p.prodP p1).prodP p2)

C. Products of tensors

C.1. Indexing tensors by Fin n1 ⊕ Fin n2 rather than Fin (n1 + n2)

noncomputable def TensorSpecies.Tensor.prodIndexEquiv {k C G : Type} [CommRing k] [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} : ↑(S.F.obj (IndexNotation.OverColor.mk (Sum.elim c c1))) ≃ₗ[k] S.Tensor (Fin.append c c1)

The equivalence between the type S.F.obj (OverColor.mk (Sum.elim c c1)) and the type S.Tensor (Fin.append c c1).

Equations

• TensorSpecies.Tensor.prodIndexEquiv = (Representation.equivOfIso (S.F.mapIso (IndexNotation.OverColor.equivToIso finSumFinEquiv ≪≫ IndexNotation.OverColor.mkIso ⋯))).toLinearEquiv

theorem TensorSpecies.Tensor.prodIndexEquiv_symm_pure {k C G : Type} [CommRing k] [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} (p : Pure S (Fin.append c c1)) : prodIndexEquiv.symm p.toTensor = (PiTensorProduct.tprod k) (Pure.prodIndexEquiv p)

C.2. The product of two tensors

noncomputable def TensorSpecies.Tensor.prodT {k C G : Type} [CommRing k] [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} : S.Tensor c →ₗ[k] S.Tensor c1 →ₗ[k] S.Tensor (Fin.append c c1)

The tensor product of two tensors as a bi-linear map from S.Tensor c and S.Tensor c1 to S.Tensor (Fin.append c c1).

Equations

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

C.3. The product of two pure tensors as a tensor

theorem TensorSpecies.Tensor.prodT_pure {k C G : Type} [CommRing k] [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) : (prodT t.toTensor) t1.toTensor = (t.prodP t1).toTensor

C.4. The product of basis vectors

theorem TensorSpecies.Tensor.prodT_basis {k C G : Type} [CommRing k] [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} (b : ComponentIdx c) (b1 : ComponentIdx c1) : (prodT ((basis c) b)) ((basis c1) b1) = (Pure.basisVector (Fin.append c c1) (ComponentIdx.prod.symm (b, b1))).toTensor

C.5. The product as an equivalence

noncomputable def TensorSpecies.Tensor.tensorEquivProd {k C G : Type} [CommRing k] [Group G] {basisIdx : C → Type} [(c : C) → Fintype (basisIdx c)] [(c : C) → DecidableEq (basisIdx c)] {S : TensorSpecies k C G basisIdx} {n n2 : ℕ} {c : Fin n → C} {c1 : Fin n2 → C} : TensorProduct k (S.Tensor c) (S.Tensor c1) ≃ₗ[k] S.Tensor (Fin.append c c1)

The linear equivalence between S.Tensor c ⊗[k] S.Tensor c1 and S.Tensor (Fin.append c c1).

Equations

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

C.6. Rewriting the basis for the product in terms of the tensor product basis

theorem TensorSpecies.Tensor.basis_prod_eq {k C G : Type} [CommRing k] [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} : basis (Fin.append c c1) = (((basis c).tensorProduct (basis c1)).reindex ComponentIdx.prod.symm).map tensorEquivProd

Rewriting basis for the product in terms of the tensor product basis.

theorem TensorSpecies.Tensor.prodT_basis_repr_apply {k C G : Type} [CommRing k] [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} (t : S.Tensor c) (t1 : S.Tensor c1) (b : ComponentIdx (Fin.append c c1)) : ((basis (Fin.append c c1)).repr ((prodT t) t1)) b = ((basis c).repr t) (ComponentIdx.prod b).1 * ((basis c1).repr t1) (ComponentIdx.prod b).2

C.7. Equivariance of the product of two tensors

@[simp]

theorem TensorSpecies.Tensor.prodT_equivariant {k C G : Type} [CommRing k] [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} (g : G) (t : S.Tensor c) (t1 : S.Tensor c1) : (prodT (g • t)) (g • t1) = g • (prodT t) t1

C.8. The product with the default tensor with no indices on the right

theorem TensorSpecies.Tensor.prodT_default_right {k C G : Type} [CommRing k] [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 : Fin 0 → C} (t : S.Tensor c) : (prodT t) default.toTensor = (permT id ⋯) t

C.9. Swapping the order of the product of two tensors

theorem TensorSpecies.Tensor.prodT_swap {k C G : Type} [CommRing k] [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} (t : S.Tensor c) (t1 : S.Tensor c1) : (prodT t) t1 = (permT (prodSwapMap n n1) ⋯) ((prodT t1) t)

C.10. Permuting the indices of the left tensor in a product

@[simp]

theorem TensorSpecies.Tensor.prodT_permT_left {k C G : Type} [CommRing k] [Group G] {basisIdx : C → Type} [(c : C) → Fintype (basisIdx c)] [(c : C) → DecidableEq (basisIdx c)] {S : TensorSpecies k C G basisIdx} {n2 : ℕ} {c2 : Fin n2 → C} {n n' : ℕ} {c : Fin n → C} {c' : Fin n' → C} (σ : Fin n' → Fin n) (h : PermCond c c' σ) (t : S.Tensor c) (t2 : S.Tensor c2) : (prodT ((permT σ h) t)) t2 = (permT (prodLeftMap n2 σ) ⋯) ((prodT t) t2)

C.11. Permuting the indices of the right tensor in a product

@[simp]

theorem TensorSpecies.Tensor.prodT_permT_right {k C G : Type} [CommRing k] [Group G] {basisIdx : C → Type} [(c : C) → Fintype (basisIdx c)] [(c : C) → DecidableEq (basisIdx c)] {S : TensorSpecies k C G basisIdx} {n2 : ℕ} {c2 : Fin n2 → C} {n n' : ℕ} {c : Fin n → C} {c' : Fin n' → C} (σ : Fin n' → Fin n) (h : PermCond c c' σ) (t : S.Tensor c) (t2 : S.Tensor c2) : (prodT t2) ((permT σ h) t) = (permT (prodRightMap n2 σ) ⋯) ((prodT t2) t)

C.12. Associativity of the product of three tensors in one direction

theorem TensorSpecies.Tensor.prodT_assoc {k C G : Type} [CommRing k] [Group G] {basisIdx : C → Type} [(c : C) → Fintype (basisIdx c)] [(c : C) → DecidableEq (basisIdx c)] {S : TensorSpecies k C G basisIdx} {n n1 n2 : ℕ} {c : Fin n → C} {c1 : Fin n1 → C} {c2 : Fin n2 → C} (t : S.Tensor c) (t1 : S.Tensor c1) (t2 : S.Tensor c2) : (prodT ((prodT t) t1)) t2 = (permT (prodAssocMap n n1 n2) ⋯) ((prodT t) ((prodT t1) t2))

C.13. Associativity of the product of three tensors in the other direction

theorem TensorSpecies.Tensor.prodT_assoc' {k C G : Type} [CommRing k] [Group G] {basisIdx : C → Type} [(c : C) → Fintype (basisIdx c)] [(c : C) → DecidableEq (basisIdx c)] {S : TensorSpecies k C G basisIdx} {n n1 n2 : ℕ} {c : Fin n → C} {c1 : Fin n1 → C} {c2 : Fin n2 → C} (t : S.Tensor c) (t1 : S.Tensor c1) (t2 : S.Tensor c2) : (prodT t) ((prodT t1) t2) = (permT (prodAssocMap' n n1 n2) ⋯) ((prodT ((prodT t) t1)) t2)