Tensors associated with a tensor species

Product

And its interaction with

• actions
• permutations

def TensorSpecies.Tensor.ComponentIdx.prodEquiv {k G : Type} [CommRing k] [Group G] {S : TensorSpecies k G} {n1 n2 : ℕ} {c : Fin n1 → S.C} {c1 : Fin n2 → S.C} : ComponentIdx (Sum.elim c c1 ∘ ⇑finSumFinEquiv.symm) ≃ ((i : Fin n1 ⊕ Fin n2) → Fin (S.repDim (Sum.elim c c1 i)))

The equivalence between ComponentIdx (Sum.elim c c1 ∘ ⇑finSumFinEquiv.symm) and Π (i : Fin n1 ⊕ Fin n2), Fin (S.repDim (Sum.elim c c1 i)).

Equations

• TensorSpecies.Tensor.ComponentIdx.prodEquiv = (finSumFinEquiv.piCongr fun (x : Fin n1 ⊕ Fin n2) => finCongr ⋯).symm

def TensorSpecies.Tensor.ComponentIdx.prod {k G : Type} [CommRing k] [Group G] {S : TensorSpecies k G} {n1 n2 : ℕ} {c : Fin n1 → S.C} {c1 : Fin n2 → S.C} (b : ComponentIdx c) (b1 : ComponentIdx c1) : ComponentIdx (Sum.elim c c1 ∘ ⇑finSumFinEquiv.symm)

The product of two component indices.

Equations

• b.prod b1 = TensorSpecies.Tensor.ComponentIdx.prodEquiv.symm fun (x : Fin n1 ⊕ Fin n2) => match x with | Sum.inl i => b i | Sum.inr i => b1 i

theorem TensorSpecies.Tensor.ComponentIdx.prod_apply_finSumFinEquiv {k G : Type} [CommRing k] [Group G] {S : TensorSpecies k G} {n1 n2 : ℕ} {c : Fin n1 → S.C} {c1 : Fin n2 → S.C} (b : ComponentIdx c) (b1 : ComponentIdx c1) (i : Fin n1 ⊕ Fin n2) : b.prod b1 (finSumFinEquiv i) = match i with | Sum.inl i => Fin.cast ⋯ (b i) | Sum.inr i => Fin.cast ⋯ (b1 i)

def TensorSpecies.Tensor.ComponentIdx.splitEquiv {k G : Type} [CommRing k] [Group G] {S : TensorSpecies k G} {n1 n2 : ℕ} {c : Fin n1 → S.C} {c1 : Fin n2 → S.C} : ComponentIdx (Sum.elim c c1 ∘ ⇑finSumFinEquiv.symm) ≃ ComponentIdx c × ComponentIdx c1

The equivalence between ComponentIdx (Sum.elim c c1 ∘ ⇑finSumFinEquiv.symm) and ComponentIdx c × ComponentIdx c1 formed by products.

Equations

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

def TensorSpecies.Tensor.Pure.prodEquiv {k G : Type} [CommRing k] [Group G] {S : TensorSpecies k G} {n1 n2 : ℕ} {c : Fin n1 → S.C} {c1 : Fin n2 → S.C} : Pure S (Sum.elim c c1 ∘ ⇑finSumFinEquiv.symm) ≃ ((i : Fin n1 ⊕ Fin n2) → ↑(S.FD.obj { as := Sum.elim c c1 i }).V)

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.

def TensorSpecies.Tensor.Pure.prodP {k G : Type} [CommRing k] [Group G] {S : TensorSpecies k G} {n1 n2 : ℕ} {c : Fin n1 → S.C} {c1 : Fin n2 → S.C} (p1 : Pure S c) (p2 : Pure S c1) : Pure S (Sum.elim c c1 ∘ ⇑finSumFinEquiv.symm)

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.prodEquiv.symm fun (x : Fin n1 ⊕ Fin n2) => match x with | Sum.inl i => p1 i | Sum.inr i => p2 i

