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

Constructors of tensors.

There are a number of ways to construct explicit tensors.

@[expose] public sectionattribute [-simp] LinearEquiv.cast_apply

Tensors with a single index.

lemma fromSingleT_symm_pure {c : C} (p : Pure S ![c]) : fromSingleT.symm p.toTensor = Pure.fromSingleP.symm p := PiTensorProduct.subsingletonEquiv_apply_tprod 0 pk:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cx:V c⊢ fromSingleT.symm (fromSingleT x) = Pure.fromSingleP.symm (Pure.fromSingleP x) All goals completed! 🐙k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cx:V cg:G⊢ (g • fun x_1 => match x_1 with | 0 => x).toTensor = Pure.toTensor fun x_1 => match x_1 with | 0 => ((rep c) g) x k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cx:V cg:G⊢ (g • fun x_1 => match x_1 with | 0 => x) = fun x_1 => match x_1 with | 0 => ((rep c) g) x k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cx✝:V cg:Gx:Fin (Nat.succ 0)⊢ (g • fun x => match x with | 0 => x✝) x = match x with | 0 => ((rep c) g) x✝ k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cx:V cg:G⊢ (g • fun x_1 => match x_1 with | 0 => x) ((fun i => i) ⟨0, ⋯⟩) = match (fun i => i) ⟨0, ⋯⟩ with | 0 => ((rep c) g) x All goals completed! 🐙k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Ch:c = c1x:V c⊢ (Pure.toTensor fun x_1 => match x_1 with | 0 => (LinearEquiv.cast h) x) = (Pure.permP id ⋯ fun x_1 => match x_1 with | 0 => x).toTensor k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Ch:c = c1x:V c⊢ (fun x_1 => match x_1 with | 0 => (LinearEquiv.cast h) x) = Pure.permP id ⋯ fun x_1 => match x_1 with | 0 => x k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Ch:c = c1x:V ci:Fin (Nat.succ 0)⊢ (match i with | 0 => (LinearEquiv.cast h) x) = Pure.permP id ⋯ (fun x_1 => match x_1 with | 0 => x) i k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Ch:c = c1x:V c⊢ (match (fun i => i) ⟨0, ⋯⟩ with | 0 => (LinearEquiv.cast h) x) = Pure.permP id ⋯ (fun x_1 => match x_1 with | 0 => x) ((fun i => i) ⟨0, ⋯⟩) All goals completed! 🐙k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cx:V cy:V (S.τ c)⊢ (S.contr (Fin.append ![c] ![S.τ c] 0)) (Pure.prodP (fun x_1 => match x_1 with | 0 => x) (fun x => match x with | 0 => y) 0 ⊗ₜ[k] (LinearEquiv.cast ⋯) (Pure.prodP (fun x_1 => match x_1 with | 0 => x) (fun x => match x with | 0 => y) 1)) • (Pure.dropPair 0 1 ⋯ (Pure.prodP (fun x_1 => match x_1 with | 0 => x) fun x => match x with | 0 => y)).toTensor = (S.contr c) (x ⊗ₜ[k] y) • default.toTensor k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cx:V cy:V (S.τ c)⊢ (Pure.dropPair 0 1 ⋯ (Pure.prodP (fun x_1 => match x_1 with | 0 => x) fun x => match x with | 0 => y)).toTensor = default.toTensor k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cx:V cy:V (S.τ c)⊢ (Pure.dropPair 0 1 ⋯ (Pure.prodP (fun x_1 => match x_1 with | 0 => x) fun x => match x with | 0 => y)).toTensor = default.toTensor k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cx:V cy:V (S.τ c)⊢ Pure.dropPair 0 1 ⋯ (Pure.prodP (fun x_1 => match x_1 with | 0 => x) fun x => match x with | 0 => y) = default k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cx:V cy:V (S.τ c)i:Fin 0⊢ Pure.dropPair 0 1 ⋯ (Pure.prodP (fun x_1 => match x_1 with | 0 => x) fun x => match x with | 0 => y) i = default i All goals completed! 🐙

Tensors with two indices.

fromPairT

