1. Physlib
  2. Relativity
  3. Tensors
  4. Contraction
  5. Pure
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

Contractions on pure tensors

@[expose] public section

Pure.contrPCoeff

dropPair

Given i j : Fin (n + 1 + 1), c : Fin (n + 1 + 1) → C and a pure tensor p : Pure S c, dropPair i j _ p is the tensor formed by dropping the ith and jth parts of p.

set_option linter.unusedVariables false in@[nolint unusedArguments] def dropPair (i j : Fin (n + 1 + 1)) (hij : i ≠ j) (p : Pure S c) : Pure S (c ∘ succSuccAbove i j) := fun m => p (succSuccAbove i j m)
@[simp] lemma dropPair_equivariant {n : ℕ} {c : Fin (n + 1 + 1) → C} (i j : Fin (n + 1 + 1)) (hij : i ≠ j) (p : Pure S c) (g : G) : dropPair i j hij (g • p) = g • dropPair i j hij 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 bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jp:Pure S cg:G⊢ dropPair i j hij (g • p) = g • dropPair i j hij 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 bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jp:Pure S cg:Gm:Fin n⊢ dropPair i j hij (g • p) m = (g • dropPair i j hij p) m 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 + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jp:Pure S cg:Gm:Fin n⊢ ((rep (c (i.succSuccAbove j m))) g) (p (i.succSuccAbove j m)) = ((rep ((c ∘ i.succSuccAbove j) m)) g) (p (i.succSuccAbove j m)) All goals completed! 🐙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 + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1hij2:i2 ≠ j2p:Pure S cm:Fin n⊢ i1 ≠ j1k: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 + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1hij2:i2 ≠ j2p:Pure S cm:Fin n⊢ i2 ≠ j2 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 + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1hij2:i2 ≠ j2p:Pure S cm:Fin n⊢ i1 ≠ j1 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 + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1hij2:i2 ≠ j2p:Pure S cm:Fin n⊢ i2 ≠ j2 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:ℕinst:DecidableEq (Fin (n + 1 + 1))c:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jp:Pure S cx:V (c i)m:Fin n⊢ i.succSuccAbove j m ≠ 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 bn:ℕinst:DecidableEq (Fin (n + 1 + 1))c:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jp:Pure S cx:V (c j)⊢ permP id ⋯ (dropPair j i ⋯ (p.update j x)) = dropPair i j hij 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 bn:ℕinst:DecidableEq (Fin (n + 1 + 1))c:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jp:Pure S cx:V (c j)⊢ permP id ⋯ (dropPair j i ⋯ p) = dropPair i j hij 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) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕinst:DecidableEq (Fin (n + 1 + 1))c:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jp:Pure S cx:V (c j)| permP id ⋯ (dropPair j 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) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕinst:DecidableEq (Fin (n + 1 + 1))c:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jp:Pure S cm:Fin nx:V (c (i.succSuccAbove j m))m':Fin nh:¬m' = m⊢ p (i.succSuccAbove j m') = dropPair i j hij p m'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:ℕinst:DecidableEq (Fin (n + 1 + 1))c:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jp:Pure S cm:Fin nx:V (c (i.succSuccAbove j m))m':Fin nh:¬m' = m⊢ m' ≠ mk: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:ℕinst:DecidableEq (Fin (n + 1 + 1))c:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jp:Pure S cm:Fin nx:V (c (i.succSuccAbove j m))m':Fin nh:¬m' = m⊢ i.succSuccAbove j m' ≠ i.succSuccAbove j m 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:ℕinst:DecidableEq (Fin (n + 1 + 1))c:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jp:Pure S cm:Fin nx:V (c (i.succSuccAbove j m))m':Fin nh:¬m' = m⊢ p (i.succSuccAbove j m') = dropPair i j hij p m' 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:ℕinst:DecidableEq (Fin (n + 1 + 1))c:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jp:Pure S cm:Fin nx:V (c (i.succSuccAbove j m))m':Fin nh:¬m' = m⊢ m' ≠ m 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:ℕinst:DecidableEq (Fin (n + 1 + 1))c:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jp:Pure S cm:Fin nx:V (c (i.succSuccAbove j m))m':Fin nh:¬m' = m⊢ i.succSuccAbove j m' ≠ i.succSuccAbove j m All goals completed! 🐙TODO "Prove lemmas relating to the commutation rules of `dropPair` and `prodP`."@[simp] lemma dropPair_permP {n n1 : ℕ} {c : Fin (n + 1 + 1) → C} {c1 : Fin (n1 + 1 + 1) → C} (i j : Fin (n1 + 1 + 1)) (hij : i ≠ j) (σ : Fin (n1 + 1 + 1) → Fin (n + 1 + 1)) (hσ : IsReindexing c c1 σ) (p : Pure S c) : dropPair i j hij (permP σ hσ p) = permP _ (hσ.succSuccAbove i j hij) (dropPair (σ i) (σ 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 bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin (n1 + 1 + 1) → Ci:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:IsReindexing c c1 σp:Pure S c⊢ σ i ≠ σ j All goals completed! 🐙) 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 bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin (n1 + 1 + 1) → Ci:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:IsReindexing c c1 σp:Pure S c⊢ dropPair i j hij (permP σ hσ p) = permP (i.funPredPredAbove j hij σ ⋯) ⋯ (dropPair (σ i) (σ j) ⋯ 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 bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin (n1 + 1 + 1) → Ci:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:IsReindexing c c1 σp:Pure S cm:Fin n1⊢ dropPair i j hij (permP σ hσ p) m = permP (i.funPredPredAbove j hij σ ⋯) ⋯ (dropPair (σ i) (σ j) ⋯ p) m 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 + 1 + 1) → Cc1:Fin (n1 + 1 + 1) → Ci:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:IsReindexing c c1 σp:Pure S cm:Fin n1⊢ (LinearEquiv.cast ⋯) (p (σ (i.succSuccAbove j m))) = (LinearEquiv.cast ⋯) (p ((σ i).succSuccAbove (σ j) ((σ i).predPredAbove (σ j) ⋯ (σ (i.succSuccAbove j m)) ⋯))) 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 + 1 + 1) → Cc1:Fin (n1 + 1 + 1) → Ci:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:IsReindexing c c1 σp:Pure S cm:Fin n1⊢ σ (i.succSuccAbove j m) = (σ i).succSuccAbove (σ j) ((σ i).predPredAbove (σ j) ⋯ (σ (i.succSuccAbove j m)) ⋯)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 + 1 + 1) → Cc1:Fin (n1 + 1 + 1) → Ci:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:IsReindexing c c1 σp:Pure S cm:Fin n1⊢ c (σ (i.succSuccAbove j m)) = c1 (i.succSuccAbove j m)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 + 1 + 1) → Cc1:Fin (n1 + 1 + 1) → Ci:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:IsReindexing c c1 σp:Pure S cm:Fin n1⊢ c ((σ i).succSuccAbove (σ j) ((σ i).predPredAbove (σ j) ⋯ (σ (i.succSuccAbove j m)) ⋯)) = c1 (i.succSuccAbove j m) 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 + 1 + 1) → Cc1:Fin (n1 + 1 + 1) → Ci:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:IsReindexing c c1 σp:Pure S cm:Fin n1⊢ σ (i.succSuccAbove j m) = (σ i).succSuccAbove (σ j) ((σ i).predPredAbove (σ j) ⋯ (σ (i.succSuccAbove j m)) ⋯) 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 + 1 + 1) → Cc1:Fin (n1 + 1 + 1) → Ci:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:IsReindexing c c1 σp:Pure S cm:Fin n1⊢ c (σ (i.succSuccAbove j m)) = c1 (i.succSuccAbove j m) 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 + 1 + 1) → Cc1:Fin (n1 + 1 + 1) → Ci:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:IsReindexing c c1 σp:Pure S cm:Fin n1⊢ c ((σ i).succSuccAbove (σ j) ((σ i).predPredAbove (σ j) ⋯ (σ (i.succSuccAbove j m)) ⋯)) = c1 (i.succSuccAbove j m) All goals completed! 🐙