theorem TensorSpecies.Tensor.Pure.prodP_apply_finSumFinEquiv {k G : Type} [CommRing k] [Group G] {S : TensorSpecies k G} {n1 n2 : ℕ} {c : Fin n1 → S.C} {c1 : Fin n2 → S.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 G : Type} [CommRing k] [Group G] {S : TensorSpecies k G} {n1 n2 : ℕ} {c : Fin n1 → S.C} {c1 : Fin n2 → S.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 G : Type} [CommRing k] [Group G] {S : TensorSpecies k G} {n1 n2 : ℕ} {c : Fin n1 → S.C} {c1 : Fin n2 → S.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)

theorem TensorSpecies.Tensor.Pure.prodP_basisVector {k G : Type} [CommRing k] [Group G] {S : TensorSpecies k G} {n n1 : ℕ} {c : Fin n → S.C} {c1 : Fin n1 → S.C} (b : ComponentIdx c) (b1 : ComponentIdx c1) : (basisVector c b).prodP (basisVector c1 b1) = basisVector (Sum.elim c c1 ∘ ⇑finSumFinEquiv.symm) (b.prod b1)

noncomputable def TensorSpecies.Tensor.prodEquiv {k G : Type} [CommRing k] [Group G] {S : TensorSpecies k G} {n1 n2 : ℕ} {c : Fin n1 → S.C} {c1 : Fin n2 → S.C} : ↑(S.F.obj (IndexNotation.OverColor.mk (Sum.elim c c1))).V ≃ₗ[k] S.Tensor (Sum.elim c c1 ∘ ⇑finSumFinEquiv.symm)

The equivalence between the type S.F.obj (OverColor.mk (Sum.elim c c1)) and the type S.Tensor (Sum.elim c c1 ∘ ⇑finSumFinEquiv.symm).

Equations

• TensorSpecies.Tensor.prodEquiv = ((Action.forget (ModuleCat k) G).mapIso (S.F.mapIso (IndexNotation.OverColor.equivToIso finSumFinEquiv))).toLinearEquiv

theorem TensorSpecies.Tensor.prodEquiv_symm_pure {k G : Type} [CommRing k] [Group G] {S : TensorSpecies k G} {n1 n2 : ℕ} {c : Fin n1 → S.C} {c1 : Fin n2 → S.C} (p : Pure S (Sum.elim c c1 ∘ ⇑finSumFinEquiv.symm)) : prodEquiv.symm p.toTensor = (PiTensorProduct.tprod k) (Pure.prodEquiv p)

noncomputable def TensorSpecies.Tensor.prodT {k G : Type} [CommRing k] [Group G] {S : TensorSpecies k G} {n1 n2 : ℕ} {c : Fin n1 → S.C} {c1 : Fin n2 → S.C} : S.Tensor c →ₗ[k] S.Tensor c1 →ₗ[k] S.Tensor (Sum.elim c c1 ∘ ⇑finSumFinEquiv.symm)

The tensor product of two tensors as a bi-linear map from S.Tensor c and S.Tensor c1 to S.Tensor (Sum.elim c c1 ∘ ⇑finSumFinEquiv.symm).

Equations

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

theorem TensorSpecies.Tensor.prodT_pure {k G : Type} [CommRing k] [Group G] {S : TensorSpecies k G} {n1 n2 : ℕ} {c : Fin n1 → S.C} {c1 : Fin n2 → S.C} (t : Pure S c) (t1 : Pure S c1) : (prodT t.toTensor) t1.toTensor = (t.prodP t1).toTensor

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

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

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)))

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)

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.prodLeftMap_permCond {k G : Type} [CommRing k] [Group G] {S : TensorSpecies k G} {n n' n2 : ℕ} {c : Fin n → S.C} {c' : Fin n' → S.C} {σ : Fin n' → Fin n} (c2 : Fin n2 → S.C) (h : PermCond c c' σ) : PermCond (Sum.elim c c2 ∘ ⇑finSumFinEquiv.symm) (Sum.elim c' c2 ∘ ⇑finSumFinEquiv.symm) (prodLeftMap n2 σ)

@[simp]

theorem TensorSpecies.Tensor.prodRightMap_permCond {k G : Type} [CommRing k] [Group G] {S : TensorSpecies k G} {n n' n2 : ℕ} {c : Fin n → S.C} {c' : Fin n' → S.C} {σ : Fin n' → Fin n} (c2 : Fin n2 → S.C) (h : PermCond c c' σ) : PermCond (Sum.elim c2 c ∘ ⇑finSumFinEquiv.symm) (Sum.elim c2 c' ∘ ⇑finSumFinEquiv.symm) (prodRightMap n2 σ)