lemma fromPairT_tmul {c1 c2 : C} (x : V c1) (y : V c2) : fromPairT (x ⊗ₜ[k] y) = permT id (And.intro Function.bijective_id (fun i => k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc1:Cc2:Cx:V c1y:V c2i:Fin (Nat.succ 0 + Nat.succ 0)⊢ Fin.append ![c1] ![c2] (id i) = ![c1, c2] i k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc1:Cc2:Cx:V c1y:V c2⊢ Fin.append ![c1] ![c2] (id ((fun i => i) ⟨0, ⋯⟩)) = ![c1, c2] ((fun i => i) ⟨0, ⋯⟩)k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc1:Cc2:Cx:V c1y:V c2⊢ Fin.append ![c1] ![c2] (id ((fun i => i) ⟨1, ⋯⟩)) = ![c1, c2] ((fun i => i) ⟨1, ⋯⟩) k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc1:Cc2:Cx:V c1y:V c2⊢ Fin.append ![c1] ![c2] (id ((fun i => i) ⟨0, ⋯⟩)) = ![c1, c2] ((fun i => i) ⟨0, ⋯⟩)k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc1:Cc2:Cx:V c1y:V c2⊢ Fin.append ![c1] ![c2] (id ((fun i => i) ⟨1, ⋯⟩)) = ![c1, c2] ((fun i => i) ⟨1, ⋯⟩) All goals completed! 🐙)) (prodT (fromSingleT (S := S) x) (fromSingleT y)) := k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc1:Cc2:Cx:V c1y:V c2⊢ fromPairT (x ⊗ₜ[k] y) = (permT id ⋯) ((prodT (fromSingleT x)) (fromSingleT y)) All goals completed! 🐙k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc1:Cc2:Cx:V c1y:V c2⊢ (Pure.permP id ⋯ (Pure.prodP (fun x_1 => match x_1 with | 0 => x) fun x => match x with | 0 => y)).toTensor = Pure.toTensor fun x_1 => match x_1 with | 0 => x | 1 => y k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc1:Cc2:Cx:V c1y:V c2⊢ Pure.permP id ⋯ (Pure.prodP (fun x_1 => match x_1 with | 0 => x) fun x => match x with | 0 => y) = fun x_1 => match x_1 with | 0 => x | 1 => y k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc1:Cc2:Cx:V c1y:V c2i:Fin (Nat.succ 0 + Nat.succ 0)⊢ Pure.permP id ⋯ (Pure.prodP (fun x_1 => match x_1 with | 0 => x) fun x => match x with | 0 => y) i = match i with | 0 => x | 1 => y k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc1:Cc2:Cx:V c1y:V c2⊢ Pure.permP id ⋯ (Pure.prodP (fun x_1 => match x_1 with | 0 => x) fun x => match x with | 0 => y) ((fun i => i) ⟨0, ⋯⟩) = match (fun i => i) ⟨0, ⋯⟩ with | 0 => x | 1 => yk:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc1:Cc2:Cx:V c1y:V c2⊢ Pure.permP id ⋯ (Pure.prodP (fun x_1 => match x_1 with | 0 => x) fun x => match x with | 0 => y) ((fun i => i) ⟨1, ⋯⟩) = match (fun i => i) ⟨1, ⋯⟩ with | 0 => x | 1 => y k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc1:Cc2:Cx:V c1y:V c2⊢ Pure.permP id ⋯ (Pure.prodP (fun x_1 => match x_1 with | 0 => x) fun x => match x with | 0 => y) ((fun i => i) ⟨0, ⋯⟩) = match (fun i => i) ⟨0, ⋯⟩ with | 0 => x | 1 => yk:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc1:Cc2:Cx:V c1y:V c2⊢ Pure.permP id ⋯ (Pure.prodP (fun x_1 => match x_1 with | 0 => x) fun x => match x with | 0 => y) ((fun i => i) ⟨1, ⋯⟩) = match (fun i => i) ⟨1, ⋯⟩ with | 0 => x | 1 => y All goals completed! 🐙k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc1:Cc2:Cg:Gx:V c1y:V c2⊢ (permT id ⋯) ((prodT (fromSingleT (((rep c1) g) x))) (fromSingleT (((rep c2) g) y))) = fromPairT (((rep c1) g) x ⊗ₜ[k] ((rep c2) g) y) All goals completed! 🐙 k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc1:Cc2:Cg:Gx:V c1 ⊗[k] V c2y:V c1 ⊗[k] V c2hx:g • fromPairT x = fromPairT ((map ((rep c1) g) ((rep c2) g)) x)hy:g • fromPairT y = fromPairT ((map ((rep c1) g) ((rep c2) g)) y)⊢ g • fromPairT (x + y) = fromPairT ((map ((rep c1) g) ((rep c2) g)) (x + y)) All goals completed! 🐙k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc1:Cc2:Cc2':Ch:c2 = c2'x:V c1y:V c2⊢ (permT (Fin.append (Fin.castAdd (Nat.succ 0)) (Fin.natAdd 1 ∘ id) ∘ id) ⋯) ((prodT (fromSingleT x)) (fromSingleT y)) = (permT id ⋯) ((prodT (fromSingleT x)) (fromSingleT y)) k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc1:Cc2:Cc2':Ch:c2 = c2'x:V c1y:V c2⊢ (permT (Fin.append (Fin.castAdd 1) (Fin.natAdd 1)) ⋯) ((prodT (fromSingleT x)) (fromSingleT y)) = (permT id ⋯) ((prodT (fromSingleT x)) (fromSingleT y)) k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc1:Cc2:Cc2':Ch:c2 = c2'x:V c1y:V c2⊢ Fin.append (Fin.castAdd 1) (Fin.natAdd 1) = id All goals completed! 🐙 k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc1:Cc2:Cc2':Ch:c2 = c2'x1:V c1 ⊗[k] V c2x2:V c1 ⊗[k] V c2h1:fromPairT ((map LinearMap.id ↑(LinearEquiv.cast h)) x1) = (permT id ⋯) (fromPairT x1)h2:fromPairT ((map LinearMap.id ↑(LinearEquiv.cast h)) x2) = (permT id ⋯) (fromPairT x2)⊢ fromPairT ((map LinearMap.id ↑(LinearEquiv.cast h)) (x1 + x2)) = (permT id ⋯) (fromPairT (x1 + x2)) All goals completed! 🐙k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc1:Cc2:Cx:V c1y:V c2⊢ (permT id ⋯) ((permT (Fin.append (Fin.natAdd (Nat.succ 0)) (Fin.castAdd (Nat.succ 0))) ⋯) ((prodT (fromSingleT x)) (fromSingleT y))) = (permT ![1, 0] ⋯) ((permT id ⋯) ((prodT (fromSingleT x)) (fromSingleT y))) k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc1:Cc2:Cx:V c1y:V c2⊢ (permT (Fin.append (Fin.natAdd 1) (Fin.castAdd 1)) ⋯) ((prodT (fromSingleT x)) (fromSingleT y)) = (permT ![1, 0] ⋯) ((prodT (fromSingleT x)) (fromSingleT y)) k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc1:Cc2:Cx:V c1y:V c2⊢ Fin.append (Fin.natAdd 1) (Fin.castAdd 1) = ![1, 0] k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc1:Cc2:Cx:V c1y:V c2i:Fin (1 + 1)⊢ ↑(Fin.append (Fin.natAdd 1) (Fin.castAdd 1) i) = ↑(![1, 0] i) k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc1:Cc2:Cx:V c1y:V c2⊢ ↑(Fin.append (Fin.natAdd 1) (Fin.castAdd 1) ((fun i => i) ⟨0, ⋯⟩)) = ↑(![1, 0] ((fun i => i) ⟨0, ⋯⟩))k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc1:Cc2:Cx:V c1y:V c2⊢ ↑(Fin.append (Fin.natAdd 1) (Fin.castAdd 1) ((fun i => i) ⟨1, ⋯⟩)) = ↑(![1, 0] ((fun i => i) ⟨1, ⋯⟩)) k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc1:Cc2:Cx:V c1y:V c2⊢ ↑(Fin.append (Fin.natAdd 1) (Fin.castAdd 1) ((fun i => i) ⟨0, ⋯⟩)) = ↑(![1, 0] ((fun i => i) ⟨0, ⋯⟩))k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc1:Cc2:Cx:V c1y:V c2⊢ ↑(Fin.append (Fin.natAdd 1) (Fin.castAdd 1) ((fun i => i) ⟨1, ⋯⟩)) = ↑(![1, 0] ((fun i => i) ⟨1, ⋯⟩)) All goals completed! 🐙 k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc1:Cc2:Cx:V c1 ⊗[k] V c2y:V c1 ⊗[k] V c2hx:fromPairT ((TensorProduct.comm k (V c1) (V c2)) x) = (permT ![1, 0] ⋯) (fromPairT x)hy:fromPairT ((TensorProduct.comm k (V c1) (V c2)) y) = (permT ![1, 0] ⋯) (fromPairT y)⊢ fromPairT ((TensorProduct.comm k (V c1) (V c2)) (x + y)) = (permT ![1, 0] ⋯) (fromPairT (x + y)) All goals completed! 🐙