Two permP–dropPair–dropPair towers over a common pure tensor agree once their composite slot maps agree pointwise. Comparing two orders of dropping two pairs of slots this way keeps every slot map an opaque variable, so the comparison closes by unification rather than by whnf-reducing the color and index-map composites.

lemma permP_dropPair_dropPair_congr {nP nOut : ℕ} {c : Fin (nP + 1 + 1 + 1 + 1) → C} {cOut : Fin nOut → C} (p : Pure S c) (aL bL : Fin (nP + 1 + 1 + 1 + 1)) (habL : aL ≠ bL) (a2L b2L : Fin (nP + 1 + 1)) (hab2L : a2L ≠ b2L) (σ1L : Fin nOut → Fin nP) (h1L : IsReindexing ((c ∘ Fin.succSuccAbove aL bL) ∘ Fin.succSuccAbove a2L b2L) cOut σ1L) (aR bR : Fin (nP + 1 + 1 + 1 + 1)) (habR : aR ≠ bR) (a2R b2R : Fin (nP + 1 + 1)) (hab2R : a2R ≠ b2R) (σ1R : Fin nOut → Fin nP) (h1R : IsReindexing ((c ∘ Fin.succSuccAbove aR bR) ∘ Fin.succSuccAbove a2R b2R) cOut σ1R) (hslot : ∀ m : Fin nOut, Fin.succSuccAbove aL bL (Fin.succSuccAbove a2L b2L (σ1L m)) = Fin.succSuccAbove aR bR (Fin.succSuccAbove a2R b2R (σ1R m))) : permP σ1L h1L (dropPair a2L b2L hab2L (dropPair aL bL habL p)) = permP σ1R h1R (dropPair a2R b2R hab2R (dropPair aR bR habR 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 bnP:ℕnOut:ℕc:Fin (nP + 1 + 1 + 1 + 1) → CcOut:Fin nOut → Cp:Pure S caL:Fin (nP + 1 + 1 + 1 + 1)bL:Fin (nP + 1 + 1 + 1 + 1)habL:aL ≠ bLa2L:Fin (nP + 1 + 1)b2L:Fin (nP + 1 + 1)hab2L:a2L ≠ b2Lσ1L:Fin nOut → Fin nPh1L:IsReindexing ((c ∘ aL.succSuccAbove bL) ∘ a2L.succSuccAbove b2L) cOut σ1LaR:Fin (nP + 1 + 1 + 1 + 1)bR:Fin (nP + 1 + 1 + 1 + 1)habR:aR ≠ bRa2R:Fin (nP + 1 + 1)b2R:Fin (nP + 1 + 1)hab2R:a2R ≠ b2Rσ1R:Fin nOut → Fin nPh1R:IsReindexing ((c ∘ aR.succSuccAbove bR) ∘ a2R.succSuccAbove b2R) cOut σ1Rhslot:∀ (m : Fin nOut), aL.succSuccAbove bL (a2L.succSuccAbove b2L (σ1L m)) = aR.succSuccAbove bR (a2R.succSuccAbove b2R (σ1R m))⊢ permP σ1L h1L (dropPair a2L b2L hab2L (dropPair aL bL habL p)) = permP σ1R h1R (dropPair a2R b2R hab2R (dropPair aR bR habR 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 bnP:ℕnOut:ℕc:Fin (nP + 1 + 1 + 1 + 1) → CcOut:Fin nOut → Cp:Pure S caL:Fin (nP + 1 + 1 + 1 + 1)bL:Fin (nP + 1 + 1 + 1 + 1)habL:aL ≠ bLa2L:Fin (nP + 1 + 1)b2L:Fin (nP + 1 + 1)hab2L:a2L ≠ b2Lσ1L:Fin nOut → Fin nPh1L:IsReindexing ((c ∘ aL.succSuccAbove bL) ∘ a2L.succSuccAbove b2L) cOut σ1LaR:Fin (nP + 1 + 1 + 1 + 1)bR:Fin (nP + 1 + 1 + 1 + 1)habR:aR ≠ bRa2R:Fin (nP + 1 + 1)b2R:Fin (nP + 1 + 1)hab2R:a2R ≠ b2Rσ1R:Fin nOut → Fin nPh1R:IsReindexing ((c ∘ aR.succSuccAbove bR) ∘ a2R.succSuccAbove b2R) cOut σ1Rhslot:∀ (m : Fin nOut), aL.succSuccAbove bL (a2L.succSuccAbove b2L (σ1L m)) = aR.succSuccAbove bR (a2R.succSuccAbove b2R (σ1R m))m:Fin nOut⊢ permP σ1L h1L (dropPair a2L b2L hab2L (dropPair aL bL habL p)) m = permP σ1R h1R (dropPair a2R b2R hab2R (dropPair aR bR habR p)) m 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 bnP:ℕnOut:ℕc:Fin (nP + 1 + 1 + 1 + 1) → CcOut:Fin nOut → Cp:Pure S caL:Fin (nP + 1 + 1 + 1 + 1)bL:Fin (nP + 1 + 1 + 1 + 1)habL:aL ≠ bLa2L:Fin (nP + 1 + 1)b2L:Fin (nP + 1 + 1)hab2L:a2L ≠ b2Lσ1L:Fin nOut → Fin nPh1L:IsReindexing ((c ∘ aL.succSuccAbove bL) ∘ a2L.succSuccAbove b2L) cOut σ1LaR:Fin (nP + 1 + 1 + 1 + 1)bR:Fin (nP + 1 + 1 + 1 + 1)habR:aR ≠ bRa2R:Fin (nP + 1 + 1)b2R:Fin (nP + 1 + 1)hab2R:a2R ≠ b2Rσ1R:Fin nOut → Fin nPh1R:IsReindexing ((c ∘ aR.succSuccAbove bR) ∘ a2R.succSuccAbove b2R) cOut σ1Rhslot:∀ (m : Fin nOut), aL.succSuccAbove bL (a2L.succSuccAbove b2L (σ1L m)) = aR.succSuccAbove bR (a2R.succSuccAbove b2R (σ1R m))m:Fin nOut⊢ (LinearEquiv.cast ⋯) (p (aL.succSuccAbove bL (a2L.succSuccAbove b2L (σ1L m)))) = (LinearEquiv.cast ⋯) (p (aR.succSuccAbove bR (a2R.succSuccAbove b2R (σ1R m)))) All goals completed! 🐙

Two permP–dropPair–permP towers over a common pure tensor agree once their composite slot maps agree pointwise. The one-contraction, inner-relabelled sibling of permP_dropPair_dropPair_congr.

lemma permP_dropPair_permP_congr {nP nOut mL mR : ℕ} {c : Fin nP → C} {cL : Fin (mL + 1 + 1) → C} {cR : Fin (mR + 1 + 1) → C} {cOut : Fin nOut → C} (p : Pure S c) (σ0L : Fin (mL + 1 + 1) → Fin nP) (h0L : IsReindexing c cL σ0L) (aL bL : Fin (mL + 1 + 1)) (habL : aL ≠ bL) (σ1L : Fin nOut → Fin mL) (h1L : IsReindexing (cL ∘ Fin.succSuccAbove aL bL) cOut σ1L) (σ0R : Fin (mR + 1 + 1) → Fin nP) (h0R : IsReindexing c cR σ0R) (aR bR : Fin (mR + 1 + 1)) (habR : aR ≠ bR) (σ1R : Fin nOut → Fin mR) (h1R : IsReindexing (cR ∘ Fin.succSuccAbove aR bR) cOut σ1R) (hslot : ∀ m : Fin nOut, σ0L (Fin.succSuccAbove aL bL (σ1L m)) = σ0R (Fin.succSuccAbove aR bR (σ1R m))) : permP σ1L h1L (dropPair aL bL habL (permP σ0L h0L p)) = permP σ1R h1R (dropPair aR bR habR (permP σ0R h0R 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 bnP:ℕnOut:ℕmL:ℕmR:ℕc:Fin nP → CcL:Fin (mL + 1 + 1) → CcR:Fin (mR + 1 + 1) → CcOut:Fin nOut → Cp:Pure S cσ0L:Fin (mL + 1 + 1) → Fin nPh0L:IsReindexing c cL σ0LaL:Fin (mL + 1 + 1)bL:Fin (mL + 1 + 1)habL:aL ≠ bLσ1L:Fin nOut → Fin mLh1L:IsReindexing (cL ∘ aL.succSuccAbove bL) cOut σ1Lσ0R:Fin (mR + 1 + 1) → Fin nPh0R:IsReindexing c cR σ0RaR:Fin (mR + 1 + 1)bR:Fin (mR + 1 + 1)habR:aR ≠ bRσ1R:Fin nOut → Fin mRh1R:IsReindexing (cR ∘ aR.succSuccAbove bR) cOut σ1Rhslot:∀ (m : Fin nOut), σ0L (aL.succSuccAbove bL (σ1L m)) = σ0R (aR.succSuccAbove bR (σ1R m))⊢ permP σ1L h1L (dropPair aL bL habL (permP σ0L h0L p)) = permP σ1R h1R (dropPair aR bR habR (permP σ0R h0R 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 bnP:ℕnOut:ℕmL:ℕmR:ℕc:Fin nP → CcL:Fin (mL + 1 + 1) → CcR:Fin (mR + 1 + 1) → CcOut:Fin nOut → Cp:Pure S cσ0L:Fin (mL + 1 + 1) → Fin nPh0L:IsReindexing c cL σ0LaL:Fin (mL + 1 + 1)bL:Fin (mL + 1 + 1)habL:aL ≠ bLσ1L:Fin nOut → Fin mLh1L:IsReindexing (cL ∘ aL.succSuccAbove bL) cOut σ1Lσ0R:Fin (mR + 1 + 1) → Fin nPh0R:IsReindexing c cR σ0RaR:Fin (mR + 1 + 1)bR:Fin (mR + 1 + 1)habR:aR ≠ bRσ1R:Fin nOut → Fin mRh1R:IsReindexing (cR ∘ aR.succSuccAbove bR) cOut σ1Rhslot:∀ (m : Fin nOut), σ0L (aL.succSuccAbove bL (σ1L m)) = σ0R (aR.succSuccAbove bR (σ1R m))m:Fin nOut⊢ permP σ1L h1L (dropPair aL bL habL (permP σ0L h0L p)) m = permP σ1R h1R (dropPair aR bR habR (permP σ0R h0R p)) m 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 bnP:ℕnOut:ℕmL:ℕmR:ℕc:Fin nP → CcL:Fin (mL + 1 + 1) → CcR:Fin (mR + 1 + 1) → CcOut:Fin nOut → Cp:Pure S cσ0L:Fin (mL + 1 + 1) → Fin nPh0L:IsReindexing c cL σ0LaL:Fin (mL + 1 + 1)bL:Fin (mL + 1 + 1)habL:aL ≠ bLσ1L:Fin nOut → Fin mLh1L:IsReindexing (cL ∘ aL.succSuccAbove bL) cOut σ1Lσ0R:Fin (mR + 1 + 1) → Fin nPh0R:IsReindexing c cR σ0RaR:Fin (mR + 1 + 1)bR:Fin (mR + 1 + 1)habR:aR ≠ bRσ1R:Fin nOut → Fin mRh1R:IsReindexing (cR ∘ aR.succSuccAbove bR) cOut σ1Rhslot:∀ (m : Fin nOut), σ0L (aL.succSuccAbove bL (σ1L m)) = σ0R (aR.succSuccAbove bR (σ1R m))m:Fin nOut⊢ (LinearEquiv.cast ⋯) ((LinearEquiv.cast ⋯) (p (σ0L (aL.succSuccAbove bL (σ1L m))))) = (LinearEquiv.cast ⋯) ((LinearEquiv.cast ⋯) (p (σ0R (aR.succSuccAbove bR (σ1R m))))) -- Each side is a two-`cast` tower, one cast from the inner `permP` and one from the outer -- `permP`-after-`dropPair`. `LinearEquiv.cast` is defeq to `_root_.cast`, so drop to the plain -- cast, fuse the tower with `cast_cast`, and close with the single-cast lemma `congr_mid`. 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 bnP:ℕnOut:ℕmL:ℕmR:ℕc:Fin nP → CcL:Fin (mL + 1 + 1) → CcR:Fin (mR + 1 + 1) → CcOut:Fin nOut → Cp:Pure S cσ0L:Fin (mL + 1 + 1) → Fin nPh0L:IsReindexing c cL σ0LaL:Fin (mL + 1 + 1)bL:Fin (mL + 1 + 1)habL:aL ≠ bLσ1L:Fin nOut → Fin mLh1L:IsReindexing (cL ∘ aL.succSuccAbove bL) cOut σ1Lσ0R:Fin (mR + 1 + 1) → Fin nPh0R:IsReindexing c cR σ0RaR:Fin (mR + 1 + 1)bR:Fin (mR + 1 + 1)habR:aR ≠ bRσ1R:Fin nOut → Fin mRh1R:IsReindexing (cR ∘ aR.succSuccAbove bR) cOut σ1Rhslot:∀ (m : Fin nOut), σ0L (aL.succSuccAbove bL (σ1L m)) = σ0R (aR.succSuccAbove bR (σ1R m))m:Fin nOut⊢ cast ⋯ (cast ⋯ (p (σ0L (aL.succSuccAbove bL (σ1L m))))) = cast ⋯ (cast ⋯ (p (σ0R (aR.succSuccAbove bR (σ1R m))))) 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 bnP:ℕnOut:ℕmL:ℕmR:ℕc:Fin nP → CcL:Fin (mL + 1 + 1) → CcR:Fin (mR + 1 + 1) → CcOut:Fin nOut → Cp:Pure S cσ0L:Fin (mL + 1 + 1) → Fin nPh0L:IsReindexing c cL σ0LaL:Fin (mL + 1 + 1)bL:Fin (mL + 1 + 1)habL:aL ≠ bLσ1L:Fin nOut → Fin mLh1L:IsReindexing (cL ∘ aL.succSuccAbove bL) cOut σ1Lσ0R:Fin (mR + 1 + 1) → Fin nPh0R:IsReindexing c cR σ0RaR:Fin (mR + 1 + 1)bR:Fin (mR + 1 + 1)habR:aR ≠ bRσ1R:Fin nOut → Fin mRh1R:IsReindexing (cR ∘ aR.succSuccAbove bR) cOut σ1Rhslot:∀ (m : Fin nOut), σ0L (aL.succSuccAbove bL (σ1L m)) = σ0R (aR.succSuccAbove bR (σ1R m))m:Fin nOut⊢ cast ⋯ (p (σ0L (aL.succSuccAbove bL (σ1L m)))) = cast ⋯ (p (σ0R (aR.succSuccAbove bR (σ1R m)))) All goals completed! 🐙

Contraction coefficient

contrPCoeff is insensitive to its proof arguments once the two contracted slots agree. Lets a coefficient comparison rewrite the slots without a congr search through the proof fields.

lemma contrPCoeff_congr {n : ℕ} {c : Fin n → C} (p : Pure S c) {i i' j j' : Fin n} (hi : i = i') (hj : j = j') {hij : i ≠ j ∧ S.τ (c i) = c j} {hij' : i' ≠ j' ∧ S.τ (c i') = c j'} : p.contrPCoeff i j hij = p.contrPCoeff i' j' hij' := 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 → Cp:Pure S ci:Fin ni':Fin nj:Fin nj':Fin nhi:i = i'hj:j = j'hij:i ≠ j ∧ S.τ (c i) = c jhij':i' ≠ j' ∧ S.τ (c i') = c j'⊢ contrPCoeff i j hij p = contrPCoeff i' j' hij' 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 bn:ℕc:Fin n → Cp:Pure S ci:Fin nj:Fin nj':Fin nhj:j = j'hij:i ≠ j ∧ S.τ (c i) = c jhij':i ≠ j' ∧ S.τ (c i) = c j'⊢ contrPCoeff i j hij p = contrPCoeff i j' hij' 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 bn:ℕc:Fin n → Cp:Pure S ci:Fin nj:Fin nhij:i ≠ j ∧ S.τ (c i) = c jhij':i ≠ j ∧ S.τ (c i) = c j⊢ contrPCoeff i j hij p = contrPCoeff i j hij' p All goals completed! 🐙
attribute [-simp] LinearEquiv.cast_apply@[simp] lemma contrPCoeff_permP {n n1 : ℕ} {c : Fin n → C} {c1 : Fin n1 → C} (i j : Fin n1) (hij : i ≠ j ∧ S.τ (c1 i) = c1 j) (σ : Fin n1 → Fin n) (hσ : IsReindexing c c1 σ) (p : Pure S c) : contrPCoeff i j hij (permP σ hσ p) = contrPCoeff (σ i) (σ 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 bn:ℕn1:ℕc:Fin n → Cc1:Fin n1 → Ci:Fin n1j:Fin n1hij:i ≠ j ∧ S.τ (c1 i) = c1 jσ:Fin n1 → Fin nhσ:IsReindexing c c1 σp:Pure S c⊢ σ i ≠ σ j ∧ S.τ (c (σ i)) = c (σ j) All goals completed! 🐙) 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 bn:ℕn1:ℕc:Fin n → Cc1:Fin n1 → Ci:Fin n1j:Fin n1hij:i ≠ j ∧ S.τ (c1 i) = c1 jσ:Fin n1 → Fin nhσ:IsReindexing c c1 σp:Pure S c⊢ contrPCoeff i j hij (permP σ hσ p) = contrPCoeff (σ i) (σ j) ⋯ 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 bn:ℕn1:ℕc:Fin n → Cc1:Fin n1 → Ci:Fin n1j:Fin n1hij:i ≠ j ∧ S.τ (c1 i) = c1 jσ:Fin n1 → Fin nhσ:IsReindexing c c1 σp:Pure S c⊢ (S.contr (c1 i)) ((LinearEquiv.cast ⋯) (p (σ i)) ⊗ₜ[k] (LinearEquiv.cast ⋯) ((LinearEquiv.cast ⋯) (p (σ j)))) = (S.contr (c (σ i))) (p (σ i) ⊗ₜ[k] (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 bn:ℕn1:ℕc:Fin n → Cc1:Fin n1 → Ci:Fin n1j:Fin n1hij:i ≠ j ∧ S.τ (c1 i) = c1 jσ:Fin n1 → Fin nhσ:IsReindexing c c1 σp:Pure S ch1:RingHomInvPair (RingHom.id k) (RingHom.id k)h2:c (σ i) = c1 ih3:c1 j = S.τ (c1 i)h4:c (σ j) = c1 jh5:c (σ j) = S.τ (c (σ i))⊢ (S.contr (c1 i)) ((LinearEquiv.cast h2) (p (σ i)) ⊗ₜ[k] (LinearEquiv.cast h3) ((LinearEquiv.cast h4) (p (σ j)))) = (S.contr (c (σ i))) (p (σ i) ⊗ₜ[k] (LinearEquiv.cast h5) (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 bn:ℕn1:ℕc:Fin n → Cc1:Fin n1 → Ci:Fin n1j:Fin n1hij:i ≠ j ∧ S.τ (c1 i) = c1 jσ:Fin n1 → Fin nhσ:IsReindexing c c1 σp:Pure S ch1:RingHomInvPair (RingHom.id k) (RingHom.id k)h2:c (σ i) = c1 ih3:c1 j = S.τ (c1 i)h4:c (σ j) = c1 jh5:c (σ j) = S.τ (c (σ i))pj:V (c (σ j))⊢ (S.contr (c1 i)) ((LinearEquiv.cast h2) (p (σ i)) ⊗ₜ[k] (LinearEquiv.cast h3) ((LinearEquiv.cast h4) pj)) = (S.contr (c (σ i))) (p (σ i) ⊗ₜ[k] (LinearEquiv.cast h5) pj) 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 → Ci:Fin n1j:Fin n1hij:i ≠ j ∧ S.τ (c1 i) = c1 jσ:Fin n1 → Fin nhσ:IsReindexing c c1 σp:Pure S ch1:RingHomInvPair (RingHom.id k) (RingHom.id k)h2:c (σ i) = c1 ih3:c1 j = S.τ (c1 i)h4:c (σ j) = c1 jh5:c (σ j) = S.τ (c (σ i))pj:V (c (σ j))pi:V (c (σ i))⊢ (S.contr (c1 i)) ((LinearEquiv.cast h2) pi ⊗ₜ[k] (LinearEquiv.cast h3) ((LinearEquiv.cast h4) pj)) = (S.contr (c (σ i))) (pi ⊗ₜ[k] (LinearEquiv.cast h5) pj) 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 → Ci:Fin n1j:Fin n1hij:i ≠ j ∧ S.τ (c1 i) = c1 jσ:Fin n1 → Fin nhσ:IsReindexing c c1 σp:Pure S ch1:RingHomInvPair (RingHom.id k) (RingHom.id k)h2:c (σ i) = c1 ih3:c1 j = S.τ (c1 i)pi:V (c (σ i))cj:Ch4:cj = c1 jh5:cj = S.τ (c (σ i))pj:V cj⊢ (S.contr (c1 i)) ((LinearEquiv.cast h2) pi ⊗ₜ[k] (LinearEquiv.cast h3) ((LinearEquiv.cast h4) pj)) = (S.contr (c (σ i))) (pi ⊗ₜ[k] (LinearEquiv.cast h5) pj) 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 → Ci:Fin n1j:Fin n1hij:i ≠ j ∧ S.τ (c1 i) = c1 jσ:Fin n1 → Fin nhσ:IsReindexing c c1 σp:Pure S ch1:RingHomInvPair (RingHom.id k) (RingHom.id k)h3:c1 j = S.τ (c1 i)cj:Ch4:cj = c1 jpj:V cjci:Ch2:ci = c1 ipi:V cih5:cj = S.τ ci⊢ (S.contr (c1 i)) ((LinearEquiv.cast h2) pi ⊗ₜ[k] (LinearEquiv.cast h3) ((LinearEquiv.cast h4) pj)) = (S.contr ci) (pi ⊗ₜ[k] (LinearEquiv.cast h5) pj) 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 → Ci:Fin n1j:Fin n1hij:i ≠ j ∧ S.τ (c1 i) = c1 jσ:Fin n1 → Fin nhσ:IsReindexing c c1 σp:Pure S ch1:RingHomInvPair (RingHom.id k) (RingHom.id k)h3:c1 j = S.τ (c1 i)cj:Ch4:cj = c1 jpj:V cjpi:V (c1 i)h5:cj = S.τ (c1 i)⊢ (S.contr (c1 i)) ((LinearEquiv.cast ⋯) pi ⊗ₜ[k] (LinearEquiv.cast h3) ((LinearEquiv.cast h4) pj)) = (S.contr (c1 i)) (pi ⊗ₜ[k] (LinearEquiv.cast h5) pj) 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 → Ci:Fin n1j:Fin n1hij:i ≠ j ∧ S.τ (c1 i) = c1 jσ:Fin n1 → Fin nhσ:IsReindexing c c1 σp:Pure S ch1:RingHomInvPair (RingHom.id k) (RingHom.id k)h3:c1 j = S.τ (c1 i)pi:V (c1 i)pj:V (c1 j)h5:c1 j = S.τ (c1 i)⊢ (S.contr (c1 i)) ((LinearEquiv.cast ⋯) pi ⊗ₜ[k] (LinearEquiv.cast h3) ((LinearEquiv.cast ⋯) pj)) = (S.contr (c1 i)) (pi ⊗ₜ[k] (LinearEquiv.cast h5) pj) All goals completed! 🐙@[simp] lemma contrPCoeff_update_succSuccAbove {n : ℕ} [inst : DecidableEq (Fin (n + 1 +1))] {c : Fin (n + 1 + 1) → C} (i j : Fin (n + 1 + 1)) (hij : i ≠ j ∧ S.τ (c i) = c j) (m : Fin n) (p : Pure S c) (x : V (c (succSuccAbove i j m))) : contrPCoeff i j hij (p.update (succSuccAbove i j m) x) = contrPCoeff i j hij 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 bn:ℕinst:DecidableEq (Fin (n + 1 + 1))c:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jm:Fin np:Pure S cx:V (c (i.succSuccAbove j m))⊢ contrPCoeff i j hij (p.update (i.succSuccAbove j m) x) = contrPCoeff i j hij 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 bn:ℕinst:DecidableEq (Fin (n + 1 + 1))c:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jm:Fin np:Pure S cx:V (c (i.succSuccAbove j m))⊢ (S.contr (c i)) (p.update (i.succSuccAbove j m) x i ⊗ₜ[k] (LinearEquiv.cast ⋯) (p.update (i.succSuccAbove j m) x j)) = (S.contr (c i)) (p i ⊗ₜ[k] (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 bn:ℕinst:DecidableEq (Fin (n + 1 + 1))c:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jm:Fin np:Pure S cx:V (c (i.succSuccAbove j m))⊢ p.update (i.succSuccAbove j m) x i = p ik: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:ℕinst:DecidableEq (Fin (n + 1 + 1))c:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jm:Fin np:Pure S cx:V (c (i.succSuccAbove j m))⊢ p.update (i.succSuccAbove j m) x j = 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 bn:ℕinst:DecidableEq (Fin (n + 1 + 1))c:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jm:Fin np:Pure S cx:V (c (i.succSuccAbove j m))⊢ p.update (i.succSuccAbove j m) x i = p 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 bn:ℕinst:DecidableEq (Fin (n + 1 + 1))c:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jm:Fin np:Pure S cx:V (c (i.succSuccAbove j m))⊢ p.update (i.succSuccAbove j m) x j = p 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:ℕinst:DecidableEq (Fin n)c:Fin n → Ci:Fin nj:Fin nhij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cx:V (c i)y:V (c i)⊢ i ≠ jk: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:ℕinst:DecidableEq (Fin n)c:Fin n → Ci:Fin nj:Fin nhij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cx:V (c i)y:V (c i)⊢ i ≠ jk: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:ℕinst:DecidableEq (Fin n)c:Fin n → Ci:Fin nj:Fin nhij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cx:V (c i)y:V (c i)⊢ i ≠ j all_goals 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:ℕinst:DecidableEq (Fin n)c:Fin n → Ci:Fin nj:Fin nhij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cx:V (c j)y:V (c j)⊢ j ≠ ik: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:ℕinst:DecidableEq (Fin n)c:Fin n → Ci:Fin nj:Fin nhij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cx:V (c j)y:V (c j)⊢ j ≠ ik: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:ℕinst:DecidableEq (Fin n)c:Fin n → Ci:Fin nj:Fin nhij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cx:V (c j)y:V (c j)⊢ j ≠ i all_goals 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:ℕinst:DecidableEq (Fin n)c:Fin n → Ci:Fin nj:Fin nhij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cr:kx:V (c i)⊢ (S.contr (c i)) (x ⊗ₜ[k] (r • (LinearEquiv.cast ⋯) (p j))) = r * (S.contr (c i)) (x ⊗ₜ[k] (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 bn:ℕinst:DecidableEq (Fin n)c:Fin n → Ci:Fin nj:Fin nhij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cr:kx:V (c i)⊢ i ≠ jk: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:ℕinst:DecidableEq (Fin n)c:Fin n → Ci:Fin nj:Fin nhij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cr:kx:V (c i)⊢ i ≠ 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 bn:ℕinst:DecidableEq (Fin n)c:Fin n → Ci:Fin nj:Fin nhij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cr:kx:V (c i)⊢ i ≠ jk: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:ℕinst:DecidableEq (Fin n)c:Fin n → Ci:Fin nj:Fin nhij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cr:kx:V (c i)⊢ i ≠ j all_goals 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:ℕinst:DecidableEq (Fin n)c:Fin n → Ci:Fin nj:Fin nhij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cr:kx:V (c j)⊢ r • (S.contr (c i)) (p i ⊗ₜ[k] (LinearEquiv.cast ⋯) x) = r * (S.contr (c i)) (p i ⊗ₜ[k] (LinearEquiv.cast ⋯) 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:ℕinst:DecidableEq (Fin n)c:Fin n → Ci:Fin nj:Fin nhij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cr:kx:V (c j)⊢ j ≠ ik: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:ℕinst:DecidableEq (Fin n)c:Fin n → Ci:Fin nj:Fin nhij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cr:kx:V (c j)⊢ j ≠ 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:ℕinst:DecidableEq (Fin n)c:Fin n → Ci:Fin nj:Fin nhij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cr:kx:V (c j)⊢ j ≠ ik: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:ℕinst:DecidableEq (Fin n)c:Fin n → Ci:Fin nj:Fin nhij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cr:kx:V (c j)⊢ j ≠ i all_goals All goals completed! 🐙lemma contrPCoeff_dropPair {n : ℕ} {c : Fin (n + 1 + 1) → C} (a b : Fin (n + 1 + 1)) (hab : a ≠ b) (i j : Fin n) (hij : i ≠ j ∧ S.τ (c (succSuccAbove a b i)) = (c (succSuccAbove a b j))) (p : Pure S c) : (p.dropPair a b hab).contrPCoeff i j hij = p.contrPCoeff (succSuccAbove a b i) (succSuccAbove a b 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 b✝n:ℕc:Fin (n + 1 + 1) → Ca:Fin (n + 1 + 1)b:Fin (n + 1 + 1)hab:a ≠ bi:Fin nj:Fin nhij:i ≠ j ∧ S.τ (c (a.succSuccAbove b i)) = c (a.succSuccAbove b j)p:Pure S c⊢ a.succSuccAbove b i ≠ a.succSuccAbove b j ∧ S.τ (c (a.succSuccAbove b i)) = c (a.succSuccAbove b 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 b✝n:ℕc:Fin (n + 1 + 1) → Ca:Fin (n + 1 + 1)b:Fin (n + 1 + 1)hab:a ≠ bi:Fin nj:Fin nhij:i ≠ j ∧ S.τ (c (a.succSuccAbove b i)) = c (a.succSuccAbove b j)p:Pure S c⊢ contrPCoeff i j hij (dropPair a b hab p) = contrPCoeff (a.succSuccAbove b i) (a.succSuccAbove b j) ⋯ 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 bn:ℕc:Fin n → Ci:Fin nj:Fin nhij:i ≠ j ∧ S.τ (c i) = c jp:Pure S c⊢ (S.contr (S.τ (c i))) ((LinearEquiv.cast ⋯) (p j) ⊗ₜ[k] (Equiv.cast ⋯) (p i)) = (S.contr (c j)) (p j ⊗ₜ[k] (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 bn:ℕc:Fin n → Ci:Fin nj:Fin nhij:i ≠ j ∧ S.τ (c i) = c jp:Pure S ch1:RingHomInvPair (RingHom.id k) (RingHom.id k)h2:c j = S.τ (c i)h3:V (c i) = V (S.τ (S.τ (c i)))h4:c i = S.τ (c j)⊢ (S.contr (S.τ (c i))) ((LinearEquiv.cast h2) (p j) ⊗ₜ[k] (Equiv.cast h3) (p i)) = (S.contr (c j)) (p j ⊗ₜ[k] (LinearEquiv.cast h4) (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 bn:ℕc:Fin n → Ci:Fin nj:Fin nhij:i ≠ j ∧ S.τ (c i) = c jp:Pure S ch1:RingHomInvPair (RingHom.id k) (RingHom.id k)h2:c j = S.τ (c i)h3:V (c i) = V (S.τ (S.τ (c i)))h4:c i = S.τ (c j)pj:V (c j)⊢ (S.contr (S.τ (c i))) ((LinearEquiv.cast h2) pj ⊗ₜ[k] (Equiv.cast h3) (p i)) = (S.contr (c j)) (pj ⊗ₜ[k] (LinearEquiv.cast h4) (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 bn:ℕc:Fin n → Ci:Fin nj:Fin nhij:i ≠ j ∧ S.τ (c i) = c jp:Pure S ch1:RingHomInvPair (RingHom.id k) (RingHom.id k)h2:c j = S.τ (c i)h3:V (c i) = V (S.τ (S.τ (c i)))h4:c i = S.τ (c j)pj:V (c j)pi:V (c i)⊢ (S.contr (S.τ (c i))) ((LinearEquiv.cast h2) pj ⊗ₜ[k] (Equiv.cast h3) pi) = (S.contr (c j)) (pj ⊗ₜ[k] (LinearEquiv.cast h4) pi) 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 → Ci:Fin nj:Fin np:Pure S ch1:RingHomInvPair (RingHom.id k) (RingHom.id k)h3:V (c i) = V (S.τ (S.τ (c i)))pi:V (c i)cj:Chij:i ≠ j ∧ S.τ (c i) = cjh2:cj = S.τ (c i)h4:c i = S.τ cjpj:V cj⊢ (S.contr (S.τ (c i))) ((LinearEquiv.cast h2) pj ⊗ₜ[k] (Equiv.cast h3) pi) = (S.contr cj) (pj ⊗ₜ[k] (LinearEquiv.cast h4) pi) 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 → Ci:Fin nj:Fin np:Pure S ch1:RingHomInvPair (RingHom.id k) (RingHom.id k)cj:Cpj:V cjci:Ch3:V ci = V (S.τ (S.τ ci))pi:V cihij:i ≠ j ∧ S.τ ci = cjh2:cj = S.τ cih4:ci = S.τ cj⊢ (S.contr (S.τ ci)) ((LinearEquiv.cast h2) pj ⊗ₜ[k] (Equiv.cast h3) pi) = (S.contr cj) (pj ⊗ₜ[k] (LinearEquiv.cast h4) pi) 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 → Ci:Fin nj:Fin np:Pure S ch1:RingHomInvPair (RingHom.id k) (RingHom.id k)ci:Ch3:V ci = V (S.τ (S.τ ci))pi:V cipj:V (S.τ ci)hij:i ≠ j ∧ S.τ ci = S.τ cih4:ci = S.τ (S.τ ci)⊢ (S.contr (S.τ ci)) ((LinearEquiv.cast ⋯) pj ⊗ₜ[k] (Equiv.cast h3) pi) = (S.contr (S.τ ci)) (pj ⊗ₜ[k] (LinearEquiv.cast h4) pi) All goals completed! 🐙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 → Ci:Fin nj:Fin np:Pure S cg:Gh1:RingHomInvPair (RingHom.id k) (RingHom.id k)pj:V (c j)ci:Chij:i ≠ j ∧ S.τ ci = c jh2:c j = S.τ cipi:V cipj':V (S.τ ci)⊢ ((Representation.trivial k G k) g) ((S.contr ci) (pi ⊗ₜ[k] pj')) = (S.contr ci) (pi ⊗ₜ[k] pj') All goals completed! 🐙

Contractions

set_option backward.isDefEq.respectTransparency false in @[simp] lemma contrP_update_add {n : ℕ} [inst : DecidableEq (Fin (n + 1 +1))] {c : Fin (n + 1 + 1) → C} (i j m : Fin (n + 1 + 1)) (hij : i ≠ j ∧ S.τ (c i) = c j) (p : Pure S c) (x y : V (c m)) : contrP i j hij (p.update m (x + y)) = contrP i j hij (p.update m x) + contrP i j hij (p.update m 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) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕinst:DecidableEq (Fin (n + 1 + 1))c:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)m:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cx:V (c m)y:V (c m)⊢ contrP i j hij (p.update m (x + y)) = contrP i j hij (p.update m x) + contrP i j hij (p.update m 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) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕinst:DecidableEq (Fin (n + 1 + 1))c:Fin (n + 1 + 1) → Cj:Fin (n + 1 + 1)m:Fin (n + 1 + 1)p:Pure S cx:V (c m)y:V (c m)hij:m ≠ j ∧ S.τ (c m) = c j⊢ contrP m j hij (p.update m (x + y)) = contrP m j hij (p.update m x) + contrP m j hij (p.update m 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) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕinst:DecidableEq (Fin (n + 1 + 1))c:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)m:Fin (n + 1 + 1)p:Pure S cx:V (c m)y:V (c m)hij:i ≠ m ∧ S.τ (c i) = c m⊢ contrP i m hij (p.update m (x + y)) = contrP i m hij (p.update m x) + contrP i m hij (p.update m 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) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕinst:DecidableEq (Fin (n + 1 + 1))c:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cm':Fin nx:V (c (i.succSuccAbove j m'))y:V (c (i.succSuccAbove j m'))⊢ contrP i j hij (p.update (i.succSuccAbove j m') (x + y)) = contrP i j hij (p.update (i.succSuccAbove j m') x) + contrP i j hij (p.update (i.succSuccAbove j m') 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) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕinst:DecidableEq (Fin (n + 1 + 1))c:Fin (n + 1 + 1) → Cj:Fin (n + 1 + 1)m:Fin (n + 1 + 1)p:Pure S cx:V (c m)y:V (c m)hij:m ≠ j ∧ S.τ (c m) = c j⊢ contrP m j hij (p.update m (x + y)) = contrP m j hij (p.update m x) + contrP m j hij (p.update m y) 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:ℕinst:DecidableEq (Fin (n + 1 + 1))c:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)m:Fin (n + 1 + 1)p:Pure S cx:V (c m)y:V (c m)hij:i ≠ m ∧ S.τ (c i) = c m⊢ contrP i m hij (p.update m (x + y)) = contrP i m hij (p.update m x) + contrP i m hij (p.update m y) 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:ℕinst:DecidableEq (Fin (n + 1 + 1))c:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cm':Fin nx:V (c (i.succSuccAbove j m'))y:V (c (i.succSuccAbove j m'))⊢ contrP i j hij (p.update (i.succSuccAbove j m') (x + y)) = contrP i j hij (p.update (i.succSuccAbove j m') x) + contrP i j hij (p.update (i.succSuccAbove j m') y) All goals completed! 🐙set_option backward.isDefEq.respectTransparency false in @[simp] lemma contrP_update_smul {n : ℕ} [inst : DecidableEq (Fin (n + 1 +1))] {c : Fin (n + 1 + 1) → C} (i j m : Fin (n + 1 + 1)) (hij : i ≠ j ∧ S.τ (c i) = c j) (p : Pure S c) (r : k) (x : V (c m)) : contrP i j hij (p.update m (r • x)) = r • contrP i j hij (p.update 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:ℕinst:DecidableEq (Fin (n + 1 + 1))c:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)m:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cr:kx:V (c m)⊢ contrP i j hij (p.update m (r • x)) = r • contrP i j hij (p.update 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:ℕinst:DecidableEq (Fin (n + 1 + 1))c:Fin (n + 1 + 1) → Cj:Fin (n + 1 + 1)m:Fin (n + 1 + 1)p:Pure S cr:kx:V (c m)hij:m ≠ j ∧ S.τ (c m) = c j⊢ contrP m j hij (p.update m (r • x)) = r • contrP m j hij (p.update 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:ℕinst:DecidableEq (Fin (n + 1 + 1))c:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)m:Fin (n + 1 + 1)p:Pure S cr:kx:V (c m)hij:i ≠ m ∧ S.τ (c i) = c m⊢ contrP i m hij (p.update m (r • x)) = r • contrP i m hij (p.update 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:ℕinst:DecidableEq (Fin (n + 1 + 1))c:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cr:km':Fin nx:V (c (i.succSuccAbove j m'))⊢ contrP i j hij (p.update (i.succSuccAbove j m') (r • x)) = r • contrP i j hij (p.update (i.succSuccAbove j 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:ℕinst:DecidableEq (Fin (n + 1 + 1))c:Fin (n + 1 + 1) → Cj:Fin (n + 1 + 1)m:Fin (n + 1 + 1)p:Pure S cr:kx:V (c m)hij:m ≠ j ∧ S.τ (c m) = c j⊢ contrP m j hij (p.update m (r • x)) = r • contrP m j hij (p.update 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:ℕinst:DecidableEq (Fin (n + 1 + 1))c:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)m:Fin (n + 1 + 1)p:Pure S cr:kx:V (c m)hij:i ≠ m ∧ S.τ (c i) = c m⊢ contrP i m hij (p.update m (r • x)) = r • contrP i m hij (p.update 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:ℕinst:DecidableEq (Fin (n + 1 + 1))c:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cr:km':Fin nx:V (c (i.succSuccAbove j m'))⊢ contrP i j hij (p.update (i.succSuccAbove j m') (r • x)) = r • contrP i j hij (p.update (i.succSuccAbove j m') x) All goals completed! 🐙@[simp] lemma contrP_equivariant {n : ℕ} {c : Fin (n + 1 + 1) → C} (i j : Fin (n + 1 + 1)) (hij : i ≠ j ∧ S.τ (c i) = c j) (p : Pure S c) (g : G) : contrP i j hij (g • p) = g • contrP i j hij 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 bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cg:G⊢ contrP i j hij (g • p) = g • contrP i j hij 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 bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S c⊢ contrPCoeff j i ⋯ p • (permP id ⋯ (dropPair j i ⋯ p)).toTensor = (permT id ⋯) (contrP j i ⋯ p) All goals completed! 🐙

contrP as a multilinear map