1. Physlib
  2. Relativity
  3. Tensors
  4. Evaluation
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.Product public import Physlib.Relativity.Tensors.Contraction.Basis public import Physlib.Meta.Sorry

Evaluation of tensor indices

@[expose] public section

##Β The evaluation coefficient.

@[simp] lemma evalPCoeff_update_self (i : Fin (n + 1)) [inst : DecidableEq (Fin (n + 1))] (Ο† : basisIdx (c i)) (p : Pure S c) (x : V (c i)) : evalPCoeff i Ο† (p.update i x) = (b (c i)).repr 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:β„•c:Fin (n + 1) β†’ Ci:Fin (n + 1)inst:DecidableEq (Fin (n + 1))Ο†:basisIdx (c i)p:Pure S cx:V (c i)⊒ evalPCoeff i Ο† (p.update i x) = ((b (c i)).repr x) Ο† All goals completed! πŸ™@[simp] lemma evalPCoeff_update_succAbove (i : Fin (n + 1)) [inst : DecidableEq (Fin (n + 1))] (j : Fin n) (Ο† : basisIdx (c i)) (p : Pure S c) (x : V (c (i.succAbove j))) : evalPCoeff i Ο† (p.update (i.succAbove j) x) = evalPCoeff i Ο† 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:β„•c:Fin (n + 1) β†’ Ci:Fin (n + 1)inst:DecidableEq (Fin (n + 1))j:Fin nΟ†:basisIdx (c i)p:Pure S cx:V (c (i.succAbove j))⊒ evalPCoeff i Ο† (p.update (i.succAbove j) x) = evalPCoeff i Ο† p All goals completed! πŸ™lemma evalPCoeff_basisVector (i : Fin (n + 1)) (Ο† : basisIdx (c i)) (b' : ComponentIdx (S := S) c) : evalPCoeff i Ο† (Pure.basisVector c b') = if b' i = Ο† then (1 : k) else 0 := 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:β„•c:Fin (n + 1) β†’ Ci:Fin (n + 1)Ο†:basisIdx (c i)b':ComponentIdx c⊒ evalPCoeff i Ο† (basisVector c b') = if b' i = Ο† then 1 else 0 All goals completed! πŸ™

Evaluation for a pure tensor.

set_option backward.isDefEq.respectTransparency false in @[simp] lemma evalP_update_add [inst : DecidableEq (Fin (n + 1))] (i j : Fin (n + 1)) (Ο† : basisIdx (c i)) (p : Pure S c) (x y: V (c j)) : evalP i Ο† (p.update j (x + y)) = evalP i Ο† (p.update j x) + evalP i Ο† (p.update j y) := 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:β„•c:Fin (n + 1) β†’ Cinst:DecidableEq (Fin (n + 1))i:Fin (n + 1)j:Fin (n + 1)Ο†:basisIdx (c i)p:Pure S cx:V (c j)y:V (c j)⊒ evalP i Ο† (p.update j (x + y)) = evalP i Ο† (p.update j x) + evalP i Ο† (p.update j y) 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:β„•c:Fin (n + 1) β†’ Cinst:DecidableEq (Fin (n + 1))i:Fin (n + 1)j:Fin (n + 1)Ο†:basisIdx (c i)p:Pure S cx:V (c j)y:V (c j)⊒ evalPCoeff i Ο† (p.update j (x + y)) β€’ ((p.update j (x + y)).drop i).toTensor = evalPCoeff i Ο† (p.update j x) β€’ ((p.update j x).drop i).toTensor + evalPCoeff i Ο† (p.update j y) β€’ ((p.update j y).drop i).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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:β„•c:Fin (n + 1) β†’ Cinst:DecidableEq (Fin (n + 1))j:Fin (n + 1)p:Pure S cx:V (c j)y:V (c j)Ο†:basisIdx (c j)⊒ evalPCoeff j Ο† (p.update j (x + y)) β€’ ((p.update j (x + y)).drop j).toTensor = evalPCoeff j Ο† (p.update j x) β€’ ((p.update j x).drop j).toTensor + evalPCoeff j Ο† (p.update j y) β€’ ((p.update j y).drop j).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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:β„•c:Fin (n + 1) β†’ Cinst:DecidableEq (Fin (n + 1))i:Fin (n + 1)Ο†:basisIdx (c i)p:Pure S cj:Fin nx:V (c (i.succAbove j))y:V (c (i.succAbove j))⊒ evalPCoeff i Ο† (p.update (i.succAbove j) (x + y)) β€’ ((p.update (i.succAbove j) (x + y)).drop i).toTensor = evalPCoeff i Ο† (p.update (i.succAbove j) x) β€’ ((p.update (i.succAbove j) x).drop i).toTensor + evalPCoeff i Ο† (p.update (i.succAbove j) y) β€’ ((p.update (i.succAbove j) y).drop i).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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:β„•c:Fin (n + 1) β†’ Cinst:DecidableEq (Fin (n + 1))j:Fin (n + 1)p:Pure S cx:V (c j)y:V (c j)Ο†:basisIdx (c j)⊒ evalPCoeff j Ο† (p.update j (x + y)) β€’ ((p.update j (x + y)).drop j).toTensor = evalPCoeff j Ο† (p.update j x) β€’ ((p.update j x).drop j).toTensor + evalPCoeff j Ο† (p.update j y) β€’ ((p.update j y).drop j).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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:β„•c:Fin (n + 1) β†’ Cinst:DecidableEq (Fin (n + 1))i:Fin (n + 1)Ο†:basisIdx (c i)p:Pure S cj:Fin nx:V (c (i.succAbove j))y:V (c (i.succAbove j))⊒ evalPCoeff i Ο† (p.update (i.succAbove j) (x + y)) β€’ ((p.update (i.succAbove j) (x + y)).drop i).toTensor = evalPCoeff i Ο† (p.update (i.succAbove j) x) β€’ ((p.update (i.succAbove j) x).drop i).toTensor + evalPCoeff i Ο† (p.update (i.succAbove j) y) β€’ ((p.update (i.succAbove j) y).drop i).toTensor All goals completed! πŸ™set_option backward.isDefEq.respectTransparency false in @[simp] lemma evalP_update_smul [inst : DecidableEq (Fin (n + 1))] (i j : Fin (n + 1)) (Ο† : basisIdx (c i)) (p : Pure S c) (r : k) (x : V (c j)) : evalP i Ο† (p.update j (r β€’ x)) = r β€’ evalP i Ο† (p.update j 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:β„•c:Fin (n + 1) β†’ Cinst:DecidableEq (Fin (n + 1))i:Fin (n + 1)j:Fin (n + 1)Ο†:basisIdx (c i)p:Pure S cr:kx:V (c j)⊒ evalP i Ο† (p.update j (r β€’ x)) = r β€’ evalP i Ο† (p.update j 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:β„•c:Fin (n + 1) β†’ Cinst:DecidableEq (Fin (n + 1))i:Fin (n + 1)j:Fin (n + 1)Ο†:basisIdx (c i)p:Pure S cr:kx:V (c j)⊒ evalPCoeff i Ο† (p.update j (r β€’ x)) β€’ ((p.update j (r β€’ x)).drop i).toTensor = r β€’ evalPCoeff i Ο† (p.update j x) β€’ ((p.update j x).drop i).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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:β„•c:Fin (n + 1) β†’ Cinst:DecidableEq (Fin (n + 1))j:Fin (n + 1)p:Pure S cr:kx:V (c j)Ο†:basisIdx (c j)⊒ evalPCoeff j Ο† (p.update j (r β€’ x)) β€’ ((p.update j (r β€’ x)).drop j).toTensor = r β€’ evalPCoeff j Ο† (p.update j x) β€’ ((p.update j x).drop j).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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:β„•c:Fin (n + 1) β†’ Cinst:DecidableEq (Fin (n + 1))i:Fin (n + 1)Ο†:basisIdx (c i)p:Pure S cr:kj:Fin nx:V (c (i.succAbove j))⊒ evalPCoeff i Ο† (p.update (i.succAbove j) (r β€’ x)) β€’ ((p.update (i.succAbove j) (r β€’ x)).drop i).toTensor = r β€’ evalPCoeff i Ο† (p.update (i.succAbove j) x) β€’ ((p.update (i.succAbove j) x).drop i).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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:β„•c:Fin (n + 1) β†’ Cinst:DecidableEq (Fin (n + 1))j:Fin (n + 1)p:Pure S cr:kx:V (c j)Ο†:basisIdx (c j)⊒ evalPCoeff j Ο† (p.update j (r β€’ x)) β€’ ((p.update j (r β€’ x)).drop j).toTensor = r β€’ evalPCoeff j Ο† (p.update j x) β€’ ((p.update j x).drop j).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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:β„•c:Fin (n + 1) β†’ Cinst:DecidableEq (Fin (n + 1))i:Fin (n + 1)Ο†:basisIdx (c i)p:Pure S cr:kj:Fin nx:V (c (i.succAbove j))⊒ evalPCoeff i Ο† (p.update (i.succAbove j) (r β€’ x)) β€’ ((p.update (i.succAbove j) (r β€’ x)).drop i).toTensor = r β€’ evalPCoeff i Ο† (p.update (i.succAbove j) x) β€’ ((p.update (i.succAbove j) x).drop i).toTensor All goals completed! πŸ™

Evaluation for a pure tensor as multilinear map.

TODO "Choose a more descriptive name for `evalT` and `evalP`, taking into consideration the namespaces they live in."@[simp] lemma evalT_pure {n : β„•} {c : Fin (n + 1) β†’ C} (i : Fin (n + 1)) (Ο† : basisIdx (c i)) (p : Pure S c) : evalT i Ο† p.toTensor = Pure.evalP i Ο† 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:β„•c:Fin (n + 1) β†’ Ci:Fin (n + 1)Ο†:basisIdx (c i)p:Pure S c⊒ (evalT i Ο†) p.toTensor = Pure.evalP i Ο† 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:β„•c:Fin (n + 1) β†’ Ci:Fin (n + 1)Ο†:basisIdx (c i)p:Pure S c⊒ (PiTensorProduct.lift (Pure.evalPMultilinear i Ο†)) ((PiTensorProduct.tprod k) p) = Pure.evalP i Ο† 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:β„•c:Fin (n + 1) β†’ Ci:Fin (n + 1)Ο†:basisIdx (c i)p:Pure S c⊒ (PiTensorProduct.lift (Pure.evalPMultilinear i Ο†)) ((PiTensorProduct.tprod k) p) = (Pure.evalPMultilinear i Ο†) p 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:β„•c:Fin (n + 1) β†’ Ci:Fin (n + 1)Ο†:basisIdx (c i)p:Pure S c| (PiTensorProduct.lift (Pure.evalPMultilinear i Ο†)) ((PiTensorProduct.tprod k) p)lemma evalT_basis {n : β„•} {c : Fin (n + 1) β†’ C} (i : Fin (n + 1)) (b : ComponentIdx c) (x : basisIdx (c i)) : evalT i x (basis (S := S) c b) = if b i = x then basis (c ∘ i.succAbove) (fun j => b (i.succAbove j)) else 0 := 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:β„•c:Fin (n + 1) β†’ Ci:Fin (n + 1)b:ComponentIdx cx:basisIdx (c i)⊒ (evalT i x) ((basis c) b) = if b i = x then (basis (c ∘ i.succAbove)) fun j => b (i.succAbove j) else 0 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:β„•c:Fin (n + 1) β†’ Ci:Fin (n + 1)b:ComponentIdx cx:basisIdx (c i)⊒ (if b i = x then ((Pure.basisVector c b).drop i).toTensor else 0) = if b i = x then (Pure.basisVector (c ∘ i.succAbove) fun j => b (i.succAbove j)).toTensor else 0 All goals completed! πŸ™attribute [-simp] Matrix.cons_val_zero Matrix.cons_val Fin.succAbove_zeroTODO "Add lemmas related to the interaction of evalT and permT, prodT and contrT."

The commutation of evaluation with permutations.

Commuting evaluation with permutations.

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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:β„•m:β„•c:Fin (n + 1) β†’ Cc':Fin (m + 1) β†’ CΟƒ:Fin (n + 1) β†’ Fin (m + 1)h:IsReindexing c' c Οƒi:Fin (n + 1)x:basisIdx (c i)b:ComponentIdx c'h1:Β¬(basisIdxCongr β‹―) (b (Οƒ i)) = xh1':b (Οƒ i) β‰  (basisIdxCongr β‹―) x⊒ (if (basisIdxCongr β‹―) (b (Οƒ i)) = x then (basis (c ∘ i.succAbove)) fun j => (basisIdxCongr β‹―) (b (Οƒ (i.succAbove j))) else 0) = (permT (if hi : Οƒ i = 0 then fun j => (Οƒ (i.succAbove j)).pred β‹― else ((Οƒ i).pred hi).predAbove ∘ Οƒ ∘ i.succAbove) β‹―) (if b (Οƒ i) = (basisIdxCongr β‹―) x then (basis (c' ∘ (Οƒ i).succAbove)) fun j => b ((Οƒ i).succAbove j) else 0) 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:β„•m:β„•c:Fin (n + 1) β†’ Cc':Fin (m + 1) β†’ CΟƒ:Fin (n + 1) β†’ Fin (m + 1)h:IsReindexing c' c Οƒi:Fin (n + 1)x:basisIdx (c i)⊒ (evalT i x) ((permT Οƒ h) 0) = (permT (if hi : Οƒ i = 0 then fun j => (Οƒ (i.succAbove j)).pred β‹― else ((Οƒ i).pred hi).predAbove ∘ Οƒ ∘ i.succAbove) β‹―) ((evalT (Οƒ i) ((basisIdxCongr β‹―) x)) 0) 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:β„•m:β„•c:Fin (n + 1) β†’ Cc':Fin (m + 1) β†’ CΟƒ:Fin (n + 1) β†’ Fin (m + 1)h✝:IsReindexing c' c Οƒi:Fin (n + 1)x:basisIdx (c i)a:kt:S.Tensor c'h:(evalT i x) ((permT Οƒ h✝) t) = (permT (if hi : Οƒ i = 0 then fun j => (Οƒ (i.succAbove j)).pred β‹― else ((Οƒ i).pred hi).predAbove ∘ Οƒ ∘ i.succAbove) β‹―) ((evalT (Οƒ i) ((basisIdxCongr β‹―) x)) t)⊒ (evalT i x) ((permT Οƒ h✝) (a β€’ t)) = (permT (if hi : Οƒ i = 0 then fun j => (Οƒ (i.succAbove j)).pred β‹― else ((Οƒ i).pred hi).predAbove ∘ Οƒ ∘ i.succAbove) β‹―) ((evalT (Οƒ i) ((basisIdxCongr β‹―) x)) (a β€’ 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:β„•m:β„•c:Fin (n + 1) β†’ Cc':Fin (m + 1) β†’ CΟƒ:Fin (n + 1) β†’ Fin (m + 1)h:IsReindexing c' c Οƒi:Fin (n + 1)x:basisIdx (c i)t1:S.Tensor c't2:S.Tensor c'h1:(evalT i x) ((permT Οƒ h) t1) = (permT (if hi : Οƒ i = 0 then fun j => (Οƒ (i.succAbove j)).pred β‹― else ((Οƒ i).pred hi).predAbove ∘ Οƒ ∘ i.succAbove) β‹―) ((evalT (Οƒ i) ((basisIdxCongr β‹―) x)) t1)h2:(evalT i x) ((permT Οƒ h) t2) = (permT (if hi : Οƒ i = 0 then fun j => (Οƒ (i.succAbove j)).pred β‹― else ((Οƒ i).pred hi).predAbove ∘ Οƒ ∘ i.succAbove) β‹―) ((evalT (Οƒ i) ((basisIdxCongr β‹―) x)) t2)⊒ (evalT i x) ((permT Οƒ h) (t1 + t2)) = (permT (if hi : Οƒ i = 0 then fun j => (Οƒ (i.succAbove j)).pred β‹― else ((Οƒ i).pred hi).predAbove ∘ Οƒ ∘ i.succAbove) β‹―) ((evalT (Οƒ i) ((basisIdxCongr β‹―) x)) (t1 + t2)) All goals completed! πŸ™

The commutation of evaluation with evaluation.

TODO "Add the lemma corresponding the the commutation of two evaluations of tensor indices."

The commutation of evaluation with contraction.

Commuting evaluation with contraction. Evaluating index k and then contracting the pair i j equals contracting the corresponding pair k.succAbove i, k.succAbove j and then evaluating the residual index, up to the identity reindexing IsReindexing.succAbove_succSuccAbove_comm.

k✝:Typeinst✝⁡:CommRing k✝C: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) β†’ Module.Basis (basisIdx c) k✝ (V c)S:TensorSpecies k✝ C G V basisIdx rep bn:β„•c:Fin (n + 1 + 1 + 1) β†’ Ck:Fin (n + 1 + 1 + 1)i:Fin (n + 1 + 1)j:Fin (n + 1 + 1)Ο†:basisIdx (c k)hij:i β‰  j ∧ S.Ο„ ((c ∘ k.succAbove) i) = (c ∘ k.succAbove) jb:ComponentIdx chs:Pure.contrPCoeff i j hij (Pure.basisVector (c ∘ k.succAbove) fun m => b (k.succAbove m)) = Pure.contrPCoeff (k.succAbove i) (k.succAbove j) β‹― (Pure.basisVector c b)hidx:βˆ€ (m : Fin n), (k.succAbove i).succSuccAbove (k.succAbove j) (((k.succAbove i).predPredAbove (k.succAbove j) β‹― k β‹―).succAbove m) = k.succAbove (i.succSuccAbove j m)hk:(k.succAbove i).succSuccAbove (k.succAbove j) ((k.succAbove i).predPredAbove (k.succAbove j) β‹― k β‹―) = khcond:(ComponentIdx.dropPair (k.succAbove i) (k.succAbove j) b ((k.succAbove i).predPredAbove (k.succAbove j) β‹― k β‹―) = (basisIdxCongr β‹―) Ο†) = (b k = Ο†)⊒ (if b k = Ο† then Pure.contrPCoeff (k.succAbove i) (k.succAbove j) β‹― (Pure.basisVector c b) β€’ (basis ((c ∘ k.succAbove) ∘ i.succSuccAbove j)) (ComponentIdx.dropPair i j fun j => b (k.succAbove j)) else 0) = if ComponentIdx.dropPair (k.succAbove i) (k.succAbove j) b ((k.succAbove i).predPredAbove (k.succAbove j) β‹― k β‹―) = (basisIdxCongr β‹―) Ο† then Pure.contrPCoeff (k.succAbove i) (k.succAbove j) β‹― (Pure.basisVector c b) β€’ (basis ((c ∘ k.succAbove) ∘ i.succSuccAbove j)) fun i_1 => (basisIdxCongr β‹―) (ComponentIdx.dropPair (k.succAbove i) (k.succAbove j) b (((k.succAbove i).predPredAbove (k.succAbove j) β‹― k β‹―).succAbove (id i_1))) else 0 k✝:Typeinst✝⁡:CommRing k✝C: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) β†’ Module.Basis (basisIdx c) k✝ (V c)S:TensorSpecies k✝ C G V basisIdx rep bn:β„•c:Fin (n + 1 + 1 + 1) β†’ Ck:Fin (n + 1 + 1 + 1)i:Fin (n + 1 + 1)j:Fin (n + 1 + 1)Ο†:basisIdx (c k)hij:i β‰  j ∧ S.Ο„ ((c ∘ k.succAbove) i) = (c ∘ k.succAbove) jb:ComponentIdx chs:Pure.contrPCoeff i j hij (Pure.basisVector (c ∘ k.succAbove) fun m => b (k.succAbove m)) = Pure.contrPCoeff (k.succAbove i) (k.succAbove j) β‹― (Pure.basisVector c b)hidx:βˆ€ (m : Fin n), (k.succAbove i).succSuccAbove (k.succAbove j) (((k.succAbove i).predPredAbove (k.succAbove j) β‹― k β‹―).succAbove m) = k.succAbove (i.succSuccAbove j m)hk:(k.succAbove i).succSuccAbove (k.succAbove j) ((k.succAbove i).predPredAbove (k.succAbove j) β‹― k β‹―) = khcond:(ComponentIdx.dropPair (k.succAbove i) (k.succAbove j) b ((k.succAbove i).predPredAbove (k.succAbove j) β‹― k β‹―) = (basisIdxCongr β‹―) Ο†) = (b k = Ο†)⊒ (if b k = Ο† then Pure.contrPCoeff (k.succAbove i) (k.succAbove j) β‹― (Pure.basisVector c b) β€’ (basis ((c ∘ k.succAbove) ∘ i.succSuccAbove j)) (ComponentIdx.dropPair i j fun j => b (k.succAbove j)) else 0) = if b k = Ο† then Pure.contrPCoeff (k.succAbove i) (k.succAbove j) β‹― (Pure.basisVector c b) β€’ (basis ((c ∘ k.succAbove) ∘ i.succSuccAbove j)) fun i_1 => (basisIdxCongr β‹―) (ComponentIdx.dropPair (k.succAbove i) (k.succAbove j) b (((k.succAbove i).predPredAbove (k.succAbove j) β‹― k β‹―).succAbove (id i_1))) else 0 k✝:Typeinst✝⁡:CommRing k✝C: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) β†’ Module.Basis (basisIdx c) k✝ (V c)S:TensorSpecies k✝ C G V basisIdx rep bn:β„•c:Fin (n + 1 + 1 + 1) β†’ Ck:Fin (n + 1 + 1 + 1)i:Fin (n + 1 + 1)j:Fin (n + 1 + 1)Ο†:basisIdx (c k)hij:i β‰  j ∧ S.Ο„ ((c ∘ k.succAbove) i) = (c ∘ k.succAbove) jb:ComponentIdx chs:Pure.contrPCoeff i j hij (Pure.basisVector (c ∘ k.succAbove) fun m => b (k.succAbove m)) = Pure.contrPCoeff (k.succAbove i) (k.succAbove j) β‹― (Pure.basisVector c b)hidx:βˆ€ (m : Fin n), (k.succAbove i).succSuccAbove (k.succAbove j) (((k.succAbove i).predPredAbove (k.succAbove j) β‹― k β‹―).succAbove m) = k.succAbove (i.succSuccAbove j m)hk:(k.succAbove i).succSuccAbove (k.succAbove j) ((k.succAbove i).predPredAbove (k.succAbove j) β‹― k β‹―) = khcond:(ComponentIdx.dropPair (k.succAbove i) (k.succAbove j) b ((k.succAbove i).predPredAbove (k.succAbove j) β‹― k β‹―) = (basisIdxCongr β‹―) Ο†) = (b k = Ο†)hbk:b k = Ο†βŠ’ Pure.contrPCoeff (k.succAbove i) (k.succAbove j) β‹― (Pure.basisVector c b) β€’ (basis ((c ∘ k.succAbove) ∘ i.succSuccAbove j)) (ComponentIdx.dropPair i j fun j => b (k.succAbove j)) = Pure.contrPCoeff (k.succAbove i) (k.succAbove j) β‹― (Pure.basisVector c b) β€’ (basis ((c ∘ k.succAbove) ∘ i.succSuccAbove j)) fun i_1 => (basisIdxCongr β‹―) (ComponentIdx.dropPair (k.succAbove i) (k.succAbove j) b (((k.succAbove i).predPredAbove (k.succAbove j) β‹― k β‹―).succAbove (id i_1)))k✝:Typeinst✝⁡:CommRing k✝C: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) β†’ Module.Basis (basisIdx c) k✝ (V c)S:TensorSpecies k✝ C G V basisIdx rep bn:β„•c:Fin (n + 1 + 1 + 1) β†’ Ck:Fin (n + 1 + 1 + 1)i:Fin (n + 1 + 1)j:Fin (n + 1 + 1)Ο†:basisIdx (c k)hij:i β‰  j ∧ S.Ο„ ((c ∘ k.succAbove) i) = (c ∘ k.succAbove) jb:ComponentIdx chs:Pure.contrPCoeff i j hij (Pure.basisVector (c ∘ k.succAbove) fun m => b (k.succAbove m)) = Pure.contrPCoeff (k.succAbove i) (k.succAbove j) β‹― (Pure.basisVector c b)hidx:βˆ€ (m : Fin n), (k.succAbove i).succSuccAbove (k.succAbove j) (((k.succAbove i).predPredAbove (k.succAbove j) β‹― k β‹―).succAbove m) = k.succAbove (i.succSuccAbove j m)hk:(k.succAbove i).succSuccAbove (k.succAbove j) ((k.succAbove i).predPredAbove (k.succAbove j) β‹― k β‹―) = khcond:(ComponentIdx.dropPair (k.succAbove i) (k.succAbove j) b ((k.succAbove i).predPredAbove (k.succAbove j) β‹― k β‹―) = (basisIdxCongr β‹―) Ο†) = (b k = Ο†)hbk:Β¬b k = Ο†βŠ’ 0 = 0 k✝:Typeinst✝⁡:CommRing k✝C: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) β†’ Module.Basis (basisIdx c) k✝ (V c)S:TensorSpecies k✝ C G V basisIdx rep bn:β„•c:Fin (n + 1 + 1 + 1) β†’ Ck:Fin (n + 1 + 1 + 1)i:Fin (n + 1 + 1)j:Fin (n + 1 + 1)Ο†:basisIdx (c k)hij:i β‰  j ∧ S.Ο„ ((c ∘ k.succAbove) i) = (c ∘ k.succAbove) jb:ComponentIdx chs:Pure.contrPCoeff i j hij (Pure.basisVector (c ∘ k.succAbove) fun m => b (k.succAbove m)) = Pure.contrPCoeff (k.succAbove i) (k.succAbove j) β‹― (Pure.basisVector c b)hidx:βˆ€ (m : Fin n), (k.succAbove i).succSuccAbove (k.succAbove j) (((k.succAbove i).predPredAbove (k.succAbove j) β‹― k β‹―).succAbove m) = k.succAbove (i.succSuccAbove j m)hk:(k.succAbove i).succSuccAbove (k.succAbove j) ((k.succAbove i).predPredAbove (k.succAbove j) β‹― k β‹―) = khcond:(ComponentIdx.dropPair (k.succAbove i) (k.succAbove j) b ((k.succAbove i).predPredAbove (k.succAbove j) β‹― k β‹―) = (basisIdxCongr β‹―) Ο†) = (b k = Ο†)hbk:b k = Ο†βŠ’ Pure.contrPCoeff (k.succAbove i) (k.succAbove j) β‹― (Pure.basisVector c b) β€’ (basis ((c ∘ k.succAbove) ∘ i.succSuccAbove j)) (ComponentIdx.dropPair i j fun j => b (k.succAbove j)) = Pure.contrPCoeff (k.succAbove i) (k.succAbove j) β‹― (Pure.basisVector c b) β€’ (basis ((c ∘ k.succAbove) ∘ i.succSuccAbove j)) fun i_1 => (basisIdxCongr β‹―) (ComponentIdx.dropPair (k.succAbove i) (k.succAbove j) b (((k.succAbove i).predPredAbove (k.succAbove j) β‹― k β‹―).succAbove (id i_1))) k✝:Typeinst✝⁡:CommRing k✝C: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) β†’ Module.Basis (basisIdx c) k✝ (V c)S:TensorSpecies k✝ C G V basisIdx rep bn:β„•c:Fin (n + 1 + 1 + 1) β†’ Ck:Fin (n + 1 + 1 + 1)i:Fin (n + 1 + 1)j:Fin (n + 1 + 1)Ο†:basisIdx (c k)hij:i β‰  j ∧ S.Ο„ ((c ∘ k.succAbove) i) = (c ∘ k.succAbove) jb:ComponentIdx chs:Pure.contrPCoeff i j hij (Pure.basisVector (c ∘ k.succAbove) fun m => b (k.succAbove m)) = Pure.contrPCoeff (k.succAbove i) (k.succAbove j) β‹― (Pure.basisVector c b)hidx:βˆ€ (m : Fin n), (k.succAbove i).succSuccAbove (k.succAbove j) (((k.succAbove i).predPredAbove (k.succAbove j) β‹― k β‹―).succAbove m) = k.succAbove (i.succSuccAbove j m)hk:(k.succAbove i).succSuccAbove (k.succAbove j) ((k.succAbove i).predPredAbove (k.succAbove j) β‹― k β‹―) = khcond:(ComponentIdx.dropPair (k.succAbove i) (k.succAbove j) b ((k.succAbove i).predPredAbove (k.succAbove j) β‹― k β‹―) = (basisIdxCongr β‹―) Ο†) = (b k = Ο†)hbk:b k = Ο†βŠ’ (basis ((c ∘ k.succAbove) ∘ i.succSuccAbove j)) (ComponentIdx.dropPair i j fun j => b (k.succAbove j)) = (basis ((c ∘ k.succAbove) ∘ i.succSuccAbove j)) fun i_1 => (basisIdxCongr β‹―) (ComponentIdx.dropPair (k.succAbove i) (k.succAbove j) b (((k.succAbove i).predPredAbove (k.succAbove j) β‹― k β‹―).succAbove (id i_1))) k✝:Typeinst✝⁡:CommRing k✝C: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) β†’ Module.Basis (basisIdx c) k✝ (V c)S:TensorSpecies k✝ C G V basisIdx rep bn:β„•c:Fin (n + 1 + 1 + 1) β†’ Ck:Fin (n + 1 + 1 + 1)i:Fin (n + 1 + 1)j:Fin (n + 1 + 1)Ο†:basisIdx (c k)hij:i β‰  j ∧ S.Ο„ ((c ∘ k.succAbove) i) = (c ∘ k.succAbove) jb:ComponentIdx chs:Pure.contrPCoeff i j hij (Pure.basisVector (c ∘ k.succAbove) fun m => b (k.succAbove m)) = Pure.contrPCoeff (k.succAbove i) (k.succAbove j) β‹― (Pure.basisVector c b)hidx:βˆ€ (m : Fin n), (k.succAbove i).succSuccAbove (k.succAbove j) (((k.succAbove i).predPredAbove (k.succAbove j) β‹― k β‹―).succAbove m) = k.succAbove (i.succSuccAbove j m)hk:(k.succAbove i).succSuccAbove (k.succAbove j) ((k.succAbove i).predPredAbove (k.succAbove j) β‹― k β‹―) = khcond:(ComponentIdx.dropPair (k.succAbove i) (k.succAbove j) b ((k.succAbove i).predPredAbove (k.succAbove j) β‹― k β‹―) = (basisIdxCongr β‹―) Ο†) = (b k = Ο†)hbk:b k = Ο†βŠ’ (ComponentIdx.dropPair i j fun j => b (k.succAbove j)) = fun i_1 => (basisIdxCongr β‹―) (ComponentIdx.dropPair (k.succAbove i) (k.succAbove j) b (((k.succAbove i).predPredAbove (k.succAbove j) β‹― k β‹―).succAbove (id i_1))) k✝:Typeinst✝⁡:CommRing k✝C: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) β†’ Module.Basis (basisIdx c) k✝ (V c)S:TensorSpecies k✝ C G V basisIdx rep bn:β„•c:Fin (n + 1 + 1 + 1) β†’ Ck:Fin (n + 1 + 1 + 1)i:Fin (n + 1 + 1)j:Fin (n + 1 + 1)Ο†:basisIdx (c k)hij:i β‰  j ∧ S.Ο„ ((c ∘ k.succAbove) i) = (c ∘ k.succAbove) jb:ComponentIdx chs:Pure.contrPCoeff i j hij (Pure.basisVector (c ∘ k.succAbove) fun m => b (k.succAbove m)) = Pure.contrPCoeff (k.succAbove i) (k.succAbove j) β‹― (Pure.basisVector c b)hidx:βˆ€ (m : Fin n), (k.succAbove i).succSuccAbove (k.succAbove j) (((k.succAbove i).predPredAbove (k.succAbove j) β‹― k β‹―).succAbove m) = k.succAbove (i.succSuccAbove j m)hk:(k.succAbove i).succSuccAbove (k.succAbove j) ((k.succAbove i).predPredAbove (k.succAbove j) β‹― k β‹―) = khcond:(ComponentIdx.dropPair (k.succAbove i) (k.succAbove j) b ((k.succAbove i).predPredAbove (k.succAbove j) β‹― k β‹―) = (basisIdxCongr β‹―) Ο†) = (b k = Ο†)hbk:b k = Ο†m:Fin n⊒ ComponentIdx.dropPair i j (fun j => b (k.succAbove j)) m = (basisIdxCongr β‹―) (ComponentIdx.dropPair (k.succAbove i) (k.succAbove j) b (((k.succAbove i).predPredAbove (k.succAbove j) β‹― k β‹―).succAbove (id m))) k✝:Typeinst✝⁡:CommRing k✝C: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) β†’ Module.Basis (basisIdx c) k✝ (V c)S:TensorSpecies k✝ C G V basisIdx rep bn:β„•c:Fin (n + 1 + 1 + 1) β†’ Ck:Fin (n + 1 + 1 + 1)i:Fin (n + 1 + 1)j:Fin (n + 1 + 1)Ο†:basisIdx (c k)hij:i β‰  j ∧ S.Ο„ ((c ∘ k.succAbove) i) = (c ∘ k.succAbove) jb:ComponentIdx chs:Pure.contrPCoeff i j hij (Pure.basisVector (c ∘ k.succAbove) fun m => b (k.succAbove m)) = Pure.contrPCoeff (k.succAbove i) (k.succAbove j) β‹― (Pure.basisVector c b)hidx:βˆ€ (m : Fin n), (k.succAbove i).succSuccAbove (k.succAbove j) (((k.succAbove i).predPredAbove (k.succAbove j) β‹― k β‹―).succAbove m) = k.succAbove (i.succSuccAbove j m)hk:(k.succAbove i).succSuccAbove (k.succAbove j) ((k.succAbove i).predPredAbove (k.succAbove j) β‹― k β‹―) = khcond:(ComponentIdx.dropPair (k.succAbove i) (k.succAbove j) b ((k.succAbove i).predPredAbove (k.succAbove j) β‹― k β‹―) = (basisIdxCongr β‹―) Ο†) = (b k = Ο†)hbk:b k = Ο†m:Fin n⊒ b (k.succAbove (i.succSuccAbove j m)) = (basisIdxCongr β‹―) (b ((k.succAbove i).succSuccAbove (k.succAbove j) (((k.succAbove i).predPredAbove (k.succAbove j) β‹― k β‹―).succAbove m))) All goals completed! πŸ™ k✝:Typeinst✝⁡:CommRing k✝C: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) β†’ Module.Basis (basisIdx c) k✝ (V c)S:TensorSpecies k✝ C G V basisIdx rep bn:β„•c:Fin (n + 1 + 1 + 1) β†’ Ck:Fin (n + 1 + 1 + 1)i:Fin (n + 1 + 1)j:Fin (n + 1 + 1)Ο†:basisIdx (c k)hij:i β‰  j ∧ S.Ο„ ((c ∘ k.succAbove) i) = (c ∘ k.succAbove) jb:ComponentIdx chs:Pure.contrPCoeff i j hij (Pure.basisVector (c ∘ k.succAbove) fun m => b (k.succAbove m)) = Pure.contrPCoeff (k.succAbove i) (k.succAbove j) β‹― (Pure.basisVector c b)hidx:βˆ€ (m : Fin n), (k.succAbove i).succSuccAbove (k.succAbove j) (((k.succAbove i).predPredAbove (k.succAbove j) β‹― k β‹―).succAbove m) = k.succAbove (i.succSuccAbove j m)hk:(k.succAbove i).succSuccAbove (k.succAbove j) ((k.succAbove i).predPredAbove (k.succAbove j) β‹― k β‹―) = khcond:(ComponentIdx.dropPair (k.succAbove i) (k.succAbove j) b ((k.succAbove i).predPredAbove (k.succAbove j) β‹― k β‹―) = (basisIdxCongr β‹―) Ο†) = (b k = Ο†)hbk:Β¬b k = Ο†βŠ’ 0 = 0 All goals completed! πŸ™ k✝:Typeinst✝⁡:CommRing k✝C: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) β†’ Module.Basis (basisIdx c) k✝ (V c)S:TensorSpecies k✝ C G V basisIdx rep bn:β„•c:Fin (n + 1 + 1 + 1) β†’ Ck:Fin (n + 1 + 1 + 1)i:Fin (n + 1 + 1)j:Fin (n + 1 + 1)Ο†:basisIdx (c k)hij:i β‰  j ∧ S.Ο„ ((c ∘ k.succAbove) i) = (c ∘ k.succAbove) j⊒ (contrT n i j hij) ((evalT k Ο†) 0) = (permT id β‹―) ((evalT ((k.succAbove i).predPredAbove (k.succAbove j) β‹― k β‹―) ((basisIdxCongr β‹―) Ο†)) ((contrT (n + 1) (k.succAbove i) (k.succAbove j) β‹―) 0)) All goals completed! πŸ™ k✝:Typeinst✝⁡:CommRing k✝C: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) β†’ Module.Basis (basisIdx c) k✝ (V c)S:TensorSpecies k✝ C G V basisIdx rep bn:β„•c:Fin (n + 1 + 1 + 1) β†’ Ck:Fin (n + 1 + 1 + 1)i:Fin (n + 1 + 1)j:Fin (n + 1 + 1)Ο†:basisIdx (c k)hij:i β‰  j ∧ S.Ο„ ((c ∘ k.succAbove) i) = (c ∘ k.succAbove) ja:k✝t:S.Tensor chb:(contrT n i j hij) ((evalT k Ο†) t) = (permT id β‹―) ((evalT ((k.succAbove i).predPredAbove (k.succAbove j) β‹― k β‹―) ((basisIdxCongr β‹―) Ο†)) ((contrT (n + 1) (k.succAbove i) (k.succAbove j) β‹―) t))⊒ (contrT n i j hij) ((evalT k Ο†) (a β€’ t)) = (permT id β‹―) ((evalT ((k.succAbove i).predPredAbove (k.succAbove j) β‹― k β‹―) ((basisIdxCongr β‹―) Ο†)) ((contrT (n + 1) (k.succAbove i) (k.succAbove j) β‹―) (a β€’ t))) All goals completed! πŸ™ k✝:Typeinst✝⁡:CommRing k✝C: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) β†’ Module.Basis (basisIdx c) k✝ (V c)S:TensorSpecies k✝ C G V basisIdx rep bn:β„•c:Fin (n + 1 + 1 + 1) β†’ Ck:Fin (n + 1 + 1 + 1)i:Fin (n + 1 + 1)j:Fin (n + 1 + 1)Ο†:basisIdx (c k)hij:i β‰  j ∧ S.Ο„ ((c ∘ k.succAbove) i) = (c ∘ k.succAbove) jt1:S.Tensor ct2:S.Tensor chb1:(contrT n i j hij) ((evalT k Ο†) t1) = (permT id β‹―) ((evalT ((k.succAbove i).predPredAbove (k.succAbove j) β‹― k β‹―) ((basisIdxCongr β‹―) Ο†)) ((contrT (n + 1) (k.succAbove i) (k.succAbove j) β‹―) t1))hb2:(contrT n i j hij) ((evalT k Ο†) t2) = (permT id β‹―) ((evalT ((k.succAbove i).predPredAbove (k.succAbove j) β‹― k β‹―) ((basisIdxCongr β‹―) Ο†)) ((contrT (n + 1) (k.succAbove i) (k.succAbove j) β‹―) t2))⊒ (contrT n i j hij) ((evalT k Ο†) (t1 + t2)) = (permT id β‹―) ((evalT ((k.succAbove i).predPredAbove (k.succAbove j) β‹― k β‹―) ((basisIdxCongr β‹―) Ο†)) ((contrT (n + 1) (k.succAbove i) (k.succAbove j) β‹―) (t1 + t2))) All goals completed! πŸ™
TODO "Add a lemma similar to `contrT_evalT` except with the contraction and evaluation the other way around."