Contraction of fromPairT with fromSingleT

lemma fromSingleTContrFromPairT_tmul {c c2 : C} (x : V c) (y1 : V (S.τ c)) (y2 : V c2) : fromSingleTContrFromPairT x (y1 ⊗ₜ[k] y2) = S.contr c (x ⊗ₜ[k] y1) • fromSingleT y2 := k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc2:Cx:V cy1:V (S.τ c)y2:V c2⊢ fromSingleTContrFromPairT x (y1 ⊗ₜ[k] y2) = (S.contr c) (x ⊗ₜ[k] y1) • fromSingleT y2 All goals completed! 🐙k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc2:Cx:V cy1:V (S.τ c)y2:V c2⊢ (permT (Fin.append (Fin.natAdd 1) (Fin.castAdd 0) ∘ id) ⋯) ((prodT (fromSingleT y2)) default.toTensor) = (permT id ⋯) (fromSingleT y2) k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc2:Cx:V cy1:V (S.τ c)y2:V c2⊢ (permT (Fin.append (Fin.natAdd 1) (Fin.castAdd 0)) ⋯) (fromSingleT y2) = (permT id ⋯) (fromSingleT y2) k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc2:Cx:V cy1:V (S.τ c)y2:V c2⊢ Fin.append (Fin.natAdd 1) (Fin.castAdd 0) = id k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc2:Cx:V cy1:V (S.τ c)y2:V c2i:Fin (0 + 1)⊢ ↑(Fin.append (Fin.natAdd 1) (Fin.castAdd 0) i) = ↑(id i) All goals completed! 🐙All goals completed! 🐙

Contraction of fromPairT with fromPairT

