Imports
/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module
public import Physlib.Relativity.Tensors.Basic
public import Physlib.Relativity.Tensors.ComponentIdx.ProductThe 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
@[expose] public sectionB. 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
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).
def Pure.prodP {n1 n2} {c : Fin n1 → C} {c1 : Fin n2 → C}
(p1 : Pure S c) (p2 : Pure S c1) : Pure S (Fin.append c c1) :=
Fin.addCases (fun i => LinearEquiv.cast (R := k) (k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn':ℕn2✝:ℕc✝:Fin n → Cc':Fin n' → Cc2:Fin n2✝ → Cn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cp1:Pure S cp2:Pure S c1i:Fin n1⊢ c i = Fin.append c c1 (Fin.castAdd n2 i) All goals completed! 🐙) (p1 i))
(fun i => LinearEquiv.cast (R := k) (k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn':ℕn2✝:ℕc✝:Fin n → Cc':Fin n' → Cc2:Fin n2✝ → Cn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cp1:Pure S cp2:Pure S c1i:Fin n2⊢ c1 i = Fin.append c c1 (Fin.natAdd n1 i) All goals completed! 🐙) (p2 i))B.3. The vectors making up product of two pure tensors
@[simp]
lemma Pure.prodP_apply_castAdd {n1 n2} {c : Fin n1 → C} {c1 : Fin n2 → C}
(p1 : Pure S c) (p2 : Pure S c1) (i : Fin n1) :
Pure.prodP p1 p2 (Fin.castAdd n2 i) =
LinearEquiv.cast (R := k) (k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn':ℕn2✝:ℕc✝:Fin n → Cc':Fin n' → Cc2:Fin n2✝ → Cn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cp1:Pure S cp2:Pure S c1i:Fin n1⊢ c i = Fin.append c c1 (Fin.castAdd n2 i) All goals completed! 🐙) (p1 i) := k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cp1:Pure S cp2:Pure S c1i:Fin n1⊢ p1.prodP p2 (Fin.castAdd n2 i) = (LinearEquiv.cast ⋯) (p1 i)
All goals completed! 🐙@[simp]
lemma Pure.prodP_apply_natAdd {n1 n2} {c : Fin n1 → C} {c1 : Fin n2 → C}
(p1 : Pure S c) (p2 : Pure S c1) (i : Fin n2) :
Pure.prodP p1 p2 (Fin.natAdd n1 i) =
LinearEquiv.cast (R := k) (k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn':ℕn2✝:ℕc✝:Fin n → Cc':Fin n' → Cc2:Fin n2✝ → Cn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cp1:Pure S cp2:Pure S c1i:Fin n2⊢ c1 i = Fin.append c c1 (Fin.natAdd n1 i) All goals completed! 🐙) (p2 i) := k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cp1:Pure S cp2:Pure S c1i:Fin n2⊢ p1.prodP p2 (Fin.natAdd n1 i) = (LinearEquiv.cast ⋯) (p2 i)
All goals completed! 🐙k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cp1:Pure S cp2:Pure S c1i:Fin n1 ⊕ Fin n2⊢ Fin.addCases (fun i => (LinearEquiv.cast ⋯) (p1 i)) (fun i => (LinearEquiv.cast ⋯) (p2 i)) (finSumFinEquiv i) =
match i with
| Sum.inl i => (LinearEquiv.cast ⋯) (p1 i)
| Sum.inr i => (LinearEquiv.cast ⋯) (p2 i)
match i with
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cp1:Pure S cp2:Pure S c1i✝:Fin n1 ⊕ Fin n2i:Fin n1⊢ Fin.addCases (fun i => (LinearEquiv.cast ⋯) (p1 i)) (fun i => (LinearEquiv.cast ⋯) (p2 i))
(finSumFinEquiv (Sum.inl i)) =
match Sum.inl i with
| Sum.inl i => (LinearEquiv.cast ⋯) (p1 i)
| Sum.inr i => (LinearEquiv.cast ⋯) (p2 i)
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cp1:Pure S cp2:Pure S c1i✝:Fin n1 ⊕ Fin n2i:Fin n1⊢ cast ⋯ (p1 i) = (LinearEquiv.cast ⋯) (p1 i)
All goals completed! 🐙
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cp1:Pure S cp2:Pure S c1i✝:Fin n1 ⊕ Fin n2i:Fin n2⊢ Fin.addCases (fun i => (LinearEquiv.cast ⋯) (p1 i)) (fun i => (LinearEquiv.cast ⋯) (p2 i))
(finSumFinEquiv (Sum.inr i)) =
match Sum.inr i with
| Sum.inl i => (LinearEquiv.cast ⋯) (p1 i)
| Sum.inr i => (LinearEquiv.cast ⋯) (p2 i)
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cp1:Pure S cp2:Pure S c1i✝:Fin n1 ⊕ Fin n2i:Fin n2⊢ cast ⋯ (p2 i) = (LinearEquiv.cast ⋯) (p2 i)
All goals completed! 🐙B.4. The product of two pure basis vectors
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin n → Cc1:Fin n1 → Cφ:ComponentIdx cφ1:ComponentIdx c1i:Fin n1⊢ (LinearEquiv.cast ⋯) ((b (c1 i)) ((basisIdxCongr ⋯) ((basisIdxCongr ⋯) (φ1 i)))) = cast ⋯ ((b (c1 i)) (φ1 i))
All goals completed! 🐙B.5. The basis components of the product of two pure tensors
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕm:ℕc:Fin n → Cc1:Fin m → Cp:Pure S cp1:Pure S c1φ:ComponentIdx (Fin.append c c1)⊢ ∏ i, ((b (Fin.append c c1 (finSumFinEquiv i))).repr (p.prodP p1 (finSumFinEquiv i))) (φ (finSumFinEquiv i)) =
(∏ i, ((b (c i)).repr (p i)) ((ComponentIdx.prod φ).1 i)) * ∏ i, ((b (c1 i)).repr (p1 i)) ((ComponentIdx.prod φ).2 i)
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕm:ℕc:Fin n → Cc1:Fin m → Cp:Pure S cp1:Pure S c1φ:ComponentIdx (Fin.append c c1)⊢ (∏ x, ((b (Fin.append c c1 (Fin.castAdd m x))).repr (p.prodP p1 (Fin.castAdd m x))) (φ (Fin.castAdd m x))) *
∏ x, ((b (Fin.append c c1 (Fin.natAdd n x))).repr (p.prodP p1 (Fin.natAdd n x))) (φ (Fin.natAdd n x)) =
(∏ i, ((b (c i)).repr (p i)) ((ComponentIdx.prod φ).1 i)) * ∏ i, ((b (c1 i)).repr (p1 i)) ((ComponentIdx.prod φ).2 i)
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕm:ℕc:Fin n → Cc1:Fin m → Cp:Pure S cp1:Pure S c1φ:ComponentIdx (Fin.append c c1)⊢ (fun x => ((b (Fin.append c c1 (Fin.castAdd m x))).repr (p.prodP p1 (Fin.castAdd m x))) (φ (Fin.castAdd m x))) =
fun i => ((b (c i)).repr (p i)) ((ComponentIdx.prod φ).1 i)k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕm:ℕc:Fin n → Cc1:Fin m → Cp:Pure S cp1:Pure S c1φ:ComponentIdx (Fin.append c c1)⊢ (fun x => ((b (Fin.append c c1 (Fin.natAdd n x))).repr (p.prodP p1 (Fin.natAdd n x))) (φ (Fin.natAdd n x))) = fun i =>
((b (c1 i)).repr (p1 i)) ((ComponentIdx.prod φ).2 i)
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕm:ℕc:Fin n → Cc1:Fin m → Cp:Pure S cp1:Pure S c1φ:ComponentIdx (Fin.append c c1)⊢ (fun x => ((b (Fin.append c c1 (Fin.castAdd m x))).repr (p.prodP p1 (Fin.castAdd m x))) (φ (Fin.castAdd m x))) =
fun i => ((b (c i)).repr (p i)) ((ComponentIdx.prod φ).1 i) k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕm:ℕc:Fin n → Cc1:Fin m → Cp:Pure S cp1:Pure S c1φ:ComponentIdx (Fin.append c c1)x:Fin n⊢ ((b (Fin.append c c1 (Fin.castAdd m x))).repr (p.prodP p1 (Fin.castAdd m x))) (φ (Fin.castAdd m x)) =
((b (c x)).repr (p x)) ((ComponentIdx.prod φ).1 x)
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕm:ℕc:Fin n → Cc1:Fin m → Cp:Pure S cp1:Pure S c1φ:ComponentIdx (Fin.append c c1)x:Fin n⊢ ((b (Fin.append c c1 (Fin.castAdd m x))).repr (cast ⋯ (p x))) (φ (Fin.castAdd m x)) =
((b (c x)).repr (p x)) ((basisIdxCongr ⋯) (φ (Fin.castAdd m x)))
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕm:ℕc:Fin n → Cc1:Fin m → Cp:Pure S cp1:Pure S c1φ:ComponentIdx (Fin.append c c1)x:Fin nh1:RingHomInvPair (RingHom.id k) (RingHom.id k)h2:V (c x) = V (Fin.append c c1 (Fin.castAdd m x))h3:Fin.append c c1 (Fin.castAdd m x) = c x⊢ ((b (Fin.append c c1 (Fin.castAdd m x))).repr (cast h2 (p x))) (φ (Fin.castAdd m x)) =
((b (c x)).repr (p x)) ((basisIdxCongr h3) (φ (Fin.castAdd m x)))
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕm:ℕc:Fin n → Cc1:Fin m → Cp:Pure S cp1:Pure S c1φ:ComponentIdx (Fin.append c c1)x:Fin nh1:RingHomInvPair (RingHom.id k) (RingHom.id k)h2:V (c x) = V (Fin.append c c1 (Fin.castAdd m x))h3:Fin.append c c1 (Fin.castAdd m x) = c xp':V (c x)⊢ ((b (Fin.append c c1 (Fin.castAdd m x))).repr (cast h2 p')) (φ (Fin.castAdd m x)) =
((b (c x)).repr p') ((basisIdxCongr h3) (φ (Fin.castAdd m x)))
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕm:ℕc:Fin n → Cc1:Fin m → Cp:Pure S cp1:Pure S c1φ:ComponentIdx (Fin.append c c1)x:Fin nh1:RingHomInvPair (RingHom.id k) (RingHom.id k)c':Ch2:V c' = V (Fin.append c c1 (Fin.castAdd m x))h3:Fin.append c c1 (Fin.castAdd m x) = c'p':V c'⊢ ((b (Fin.append c c1 (Fin.castAdd m x))).repr (cast h2 p')) (φ (Fin.castAdd m x)) =
((b c').repr p') ((basisIdxCongr h3) (φ (Fin.castAdd m x)))
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕm:ℕc:Fin n → Cc1:Fin m → Cp:Pure S cp1:Pure S c1φ:ComponentIdx (Fin.append c c1)x:Fin nh1:RingHomInvPair (RingHom.id k) (RingHom.id k)h2:V (Fin.append c c1 (Fin.castAdd m x)) = V (Fin.append c c1 (Fin.castAdd m x))p':V (Fin.append c c1 (Fin.castAdd m x))⊢ ((b (Fin.append c c1 (Fin.castAdd m x))).repr (cast h2 p')) (φ (Fin.castAdd m x)) =
((b (Fin.append c c1 (Fin.castAdd m x))).repr p') ((basisIdxCongr ⋯) (φ (Fin.castAdd m x)))
All goals completed! 🐙
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕm:ℕc:Fin n → Cc1:Fin m → Cp:Pure S cp1:Pure S c1φ:ComponentIdx (Fin.append c c1)⊢ (fun x => ((b (Fin.append c c1 (Fin.natAdd n x))).repr (p.prodP p1 (Fin.natAdd n x))) (φ (Fin.natAdd n x))) = fun i =>
((b (c1 i)).repr (p1 i)) ((ComponentIdx.prod φ).2 i) k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕm:ℕc:Fin n → Cc1:Fin m → Cp:Pure S cp1:Pure S c1φ:ComponentIdx (Fin.append c c1)x:Fin m⊢ ((b (Fin.append c c1 (Fin.natAdd n x))).repr (p.prodP p1 (Fin.natAdd n x))) (φ (Fin.natAdd n x)) =
((b (c1 x)).repr (p1 x)) ((ComponentIdx.prod φ).2 x)
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕm:ℕc:Fin n → Cc1:Fin m → Cp:Pure S cp1:Pure S c1φ:ComponentIdx (Fin.append c c1)x:Fin m⊢ ((b (Fin.append c c1 (Fin.natAdd n x))).repr (cast ⋯ (p1 x))) (φ (Fin.natAdd n x)) =
((b (c1 x)).repr (p1 x)) ((basisIdxCongr ⋯) (φ (Fin.natAdd n x)))
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕm:ℕc:Fin n → Cc1:Fin m → Cp:Pure S cp1:Pure S c1φ:ComponentIdx (Fin.append c c1)x:Fin mh1:RingHomInvPair (RingHom.id k) (RingHom.id k)h2:V (c1 x) = V (Fin.append c c1 (Fin.natAdd n x))h3:Fin.append c c1 (Fin.natAdd n x) = c1 x⊢ ((b (Fin.append c c1 (Fin.natAdd n x))).repr (cast h2 (p1 x))) (φ (Fin.natAdd n x)) =
((b (c1 x)).repr (p1 x)) ((basisIdxCongr h3) (φ (Fin.natAdd n x)))
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕm:ℕc:Fin n → Cc1:Fin m → Cp:Pure S cp1:Pure S c1φ:ComponentIdx (Fin.append c c1)x:Fin mh1:RingHomInvPair (RingHom.id k) (RingHom.id k)h2:V (c1 x) = V (Fin.append c c1 (Fin.natAdd n x))h3:Fin.append c c1 (Fin.natAdd n x) = c1 xp1':V (c1 x)⊢ ((b (Fin.append c c1 (Fin.natAdd n x))).repr (cast h2 p1')) (φ (Fin.natAdd n x)) =
((b (c1 x)).repr p1') ((basisIdxCongr h3) (φ (Fin.natAdd n x)))
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕm:ℕc:Fin n → Cc1:Fin m → Cp:Pure S cp1:Pure S c1φ:ComponentIdx (Fin.append c c1)x:Fin mh1:RingHomInvPair (RingHom.id k) (RingHom.id k)c1':Ch2:V c1' = V (Fin.append c c1 (Fin.natAdd n x))h3:Fin.append c c1 (Fin.natAdd n x) = c1'p1':V c1'⊢ ((b (Fin.append c c1 (Fin.natAdd n x))).repr (cast h2 p1')) (φ (Fin.natAdd n x)) =
((b c1').repr p1') ((basisIdxCongr h3) (φ (Fin.natAdd n x)))
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕm:ℕc:Fin n → Cc1:Fin m → Cp:Pure S cp1:Pure S c1φ:ComponentIdx (Fin.append c c1)x:Fin mh1:RingHomInvPair (RingHom.id k) (RingHom.id k)h2:V (Fin.append c c1 (Fin.natAdd n x)) = V (Fin.append c c1 (Fin.natAdd n x))p1':V (Fin.append c c1 (Fin.natAdd n x))⊢ ((b (Fin.append c c1 (Fin.natAdd n x))).repr (cast h2 p1')) (φ (Fin.natAdd n x)) =
((b (Fin.append c c1 (Fin.natAdd n x))).repr p1') ((basisIdxCongr ⋯) (φ (Fin.natAdd n x)))
All goals completed! 🐙B.6. Equivariance of the product of two pure tensors
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cg:Gp:Pure S cp1:Pure S c1⊢ (∀ (i : Fin n1), (g • p).prodP (g • p1) (Fin.castAdd n2 i) = (g • p.prodP p1) (Fin.castAdd n2 i)) ∧
∀ (j : Fin n2), (g • p).prodP (g • p1) (Fin.natAdd n1 j) = (g • p.prodP p1) (Fin.natAdd n1 j)
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cg:Gp:Pure S cp1:Pure S c1⊢ (∀ (i : Fin n1),
(LinearEquiv.cast ⋯) (((rep (c i)) g) (p i)) =
((rep (Fin.append c c1 (Fin.castAdd n2 i))) g) ((LinearEquiv.cast ⋯) (p i))) ∧
∀ (j : Fin n2),
(LinearEquiv.cast ⋯) (((rep (c1 j)) g) (p1 j)) =
((rep (Fin.append c c1 (Fin.natAdd n1 j))) g) ((LinearEquiv.cast ⋯) (p1 j))
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cg:Gp:Pure S cp1:Pure S c1⊢ ∀ (i : Fin n1),
(LinearEquiv.cast ⋯) (((rep (c i)) g) (p i)) =
((rep (Fin.append c c1 (Fin.castAdd n2 i))) g) ((LinearEquiv.cast ⋯) (p i))k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cg:Gp:Pure S cp1:Pure S c1⊢ ∀ (j : Fin n2),
(LinearEquiv.cast ⋯) (((rep (c1 j)) g) (p1 j)) =
((rep (Fin.append c c1 (Fin.natAdd n1 j))) g) ((LinearEquiv.cast ⋯) (p1 j))
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cg:Gp:Pure S cp1:Pure S c1⊢ ∀ (i : Fin n1),
(LinearEquiv.cast ⋯) (((rep (c i)) g) (p i)) =
((rep (Fin.append c c1 (Fin.castAdd n2 i))) g) ((LinearEquiv.cast ⋯) (p i)) k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cg:Gp:Pure S cp1:Pure S c1j:Fin n1⊢ (LinearEquiv.cast ⋯) (((rep (c j)) g) (p j)) =
((rep (Fin.append c c1 (Fin.castAdd n2 j))) g) ((LinearEquiv.cast ⋯) (p j))
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cg:Gp:Pure S cp1:Pure S c1j:Fin n1h1:RingHomInvPair (RingHom.id k) (RingHom.id k)h2:c j = Fin.append c c1 (Fin.castAdd n2 j)⊢ (LinearEquiv.cast h2) (((rep (c j)) g) (p j)) =
((rep (Fin.append c c1 (Fin.castAdd n2 j))) g) ((LinearEquiv.cast h2) (p j))
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cg:Gp:Pure S cp1:Pure S c1j:Fin n1h1:RingHomInvPair (RingHom.id k) (RingHom.id k)h2:c j = Fin.append c c1 (Fin.castAdd n2 j)p':V (c j)⊢ (LinearEquiv.cast h2) (((rep (c j)) g) p') = ((rep (Fin.append c c1 (Fin.castAdd n2 j))) g) ((LinearEquiv.cast h2) p')
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cg:Gp:Pure S cp1:Pure S c1j:Fin n1h1:RingHomInvPair (RingHom.id k) (RingHom.id k)c':Ch2:c' = Fin.append c c1 (Fin.castAdd n2 j)p':V c'⊢ (LinearEquiv.cast h2) (((rep c') g) p') = ((rep (Fin.append c c1 (Fin.castAdd n2 j))) g) ((LinearEquiv.cast h2) p')
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cg:Gp:Pure S cp1:Pure S c1j:Fin n1h1:RingHomInvPair (RingHom.id k) (RingHom.id k)p':V (Fin.append c c1 (Fin.castAdd n2 j))⊢ (LinearEquiv.cast ⋯) (((rep (Fin.append c c1 (Fin.castAdd n2 j))) g) p') =
((rep (Fin.append c c1 (Fin.castAdd n2 j))) g) ((LinearEquiv.cast ⋯) p')
All goals completed! 🐙
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cg:Gp:Pure S cp1:Pure S c1⊢ ∀ (j : Fin n2),
(LinearEquiv.cast ⋯) (((rep (c1 j)) g) (p1 j)) =
((rep (Fin.append c c1 (Fin.natAdd n1 j))) g) ((LinearEquiv.cast ⋯) (p1 j)) k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cg:Gp:Pure S cp1:Pure S c1j:Fin n2⊢ (LinearEquiv.cast ⋯) (((rep (c1 j)) g) (p1 j)) =
((rep (Fin.append c c1 (Fin.natAdd n1 j))) g) ((LinearEquiv.cast ⋯) (p1 j))
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cg:Gp:Pure S cp1:Pure S c1j:Fin n2h1:RingHomInvPair (RingHom.id k) (RingHom.id k)h2:c1 j = Fin.append c c1 (Fin.natAdd n1 j)⊢ (LinearEquiv.cast h2) (((rep (c1 j)) g) (p1 j)) =
((rep (Fin.append c c1 (Fin.natAdd n1 j))) g) ((LinearEquiv.cast h2) (p1 j))
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cg:Gp:Pure S cp1:Pure S c1j:Fin n2h1:RingHomInvPair (RingHom.id k) (RingHom.id k)h2:c1 j = Fin.append c c1 (Fin.natAdd n1 j)p1':V (c1 j)⊢ (LinearEquiv.cast h2) (((rep (c1 j)) g) p1') = ((rep (Fin.append c c1 (Fin.natAdd n1 j))) g) ((LinearEquiv.cast h2) p1')
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cg:Gp:Pure S cp1:Pure S c1j:Fin n2h1:RingHomInvPair (RingHom.id k) (RingHom.id k)c1':Ch2:c1' = Fin.append c c1 (Fin.natAdd n1 j)p1':V c1'⊢ (LinearEquiv.cast h2) (((rep c1') g) p1') = ((rep (Fin.append c c1 (Fin.natAdd n1 j))) g) ((LinearEquiv.cast h2) p1')
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cg:Gp:Pure S cp1:Pure S c1j:Fin n2h1:RingHomInvPair (RingHom.id k) (RingHom.id k)p1':V (Fin.append c c1 (Fin.natAdd n1 j))⊢ (LinearEquiv.cast ⋯) (((rep (Fin.append c c1 (Fin.natAdd n1 j))) g) p1') =
((rep (Fin.append c c1 (Fin.natAdd n1 j))) g) ((LinearEquiv.cast ⋯) p1')
All goals completed! 🐙B.7. Product with a tensor with no indices on the right
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin n → Cc1:Fin 0 → Cp:Pure S cp0:Pure S c1j:Fin n ⊕ Fin 0⊢ (match j with
| Sum.inl i => (LinearEquiv.cast ⋯) (p i)
| Sum.inr i => (LinearEquiv.cast ⋯) (p0 i)) =
permP id ⋯ p (finSumFinEquiv j)
match j with
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin n → Cc1:Fin 0 → Cp:Pure S cp0:Pure S c1j✝:Fin n ⊕ Fin 0j:Fin n⊢ (match Sum.inl j with
| Sum.inl i => (LinearEquiv.cast ⋯) (p i)
| Sum.inr i => (LinearEquiv.cast ⋯) (p0 i)) =
permP id ⋯ p (finSumFinEquiv (Sum.inl j)) All goals completed! 🐙
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin n → Cc1:Fin 0 → Cp:Pure S cp0:Pure S c1j✝:Fin n ⊕ Fin 0j:Fin 0⊢ (match Sum.inr j with
| Sum.inl i => (LinearEquiv.cast ⋯) (p i)
| Sum.inr i => (LinearEquiv.cast ⋯) (p0 i)) =
permP id ⋯ p (finSumFinEquiv (Sum.inr j)) All goals completed! 🐙B.8. Swapping the order of the product of two pure tensors
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin n → Cc1:Fin n1 → Cp:Pure S cp1:Pure S c1i✝:Fin (n + n1)i:Fin n1h0:Fin.append (Fin.natAdd n1) (Fin.castAdd n) (Fin.natAdd n i) = Fin.castAdd n i⊢ p.prodP p1 (Fin.natAdd n i) = permP (Fin.append (Fin.natAdd n1) (Fin.castAdd n)) ⋯ (p1.prodP p) (Fin.natAdd n i)
All goals completed! 🐙B.9. Permuting the indices of the left tensor in a product
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn2:ℕc2:Fin n2 → Cn:ℕn':ℕc:Fin n → Cc':Fin n' → Cσ:Fin n' → Fin nh:IsReindexing c c' σp:Pure S cp2:Pure S c2i✝:Fin (n' + n2)i:Fin n2h0:Fin.append (Fin.castAdd n2 ∘ σ) (Fin.natAdd n) (Fin.natAdd n' i) = Fin.natAdd n i⊢ (permP σ h p).prodP p2 (Fin.natAdd n' i) =
permP (Fin.append (Fin.castAdd n2 ∘ σ) (Fin.natAdd n)) ⋯ (p.prodP p2) (Fin.natAdd n' i)
All goals completed! 🐙B.10. Permuting the indices of the right tensor in a product
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn2:ℕc2:Fin n2 → Cn:ℕn':ℕc:Fin n → Cc':Fin n' → Cσ:Fin n' → Fin nh:IsReindexing c c' σp:Pure S cp2:Pure S c2i✝:Fin (n2 + n')i:Fin n'h0:Fin.append (Fin.castAdd n) (Fin.natAdd n2 ∘ σ) (Fin.natAdd n2 i) = Fin.natAdd n2 (σ i)⊢ p2.prodP (permP σ h p) (Fin.natAdd n2 i) =
permP (Fin.append (Fin.castAdd n) (Fin.natAdd n2 ∘ σ)) ⋯ (p2.prodP p) (Fin.natAdd n2 i)
All goals completed! 🐙B.11. Associativity of the product of three pure tensors in one direction
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕn2:ℕc:Fin n → Cc1:Fin n1 → Cc2:Fin n2 → Cp:Pure S cp1:Pure S c1p2:Pure S c2i✝¹:Fin (n + n1 + n2)i✝:Fin (n + n1)i:Fin n1h0:Fin.cast ⋯ (Fin.castAdd n2 (Fin.natAdd n i)) = Fin.natAdd n (Fin.castAdd n2 i)⊢ (p.prodP p1).prodP p2 (Fin.castAdd n2 (Fin.natAdd n i)) =
permP (Fin.cast ⋯) ⋯ (p.prodP (p1.prodP p2)) (Fin.castAdd n2 (Fin.natAdd n i))
All goals completed! 🐙B.12. Associativity of the product of three pure tensors in the other direction
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕn2:ℕc:Fin n → Cc1:Fin n1 → Cc2:Fin n2 → Cp:Pure S cp1:Pure S c1p2:Pure S c2i✝¹:Fin (n + (n1 + n2))i✝:Fin (n1 + n2)i:Fin n2h0:Fin.cast ⋯ (Fin.natAdd n (Fin.natAdd n1 i)) = Fin.natAdd (n + n1) i⊢ p.prodP (p1.prodP p2) (Fin.natAdd n (Fin.natAdd n1 i)) =
permP (Fin.cast ⋯) ⋯ ((p.prodP p1).prodP p2) (Fin.natAdd n (Fin.natAdd n1 i))
All goals completed! 🐙B.13. Linearity of the product
attribute [-simp] LinearEquiv.cast_applyk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cp1:Pure S cp2:Pure S c1i:Fin n1x:V (c i)j:Fin n2h1:RingHomInvPair (RingHom.id k) (RingHom.id k)h2:c1 j = Fin.append c c1 (Fin.natAdd n1 j)h3:c i = Fin.append c c1 (Fin.castAdd n2 i)⊢ (LinearEquiv.cast h2) (p2 j) = p1.prodP p2 (Fin.natAdd n1 j)k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cp1:Pure S cp2:Pure S c1i:Fin n1x:V (c i)j:Fin n2h1:RingHomInvPair (RingHom.id k) (RingHom.id k)h2:c1 j = Fin.append c c1 (Fin.natAdd n1 j)h3:c i = Fin.append c c1 (Fin.castAdd n2 i)⊢ Fin.castAdd n2 i ≠ Fin.natAdd n1 j
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cp1:Pure S cp2:Pure S c1i:Fin n1x:V (c i)j:Fin n2h1:RingHomInvPair (RingHom.id k) (RingHom.id k)h2:c1 j = Fin.append c c1 (Fin.natAdd n1 j)h3:c i = Fin.append c c1 (Fin.castAdd n2 i)⊢ (LinearEquiv.cast h2) (p2 j) = p1.prodP p2 (Fin.natAdd n1 j) All goals completed! 🐙
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cp1:Pure S cp2:Pure S c1i:Fin n1x:V (c i)j:Fin n2h1:RingHomInvPair (RingHom.id k) (RingHom.id k)h2:c1 j = Fin.append c c1 (Fin.natAdd n1 j)h3:c i = Fin.append c c1 (Fin.castAdd n2 i)⊢ Fin.castAdd n2 i ≠ Fin.natAdd n1 j k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cp1:Pure S cp2:Pure S c1i:Fin n1x:V (c i)j:Fin n2h1:RingHomInvPair (RingHom.id k) (RingHom.id k)h2:c1 j = Fin.append c c1 (Fin.natAdd n1 j)h3:c i = Fin.append c c1 (Fin.castAdd n2 i)⊢ ¬↑i = n1 + ↑j
All goals completed! 🐙k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cp1:Pure S cp2:Pure S c1i:Fin n2x:V (c1 i)j:Fin n2h1:RingHomInvPair (RingHom.id k) (RingHom.id k)h2:c1 j = Fin.append c c1 (Fin.natAdd n1 j)h3:c1 i = Fin.append c c1 (Fin.natAdd n1 i)h:¬j = i⊢ (LinearEquiv.cast h2) (p2 j) = p1.prodP p2 (Fin.natAdd n1 j)
All goals completed! 🐙lemma Pure.prodP_update_add_toTensor_left {n1 n2} {c : Fin n1 → C} {c1 : Fin n2 → C}
(p1 : Pure S c) (p2 : Pure S c1) (i : Fin n2) (x y : V (c1 i)) :
(Pure.prodP p1 (Pure.update p2 i (x + y))).toTensor
= (Pure.prodP p1 (Pure.update p2 i x)).toTensor
+ (Pure.prodP p1 (Pure.update p2 i y)).toTensor := k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cp1:Pure S cp2:Pure S c1i:Fin n2x:V (c1 i)y:V (c1 i)⊢ (p1.prodP (p2.update i (x + y))).toTensor = (p1.prodP (p2.update i x)).toTensor + (p1.prodP (p2.update i y)).toTensor All goals completed! 🐙C. Products of tensors
C.2. The product of two tensors
C.3. The product of two pure tensors as a tensor
lemma prodT_pure {n1 n2} {c : Fin n1 → C} {c1 : Fin n2 → C}
(t : Pure S c) (t1 : Pure S c1) :
(t.toTensor).prodT (t1.toTensor) = (Pure.prodP t t1).toTensor := k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Ct:Pure S ct1:Pure S c1⊢ (prodT t.toTensor) t1.toTensor = (t.prodP t1).toTensor
All goals completed! 🐙C.4. The product of basis vectors
All goals completed! 🐙k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cb:ComponentIdx cb1:ComponentIdx c1⊢ (Pure.basisVector (Fin.append c c1) (ComponentIdx.prod.symm (b, b1))).toTensor =
(basis (Fin.append c c1)) (ComponentIdx.prod.symm (b, b1))
All goals completed! 🐙C.5. The product as an equivalence
The linear equivalence between S.Tensor c ⊗[k] S.Tensor c1 and
S.Tensor (Fin.append c c1).
set_option synthInstance.maxHeartbeats 0 inAll goals completed! 🐙
right_inv x := k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn✝:ℕn':ℕn2✝:ℕc✝:Fin n✝ → Cc':Fin n' → Cc2:Fin n2✝ → Cn:ℕn2:ℕc:Fin n → Cc1:Fin n2 → Cx:S.Tensor (Fin.append c c1)⊢ (lift prodT).toFun
((((basis (Fin.append c c1)).constr k) fun b_1 =>
(basis c) (ComponentIdx.prod b_1).1 ⊗ₜ[k] (basis c1) (ComponentIdx.prod b_1).2)
x) =
x
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn✝:ℕn':ℕn2✝:ℕc✝:Fin n✝ → Cc':Fin n' → Cc2:Fin n2✝ → Cn:ℕn2:ℕc:Fin n → Cc1:Fin n2 → Cx:S.Tensor (Fin.append c c1)⊢ ∑ x_1,
((basis (Fin.append c c1)).repr x) x_1 •
(prodT ((basis c) (ComponentIdx.prod x_1).1)) ((basis c1) (ComponentIdx.prod x_1).2) =
x
conv_rhs => k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn✝:ℕn':ℕn2✝:ℕc✝:Fin n✝ → Cc':Fin n' → Cc2:Fin n2✝ → Cn:ℕn2:ℕc:Fin n → Cc1:Fin n2 → Cx:S.Tensor (Fin.append c c1)| ∑ i, ((basis (Fin.append c c1)).repr x) i • (basis (Fin.append c c1)) i
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn✝:ℕn':ℕn2✝:ℕc✝:Fin n✝ → Cc':Fin n' → Cc2:Fin n2✝ → Cn:ℕn2:ℕc:Fin n → Cc1:Fin n2 → Cx:S.Tensor (Fin.append c c1)⊢ (fun x_1 =>
((basis (Fin.append c c1)).repr x) x_1 •
(prodT ((basis c) (ComponentIdx.prod x_1).1)) ((basis c1) (ComponentIdx.prod x_1).2)) =
fun i => ((basis (Fin.append c c1)).repr x) i • (basis (Fin.append c c1)) i
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn✝:ℕn':ℕn2✝:ℕc✝:Fin n✝ → Cc':Fin n' → Cc2:Fin n2✝ → Cn:ℕn2:ℕc:Fin n → Cc1:Fin n2 → Cx:S.Tensor (Fin.append c c1)φ:ComponentIdx (Fin.append c c1)⊢ ((basis (Fin.append c c1)).repr x) φ •
(prodT ((basis c) (ComponentIdx.prod φ).1)) ((basis c1) (ComponentIdx.prod φ).2) =
((basis (Fin.append c c1)).repr x) φ • (basis (Fin.append c c1)) φ
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn✝:ℕn':ℕn2✝:ℕc✝:Fin n✝ → Cc':Fin n' → Cc2:Fin n2✝ → Cn:ℕn2:ℕc:Fin n → Cc1:Fin n2 → Cx:S.Tensor (Fin.append c c1)φ:ComponentIdx (Fin.append c c1)⊢ (prodT ((basis c) (ComponentIdx.prod φ).1)) ((basis c1) (ComponentIdx.prod φ).2) = (basis (Fin.append c c1)) φ
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn✝:ℕn':ℕn2✝:ℕc✝:Fin n✝ → Cc':Fin n' → Cc2:Fin n2✝ → Cn:ℕn2:ℕc:Fin n → Cc1:Fin n2 → Cx:S.Tensor (Fin.append c c1)φ:ComponentIdx (Fin.append c c1)⊢ (Pure.basisVector (Fin.append c c1) φ).toTensor = (basis (Fin.append c c1)) φ
All goals completed! 🐙C.6. Rewriting the basis for the product in terms of the tensor product basis
Rewriting basis for the product in terms of the tensor product basis.
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cb:ComponentIdx (Fin.append c c1)⊢ (basis (Fin.append c c1)) b =
(basis (Fin.append c c1))
(ComponentIdx.prod.symm
(fun i => (basisIdxCongr ⋯) (b (Fin.castAdd n2 i)), fun i => (basisIdxCongr ⋯) (b (Fin.natAdd n1 i))))
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cb:ComponentIdx (Fin.append c c1)⊢ b =
ComponentIdx.prod.symm
(fun i => (basisIdxCongr ⋯) (b (Fin.castAdd n2 i)), fun i => (basisIdxCongr ⋯) (b (Fin.natAdd n1 i)))
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cb:ComponentIdx (Fin.append c c1)i:Fin (n1 + n2)⊢ b i =
ComponentIdx.prod.symm
(fun i => (basisIdxCongr ⋯) (b (Fin.castAdd n2 i)), fun i => (basisIdxCongr ⋯) (b (Fin.natAdd n1 i))) i
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cb:ComponentIdx (Fin.append c c1)i:Fin n1 ⊕ Fin n2⊢ b (finSumFinEquiv i) =
ComponentIdx.prod.symm
(fun i => (basisIdxCongr ⋯) (b (Fin.castAdd n2 i)), fun i => (basisIdxCongr ⋯) (b (Fin.natAdd n1 i)))
(finSumFinEquiv i)
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cb:ComponentIdx (Fin.append c c1)i:Fin n1⊢ b (finSumFinEquiv (Sum.inl i)) =
ComponentIdx.prod.symm
(fun i => (basisIdxCongr ⋯) (b (Fin.castAdd n2 i)), fun i => (basisIdxCongr ⋯) (b (Fin.natAdd n1 i)))
(finSumFinEquiv (Sum.inl i))k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cb:ComponentIdx (Fin.append c c1)i:Fin n2⊢ b (finSumFinEquiv (Sum.inr i)) =
ComponentIdx.prod.symm
(fun i => (basisIdxCongr ⋯) (b (Fin.castAdd n2 i)), fun i => (basisIdxCongr ⋯) (b (Fin.natAdd n1 i)))
(finSumFinEquiv (Sum.inr i)) k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cb:ComponentIdx (Fin.append c c1)i:Fin n1⊢ b (finSumFinEquiv (Sum.inl i)) =
ComponentIdx.prod.symm
(fun i => (basisIdxCongr ⋯) (b (Fin.castAdd n2 i)), fun i => (basisIdxCongr ⋯) (b (Fin.natAdd n1 i)))
(finSumFinEquiv (Sum.inl i))k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cb:ComponentIdx (Fin.append c c1)i:Fin n2⊢ b (finSumFinEquiv (Sum.inr i)) =
ComponentIdx.prod.symm
(fun i => (basisIdxCongr ⋯) (b (Fin.castAdd n2 i)), fun i => (basisIdxCongr ⋯) (b (Fin.natAdd n1 i)))
(finSumFinEquiv (Sum.inr i)) All goals completed! 🐙k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕm:ℕc:Fin n → Cc1:Fin m → Ct✝:S.Tensor ct1:S.Tensor c1b:ComponentIdx (Fin.append c c1)r:kt:S.Tensor chp:((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⊢ r * (((basis c).repr t) (ComponentIdx.prod b).1 * ((basis c1).repr t1) (ComponentIdx.prod b).2) =
r * ((basis c).repr t) (ComponentIdx.prod b).1 * ((basis c1).repr t1) (ComponentIdx.prod b).2
All goals completed! 🐙
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕm:ℕc:Fin n → Cc1:Fin m → Ct:S.Tensor ct1:S.Tensor c1b:ComponentIdx (Fin.append c c1)⊢ ∀ (t1_1 t2 : S.Tensor c),
((basis (Fin.append c c1)).repr ((prodT t1_1) t1)) b =
((basis c).repr t1_1) (ComponentIdx.prod b).1 * ((basis c1).repr t1) (ComponentIdx.prod b).2 →
((basis (Fin.append c c1)).repr ((prodT t2) t1)) b =
((basis c).repr t2) (ComponentIdx.prod b).1 * ((basis c1).repr t1) (ComponentIdx.prod b).2 →
((basis (Fin.append c c1)).repr ((prodT (t1_1 + t2)) t1)) b =
((basis c).repr (t1_1 + t2)) (ComponentIdx.prod b).1 * ((basis c1).repr t1) (ComponentIdx.prod b).2 k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕm:ℕc:Fin n → Cc1:Fin m → Ct:S.Tensor ct1✝:S.Tensor c1b:ComponentIdx (Fin.append c c1)t1:S.Tensor ct2:S.Tensor chp1:((basis (Fin.append c c1)).repr ((prodT t1) t1✝)) b =
((basis c).repr t1) (ComponentIdx.prod b).1 * ((basis c1).repr t1✝) (ComponentIdx.prod b).2hp2:((basis (Fin.append c c1)).repr ((prodT t2) t1✝)) b =
((basis c).repr t2) (ComponentIdx.prod b).1 * ((basis c1).repr t1✝) (ComponentIdx.prod b).2⊢ ((basis (Fin.append c c1)).repr ((prodT (t1 + t2)) t1✝)) b =
((basis c).repr (t1 + t2)) (ComponentIdx.prod b).1 * ((basis c1).repr t1✝) (ComponentIdx.prod b).2
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕm:ℕc:Fin n → Cc1:Fin m → Ct:S.Tensor ct1✝:S.Tensor c1b:ComponentIdx (Fin.append c c1)t1:S.Tensor ct2:S.Tensor chp1:((basis (Fin.append c c1)).repr ((prodT t1) t1✝)) b =
((basis c).repr t1) (ComponentIdx.prod b).1 * ((basis c1).repr t1✝) (ComponentIdx.prod b).2hp2:((basis (Fin.append c c1)).repr ((prodT t2) t1✝)) b =
((basis c).repr t2) (ComponentIdx.prod b).1 * ((basis c1).repr t1✝) (ComponentIdx.prod b).2⊢ ((basis c).repr t1) (ComponentIdx.prod b).1 * ((basis c1).repr t1✝) (ComponentIdx.prod b).2 +
((basis c).repr t2) (ComponentIdx.prod b).1 * ((basis c1).repr t1✝) (ComponentIdx.prod b).2 =
(((basis c).repr t1) (ComponentIdx.prod b).1 + ((basis c).repr t2) (ComponentIdx.prod b).1) *
((basis c1).repr t1✝) (ComponentIdx.prod b).2
All goals completed! 🐙C.7. Equivariance of the product of two tensors
@[simp]
lemma prodT_equivariant {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 := k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cg:Gt:S.Tensor ct1:S.Tensor c1⊢ (prodT (g • t)) (g • t1) = g • (prodT t) t1
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cg:Gt1:S.Tensor c1p:Pure S c⊢ (prodT (g • p.toTensor)) (g • t1) = g • (prodT p.toTensor) t1k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cg:Gt1:S.Tensor c1r:kt:S.Tensor cht:(prodT (g • t)) (g • t1) = g • (prodT t) t1⊢ (prodT (g • r • t)) (g • t1) = g • (prodT (r • t)) t1k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cg:Gt1✝:S.Tensor c1t1:S.Tensor ct2:S.Tensor cht1:(prodT (g • t1)) (g • t1✝) = g • (prodT t1) t1✝ht2:(prodT (g • t2)) (g • t1✝) = g • (prodT t2) t1✝⊢ (prodT (g • (t1 + t2))) (g • t1✝) = g • (prodT (t1 + t2)) t1✝
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cg:Gt1:S.Tensor c1p:Pure S c⊢ (prodT (g • p.toTensor)) (g • t1) = g • (prodT p.toTensor) t1 k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cg:Gp:Pure S cq:Pure S c1⊢ (prodT (g • p.toTensor)) (g • q.toTensor) = g • (prodT p.toTensor) q.toTensork:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cg:Gp:Pure S cr:kt:S.Tensor c1ht:(prodT (g • p.toTensor)) (g • t) = g • (prodT p.toTensor) t⊢ (prodT (g • p.toTensor)) (g • r • t) = g • (prodT p.toTensor) (r • t)k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cg:Gp:Pure S ct1:S.Tensor c1t2:S.Tensor c1ht1:(prodT (g • p.toTensor)) (g • t1) = g • (prodT p.toTensor) t1ht2:(prodT (g • p.toTensor)) (g • t2) = g • (prodT p.toTensor) t2⊢ (prodT (g • p.toTensor)) (g • (t1 + t2)) = g • (prodT p.toTensor) (t1 + t2)
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cg:Gp:Pure S cq:Pure S c1⊢ (prodT (g • p.toTensor)) (g • q.toTensor) = g • (prodT p.toTensor) q.toTensor All goals completed! 🐙
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cg:Gp:Pure S cr:kt:S.Tensor c1ht:(prodT (g • p.toTensor)) (g • t) = g • (prodT p.toTensor) t⊢ (prodT (g • p.toTensor)) (g • r • t) = g • (prodT p.toTensor) (r • t) All goals completed! 🐙
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cg:Gp:Pure S ct1:S.Tensor c1t2:S.Tensor c1ht1:(prodT (g • p.toTensor)) (g • t1) = g • (prodT p.toTensor) t1ht2:(prodT (g • p.toTensor)) (g • t2) = g • (prodT p.toTensor) t2⊢ (prodT (g • p.toTensor)) (g • (t1 + t2)) = g • (prodT p.toTensor) (t1 + t2) All goals completed! 🐙
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cg:Gt1:S.Tensor c1r:kt:S.Tensor cht:(prodT (g • t)) (g • t1) = g • (prodT t) t1⊢ (prodT (g • r • t)) (g • t1) = g • (prodT (r • t)) t1 All goals completed! 🐙
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cg:Gt1✝:S.Tensor c1t1:S.Tensor ct2:S.Tensor cht1:(prodT (g • t1)) (g • t1✝) = g • (prodT t1) t1✝ht2:(prodT (g • t2)) (g • t1✝) = g • (prodT t2) t1✝⊢ (prodT (g • (t1 + t2))) (g • t1✝) = g • (prodT (t1 + t2)) t1✝ All goals completed! 🐙C.8. The product with the default tensor with no indices on the right
All goals completed! 🐙
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin n → Cc1:Fin 0 → Cr:kt:S.Tensor cht:(prodT t) default.toTensor = (permT id ⋯) t⊢ (prodT (r • t)) default.toTensor = (permT id ⋯) (r • t) All goals completed! 🐙
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin n → Cc1:Fin 0 → Ct1:S.Tensor ct2:S.Tensor cht1:(prodT t1) default.toTensor = (permT id ⋯) t1ht2:(prodT t2) default.toTensor = (permT id ⋯) t2⊢ (prodT (t1 + t2)) default.toTensor = (permT id ⋯) (t1 + t2) All goals completed! 🐙k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin n → Cc1:Fin 0 → Ct:S.Tensor ct1:S.Tensor c1⊢ toField t1 • (prodT t) ((basis c1) default) = toField t1 • (permT id ⋯) t
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin n → Cc1:Fin 0 → Ct:S.Tensor ct1:S.Tensor c1⊢ (prodT t) ((basis c1) default) = (permT id ⋯) t
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin n → Cc1:Fin 0 → Ct:S.Tensor ct1:S.Tensor c1⊢ (basis c1) default = default.toTensor
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin n → Cc1:Fin 0 → Ct:S.Tensor ct1:S.Tensor c1⊢ (Pure.basisVector c1 default).toTensor = default.toTensor
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin n → Cc1:Fin 0 → Ct:S.Tensor ct1:S.Tensor c1⊢ Pure.basisVector c1 default = default
All goals completed! 🐙C.9. Swapping the order of the product of two tensors
lemma prodT_swap {n n1} {c : Fin n → C} {c1 : Fin n1 → C} (t : S.Tensor c) (t1 : S.Tensor c1) :
prodT t t1 = permT _ IsReindexing.append_swap (prodT t1 t) := k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin n → Cc1:Fin n1 → Ct:S.Tensor ct1:S.Tensor c1⊢ (prodT t) t1 = (permT (Fin.append (Fin.natAdd n1) (Fin.castAdd n)) ⋯) ((prodT t1) t)
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin n → Cc1:Fin n1 → Ct1:S.Tensor c1p:Pure S c⊢ (prodT p.toTensor) t1 = (permT (Fin.append (Fin.natAdd n1) (Fin.castAdd n)) ⋯) ((prodT t1) p.toTensor)k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin n → Cc1:Fin n1 → Ct1:S.Tensor c1r:kt:S.Tensor cht:(prodT t) t1 = (permT (Fin.append (Fin.natAdd n1) (Fin.castAdd n)) ⋯) ((prodT t1) t)⊢ (prodT (r • t)) t1 = (permT (Fin.append (Fin.natAdd n1) (Fin.castAdd n)) ⋯) ((prodT t1) (r • t))k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin n → Cc1:Fin n1 → Ct1✝:S.Tensor c1t1:S.Tensor ct2:S.Tensor cht1:(prodT t1) t1✝ = (permT (Fin.append (Fin.natAdd n1) (Fin.castAdd n)) ⋯) ((prodT t1✝) t1)ht2:(prodT t2) t1✝ = (permT (Fin.append (Fin.natAdd n1) (Fin.castAdd n)) ⋯) ((prodT t1✝) t2)⊢ (prodT (t1 + t2)) t1✝ = (permT (Fin.append (Fin.natAdd n1) (Fin.castAdd n)) ⋯) ((prodT t1✝) (t1 + t2))
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin n → Cc1:Fin n1 → Ct1:S.Tensor c1p:Pure S c⊢ (prodT p.toTensor) t1 = (permT (Fin.append (Fin.natAdd n1) (Fin.castAdd n)) ⋯) ((prodT t1) p.toTensor) k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin n → Cc1:Fin n1 → Cp:Pure S cq:Pure S c1⊢ (prodT p.toTensor) q.toTensor = (permT (Fin.append (Fin.natAdd n1) (Fin.castAdd n)) ⋯) ((prodT q.toTensor) p.toTensor)k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin n → Cc1:Fin n1 → Cp:Pure S cr:kt:S.Tensor c1ht:(prodT p.toTensor) t = (permT (Fin.append (Fin.natAdd n1) (Fin.castAdd n)) ⋯) ((prodT t) p.toTensor)⊢ (prodT p.toTensor) (r • t) = (permT (Fin.append (Fin.natAdd n1) (Fin.castAdd n)) ⋯) ((prodT (r • t)) p.toTensor)k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin n → Cc1:Fin n1 → Cp:Pure S ct1:S.Tensor c1t2:S.Tensor c1ht1:(prodT p.toTensor) t1 = (permT (Fin.append (Fin.natAdd n1) (Fin.castAdd n)) ⋯) ((prodT t1) p.toTensor)ht2:(prodT p.toTensor) t2 = (permT (Fin.append (Fin.natAdd n1) (Fin.castAdd n)) ⋯) ((prodT t2) p.toTensor)⊢ (prodT p.toTensor) (t1 + t2) = (permT (Fin.append (Fin.natAdd n1) (Fin.castAdd n)) ⋯) ((prodT (t1 + t2)) p.toTensor)
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin n → Cc1:Fin n1 → Cp:Pure S cq:Pure S c1⊢ (prodT p.toTensor) q.toTensor = (permT (Fin.append (Fin.natAdd n1) (Fin.castAdd n)) ⋯) ((prodT q.toTensor) p.toTensor) All goals completed! 🐙
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin n → Cc1:Fin n1 → Cp:Pure S cr:kt:S.Tensor c1ht:(prodT p.toTensor) t = (permT (Fin.append (Fin.natAdd n1) (Fin.castAdd n)) ⋯) ((prodT t) p.toTensor)⊢ (prodT p.toTensor) (r • t) = (permT (Fin.append (Fin.natAdd n1) (Fin.castAdd n)) ⋯) ((prodT (r • t)) p.toTensor) All goals completed! 🐙
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin n → Cc1:Fin n1 → Cp:Pure S ct1:S.Tensor c1t2:S.Tensor c1ht1:(prodT p.toTensor) t1 = (permT (Fin.append (Fin.natAdd n1) (Fin.castAdd n)) ⋯) ((prodT t1) p.toTensor)ht2:(prodT p.toTensor) t2 = (permT (Fin.append (Fin.natAdd n1) (Fin.castAdd n)) ⋯) ((prodT t2) p.toTensor)⊢ (prodT p.toTensor) (t1 + t2) = (permT (Fin.append (Fin.natAdd n1) (Fin.castAdd n)) ⋯) ((prodT (t1 + t2)) p.toTensor) All goals completed! 🐙
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin n → Cc1:Fin n1 → Ct1:S.Tensor c1r:kt:S.Tensor cht:(prodT t) t1 = (permT (Fin.append (Fin.natAdd n1) (Fin.castAdd n)) ⋯) ((prodT t1) t)⊢ (prodT (r • t)) t1 = (permT (Fin.append (Fin.natAdd n1) (Fin.castAdd n)) ⋯) ((prodT t1) (r • t)) All goals completed! 🐙
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin n → Cc1:Fin n1 → Ct1✝:S.Tensor c1t1:S.Tensor ct2:S.Tensor cht1:(prodT t1) t1✝ = (permT (Fin.append (Fin.natAdd n1) (Fin.castAdd n)) ⋯) ((prodT t1✝) t1)ht2:(prodT t2) t1✝ = (permT (Fin.append (Fin.natAdd n1) (Fin.castAdd n)) ⋯) ((prodT t1✝) t2)⊢ (prodT (t1 + t2)) t1✝ = (permT (Fin.append (Fin.natAdd n1) (Fin.castAdd n)) ⋯) ((prodT t1✝) (t1 + t2)) All goals completed! 🐙C.10. Permuting the indices of the left tensor in a product
@[simp]
lemma prodT_permT_left {n n'} {c : Fin n → C} {c' : Fin n' → C}
(σ : Fin n' → Fin n) (h : IsReindexing c c' σ) (t : S.Tensor c) (t2 : S.Tensor c2) :
prodT (permT σ h t) t2 = permT _ (h.append_congr_left c2) (prodT t t2) := k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn2:ℕc2:Fin n2 → Cn:ℕn':ℕc:Fin n → Cc':Fin n' → Cσ:Fin n' → Fin nh:IsReindexing c c' σt:S.Tensor ct2:S.Tensor c2⊢ (prodT ((permT σ h) t)) t2 = (permT (Fin.append (Fin.castAdd n2 ∘ σ) (Fin.natAdd n)) ⋯) ((prodT t) t2)
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn2:ℕc2:Fin n2 → Cn:ℕn':ℕc:Fin n → Cc':Fin n' → Cσ:Fin n' → Fin nh:IsReindexing c c' σt2:S.Tensor c2p:Pure S c⊢ (prodT ((permT σ h) p.toTensor)) t2 = (permT (Fin.append (Fin.castAdd n2 ∘ σ) (Fin.natAdd n)) ⋯) ((prodT p.toTensor) t2)k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn2:ℕc2:Fin n2 → Cn:ℕn':ℕc:Fin n → Cc':Fin n' → Cσ:Fin n' → Fin nh:IsReindexing c c' σt2:S.Tensor c2r:kt:S.Tensor cht:(prodT ((permT σ h) t)) t2 = (permT (Fin.append (Fin.castAdd n2 ∘ σ) (Fin.natAdd n)) ⋯) ((prodT t) t2)⊢ (prodT ((permT σ h) (r • t))) t2 = (permT (Fin.append (Fin.castAdd n2 ∘ σ) (Fin.natAdd n)) ⋯) ((prodT (r • t)) t2)k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn2:ℕc2:Fin n2 → Cn:ℕn':ℕc:Fin n → Cc':Fin n' → Cσ:Fin n' → Fin nh:IsReindexing c c' σt2✝:S.Tensor c2t1:S.Tensor ct2:S.Tensor cht1:(prodT ((permT σ h) t1)) t2✝ = (permT (Fin.append (Fin.castAdd n2 ∘ σ) (Fin.natAdd n)) ⋯) ((prodT t1) t2✝)ht2:(prodT ((permT σ h) t2)) t2✝ = (permT (Fin.append (Fin.castAdd n2 ∘ σ) (Fin.natAdd n)) ⋯) ((prodT t2) t2✝)⊢ (prodT ((permT σ h) (t1 + t2))) t2✝ = (permT (Fin.append (Fin.castAdd n2 ∘ σ) (Fin.natAdd n)) ⋯) ((prodT (t1 + t2)) t2✝)
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn2:ℕc2:Fin n2 → Cn:ℕn':ℕc:Fin n → Cc':Fin n' → Cσ:Fin n' → Fin nh:IsReindexing c c' σt2:S.Tensor c2p:Pure S c⊢ (prodT ((permT σ h) p.toTensor)) t2 = (permT (Fin.append (Fin.castAdd n2 ∘ σ) (Fin.natAdd n)) ⋯) ((prodT p.toTensor) t2) k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn2:ℕc2:Fin n2 → Cn:ℕn':ℕc:Fin n → Cc':Fin n' → Cσ:Fin n' → Fin nh:IsReindexing c c' σp:Pure S cq:Pure S c2⊢ (prodT ((permT σ h) p.toTensor)) q.toTensor =
(permT (Fin.append (Fin.castAdd n2 ∘ σ) (Fin.natAdd n)) ⋯) ((prodT p.toTensor) q.toTensor)k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn2:ℕc2:Fin n2 → Cn:ℕn':ℕc:Fin n → Cc':Fin n' → Cσ:Fin n' → Fin nh:IsReindexing c c' σp:Pure S cr:kt:S.Tensor c2ht:(prodT ((permT σ h) p.toTensor)) t = (permT (Fin.append (Fin.castAdd n2 ∘ σ) (Fin.natAdd n)) ⋯) ((prodT p.toTensor) t)⊢ (prodT ((permT σ h) p.toTensor)) (r • t) =
(permT (Fin.append (Fin.castAdd n2 ∘ σ) (Fin.natAdd n)) ⋯) ((prodT p.toTensor) (r • t))k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn2:ℕc2:Fin n2 → Cn:ℕn':ℕc:Fin n → Cc':Fin n' → Cσ:Fin n' → Fin nh:IsReindexing c c' σp:Pure S ct1:S.Tensor c2t2:S.Tensor c2ht1:(prodT ((permT σ h) p.toTensor)) t1 = (permT (Fin.append (Fin.castAdd n2 ∘ σ) (Fin.natAdd n)) ⋯) ((prodT p.toTensor) t1)ht2:(prodT ((permT σ h) p.toTensor)) t2 = (permT (Fin.append (Fin.castAdd n2 ∘ σ) (Fin.natAdd n)) ⋯) ((prodT p.toTensor) t2)⊢ (prodT ((permT σ h) p.toTensor)) (t1 + t2) =
(permT (Fin.append (Fin.castAdd n2 ∘ σ) (Fin.natAdd n)) ⋯) ((prodT p.toTensor) (t1 + t2))
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn2:ℕc2:Fin n2 → Cn:ℕn':ℕc:Fin n → Cc':Fin n' → Cσ:Fin n' → Fin nh:IsReindexing c c' σp:Pure S cq:Pure S c2⊢ (prodT ((permT σ h) p.toTensor)) q.toTensor =
(permT (Fin.append (Fin.castAdd n2 ∘ σ) (Fin.natAdd n)) ⋯) ((prodT p.toTensor) q.toTensor) All goals completed! 🐙
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn2:ℕc2:Fin n2 → Cn:ℕn':ℕc:Fin n → Cc':Fin n' → Cσ:Fin n' → Fin nh:IsReindexing c c' σp:Pure S cr:kt:S.Tensor c2ht:(prodT ((permT σ h) p.toTensor)) t = (permT (Fin.append (Fin.castAdd n2 ∘ σ) (Fin.natAdd n)) ⋯) ((prodT p.toTensor) t)⊢ (prodT ((permT σ h) p.toTensor)) (r • t) =
(permT (Fin.append (Fin.castAdd n2 ∘ σ) (Fin.natAdd n)) ⋯) ((prodT p.toTensor) (r • t)) All goals completed! 🐙
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn2:ℕc2:Fin n2 → Cn:ℕn':ℕc:Fin n → Cc':Fin n' → Cσ:Fin n' → Fin nh:IsReindexing c c' σp:Pure S ct1:S.Tensor c2t2:S.Tensor c2ht1:(prodT ((permT σ h) p.toTensor)) t1 = (permT (Fin.append (Fin.castAdd n2 ∘ σ) (Fin.natAdd n)) ⋯) ((prodT p.toTensor) t1)ht2:(prodT ((permT σ h) p.toTensor)) t2 = (permT (Fin.append (Fin.castAdd n2 ∘ σ) (Fin.natAdd n)) ⋯) ((prodT p.toTensor) t2)⊢ (prodT ((permT σ h) p.toTensor)) (t1 + t2) =
(permT (Fin.append (Fin.castAdd n2 ∘ σ) (Fin.natAdd n)) ⋯) ((prodT p.toTensor) (t1 + t2)) All goals completed! 🐙
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn2:ℕc2:Fin n2 → Cn:ℕn':ℕc:Fin n → Cc':Fin n' → Cσ:Fin n' → Fin nh:IsReindexing c c' σt2:S.Tensor c2r:kt:S.Tensor cht:(prodT ((permT σ h) t)) t2 = (permT (Fin.append (Fin.castAdd n2 ∘ σ) (Fin.natAdd n)) ⋯) ((prodT t) t2)⊢ (prodT ((permT σ h) (r • t))) t2 = (permT (Fin.append (Fin.castAdd n2 ∘ σ) (Fin.natAdd n)) ⋯) ((prodT (r • t)) t2) All goals completed! 🐙
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn2:ℕc2:Fin n2 → Cn:ℕn':ℕc:Fin n → Cc':Fin n' → Cσ:Fin n' → Fin nh:IsReindexing c c' σt2✝:S.Tensor c2t1:S.Tensor ct2:S.Tensor cht1:(prodT ((permT σ h) t1)) t2✝ = (permT (Fin.append (Fin.castAdd n2 ∘ σ) (Fin.natAdd n)) ⋯) ((prodT t1) t2✝)ht2:(prodT ((permT σ h) t2)) t2✝ = (permT (Fin.append (Fin.castAdd n2 ∘ σ) (Fin.natAdd n)) ⋯) ((prodT t2) t2✝)⊢ (prodT ((permT σ h) (t1 + t2))) t2✝ = (permT (Fin.append (Fin.castAdd n2 ∘ σ) (Fin.natAdd n)) ⋯) ((prodT (t1 + t2)) t2✝) All goals completed! 🐙C.11. Permuting the indices of the right tensor in a product
@[simp]
lemma prodT_permT_right {n n'} {c : Fin n → C} {c' : Fin n' → C}
(σ : Fin n' → Fin n) (h : IsReindexing c c' σ) (t : S.Tensor c) (t2 : S.Tensor c2) :
prodT t2 (permT σ h t) = permT _ (h.append_congr_right c2) (prodT t2 t) := k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn2:ℕc2:Fin n2 → Cn:ℕn':ℕc:Fin n → Cc':Fin n' → Cσ:Fin n' → Fin nh:IsReindexing c c' σt:S.Tensor ct2:S.Tensor c2⊢ (prodT t2) ((permT σ h) t) = (permT (Fin.append (Fin.castAdd n) (Fin.natAdd n2 ∘ σ)) ⋯) ((prodT t2) t)
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn2:ℕc2:Fin n2 → Cn:ℕn':ℕc:Fin n → Cc':Fin n' → Cσ:Fin n' → Fin nh:IsReindexing c c' σt2:S.Tensor c2p:Pure S c⊢ (prodT t2) ((permT σ h) p.toTensor) = (permT (Fin.append (Fin.castAdd n) (Fin.natAdd n2 ∘ σ)) ⋯) ((prodT t2) p.toTensor)k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn2:ℕc2:Fin n2 → Cn:ℕn':ℕc:Fin n → Cc':Fin n' → Cσ:Fin n' → Fin nh:IsReindexing c c' σt2:S.Tensor c2r:kt:S.Tensor cht:(prodT t2) ((permT σ h) t) = (permT (Fin.append (Fin.castAdd n) (Fin.natAdd n2 ∘ σ)) ⋯) ((prodT t2) t)⊢ (prodT t2) ((permT σ h) (r • t)) = (permT (Fin.append (Fin.castAdd n) (Fin.natAdd n2 ∘ σ)) ⋯) ((prodT t2) (r • t))k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn2:ℕc2:Fin n2 → Cn:ℕn':ℕc:Fin n → Cc':Fin n' → Cσ:Fin n' → Fin nh:IsReindexing c c' σt2✝:S.Tensor c2t1:S.Tensor ct2:S.Tensor cht1:(prodT t2✝) ((permT σ h) t1) = (permT (Fin.append (Fin.castAdd n) (Fin.natAdd n2 ∘ σ)) ⋯) ((prodT t2✝) t1)ht2:(prodT t2✝) ((permT σ h) t2) = (permT (Fin.append (Fin.castAdd n) (Fin.natAdd n2 ∘ σ)) ⋯) ((prodT t2✝) t2)⊢ (prodT t2✝) ((permT σ h) (t1 + t2)) = (permT (Fin.append (Fin.castAdd n) (Fin.natAdd n2 ∘ σ)) ⋯) ((prodT t2✝) (t1 + t2))
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn2:ℕc2:Fin n2 → Cn:ℕn':ℕc:Fin n → Cc':Fin n' → Cσ:Fin n' → Fin nh:IsReindexing c c' σt2:S.Tensor c2p:Pure S c⊢ (prodT t2) ((permT σ h) p.toTensor) = (permT (Fin.append (Fin.castAdd n) (Fin.natAdd n2 ∘ σ)) ⋯) ((prodT t2) p.toTensor) k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn2:ℕc2:Fin n2 → Cn:ℕn':ℕc:Fin n → Cc':Fin n' → Cσ:Fin n' → Fin nh:IsReindexing c c' σp:Pure S cq:Pure S c2⊢ (prodT q.toTensor) ((permT σ h) p.toTensor) =
(permT (Fin.append (Fin.castAdd n) (Fin.natAdd n2 ∘ σ)) ⋯) ((prodT q.toTensor) p.toTensor)k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn2:ℕc2:Fin n2 → Cn:ℕn':ℕc:Fin n → Cc':Fin n' → Cσ:Fin n' → Fin nh:IsReindexing c c' σp:Pure S cr:kt:S.Tensor c2ht:(prodT t) ((permT σ h) p.toTensor) = (permT (Fin.append (Fin.castAdd n) (Fin.natAdd n2 ∘ σ)) ⋯) ((prodT t) p.toTensor)⊢ (prodT (r • t)) ((permT σ h) p.toTensor) =
(permT (Fin.append (Fin.castAdd n) (Fin.natAdd n2 ∘ σ)) ⋯) ((prodT (r • t)) p.toTensor)k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn2:ℕc2:Fin n2 → Cn:ℕn':ℕc:Fin n → Cc':Fin n' → Cσ:Fin n' → Fin nh:IsReindexing c c' σp:Pure S ct1:S.Tensor c2t2:S.Tensor c2ht1:(prodT t1) ((permT σ h) p.toTensor) = (permT (Fin.append (Fin.castAdd n) (Fin.natAdd n2 ∘ σ)) ⋯) ((prodT t1) p.toTensor)ht2:(prodT t2) ((permT σ h) p.toTensor) = (permT (Fin.append (Fin.castAdd n) (Fin.natAdd n2 ∘ σ)) ⋯) ((prodT t2) p.toTensor)⊢ (prodT (t1 + t2)) ((permT σ h) p.toTensor) =
(permT (Fin.append (Fin.castAdd n) (Fin.natAdd n2 ∘ σ)) ⋯) ((prodT (t1 + t2)) p.toTensor)
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn2:ℕc2:Fin n2 → Cn:ℕn':ℕc:Fin n → Cc':Fin n' → Cσ:Fin n' → Fin nh:IsReindexing c c' σp:Pure S cq:Pure S c2⊢ (prodT q.toTensor) ((permT σ h) p.toTensor) =
(permT (Fin.append (Fin.castAdd n) (Fin.natAdd n2 ∘ σ)) ⋯) ((prodT q.toTensor) p.toTensor) All goals completed! 🐙
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn2:ℕc2:Fin n2 → Cn:ℕn':ℕc:Fin n → Cc':Fin n' → Cσ:Fin n' → Fin nh:IsReindexing c c' σp:Pure S cr:kt:S.Tensor c2ht:(prodT t) ((permT σ h) p.toTensor) = (permT (Fin.append (Fin.castAdd n) (Fin.natAdd n2 ∘ σ)) ⋯) ((prodT t) p.toTensor)⊢ (prodT (r • t)) ((permT σ h) p.toTensor) =
(permT (Fin.append (Fin.castAdd n) (Fin.natAdd n2 ∘ σ)) ⋯) ((prodT (r • t)) p.toTensor) All goals completed! 🐙
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn2:ℕc2:Fin n2 → Cn:ℕn':ℕc:Fin n → Cc':Fin n' → Cσ:Fin n' → Fin nh:IsReindexing c c' σp:Pure S ct1:S.Tensor c2t2:S.Tensor c2ht1:(prodT t1) ((permT σ h) p.toTensor) = (permT (Fin.append (Fin.castAdd n) (Fin.natAdd n2 ∘ σ)) ⋯) ((prodT t1) p.toTensor)ht2:(prodT t2) ((permT σ h) p.toTensor) = (permT (Fin.append (Fin.castAdd n) (Fin.natAdd n2 ∘ σ)) ⋯) ((prodT t2) p.toTensor)⊢ (prodT (t1 + t2)) ((permT σ h) p.toTensor) =
(permT (Fin.append (Fin.castAdd n) (Fin.natAdd n2 ∘ σ)) ⋯) ((prodT (t1 + t2)) p.toTensor) All goals completed! 🐙
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn2:ℕc2:Fin n2 → Cn:ℕn':ℕc:Fin n → Cc':Fin n' → Cσ:Fin n' → Fin nh:IsReindexing c c' σt2:S.Tensor c2r:kt:S.Tensor cht:(prodT t2) ((permT σ h) t) = (permT (Fin.append (Fin.castAdd n) (Fin.natAdd n2 ∘ σ)) ⋯) ((prodT t2) t)⊢ (prodT t2) ((permT σ h) (r • t)) = (permT (Fin.append (Fin.castAdd n) (Fin.natAdd n2 ∘ σ)) ⋯) ((prodT t2) (r • t)) All goals completed! 🐙
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn2:ℕc2:Fin n2 → Cn:ℕn':ℕc:Fin n → Cc':Fin n' → Cσ:Fin n' → Fin nh:IsReindexing c c' σt2✝:S.Tensor c2t1:S.Tensor ct2:S.Tensor cht1:(prodT t2✝) ((permT σ h) t1) = (permT (Fin.append (Fin.castAdd n) (Fin.natAdd n2 ∘ σ)) ⋯) ((prodT t2✝) t1)ht2:(prodT t2✝) ((permT σ h) t2) = (permT (Fin.append (Fin.castAdd n) (Fin.natAdd n2 ∘ σ)) ⋯) ((prodT t2✝) t2)⊢ (prodT t2✝) ((permT σ h) (t1 + t2)) = (permT (Fin.append (Fin.castAdd n) (Fin.natAdd n2 ∘ σ)) ⋯) ((prodT t2✝) (t1 + t2)) All goals completed! 🐙C.12. Associativity of the product of three tensors in one direction
lemma prodT_assoc {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 _ IsReindexing.append_assoc_right (prodT t (prodT t1 t2)) := k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕn2:ℕc:Fin n → Cc1:Fin n1 → Cc2:Fin n2 → Ct:S.Tensor ct1:S.Tensor c1t2:S.Tensor c2⊢ (prodT ((prodT t) t1)) t2 = (permT (Fin.cast ⋯) ⋯) ((prodT t) ((prodT t1) t2))
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕn2:ℕc:Fin n → Cc1:Fin n1 → Cc2:Fin n2 → Ct1:S.Tensor c1t2:S.Tensor c2p:Pure S c⊢ (prodT ((prodT p.toTensor) t1)) t2 = (permT (Fin.cast ⋯) ⋯) ((prodT p.toTensor) ((prodT t1) t2))k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕn2:ℕc:Fin n → Cc1:Fin n1 → Cc2:Fin n2 → Ct1:S.Tensor c1t2:S.Tensor c2r:kt:S.Tensor cht:(prodT ((prodT t) t1)) t2 = (permT (Fin.cast ⋯) ⋯) ((prodT t) ((prodT t1) t2))⊢ (prodT ((prodT (r • t)) t1)) t2 = (permT (Fin.cast ⋯) ⋯) ((prodT (r • t)) ((prodT t1) t2))k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕn2:ℕc:Fin n → Cc1:Fin n1 → Cc2:Fin n2 → Ct1✝:S.Tensor c1t2✝:S.Tensor c2t1:S.Tensor ct2:S.Tensor cht1:(prodT ((prodT t1) t1✝)) t2✝ = (permT (Fin.cast ⋯) ⋯) ((prodT t1) ((prodT t1✝) t2✝))ht2:(prodT ((prodT t2) t1✝)) t2✝ = (permT (Fin.cast ⋯) ⋯) ((prodT t2) ((prodT t1✝) t2✝))⊢ (prodT ((prodT (t1 + t2)) t1✝)) t2✝ = (permT (Fin.cast ⋯) ⋯) ((prodT (t1 + t2)) ((prodT t1✝) t2✝))
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕn2:ℕc:Fin n → Cc1:Fin n1 → Cc2:Fin n2 → Ct1:S.Tensor c1t2:S.Tensor c2p:Pure S c⊢ (prodT ((prodT p.toTensor) t1)) t2 = (permT (Fin.cast ⋯) ⋯) ((prodT p.toTensor) ((prodT t1) t2)) k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕn2:ℕc:Fin n → Cc1:Fin n1 → Cc2:Fin n2 → Ct2:S.Tensor c2p:Pure S cq:Pure S c1⊢ (prodT ((prodT p.toTensor) q.toTensor)) t2 = (permT (Fin.cast ⋯) ⋯) ((prodT p.toTensor) ((prodT q.toTensor) t2))k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕn2:ℕc:Fin n → Cc1:Fin n1 → Cc2:Fin n2 → Ct2:S.Tensor c2p:Pure S cr:kt:S.Tensor c1ht:(prodT ((prodT p.toTensor) t)) t2 = (permT (Fin.cast ⋯) ⋯) ((prodT p.toTensor) ((prodT t) t2))⊢ (prodT ((prodT p.toTensor) (r • t))) t2 = (permT (Fin.cast ⋯) ⋯) ((prodT p.toTensor) ((prodT (r • t)) t2))k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕn2:ℕc:Fin n → Cc1:Fin n1 → Cc2:Fin n2 → Ct2✝:S.Tensor c2p:Pure S ct1:S.Tensor c1t2:S.Tensor c1ht1:(prodT ((prodT p.toTensor) t1)) t2✝ = (permT (Fin.cast ⋯) ⋯) ((prodT p.toTensor) ((prodT t1) t2✝))ht2:(prodT ((prodT p.toTensor) t2)) t2✝ = (permT (Fin.cast ⋯) ⋯) ((prodT p.toTensor) ((prodT t2) t2✝))⊢ (prodT ((prodT p.toTensor) (t1 + t2))) t2✝ = (permT (Fin.cast ⋯) ⋯) ((prodT p.toTensor) ((prodT (t1 + t2)) t2✝))
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕn2:ℕc:Fin n → Cc1:Fin n1 → Cc2:Fin n2 → Ct2:S.Tensor c2p:Pure S cq:Pure S c1⊢ (prodT ((prodT p.toTensor) q.toTensor)) t2 = (permT (Fin.cast ⋯) ⋯) ((prodT p.toTensor) ((prodT q.toTensor) t2)) k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕn2:ℕc:Fin n → Cc1:Fin n1 → Cc2:Fin n2 → Cp:Pure S cq✝:Pure S c1q:Pure S c2⊢ (prodT ((prodT p.toTensor) q✝.toTensor)) q.toTensor =
(permT (Fin.cast ⋯) ⋯) ((prodT p.toTensor) ((prodT q✝.toTensor) q.toTensor))k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕn2:ℕc:Fin n → Cc1:Fin n1 → Cc2:Fin n2 → Cp:Pure S cq:Pure S c1r:kt:S.Tensor c2ht:(prodT ((prodT p.toTensor) q.toTensor)) t = (permT (Fin.cast ⋯) ⋯) ((prodT p.toTensor) ((prodT q.toTensor) t))⊢ (prodT ((prodT p.toTensor) q.toTensor)) (r • t) =
(permT (Fin.cast ⋯) ⋯) ((prodT p.toTensor) ((prodT q.toTensor) (r • t)))k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕn2:ℕc:Fin n → Cc1:Fin n1 → Cc2:Fin n2 → Cp:Pure S cq:Pure S c1t1:S.Tensor c2t2:S.Tensor c2ht1:(prodT ((prodT p.toTensor) q.toTensor)) t1 = (permT (Fin.cast ⋯) ⋯) ((prodT p.toTensor) ((prodT q.toTensor) t1))ht2:(prodT ((prodT p.toTensor) q.toTensor)) t2 = (permT (Fin.cast ⋯) ⋯) ((prodT p.toTensor) ((prodT q.toTensor) t2))⊢ (prodT ((prodT p.toTensor) q.toTensor)) (t1 + t2) =
(permT (Fin.cast ⋯) ⋯) ((prodT p.toTensor) ((prodT q.toTensor) (t1 + t2)))
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕn2:ℕc:Fin n → Cc1:Fin n1 → Cc2:Fin n2 → Cp:Pure S cq✝:Pure S c1q:Pure S c2⊢ (prodT ((prodT p.toTensor) q✝.toTensor)) q.toTensor =
(permT (Fin.cast ⋯) ⋯) ((prodT p.toTensor) ((prodT q✝.toTensor) q.toTensor)) All goals completed! 🐙
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕn2:ℕc:Fin n → Cc1:Fin n1 → Cc2:Fin n2 → Cp:Pure S cq:Pure S c1r:kt:S.Tensor c2ht:(prodT ((prodT p.toTensor) q.toTensor)) t = (permT (Fin.cast ⋯) ⋯) ((prodT p.toTensor) ((prodT q.toTensor) t))⊢ (prodT ((prodT p.toTensor) q.toTensor)) (r • t) =
(permT (Fin.cast ⋯) ⋯) ((prodT p.toTensor) ((prodT q.toTensor) (r • t))) All goals completed! 🐙
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕn2:ℕc:Fin n → Cc1:Fin n1 → Cc2:Fin n2 → Cp:Pure S cq:Pure S c1t1:S.Tensor c2t2:S.Tensor c2ht1:(prodT ((prodT p.toTensor) q.toTensor)) t1 = (permT (Fin.cast ⋯) ⋯) ((prodT p.toTensor) ((prodT q.toTensor) t1))ht2:(prodT ((prodT p.toTensor) q.toTensor)) t2 = (permT (Fin.cast ⋯) ⋯) ((prodT p.toTensor) ((prodT q.toTensor) t2))⊢ (prodT ((prodT p.toTensor) q.toTensor)) (t1 + t2) =
(permT (Fin.cast ⋯) ⋯) ((prodT p.toTensor) ((prodT q.toTensor) (t1 + t2))) All goals completed! 🐙
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕn2:ℕc:Fin n → Cc1:Fin n1 → Cc2:Fin n2 → Ct2:S.Tensor c2p:Pure S cr:kt:S.Tensor c1ht:(prodT ((prodT p.toTensor) t)) t2 = (permT (Fin.cast ⋯) ⋯) ((prodT p.toTensor) ((prodT t) t2))⊢ (prodT ((prodT p.toTensor) (r • t))) t2 = (permT (Fin.cast ⋯) ⋯) ((prodT p.toTensor) ((prodT (r • t)) t2)) All goals completed! 🐙
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕn2:ℕc:Fin n → Cc1:Fin n1 → Cc2:Fin n2 → Ct2✝:S.Tensor c2p:Pure S ct1:S.Tensor c1t2:S.Tensor c1ht1:(prodT ((prodT p.toTensor) t1)) t2✝ = (permT (Fin.cast ⋯) ⋯) ((prodT p.toTensor) ((prodT t1) t2✝))ht2:(prodT ((prodT p.toTensor) t2)) t2✝ = (permT (Fin.cast ⋯) ⋯) ((prodT p.toTensor) ((prodT t2) t2✝))⊢ (prodT ((prodT p.toTensor) (t1 + t2))) t2✝ = (permT (Fin.cast ⋯) ⋯) ((prodT p.toTensor) ((prodT (t1 + t2)) t2✝)) All goals completed! 🐙
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕn2:ℕc:Fin n → Cc1:Fin n1 → Cc2:Fin n2 → Ct1:S.Tensor c1t2:S.Tensor c2r:kt:S.Tensor cht:(prodT ((prodT t) t1)) t2 = (permT (Fin.cast ⋯) ⋯) ((prodT t) ((prodT t1) t2))⊢ (prodT ((prodT (r • t)) t1)) t2 = (permT (Fin.cast ⋯) ⋯) ((prodT (r • t)) ((prodT t1) t2)) All goals completed! 🐙
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕn2:ℕc:Fin n → Cc1:Fin n1 → Cc2:Fin n2 → Ct1✝:S.Tensor c1t2✝:S.Tensor c2t1:S.Tensor ct2:S.Tensor cht1:(prodT ((prodT t1) t1✝)) t2✝ = (permT (Fin.cast ⋯) ⋯) ((prodT t1) ((prodT t1✝) t2✝))ht2:(prodT ((prodT t2) t1✝)) t2✝ = (permT (Fin.cast ⋯) ⋯) ((prodT t2) ((prodT t1✝) t2✝))⊢ (prodT ((prodT (t1 + t2)) t1✝)) t2✝ = (permT (Fin.cast ⋯) ⋯) ((prodT (t1 + t2)) ((prodT t1✝) t2✝)) All goals completed! 🐙C.13. Associativity of the product of three tensors in the other direction
lemma prodT_assoc' {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 _ IsReindexing.append_assoc_left (prodT (prodT t t1) t2) := k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕn2:ℕc:Fin n → Cc1:Fin n1 → Cc2:Fin n2 → Ct:S.Tensor ct1:S.Tensor c1t2:S.Tensor c2⊢ (prodT t) ((prodT t1) t2) = (permT (Fin.cast ⋯) ⋯) ((prodT ((prodT t) t1)) t2)
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕn2:ℕc:Fin n → Cc1:Fin n1 → Cc2:Fin n2 → Ct1:S.Tensor c1t2:S.Tensor c2p:Pure S c⊢ (prodT p.toTensor) ((prodT t1) t2) = (permT (Fin.cast ⋯) ⋯) ((prodT ((prodT p.toTensor) t1)) t2)k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕn2:ℕc:Fin n → Cc1:Fin n1 → Cc2:Fin n2 → Ct1:S.Tensor c1t2:S.Tensor c2r:kt:S.Tensor cht:(prodT t) ((prodT t1) t2) = (permT (Fin.cast ⋯) ⋯) ((prodT ((prodT t) t1)) t2)⊢ (prodT (r • t)) ((prodT t1) t2) = (permT (Fin.cast ⋯) ⋯) ((prodT ((prodT (r • t)) t1)) t2)k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕn2:ℕc:Fin n → Cc1:Fin n1 → Cc2:Fin n2 → Ct1✝:S.Tensor c1t2✝:S.Tensor c2t1:S.Tensor ct2:S.Tensor cht1:(prodT t1) ((prodT t1✝) t2✝) = (permT (Fin.cast ⋯) ⋯) ((prodT ((prodT t1) t1✝)) t2✝)ht2:(prodT t2) ((prodT t1✝) t2✝) = (permT (Fin.cast ⋯) ⋯) ((prodT ((prodT t2) t1✝)) t2✝)⊢ (prodT (t1 + t2)) ((prodT t1✝) t2✝) = (permT (Fin.cast ⋯) ⋯) ((prodT ((prodT (t1 + t2)) t1✝)) t2✝)
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕn2:ℕc:Fin n → Cc1:Fin n1 → Cc2:Fin n2 → Ct1:S.Tensor c1t2:S.Tensor c2p:Pure S c⊢ (prodT p.toTensor) ((prodT t1) t2) = (permT (Fin.cast ⋯) ⋯) ((prodT ((prodT p.toTensor) t1)) t2) k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕn2:ℕc:Fin n → Cc1:Fin n1 → Cc2:Fin n2 → Ct2:S.Tensor c2p:Pure S cq:Pure S c1⊢ (prodT p.toTensor) ((prodT q.toTensor) t2) = (permT (Fin.cast ⋯) ⋯) ((prodT ((prodT p.toTensor) q.toTensor)) t2)k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕn2:ℕc:Fin n → Cc1:Fin n1 → Cc2:Fin n2 → Ct2:S.Tensor c2p:Pure S cr:kt:S.Tensor c1ht:(prodT p.toTensor) ((prodT t) t2) = (permT (Fin.cast ⋯) ⋯) ((prodT ((prodT p.toTensor) t)) t2)⊢ (prodT p.toTensor) ((prodT (r • t)) t2) = (permT (Fin.cast ⋯) ⋯) ((prodT ((prodT p.toTensor) (r • t))) t2)k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕn2:ℕc:Fin n → Cc1:Fin n1 → Cc2:Fin n2 → Ct2✝:S.Tensor c2p:Pure S ct1:S.Tensor c1t2:S.Tensor c1ht1:(prodT p.toTensor) ((prodT t1) t2✝) = (permT (Fin.cast ⋯) ⋯) ((prodT ((prodT p.toTensor) t1)) t2✝)ht2:(prodT p.toTensor) ((prodT t2) t2✝) = (permT (Fin.cast ⋯) ⋯) ((prodT ((prodT p.toTensor) t2)) t2✝)⊢ (prodT p.toTensor) ((prodT (t1 + t2)) t2✝) = (permT (Fin.cast ⋯) ⋯) ((prodT ((prodT p.toTensor) (t1 + t2))) t2✝)
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕn2:ℕc:Fin n → Cc1:Fin n1 → Cc2:Fin n2 → Ct2:S.Tensor c2p:Pure S cq:Pure S c1⊢ (prodT p.toTensor) ((prodT q.toTensor) t2) = (permT (Fin.cast ⋯) ⋯) ((prodT ((prodT p.toTensor) q.toTensor)) t2) k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕn2:ℕc:Fin n → Cc1:Fin n1 → Cc2:Fin n2 → Cp:Pure S cq✝:Pure S c1q:Pure S c2⊢ (prodT p.toTensor) ((prodT q✝.toTensor) q.toTensor) =
(permT (Fin.cast ⋯) ⋯) ((prodT ((prodT p.toTensor) q✝.toTensor)) q.toTensor)k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕn2:ℕc:Fin n → Cc1:Fin n1 → Cc2:Fin n2 → Cp:Pure S cq:Pure S c1r:kt:S.Tensor c2ht:(prodT p.toTensor) ((prodT q.toTensor) t) = (permT (Fin.cast ⋯) ⋯) ((prodT ((prodT p.toTensor) q.toTensor)) t)⊢ (prodT p.toTensor) ((prodT q.toTensor) (r • t)) =
(permT (Fin.cast ⋯) ⋯) ((prodT ((prodT p.toTensor) q.toTensor)) (r • t))k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕn2:ℕc:Fin n → Cc1:Fin n1 → Cc2:Fin n2 → Cp:Pure S cq:Pure S c1t1:S.Tensor c2t2:S.Tensor c2ht1:(prodT p.toTensor) ((prodT q.toTensor) t1) = (permT (Fin.cast ⋯) ⋯) ((prodT ((prodT p.toTensor) q.toTensor)) t1)ht2:(prodT p.toTensor) ((prodT q.toTensor) t2) = (permT (Fin.cast ⋯) ⋯) ((prodT ((prodT p.toTensor) q.toTensor)) t2)⊢ (prodT p.toTensor) ((prodT q.toTensor) (t1 + t2)) =
(permT (Fin.cast ⋯) ⋯) ((prodT ((prodT p.toTensor) q.toTensor)) (t1 + t2))
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕn2:ℕc:Fin n → Cc1:Fin n1 → Cc2:Fin n2 → Cp:Pure S cq✝:Pure S c1q:Pure S c2⊢ (prodT p.toTensor) ((prodT q✝.toTensor) q.toTensor) =
(permT (Fin.cast ⋯) ⋯) ((prodT ((prodT p.toTensor) q✝.toTensor)) q.toTensor) All goals completed! 🐙
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕn2:ℕc:Fin n → Cc1:Fin n1 → Cc2:Fin n2 → Cp:Pure S cq:Pure S c1r:kt:S.Tensor c2ht:(prodT p.toTensor) ((prodT q.toTensor) t) = (permT (Fin.cast ⋯) ⋯) ((prodT ((prodT p.toTensor) q.toTensor)) t)⊢ (prodT p.toTensor) ((prodT q.toTensor) (r • t)) =
(permT (Fin.cast ⋯) ⋯) ((prodT ((prodT p.toTensor) q.toTensor)) (r • t)) All goals completed! 🐙
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕn2:ℕc:Fin n → Cc1:Fin n1 → Cc2:Fin n2 → Cp:Pure S cq:Pure S c1t1:S.Tensor c2t2:S.Tensor c2ht1:(prodT p.toTensor) ((prodT q.toTensor) t1) = (permT (Fin.cast ⋯) ⋯) ((prodT ((prodT p.toTensor) q.toTensor)) t1)ht2:(prodT p.toTensor) ((prodT q.toTensor) t2) = (permT (Fin.cast ⋯) ⋯) ((prodT ((prodT p.toTensor) q.toTensor)) t2)⊢ (prodT p.toTensor) ((prodT q.toTensor) (t1 + t2)) =
(permT (Fin.cast ⋯) ⋯) ((prodT ((prodT p.toTensor) q.toTensor)) (t1 + t2)) All goals completed! 🐙
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕn2:ℕc:Fin n → Cc1:Fin n1 → Cc2:Fin n2 → Ct2:S.Tensor c2p:Pure S cr:kt:S.Tensor c1ht:(prodT p.toTensor) ((prodT t) t2) = (permT (Fin.cast ⋯) ⋯) ((prodT ((prodT p.toTensor) t)) t2)⊢ (prodT p.toTensor) ((prodT (r • t)) t2) = (permT (Fin.cast ⋯) ⋯) ((prodT ((prodT p.toTensor) (r • t))) t2) All goals completed! 🐙
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕn2:ℕc:Fin n → Cc1:Fin n1 → Cc2:Fin n2 → Ct2✝:S.Tensor c2p:Pure S ct1:S.Tensor c1t2:S.Tensor c1ht1:(prodT p.toTensor) ((prodT t1) t2✝) = (permT (Fin.cast ⋯) ⋯) ((prodT ((prodT p.toTensor) t1)) t2✝)ht2:(prodT p.toTensor) ((prodT t2) t2✝) = (permT (Fin.cast ⋯) ⋯) ((prodT ((prodT p.toTensor) t2)) t2✝)⊢ (prodT p.toTensor) ((prodT (t1 + t2)) t2✝) = (permT (Fin.cast ⋯) ⋯) ((prodT ((prodT p.toTensor) (t1 + t2))) t2✝) All goals completed! 🐙
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕn2:ℕc:Fin n → Cc1:Fin n1 → Cc2:Fin n2 → Ct1:S.Tensor c1t2:S.Tensor c2r:kt:S.Tensor cht:(prodT t) ((prodT t1) t2) = (permT (Fin.cast ⋯) ⋯) ((prodT ((prodT t) t1)) t2)⊢ (prodT (r • t)) ((prodT t1) t2) = (permT (Fin.cast ⋯) ⋯) ((prodT ((prodT (r • t)) t1)) t2) All goals completed! 🐙
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕn2:ℕc:Fin n → Cc1:Fin n1 → Cc2:Fin n2 → Ct1✝:S.Tensor c1t2✝:S.Tensor c2t1:S.Tensor ct2:S.Tensor cht1:(prodT t1) ((prodT t1✝) t2✝) = (permT (Fin.cast ⋯) ⋯) ((prodT ((prodT t1) t1✝)) t2✝)ht2:(prodT t2) ((prodT t1✝) t2✝) = (permT (Fin.cast ⋯) ⋯) ((prodT ((prodT t2) t1✝)) t2✝)⊢ (prodT (t1 + t2)) ((prodT t1✝) t2✝) = (permT (Fin.cast ⋯) ⋯) ((prodT ((prodT (t1 + t2)) t1✝)) t2✝) All goals completed! 🐙