The commutation of evaluation with products.

Evaluating an index in the right factor of a tensor product commutes with forming the product, up to the identity reindexing which identifies the two ways of removing that index from the appended color list.

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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:β„•n1:β„•c:Fin n β†’ Cc1:Fin (n1 + 1) β†’ Ci:Fin (n1 + 1)x:basisIdx (c1 i)b:ComponentIdx cb1:ComponentIdx c1hi:Β¬b1 i = xhprod:ComponentIdx.prod.symm (b, b1) (Fin.natAdd n i) β‰  (basisIdxCongr β‹―) x⊒ (permT id β‹―) 0 = (prodT ((basis c) b)) 0 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:β„•n1:β„•c:Fin n β†’ Cc1:Fin (n1 + 1) β†’ Ci:Fin (n1 + 1)x:basisIdx (c1 i)b:ComponentIdx c⊒ (permT id β‹―) ((evalT (Fin.natAdd n i) ((basisIdxCongr β‹―) x)) ((prodT ((basis c) b)) 0)) = (prodT ((basis c) b)) ((evalT i x) 0) 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:β„•n1:β„•c:Fin n β†’ Cc1:Fin (n1 + 1) β†’ Ci:Fin (n1 + 1)x:basisIdx (c1 i)b:ComponentIdx ca:kt:S.Tensor c1ht:(permT id β‹―) ((evalT (Fin.natAdd n i) ((basisIdxCongr β‹―) x)) ((prodT ((basis c) b)) t)) = (prodT ((basis c) b)) ((evalT i x) t)⊒ (permT id β‹―) ((evalT (Fin.natAdd n i) ((basisIdxCongr β‹―) x)) ((prodT ((basis c) b)) (a β€’ t))) = (prodT ((basis c) b)) ((evalT i x) (a β€’ 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:β„•n1:β„•c:Fin n β†’ Cc1:Fin (n1 + 1) β†’ Ci:Fin (n1 + 1)x:basisIdx (c1 i)b:ComponentIdx ct2:S.Tensor c1t3:S.Tensor c1ht2:(permT id β‹―) ((evalT (Fin.natAdd n i) ((basisIdxCongr β‹―) x)) ((prodT ((basis c) b)) t2)) = (prodT ((basis c) b)) ((evalT i x) t2)ht3:(permT id β‹―) ((evalT (Fin.natAdd n i) ((basisIdxCongr β‹―) x)) ((prodT ((basis c) b)) t3)) = (prodT ((basis c) b)) ((evalT i x) t3)⊒ (permT id β‹―) ((evalT (Fin.natAdd n i) ((basisIdxCongr β‹―) x)) ((prodT ((basis c) b)) (t2 + t3))) = (prodT ((basis c) b)) ((evalT i x) (t2 + t3)) 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:β„•n1:β„•c:Fin n β†’ Cc1:Fin (n1 + 1) β†’ Ci:Fin (n1 + 1)x:basisIdx (c1 i)t1:S.Tensor c1⊒ (permT id β‹―) ((evalT (Fin.natAdd n i) ((basisIdxCongr β‹―) x)) ((prodT 0) t1)) = (prodT 0) ((evalT i x) 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:β„•n1:β„•c:Fin n β†’ Cc1:Fin (n1 + 1) β†’ Ci:Fin (n1 + 1)x:basisIdx (c1 i)t1:S.Tensor c1a:kt:S.Tensor cht:(permT id β‹―) ((evalT (Fin.natAdd n i) ((basisIdxCongr β‹―) x)) ((prodT t) t1)) = (prodT t) ((evalT i x) t1)⊒ (permT id β‹―) ((evalT (Fin.natAdd n i) ((basisIdxCongr β‹―) x)) ((prodT (a β€’ t)) t1)) = (prodT (a β€’ t)) ((evalT i x) 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:β„•n1:β„•c:Fin n β†’ Cc1:Fin (n1 + 1) β†’ Ci:Fin (n1 + 1)x:basisIdx (c1 i)t1:S.Tensor c1t2:S.Tensor ct3:S.Tensor cht2:(permT id β‹―) ((evalT (Fin.natAdd n i) ((basisIdxCongr β‹―) x)) ((prodT t2) t1)) = (prodT t2) ((evalT i x) t1)ht3:(permT id β‹―) ((evalT (Fin.natAdd n i) ((basisIdxCongr β‹―) x)) ((prodT t3) t1)) = (prodT t3) ((evalT i x) t1)⊒ (permT id β‹―) ((evalT (Fin.natAdd n i) ((basisIdxCongr β‹―) x)) ((prodT (t2 + t3)) t1)) = (prodT (t2 + t3)) ((evalT i x) t1) All goals completed! πŸ™
TODO "Add a lemmas related to the commutation of evaluation with contraction."

Other properties of evaluation

Evaluating the single-index basis tensor basis ![c] (single.symm b) at the index x yields the field element 1 if b = x (transported across ![c] 0 = c) and 0 otherwise: evaluation of a one-index basis tensor is the Kronecker delta.

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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝c:Cb:basisIdx cx:basisIdx (![c] 0)⊒ toField (if ComponentIdx.single.symm b 0 = x then (basis (![c] ∘ Fin.succAbove 0)) fun j => ComponentIdx.single.symm b (Fin.succAbove 0 j) else 0) = if (basisIdxCongr β‹―) b = x then 1 else 0 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝c:Cb:basisIdx cx:basisIdx (![c] 0)⊒ toField (if (basisIdxCongr β‹―) b = x then (basis (![c] ∘ Fin.succAbove 0)) fun j => (basisIdxCongr β‹―) b else 0) = if (basisIdxCongr β‹―) b = x then 1 else 0 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝c:Cb:basisIdx cx:basisIdx (![c] 0)h✝:(basisIdxCongr β‹―) b = x⊒ toField ((basis (![c] ∘ Fin.succAbove 0)) fun j => (basisIdxCongr β‹―) b) = 1k: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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝c:Cb:basisIdx cx:basisIdx (![c] 0)h✝:Β¬(basisIdxCongr β‹―) b = x⊒ toField 0 = 0 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝c:Cb:basisIdx cx:basisIdx (![c] 0)h✝:(basisIdxCongr β‹―) b = x⊒ toField ((basis (![c] ∘ Fin.succAbove 0)) fun j => (basisIdxCongr β‹―) b) = 1 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝c:Cb:basisIdx cx:basisIdx (![c] 0)h✝:Β¬(basisIdxCongr β‹―) b = x⊒ toField 0 = 0 All goals completed! πŸ™

Basis expansion of a one-index tensor: every t : Tensor S ![c] is the sum over basis indices i of its evaluation coefficient toField (evalT 0 i t) times the corresponding basis tensor.

lemma eq_sum_evalT_of_single_tensor_basis {c : C} (t : Tensor S ![c]) : t = βˆ‘ i, toField (evalT 0 i t) β€’ basis ![c] (ComponentIdx.single.symm (basisIdxCongr (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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Ct:S.Tensor ![c]i:basisIdx (![c] 0)⊒ ![c] 0 = c All goals completed! πŸ™) 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Ct:S.Tensor ![c]⊒ t = βˆ‘ i, toField ((evalT 0 i) t) β€’ (basis ![c]) (ComponentIdx.single.symm ((basisIdxCongr β‹―) 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cb:ComponentIdx ![c]⊒ (basis ![c]) b = βˆ‘ i, toField ((evalT 0 i) ((basis ![c]) b)) β€’ (basis ![c]) (ComponentIdx.single.symm ((basisIdxCongr β‹―) 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:C⊒ 0 = βˆ‘ i, toField ((evalT 0 i) 0) β€’ (basis ![c]) (ComponentIdx.single.symm ((basisIdxCongr β‹―) 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Ca:kt:S.Tensor ![c]h:t = βˆ‘ i, toField ((evalT 0 i) t) β€’ (basis ![c]) (ComponentIdx.single.symm ((basisIdxCongr β‹―) i))⊒ a β€’ t = βˆ‘ i, toField ((evalT 0 i) (a β€’ t)) β€’ (basis ![c]) (ComponentIdx.single.symm ((basisIdxCongr β‹―) 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Ct1:S.Tensor ![c]t2:S.Tensor ![c]h1:t1 = βˆ‘ i, toField ((evalT 0 i) t1) β€’ (basis ![c]) (ComponentIdx.single.symm ((basisIdxCongr β‹―) i))h2:t2 = βˆ‘ i, toField ((evalT 0 i) t2) β€’ (basis ![c]) (ComponentIdx.single.symm ((basisIdxCongr β‹―) i))⊒ t1 + t2 = βˆ‘ i, toField ((evalT 0 i) (t1 + t2)) β€’ (basis ![c]) (ComponentIdx.single.symm ((basisIdxCongr β‹―) 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cb:ComponentIdx ![c]⊒ (basis ![c]) b = βˆ‘ i, toField ((evalT 0 i) ((basis ![c]) b)) β€’ (basis ![c]) (ComponentIdx.single.symm ((basisIdxCongr β‹―) 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Ci:basisIdx c⊒ (basis ![c]) (ComponentIdx.single.symm i) = βˆ‘ i_1, toField ((evalT 0 i_1) ((basis ![c]) (ComponentIdx.single.symm i))) β€’ (basis ![c]) (ComponentIdx.single.symm ((basisIdxCongr β‹―) i_1)) 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Ci✝:basisIdx ci:basisIdx (![c] 0)| toField ((evalT 0 i) ((basis ![c]) (ComponentIdx.single.symm i✝))) β€’ (basis ![c]) (ComponentIdx.single.symm ((basisIdxCongr β‹―) 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Ci✝:basisIdx ci:basisIdx (![c] 0)| (if (basisIdxCongr β‹―) i✝ = i then 1 else 0) β€’ (basis ![c]) (ComponentIdx.single.symm ((basisIdxCongr β‹―) 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:C⊒ 0 = βˆ‘ i, toField ((evalT 0 i) 0) β€’ (basis ![c]) (ComponentIdx.single.symm ((basisIdxCongr β‹―) 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Ca:kt:S.Tensor ![c]h:t = βˆ‘ i, toField ((evalT 0 i) t) β€’ (basis ![c]) (ComponentIdx.single.symm ((basisIdxCongr β‹―) i))⊒ a β€’ t = βˆ‘ i, toField ((evalT 0 i) (a β€’ t)) β€’ (basis ![c]) (ComponentIdx.single.symm ((basisIdxCongr β‹―) i)) conv_lhs => 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Ca:kt:S.Tensor ![c]h:t = βˆ‘ i, toField ((evalT 0 i) t) β€’ (basis ![c]) (ComponentIdx.single.symm ((basisIdxCongr β‹―) i))| a β€’ βˆ‘ i, toField ((evalT 0 i) t) β€’ (basis ![c]) (ComponentIdx.single.symm ((basisIdxCongr β‹―) 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Ct1:S.Tensor ![c]t2:S.Tensor ![c]h1:t1 = βˆ‘ i, toField ((evalT 0 i) t1) β€’ (basis ![c]) (ComponentIdx.single.symm ((basisIdxCongr β‹―) i))h2:t2 = βˆ‘ i, toField ((evalT 0 i) t2) β€’ (basis ![c]) (ComponentIdx.single.symm ((basisIdxCongr β‹―) i))⊒ t1 + t2 = βˆ‘ i, toField ((evalT 0 i) (t1 + t2)) β€’ (basis ![c]) (ComponentIdx.single.symm ((basisIdxCongr β‹―) 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Ct1:S.Tensor ![c]t2:S.Tensor ![c]h1:t1 = βˆ‘ i, toField ((evalT 0 i) t1) β€’ (basis ![c]) (ComponentIdx.single.symm ((basisIdxCongr β‹―) i))h2:t2 = βˆ‘ i, toField ((evalT 0 i) t2) β€’ (basis ![c]) (ComponentIdx.single.symm ((basisIdxCongr β‹―) i))⊒ t1 + t2 = βˆ‘ x, toField ((evalT 0 x) t1) β€’ (basis ![c]) (ComponentIdx.single.symm ((basisIdxCongr β‹―) x)) + βˆ‘ x, toField ((evalT 0 x) t2) β€’ (basis ![c]) (ComponentIdx.single.symm ((basisIdxCongr β‹―) x)) All goals completed! πŸ™

Reconstruction of a tensor from the evaluations of its last index: every t : Tensor S c is the sum over basis indices i of the evaluation evalT (Fin.last n) i t tensored with the basis covector basis ![c (Fin.last n)] (single.symm i), with the appended index permuted back into the last slot.

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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:β„•c:Fin (n + 1) β†’ Cb:ComponentIdx ch1✝¹:IsReindexing (Fin.append (c ∘ (Fin.last n).succAbove) ![c (Fin.last n)]) c idh2:SMulCommClass k k (S.Tensor (Fin.append (c ∘ (Fin.last n).succAbove) ![c (Fin.last n)]))j:basisIdx (c (Fin.last n))h1✝:j ∈ Finset.univh1:j β‰  b (Fin.last n)⊒ (permT id h1✝¹) ((prodT 0) ((basis ![c (Fin.last n)]) (ComponentIdx.single.symm j))) = 0 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:β„•c:Fin (n + 1) β†’ Cb:ComponentIdx ch1:IsReindexing (Fin.append (c ∘ (Fin.last n).succAbove) ![c (Fin.last n)]) c idh2:SMulCommClass k k (S.Tensor (Fin.append (c ∘ (Fin.last n).succAbove) ![c (Fin.last n)]))⊒ b (Fin.last n) βˆ‰ Finset.univ β†’ (permT id h1) ((prodT (if b (Fin.last n) = b (Fin.last n) then (basis (c ∘ (Fin.last n).succAbove)) fun j => b ((Fin.last n).succAbove j) else 0)) ((basis ![c (Fin.last n)]) (ComponentIdx.single.symm (b (Fin.last n))))) = 0 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:β„•c:Fin (n + 1) β†’ C⊒ 0 = βˆ‘ i, (permT id β‹―) ((prodT ((evalT (Fin.last n) i) 0)) ((basis ![c (Fin.last n)]) (ComponentIdx.single.symm 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:β„•c:Fin (n + 1) β†’ Ca:kt:S.Tensor ch:t = βˆ‘ i, (permT id β‹―) ((prodT ((evalT (Fin.last n) i) t)) ((basis ![c (Fin.last n)]) (ComponentIdx.single.symm i)))⊒ a β€’ t = βˆ‘ i, (permT id β‹―) ((prodT ((evalT (Fin.last n) i) (a β€’ t))) ((basis ![c (Fin.last n)]) (ComponentIdx.single.symm i))) conv_lhs => 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:β„•c:Fin (n + 1) β†’ Ca:kt:S.Tensor ch:t = βˆ‘ i, (permT id β‹―) ((prodT ((evalT (Fin.last n) i) t)) ((basis ![c (Fin.last n)]) (ComponentIdx.single.symm i)))| a β€’ βˆ‘ i, (permT id β‹―) ((prodT ((evalT (Fin.last n) i) t)) ((basis ![c (Fin.last n)]) (ComponentIdx.single.symm 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:β„•c:Fin (n + 1) β†’ Ct1:S.Tensor ct2:S.Tensor ch1:t1 = βˆ‘ i, (permT id β‹―) ((prodT ((evalT (Fin.last n) i) t1)) ((basis ![c (Fin.last n)]) (ComponentIdx.single.symm i)))h2:t2 = βˆ‘ i, (permT id β‹―) ((prodT ((evalT (Fin.last n) i) t2)) ((basis ![c (Fin.last n)]) (ComponentIdx.single.symm i)))⊒ t1 + t2 = βˆ‘ i, (permT id β‹―) ((prodT ((evalT (Fin.last n) i) (t1 + t2))) ((basis ![c (Fin.last n)]) (ComponentIdx.single.symm 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:β„•c:Fin (n + 1) β†’ Ct1:S.Tensor ct2:S.Tensor ch1:t1 = βˆ‘ i, (permT id β‹―) ((prodT ((evalT (Fin.last n) i) t1)) ((basis ![c (Fin.last n)]) (ComponentIdx.single.symm i)))h2:t2 = βˆ‘ i, (permT id β‹―) ((prodT ((evalT (Fin.last n) i) t2)) ((basis ![c (Fin.last n)]) (ComponentIdx.single.symm i)))⊒ t1 + t2 = βˆ‘ x, (permT id β‹―) ((prodT ((evalT (Fin.last n) x) t1)) ((basis ![c (Fin.last n)]) (ComponentIdx.single.symm x))) + βˆ‘ x, (permT id β‹―) ((prodT ((evalT (Fin.last n) x) t2)) ((basis ![c (Fin.last n)]) (ComponentIdx.single.symm x))) All goals completed! πŸ™

Reconstruction of a tensor from the evaluations of its first index: every t : Tensor S c is the sum over basis indices i of the basis covector basis ![c 0] (single.symm i) tensored with the evaluation evalT 0 i t, with the prepended index permuted back into the first slot. This is the first-index analogue of eq_sum_evalT.

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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:β„•c:Fin (n + 1) β†’ Cb:ComponentIdx ch1✝¹:NeZero (n + 1)h2:n + 1 = Nat.succ 0 + nh3:IsReindexing (Fin.append ![c 0] (c ∘ Fin.succAbove 0)) c (Fin.cast h2)pf✝:SMulCommClass k k (S.Tensor (Fin.append ![c 0] (c ∘ Fin.succAbove 0)))j:basisIdx (c 0)h1✝:j ∈ Finset.univh1:j β‰  b 0⊒ (permT (Fin.cast h2) h3) ((prodT ((basis ![c 0]) (ComponentIdx.single.symm j))) 0) = 0 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:β„•c:Fin (n + 1) β†’ Cb:ComponentIdx ch1:NeZero (n + 1)h2:n + 1 = Nat.succ 0 + nh3:IsReindexing (Fin.append ![c 0] (c ∘ Fin.succAbove 0)) c (Fin.cast h2)pf✝:SMulCommClass k k (S.Tensor (Fin.append ![c 0] (c ∘ Fin.succAbove 0)))⊒ b 0 βˆ‰ Finset.univ β†’ (permT (Fin.cast h2) h3) ((prodT ((basis ![c 0]) (ComponentIdx.single.symm (b 0)))) (if b 0 = b 0 then (basis (c ∘ Fin.succAbove 0)) fun j => b (Fin.succAbove 0 j) else 0)) = 0 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:β„•c:Fin (n + 1) β†’ C⊒ 0 = βˆ‘ i, (permT (Fin.cast β‹―) β‹―) ((prodT ((basis ![c 0]) (ComponentIdx.single.symm i))) ((evalT 0 i) 0)) 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:β„•c:Fin (n + 1) β†’ Ca:kt:S.Tensor ch:t = βˆ‘ i, (permT (Fin.cast β‹―) β‹―) ((prodT ((basis ![c 0]) (ComponentIdx.single.symm i))) ((evalT 0 i) t))⊒ a β€’ t = βˆ‘ i, (permT (Fin.cast β‹―) β‹―) ((prodT ((basis ![c 0]) (ComponentIdx.single.symm i))) ((evalT 0 i) (a β€’ t))) conv_lhs => 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:β„•c:Fin (n + 1) β†’ Ca:kt:S.Tensor ch:t = βˆ‘ i, (permT (Fin.cast β‹―) β‹―) ((prodT ((basis ![c 0]) (ComponentIdx.single.symm i))) ((evalT 0 i) t))| a β€’ βˆ‘ i, (permT (Fin.cast β‹―) β‹―) ((prodT ((basis ![c 0]) (ComponentIdx.single.symm i))) ((evalT 0 i) 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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:β„•c:Fin (n + 1) β†’ Ct1:S.Tensor ct2:S.Tensor ch1:t1 = βˆ‘ i, (permT (Fin.cast β‹―) β‹―) ((prodT ((basis ![c 0]) (ComponentIdx.single.symm i))) ((evalT 0 i) t1))h2:t2 = βˆ‘ i, (permT (Fin.cast β‹―) β‹―) ((prodT ((basis ![c 0]) (ComponentIdx.single.symm i))) ((evalT 0 i) t2))⊒ t1 + t2 = βˆ‘ i, (permT (Fin.cast β‹―) β‹―) ((prodT ((basis ![c 0]) (ComponentIdx.single.symm i))) ((evalT 0 i) (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) β†’ Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:β„•c:Fin (n + 1) β†’ Ct1:S.Tensor ct2:S.Tensor ch1:t1 = βˆ‘ i, (permT (Fin.cast β‹―) β‹―) ((prodT ((basis ![c 0]) (ComponentIdx.single.symm i))) ((evalT 0 i) t1))h2:t2 = βˆ‘ i, (permT (Fin.cast β‹―) β‹―) ((prodT ((basis ![c 0]) (ComponentIdx.single.symm i))) ((evalT 0 i) t2))⊒ t1 + t2 = βˆ‘ x, (permT (Fin.cast β‹―) β‹―) ((prodT ((basis ![c 0]) (ComponentIdx.single.symm x))) ((evalT 0 x) t1)) + βˆ‘ x, (permT (Fin.cast β‹―) β‹―) ((prodT ((basis ![c 0]) (ComponentIdx.single.symm x))) ((evalT 0 x) t2)) All goals completed! πŸ™
All goals completed! πŸ™All goals completed! πŸ™