lemma fromPairTContr_tmul_tmul {c c1 c2 : C} (x1 : V c1) (x2 : V c) (y1 : V (S.τ c)) (y2 : V c2) : fromPairTContr (x1 ⊗ₜ[k] x2) (y1 ⊗ₜ[k] y2) = (S.contr c) (x2 ⊗ₜ[k] y1) • fromPairT (x1 ⊗ₜ[k] y2) := k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cc2:Cx1:V c1x2:V cy1:V (S.τ c)y2:V c2⊢ fromPairTContr (x1 ⊗ₜ[k] x2) (y1 ⊗ₜ[k] y2) = (S.contr c) (x2 ⊗ₜ[k] y1) • fromPairT (x1 ⊗ₜ[k] y2) All goals completed! 🐙lemma fromPairT_contr_fromPairT_eq_fromPairTContr_tmul (c c1 c2 : C) (x1 : V c1) (x2 : V c) (y1 : V (S.τ c)) (y2 : V c2) : contrT 2 1 2 (k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cc2:Cx1:V c1x2:V cy1:V (S.τ c)y2:V c2⊢ 1 ≠ 2 ∧ S.τ (Fin.append ![c1, c] ![S.τ c, c2] 1) = Fin.append ![c1, c] ![S.τ c, c2] 2 k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cc2:Cx1:V c1x2:V cy1:V (S.τ c)y2:V c2⊢ S.τ (Fin.append ![c1, c] ![S.τ c, c2] 1) = Fin.append ![c1, c] ![S.τ c, c2] 2; All goals completed! 🐙) (prodT (fromPairT (x1 ⊗ₜ[k] x2)) (fromPairT (y1 ⊗ₜ[k] y2))) = permT id (k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cc2:Cx1:V c1x2:V cy1:V (S.τ c)y2:V c2⊢ IsReindexing ![c1, c2] (Fin.append ![c1, c] ![S.τ c, c2] ∘ Fin.succSuccAbove 1 2) id k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cc2:Cx1:V c1x2:V cy1:V (S.τ c)y2:V c2⊢ c1 = Fin.append ![c1, c] ![S.τ c, c2] (Fin.succSuccAbove 1 2 0) ∧ c2 = Fin.append ![c1, c] ![S.τ c, c2] (Fin.succSuccAbove 1 2 1); All goals completed! 🐙) (fromPairTContr (x1 ⊗ₜ[k] x2) (y1 ⊗ₜ[k] y2)) := k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cc2:Cx1:V c1x2:V cy1:V (S.τ c)y2:V c2⊢ (contrT 2 1 2 ⋯) ((prodT (fromPairT (x1 ⊗ₜ[k] x2))) (fromPairT (y1 ⊗ₜ[k] y2))) = (permT id ⋯) (fromPairTContr (x1 ⊗ₜ[k] x2) (y1 ⊗ₜ[k] y2)) k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cc2:Cx1:V c1x2:V cy1:V (S.τ c)y2:V c2⊢ Pure.contrPCoeff 1 2 ⋯ (Pure.prodP (fun x => match x with | 0 => x1 | 1 => x2) fun x => match x with | 0 => y1 | 1 => y2) • (Pure.dropPair 1 2 ⋯ (Pure.prodP (fun x => match x with | 0 => x1 | 1 => x2) fun x => match x with | 0 => y1 | 1 => y2)).toTensor = (S.contr c) (x2 ⊗ₜ[k] y1) • (Pure.permP id ⋯ fun x => match x with | 0 => x1 | 1 => y2).toTensor k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cc2:Cx1:V c1x2:V cy1:V (S.τ c)y2:V c2⊢ Pure.dropPair 1 2 ⋯ (Pure.prodP (fun x => match x with | 0 => x1 | 1 => x2) fun x => match x with | 0 => y1 | 1 => y2) = Pure.permP id ⋯ fun x => match x with | 0 => x1 | 1 => y2 k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cc2:Cx1:V c1x2:V cy1:V (S.τ c)y2:V c2i:Fin 2⊢ Pure.dropPair 1 2 ⋯ (Pure.prodP (fun x => match x with | 0 => x1 | 1 => x2) fun x => match x with | 0 => y1 | 1 => y2) i = Pure.permP id ⋯ (fun x => match x with | 0 => x1 | 1 => y2) i k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cc2:Cx1:V c1x2:V cy1:V (S.τ c)y2:V c2⊢ Pure.dropPair 1 2 ⋯ (Pure.prodP (fun x => match x with | 0 => x1 | 1 => x2) fun x => match x with | 0 => y1 | 1 => y2) ((fun i => i) ⟨0, ⋯⟩) = Pure.permP id ⋯ (fun x => match x with | 0 => x1 | 1 => y2) ((fun i => i) ⟨0, ⋯⟩)k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cc2:Cx1:V c1x2:V cy1:V (S.τ c)y2:V c2⊢ Pure.dropPair 1 2 ⋯ (Pure.prodP (fun x => match x with | 0 => x1 | 1 => x2) fun x => match x with | 0 => y1 | 1 => y2) ((fun i => i) ⟨1, ⋯⟩) = Pure.permP id ⋯ (fun x => match x with | 0 => x1 | 1 => y2) ((fun i => i) ⟨1, ⋯⟩) k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cc2:Cx1:V c1x2:V cy1:V (S.τ c)y2:V c2⊢ Pure.dropPair 1 2 ⋯ (Pure.prodP (fun x => match x with | 0 => x1 | 1 => x2) fun x => match x with | 0 => y1 | 1 => y2) ((fun i => i) ⟨0, ⋯⟩) = Pure.permP id ⋯ (fun x => match x with | 0 => x1 | 1 => y2) ((fun i => i) ⟨0, ⋯⟩)k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cc2:Cx1:V c1x2:V cy1:V (S.τ c)y2:V c2⊢ Pure.dropPair 1 2 ⋯ (Pure.prodP (fun x => match x with | 0 => x1 | 1 => x2) fun x => match x with | 0 => y1 | 1 => y2) ((fun i => i) ⟨1, ⋯⟩) = Pure.permP id ⋯ (fun x => match x with | 0 => x1 | 1 => y2) ((fun i => i) ⟨1, ⋯⟩) All goals completed! 🐙k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cc2:Cy:V (S.τ c) ⊗[k] V c2a:V c1 ⊗[k] V cb:V c1 ⊗[k] V cha:(contrT 2 1 2 ⋯) ((prodT (fromPairT a)) (fromPairT y)) = (permT id ⋯) (fromPairT ((LinearEquiv.lTensor (V c1) (TensorProduct.lid k (V c2))) ((LinearMap.lTensor (V c1) (LinearMap.rTensor (V c2) (S.contr c).toLinearMap)) ((LinearEquiv.lTensor (V c1) (TensorProduct.assoc k (V c) (V (S.τ c)) (V c2)).symm) ((TensorProduct.assoc k (V c1) (V c) (V (S.τ c) ⊗[k] V c2)) (a ⊗ₜ[k] y))))))hb:(contrT 2 1 2 ⋯) ((prodT (fromPairT b)) (fromPairT y)) = (permT id ⋯) (fromPairT ((LinearEquiv.lTensor (V c1) (TensorProduct.lid k (V c2))) ((LinearMap.lTensor (V c1) (LinearMap.rTensor (V c2) (S.contr c).toLinearMap)) ((LinearEquiv.lTensor (V c1) (TensorProduct.assoc k (V c) (V (S.τ c)) (V c2)).symm) ((TensorProduct.assoc k (V c1) (V c) (V (S.τ c) ⊗[k] V c2)) (b ⊗ₜ[k] y))))))⊢ (contrT 2 1 2 ⋯) ((prodT (fromPairT a) + prodT (fromPairT b)) (fromPairT y)) = (contrT 2 1 2 ⋯) ((prodT (fromPairT a)) (fromPairT y)) + (contrT 2 1 2 ⋯) ((prodT (fromPairT b)) (fromPairT y)) All goals completed! 🐙k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cφ:ComponentIdx ![c, c1]x:V cy:V c1⊢ ((b c1).repr (Pure.permP id ⋯ (Pure.prodP (fun x_1 => match x_1 with | 0 => x) fun x => match x with | 0 => y) 1)) (φ 1) * ((b c).repr (Pure.permP id ⋯ (Pure.prodP (fun x_1 => match x_1 with | 0 => x) fun x => match x with | 0 => y) 0)) (φ 0) = ((b c1).repr y) (φ 1) * ((b c).repr x) (φ 0) All goals completed! 🐙 k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cφ:ComponentIdx ![c, c1]x:V c ⊗[k] V c1y:V c ⊗[k] V c1hx:((basis ![c, c1]).repr (fromPairT x)) φ = (((b c).tensorProduct (b c1)).repr x) (φ 0, φ 1)hy:((basis ![c, c1]).repr (fromPairT y)) φ = (((b c).tensorProduct (b c1)).repr y) (φ 0, φ 1)⊢ ((basis ![c, c1]).repr (fromPairT (x + y))) φ = (((b c).tensorProduct (b c1)).repr (x + y)) (φ 0, φ 1) All goals completed! 🐙k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cb0:basisIdx cb1:basisIdx c1b:ComponentIdx ![c, c1]⊢ (((b✝ c).tensorProduct (b✝ c1)).repr ((b✝ c) b0 ⊗ₜ[k] (b✝ c1) b1)) (b 0, b 1) = (Finsupp.single (fun x => match x with | 0 => b0 | 1 => b1) 1) b k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cb0:basisIdx cb1:basisIdx c1b:ComponentIdx ![c, c1]⊢ (if b0 = b 0 then if b1 = b 1 then 1 else 0 else 0) = if (fun x => match x with | 0 => b0 | 1 => b1) = b then 1 else 0 conv_rhs => k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cb0:basisIdx cb1:basisIdx c1b:ComponentIdx ![c, c1]| (fun x => match x with | 0 => b0 | 1 => b1) = bk:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cb0:basisIdx cb1:basisIdx c1b:ComponentIdx ![c, c1]⊢ Decidable ?m.314 k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cb0:basisIdx cb1:basisIdx c1b:ComponentIdx ![c, c1]| ∀ (x : Fin 2), (match x with | 0 => b0 | 1 => b1) = b xk:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cb0:basisIdx cb1:basisIdx c1b:ComponentIdx ![c, c1]⊢ Decidable ?m.314 k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cb0:basisIdx cb1:basisIdx c1b:ComponentIdx ![c, c1]| (match 0 with | 0 => b0 | 1 => b1) = b 0 ∧ (match 1 with | 0 => b0 | 1 => b1) = b 1k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cb0:basisIdx cb1:basisIdx c1b:ComponentIdx ![c, c1]⊢ Decidable ?m.314 k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cb0:basisIdx cb1:basisIdx c1b:ComponentIdx ![c, c1]| b0 = b 0 ∧ b1 = b 1k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cb0:basisIdx cb1:basisIdx c1b:ComponentIdx ![c, c1]⊢ Decidable ?m.314 k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cb0:basisIdx cb1:basisIdx c1b:ComponentIdx ![c, c1]h✝:b0 = b 0⊢ (if b1 = b 1 then 1 else 0) = if b0 = b 0 ∧ b1 = b 1 then 1 else 0k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cb0:basisIdx cb1:basisIdx c1b:ComponentIdx ![c, c1]h✝:¬b0 = b 0⊢ 0 = if b0 = b 0 ∧ b1 = b 1 then 1 else 0 next h k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cb0:basisIdx cb1:basisIdx c1b:ComponentIdx ![c, c1]h:b0 = b 0⊢ (if b1 = b 1 then 1 else 0) = if b0 = b 0 ∧ b1 = b 1 then 1 else 0 k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cb1:basisIdx c1b:ComponentIdx ![c, c1]⊢ (if b1 = b 1 then 1 else 0) = if b 0 = b 0 ∧ b1 = b 1 then 1 else 0 All goals completed! 🐙 next h k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cb0:basisIdx cb1:basisIdx c1b:ComponentIdx ![c, c1]h:¬b0 = b 0⊢ 0 = if b0 = b 0 ∧ b1 = b 1 then 1 else 0 All goals completed! 🐙