@[simp]

theorem TensorSpecies.Tensor.prodSwapMap_permCond {k G : Type} [CommRing k] [Group G] {S : TensorSpecies k G} {n1 n2 : ℕ} {c : Fin n1 → S.C} {c2 : Fin n2 → S.C} : PermCond (Sum.elim c c2 ∘ ⇑finSumFinEquiv.symm) (Sum.elim c2 c ∘ ⇑finSumFinEquiv.symm) (prodSwapMap n2 n1)

@[simp]

theorem TensorSpecies.Tensor.prodAssocMap_permCond {k G : Type} [CommRing k] [Group G] {S : TensorSpecies k G} {n1 n2 n3 : ℕ} {c : Fin n1 → S.C} {c2 : Fin n2 → S.C} {c3 : Fin n3 → S.C} : PermCond (Sum.elim c (Sum.elim c2 c3 ∘ ⇑finSumFinEquiv.symm) ∘ ⇑finSumFinEquiv.symm) (Sum.elim (Sum.elim c c2 ∘ ⇑finSumFinEquiv.symm) c3 ∘ ⇑finSumFinEquiv.symm) (prodAssocMap n1 n2 n3)

@[simp]

theorem TensorSpecies.Tensor.prodAssocMap'_permCond {k G : Type} [CommRing k] [Group G] {S : TensorSpecies k G} {n1 n2 n3 : ℕ} {c : Fin n1 → S.C} {c2 : Fin n2 → S.C} {c3 : Fin n3 → S.C} : PermCond (Sum.elim (Sum.elim c c2 ∘ ⇑finSumFinEquiv.symm) c3 ∘ ⇑finSumFinEquiv.symm) (Sum.elim c (Sum.elim c2 c3 ∘ ⇑finSumFinEquiv.symm) ∘ ⇑finSumFinEquiv.symm) (prodAssocMap' n1 n2 n3)

Relationships assocaited with products

theorem TensorSpecies.Tensor.Pure.prodP_component {k G : Type} [CommRing k] [Group G] {S : TensorSpecies k G} {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} (p : Pure S c) (p1 : Pure S c1) (b : ComponentIdx (Sum.elim c c1 ∘ ⇑finSumFinEquiv.symm)) : (p.prodP p1).component b = p.component (ComponentIdx.splitEquiv b).1 * p1.component (ComponentIdx.splitEquiv b).2

theorem TensorSpecies.Tensor.prodT_basis_repr_apply {k G : Type} [CommRing k] [Group G] {S : TensorSpecies k G} {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} (t : S.Tensor c) (t1 : S.Tensor c1) (b : ComponentIdx (Sum.elim c c1 ∘ ⇑finSumFinEquiv.symm)) : ((basis (Sum.elim c c1 ∘ ⇑finSumFinEquiv.symm)).repr ((prodT t) t1)) b = ((basis c).repr t) (ComponentIdx.splitEquiv b).1 * ((basis c1).repr t1) (ComponentIdx.splitEquiv b).2

@[simp]

theorem TensorSpecies.Tensor.Pure.prodP_equivariant {k G : Type} [CommRing k] [Group G] {S : TensorSpecies k G} {n1 n2 : ℕ} {c : Fin n1 → S.C} {c1 : Fin n2 → S.C} (g : G) (p : Pure S c) (p1 : Pure S c1) : (g • p).prodP (g • p1) = g • p.prodP p1

@[simp]

theorem TensorSpecies.Tensor.prodT_equivariant {k G : Type} [CommRing k] [Group G] {S : TensorSpecies k G} {n1 n2 : ℕ} {c : Fin n1 → S.C} {c1 : Fin n2 → S.C} (g : G) (t : S.Tensor c) (t1 : S.Tensor c1) : (prodT (g • t)) (g • t1) = g • (prodT t) t1