fromConstPair

Tensors formed by fromConstPair are invariant under the group action.

k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc1:Cc2:Cv:(Representation.trivial k G k).IntertwiningMap ((rep c1).tprod (rep c2))g:G⊢ fromPairT ((map ((rep c1) g) ((rep c2) g)) (v 1)) = fromPairT (v 1) All goals completed! 🐙

fromTripleT

lemma fromTripleT_tmul {c1 c2 c3 : C} (x : V c1) (y : V c2) (z : V c3) : fromTripleT (x ⊗ₜ[k] (y ⊗ₜ[k] z)) = permT id (And.intro Function.bijective_id (fun i => k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc1:Cc2:Cc3:Cx:V c1y:V c2z:V c3i:Fin (Nat.succ 0 + (Nat.succ 0 + Nat.succ 0))⊢ Fin.append ![c1] (Fin.append ![c2] ![c3]) (id i) = ![c1, c2, c3] i k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc1:Cc2:Cc3:Cx:V c1y:V c2z:V c3⊢ Fin.append ![c1] (Fin.append ![c2] ![c3]) (id ((fun i => i) ⟨0, ⋯⟩)) = ![c1, c2, c3] ((fun i => i) ⟨0, ⋯⟩)k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc1:Cc2:Cc3:Cx:V c1y:V c2z:V c3⊢ Fin.append ![c1] (Fin.append ![c2] ![c3]) (id ((fun i => i) ⟨1, ⋯⟩)) = ![c1, c2, c3] ((fun i => i) ⟨1, ⋯⟩)k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc1:Cc2:Cc3:Cx:V c1y:V c2z:V c3⊢ Fin.append ![c1] (Fin.append ![c2] ![c3]) (id ((fun i => i) ⟨2, ⋯⟩)) = ![c1, c2, c3] ((fun i => i) ⟨2, ⋯⟩) k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc1:Cc2:Cc3:Cx:V c1y:V c2z:V c3⊢ Fin.append ![c1] (Fin.append ![c2] ![c3]) (id ((fun i => i) ⟨0, ⋯⟩)) = ![c1, c2, c3] ((fun i => i) ⟨0, ⋯⟩)k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc1:Cc2:Cc3:Cx:V c1y:V c2z:V c3⊢ Fin.append ![c1] (Fin.append ![c2] ![c3]) (id ((fun i => i) ⟨1, ⋯⟩)) = ![c1, c2, c3] ((fun i => i) ⟨1, ⋯⟩)k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc1:Cc2:Cc3:Cx:V c1y:V c2z:V c3⊢ Fin.append ![c1] (Fin.append ![c2] ![c3]) (id ((fun i => i) ⟨2, ⋯⟩)) = ![c1, c2, c3] ((fun i => i) ⟨2, ⋯⟩) All goals completed! 🐙)) (prodT (fromSingleT (S := S) x) (prodT (fromSingleT y) (fromSingleT z))) := k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc1:Cc2:Cc3:Cx:V c1y:V c2z:V c3⊢ fromTripleT (x ⊗ₜ[k] (y ⊗ₜ[k] z)) = (permT id ⋯) ((prodT (fromSingleT x)) ((prodT (fromSingleT y)) (fromSingleT z))) All goals completed! 🐙k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc1:Cc2:Cc3:Cg:Gx:V c1y:V c2z:V c3⊢ (permT id ⋯) ((prodT (g • fromSingleT x)) ((prodT (g • fromSingleT y)) (g • fromSingleT z))) = (permT id ⋯) ((prodT (fromSingleT (((rep c1) g) x))) ((prodT (fromSingleT (((rep c2) g) y))) (fromSingleT (((rep c3) g) z)))) All goals completed! 🐙 k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc1:Cc2:Cc3:Cg:Gx:V c1a:V c2 ⊗[k] V c3b:V c2 ⊗[k] V c3ha:g • fromTripleT (x ⊗ₜ[k] a) = fromTripleT ((map ((rep c1) g) (map ((rep c2) g) ((rep c3) g))) (x ⊗ₜ[k] a))hb:g • fromTripleT (x ⊗ₜ[k] b) = fromTripleT ((map ((rep c1) g) (map ((rep c2) g) ((rep c3) g))) (x ⊗ₜ[k] b))⊢ g • fromTripleT (x ⊗ₜ[k] (a + b)) = fromTripleT ((map ((rep c1) g) (map ((rep c2) g) ((rep c3) g))) (x ⊗ₜ[k] (a + b))) All goals completed! 🐙 k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc1:Cc2:Cc3:Cg:Ga:V c1 ⊗[k] (V c2 ⊗[k] V c3)b:V c1 ⊗[k] (V c2 ⊗[k] V c3)ha:g • fromTripleT a = fromTripleT ((map ((rep c1) g) (map ((rep c2) g) ((rep c3) g))) a)hb:g • fromTripleT b = fromTripleT ((map ((rep c1) g) (map ((rep c2) g) ((rep c3) g))) b)⊢ g • fromTripleT (a + b) = fromTripleT ((map ((rep c1) g) (map ((rep c2) g) ((rep c3) g))) (a + b)) All goals completed! 🐙All goals completed! 🐙 k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cc2:Cφ:ComponentIdx ![c, c1, c2]a:V c ⊗[k] (V c1 ⊗[k] V c2)b:V c ⊗[k] (V c1 ⊗[k] V c2)ha:((basis ![c, c1, c2]).repr (fromTripleT a)) φ = (((b✝ c).tensorProduct ((b✝ c1).tensorProduct (b✝ c2))).repr a) (φ 0, φ 1, φ 2)hb:((basis ![c, c1, c2]).repr (fromTripleT b)) φ = (((b✝ c).tensorProduct ((b✝ c1).tensorProduct (b✝ c2))).repr b) (φ 0, φ 1, φ 2)⊢ ((basis ![c, c1, c2]).repr (fromTripleT (a + b))) φ = (((b✝ c).tensorProduct ((b✝ c1).tensorProduct (b✝ c2))).repr (a + b)) (φ 0, φ 1, φ 2) All goals completed! 🐙k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cc2:Cb0:basisIdx cb1:basisIdx c1b2:basisIdx c2b:ComponentIdx ![c, c1, c2]⊢ (((b✝ c).tensorProduct ((b✝ c1).tensorProduct (b✝ c2))).repr ((b✝ c) b0 ⊗ₜ[k] ((b✝ c1) b1 ⊗ₜ[k] (b✝ c2) b2))) (b 0, b 1, b 2) = (Finsupp.single (fun x => match x with | 0 => b0 | 1 => b1 | 2 => b2) 1) b k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cc2:Cb0:basisIdx cb1:basisIdx c1b2:basisIdx c2b:ComponentIdx ![c, c1, c2]⊢ (if b0 = b 0 then if b1 = b 1 then if b2 = b 2 then 1 else 0 else 0 else 0) = if (fun x => match x with | 0 => b0 | 1 => b1 | 2 => b2) = b then 1 else 0 conv_rhs => k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cc2:Cb0:basisIdx cb1:basisIdx c1b2:basisIdx c2b:ComponentIdx ![c, c1, c2]| (fun x => match x with | 0 => b0 | 1 => b1 | 2 => b2) = bk:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cc2:Cb0:basisIdx cb1:basisIdx c1b2:basisIdx c2b:ComponentIdx ![c, c1, c2]⊢ Decidable ?m.394 k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cc2:Cb0:basisIdx cb1:basisIdx c1b2:basisIdx c2b:ComponentIdx ![c, c1, c2]| ∀ (x : Fin 3), (match x with | 0 => b0 | 1 => b1 | 2 => b2) = b xk:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cc2:Cb0:basisIdx cb1:basisIdx c1b2:basisIdx c2b:ComponentIdx ![c, c1, c2]⊢ Decidable ?m.394 k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cc2:Cb0:basisIdx cb1:basisIdx c1b2:basisIdx c2b:ComponentIdx ![c, c1, c2]| (match 0 with | 0 => b0 | 1 => b1 | 2 => b2) = b 0 ∧ (match Fin.succ 0 with | 0 => b0 | 1 => b1 | 2 => b2) = b (Fin.succ 0) ∧ (match Fin.succ 1 with | 0 => b0 | 1 => b1 | 2 => b2) = b (Fin.succ 1)k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cc2:Cb0:basisIdx cb1:basisIdx c1b2:basisIdx c2b:ComponentIdx ![c, c1, c2]⊢ Decidable ?m.394 k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cc2:Cb0:basisIdx cb1:basisIdx c1b2:basisIdx c2b:ComponentIdx ![c, c1, c2]| b0 = b 0 ∧ b1 = b 1 ∧ b2 = b 2k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cc2:Cb0:basisIdx cb1:basisIdx c1b2:basisIdx c2b:ComponentIdx ![c, c1, c2]⊢ Decidable ?m.394 k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cc2:Cb0:basisIdx cb1:basisIdx c1b2:basisIdx c2b:ComponentIdx ![c, c1, c2]h✝:b0 = b 0⊢ (if b1 = b 1 then if b2 = b 2 then 1 else 0 else 0) = if b0 = b 0 ∧ b1 = b 1 ∧ b2 = b 2 then 1 else 0k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cc2:Cb0:basisIdx cb1:basisIdx c1b2:basisIdx c2b:ComponentIdx ![c, c1, c2]h✝:¬b0 = b 0⊢ 0 = if b0 = b 0 ∧ b1 = b 1 ∧ b2 = b 2 then 1 else 0 next h k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cc2:Cb0:basisIdx cb1:basisIdx c1b2:basisIdx c2b:ComponentIdx ![c, c1, c2]h:b0 = b 0⊢ (if b1 = b 1 then if b2 = b 2 then 1 else 0 else 0) = if b0 = b 0 ∧ b1 = b 1 ∧ b2 = b 2 then 1 else 0 k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cc2:Cb1:basisIdx c1b2:basisIdx c2b:ComponentIdx ![c, c1, c2]⊢ (if b1 = b 1 then if b2 = b 2 then 1 else 0 else 0) = if b 0 = b 0 ∧ b1 = b 1 ∧ b2 = b 2 then 1 else 0 k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cc2:Cb1:basisIdx c1b2:basisIdx c2b:ComponentIdx ![c, c1, c2]⊢ (if b1 = b 1 then if b2 = b 2 then 1 else 0 else 0) = if b1 = b 1 ∧ b2 = b 2 then 1 else 0 k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cc2:Cb1:basisIdx c1b2:basisIdx c2b:ComponentIdx ![c, c1, c2]h✝:b1 = b 1⊢ (if b2 = b 2 then 1 else 0) = if b1 = b 1 ∧ b2 = b 2 then 1 else 0k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cc2:Cb1:basisIdx c1b2:basisIdx c2b:ComponentIdx ![c, c1, c2]h✝:¬b1 = b 1⊢ 0 = if b1 = b 1 ∧ b2 = b 2 then 1 else 0 next h k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cc2:Cb1:basisIdx c1b2:basisIdx c2b:ComponentIdx ![c, c1, c2]h:b1 = b 1⊢ (if b2 = b 2 then 1 else 0) = if b1 = b 1 ∧ b2 = b 2 then 1 else 0 k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cc2:Cb2:basisIdx c2b:ComponentIdx ![c, c1, c2]⊢ (if b2 = b 2 then 1 else 0) = if b 1 = b 1 ∧ b2 = b 2 then 1 else 0 All goals completed! 🐙 next h k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cc2:Cb1:basisIdx c1b2:basisIdx c2b:ComponentIdx ![c, c1, c2]h:¬b1 = b 1⊢ 0 = if b1 = b 1 ∧ b2 = b 2 then 1 else 0 All goals completed! 🐙 next h k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b✝:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Cc2:Cb0:basisIdx cb1:basisIdx c1b2:basisIdx c2b:ComponentIdx ![c, c1, c2]h:¬b0 = b 0⊢ 0 = if b0 = b 0 ∧ b1 = b 1 ∧ b2 = b 2 then 1 else 0 All goals completed! 🐙

fromConstTriple

Tensors formed by fromConstPair are invariant under the group action.

k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc1:Cc2:Cc3:Cv:(Representation.trivial k G k).IntertwiningMap ((rep c1).tprod ((rep c2).tprod (rep c3)))g:G⊢ fromTripleT ((map ((rep c1) g) (map ((rep c2) g) ((rep c3) g))) (v 1)) = fromTripleT (v 1) All goals completed! 🐙