theorem TensorSpecies.Tensor.Pure.prodP_swap {k G : Type} [CommRing k] [Group G] {S : TensorSpecies k G} {n n1 : ℕ} {c : Fin n → S.C} {c1 : Fin n1 → S.C} (p : Pure S c) (p1 : Pure S c1) : p.prodP p1 = permP (prodSwapMap n n1) ⋯ (p1.prodP p)

theorem TensorSpecies.Tensor.prodT_swap {k G : Type} [CommRing k] [Group G] {S : TensorSpecies k G} {n n1 : ℕ} {c : Fin n → S.C} {c1 : Fin n1 → S.C} (t : S.Tensor c) (t1 : S.Tensor c1) : (prodT t) t1 = (permT (prodSwapMap n n1) ⋯) ((prodT t1) t)

@[simp]

theorem TensorSpecies.Tensor.Pure.prodP_permP_left {k G : Type} [CommRing k] [Group G] {S : TensorSpecies k G} {n2 : ℕ} {c2 : Fin n2 → S.C} {n n' : ℕ} {c : Fin n → S.C} {c' : Fin n' → S.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)

@[simp]

theorem TensorSpecies.Tensor.prodT_permT_left {k G : Type} [CommRing k] [Group G] {S : TensorSpecies k G} {n2 : ℕ} {c2 : Fin n2 → S.C} {n n' : ℕ} {c : Fin n → S.C} {c' : Fin n' → S.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)

@[simp]

theorem TensorSpecies.Tensor.Pure.prodP_permP_right {k G : Type} [CommRing k] [Group G] {S : TensorSpecies k G} {n2 : ℕ} {c2 : Fin n2 → S.C} {n n' : ℕ} {c : Fin n → S.C} {c' : Fin n' → S.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)

@[simp]

theorem TensorSpecies.Tensor.prodT_permT_right {k G : Type} [CommRing k] [Group G] {S : TensorSpecies k G} {n2 : ℕ} {c2 : Fin n2 → S.C} {n n' : ℕ} {c : Fin n → S.C} {c' : Fin n' → S.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)

theorem TensorSpecies.Tensor.Pure.prodP_assoc {k G : Type} [CommRing k] [Group G] {S : TensorSpecies k G} {n n1 n2 : ℕ} {c : Fin n → S.C} {c1 : Fin n1 → S.C} {c2 : Fin n2 → S.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))

theorem TensorSpecies.Tensor.prodT_assoc {k G : Type} [CommRing k] [Group G] {S : TensorSpecies k G} {n n1 n2 : ℕ} {c : Fin n → S.C} {c1 : Fin n1 → S.C} {c2 : Fin n2 → S.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))

theorem TensorSpecies.Tensor.Pure.prodP_assoc' {k G : Type} [CommRing k] [Group G] {S : TensorSpecies k G} {n n1 n2 : ℕ} {c : Fin n → S.C} {c1 : Fin n1 → S.C} {c2 : Fin n2 → S.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)

theorem TensorSpecies.Tensor.prodT_assoc' {k G : Type} [CommRing k] [Group G] {S : TensorSpecies k G} {n n1 n2 : ℕ} {c : Fin n → S.C} {c1 : Fin n1 → S.C} {c2 : Fin n2 → S.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)

theorem TensorSpecies.Tensor.Pure.prodP_zero_right_permCond {k G : Type} [CommRing k] [Group G] {S : TensorSpecies k G} {n : ℕ} {c : Fin n → S.C} {c1 : Fin 0 → S.C} : PermCond c (Sum.elim c c1 ∘ ⇑finSumFinEquiv.symm) id

theorem TensorSpecies.Tensor.Pure.prodP_zero_right {k G : Type} [CommRing k] [Group G] {S : TensorSpecies k G} {n : ℕ} {c : Fin n → S.C} {c1 : Fin 0 → S.C} (p : Pure S c) (p0 : Pure S c1) : p.prodP p0 = permP id ⋯ p

theorem TensorSpecies.Tensor.prodT_default_right {k G : Type} [CommRing k] [Group G] {S : TensorSpecies k G} {n : ℕ} {c : Fin n → S.C} {c1 : Fin 0 → S.C} (t : S.Tensor c) : (prodT t) default.toTensor = (permT id ⋯) t