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

The unit tensors

@[expose] public sectionattribute [-simp] LinearEquiv.cast_applylemma unitTensor_congr {c c1 : C} (h : c = c1) : unitTensor c = 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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Ch:c = c1⊢ IsReindexing ![S.τ c1, c1] ![S.τ c, c] id All goals completed! 🐙) (unitTensor (S := S) c1) := 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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cc1:Ch:c = c1⊢ unitTensor c = (permT id ⋯) (unitTensor c1) 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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:C⊢ unitTensor c = (permT id ⋯) (unitTensor c) All goals completed! 🐙

The unit tensor is symmetric on dualing the color.

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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cx✝:V (S.τ (S.τ c))y:V (S.τ c)p:Tensor.Pure S ![S.τ c]x:Tensor.Pure S ![S.τ (S.τ c)]⊢ (Pure.permP id ⋯ (p.prodP (Pure.permP id ⋯ x))).toTensor = (Pure.permP ![1, 0] ⋯ (x.prodP p)).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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cx✝:V (S.τ (S.τ c))y:V (S.τ c)p:Tensor.Pure S ![S.τ c]x:Tensor.Pure S ![S.τ (S.τ c)]⊢ Pure.permP id ⋯ (p.prodP (Pure.permP id ⋯ x)) = Pure.permP ![1, 0] ⋯ (x.prodP p) 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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cx✝:V (S.τ (S.τ c))y:V (S.τ c)p:Tensor.Pure S ![S.τ c]x:Tensor.Pure S ![S.τ (S.τ c)]i:Fin 2⊢ Pure.permP id ⋯ (p.prodP (Pure.permP id ⋯ x)) i = Pure.permP ![1, 0] ⋯ (x.prodP p) 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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cx✝:V (S.τ (S.τ c))y:V (S.τ c)p:Tensor.Pure S ![S.τ c]x:Tensor.Pure S ![S.τ (S.τ c)]⊢ Pure.permP id ⋯ (p.prodP (Pure.permP id ⋯ x)) ((fun i => i) ⟨0, ⋯⟩) = Pure.permP ![1, 0] ⋯ (x.prodP p) ((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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cx✝:V (S.τ (S.τ c))y:V (S.τ c)p:Tensor.Pure S ![S.τ c]x:Tensor.Pure S ![S.τ (S.τ c)]⊢ Pure.permP id ⋯ (p.prodP (Pure.permP id ⋯ x)) ((fun i => i) ⟨1, ⋯⟩) = Pure.permP ![1, 0] ⋯ (x.prodP p) ((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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cx✝:V (S.τ (S.τ c))y:V (S.τ c)p:Tensor.Pure S ![S.τ c]x:Tensor.Pure S ![S.τ (S.τ c)]⊢ Pure.permP id ⋯ (p.prodP (Pure.permP id ⋯ x)) ((fun i => i) ⟨0, ⋯⟩) = Pure.permP ![1, 0] ⋯ (x.prodP p) ((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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cx✝:V (S.τ (S.τ c))y:V (S.τ c)p:Tensor.Pure S ![S.τ c]x:Tensor.Pure S ![S.τ (S.τ c)]⊢ Pure.permP id ⋯ (p.prodP (Pure.permP id ⋯ x)) ((fun i => i) ⟨1, ⋯⟩) = Pure.permP ![1, 0] ⋯ (x.prodP p) ((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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cx:V (S.τ (S.τ c))y:V (S.τ c)p:Tensor.Pure S ![S.τ c]r:kt:S.Tensor ![S.τ (S.τ c)]a✝:(permT id ⋯) ((prodT p.toTensor) ((permT id ⋯) t)) = (permT ![1, 0] ⋯) ((prodT t) p.toTensor)⊢ (permT id ⋯) ((prodT p.toTensor) ((permT id ⋯) (r • t))) = (permT ![1, 0] ⋯) ((prodT (r • t)) p.toTensor) 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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cx:V (S.τ (S.τ c))y:V (S.τ c)p:Tensor.Pure S ![S.τ c]t1✝:S.Tensor ![S.τ (S.τ c)]t2✝:S.Tensor ![S.τ (S.τ c)]a✝¹:(permT id ⋯) ((prodT p.toTensor) ((permT id ⋯) t1✝)) = (permT ![1, 0] ⋯) ((prodT t1✝) p.toTensor)a✝:(permT id ⋯) ((prodT p.toTensor) ((permT id ⋯) t2✝)) = (permT ![1, 0] ⋯) ((prodT t2✝) p.toTensor)⊢ (permT id ⋯) ((prodT p.toTensor) ((permT id ⋯) (t1✝ + t2✝))) = (permT ![1, 0] ⋯) ((prodT (t1✝ + t2✝)) p.toTensor) 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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cx✝:V (S.τ (S.τ c))y:V (S.τ c)x:S.Tensor ![S.τ (S.τ c)]r✝:kt✝:S.Tensor ![S.τ c]a✝:(permT id ⋯) ((prodT t✝) ((permT id ⋯) x)) = (permT ![1, 0] ⋯) ((prodT x) t✝)⊢ (permT id ⋯) ((prodT (r✝ • t✝)) ((permT id ⋯) x)) = (permT ![1, 0] ⋯) ((prodT x) (r✝ • t✝)) 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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cx✝:V (S.τ (S.τ c))y:V (S.τ c)x:S.Tensor ![S.τ (S.τ c)]t1✝:S.Tensor ![S.τ c]t2✝:S.Tensor ![S.τ c]a✝¹:(permT id ⋯) ((prodT t1✝) ((permT id ⋯) x)) = (permT ![1, 0] ⋯) ((prodT x) t1✝)a✝:(permT id ⋯) ((prodT t2✝) ((permT id ⋯) x)) = (permT ![1, 0] ⋯) ((prodT x) t2✝)⊢ (permT id ⋯) ((prodT (t1✝ + t2✝)) ((permT id ⋯) x)) = (permT ![1, 0] ⋯) ((prodT x) (t1✝ + t2✝)) 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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cx✝:TensorProduct k (V (S.τ (S.τ c))) (V (S.τ c))y✝:TensorProduct k (V (S.τ (S.τ c))) (V (S.τ c))a✝¹:(permT id ⋯) ((TensorProduct.lift prodT) ((TensorProduct.map ↑fromSingleT ↑((LinearEquiv.cast ⋯).trans fromSingleT)) ((TensorProduct.comm k (V (S.τ (S.τ c))) (V (S.τ c))) x✝))) = (permT ![1, 0] ⋯) ((TensorProduct.lift prodT) ((TensorProduct.map ↑fromSingleT ↑fromSingleT) x✝))a✝:(permT id ⋯) ((TensorProduct.lift prodT) ((TensorProduct.map ↑fromSingleT ↑((LinearEquiv.cast ⋯).trans fromSingleT)) ((TensorProduct.comm k (V (S.τ (S.τ c))) (V (S.τ c))) y✝))) = (permT ![1, 0] ⋯) ((TensorProduct.lift prodT) ((TensorProduct.map ↑fromSingleT ↑fromSingleT) y✝))⊢ (permT id ⋯) ((TensorProduct.lift prodT) ((TensorProduct.map ↑fromSingleT ↑((LinearEquiv.cast ⋯).trans fromSingleT)) ((TensorProduct.comm k (V (S.τ (S.τ c))) (V (S.τ c))) (x✝ + y✝)))) = (permT ![1, 0] ⋯) ((TensorProduct.lift prodT) ((TensorProduct.map ↑fromSingleT ↑fromSingleT) (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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:C⊢ (permT ![1, 0] ⋯) (unitTensor (S.τ (S.τ c))) = (permT ![1, 0] ⋯) ((permT id ⋯) (unitTensor (S.τ (S.τ c)))) All goals completed! 🐙lemma unit_fromSingleTContrFromPairT_eq_fromSingleT {c : C} (x : V c) : fromSingleTContrFromPairT x ((S.unit c) (1 : k)) = fromSingleT 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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cx:V c⊢ fromSingleTContrFromPairT x ((S.unit c) 1) = fromSingleT x 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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cx:V c| fromSingleT ((TensorProduct.lid k (V c)) ((LinearMap.rTensor (V c) (S.contr c).toLinearMap) ((TensorProduct.assoc k (V c) (V (S.τ c)) (V c)).symm (x ⊗ₜ[k] (S.unit c) 1)))) All goals completed! 🐙

This lemma represents the de-categorification of S.contr_unit.

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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cx:S.Tensor ![S.τ c]⊢ (permT ((Fin.append (Fin.castAdd 1 ∘ ![1, 0]) (Fin.natAdd (Nat.succ 0).succ) 1).funPredPredAbove (Fin.append (Fin.castAdd 1 ∘ ![1, 0]) (Fin.natAdd (Nat.succ 0).succ) 2) ⋯ (Fin.append (Fin.natAdd 1) (Fin.castAdd (Nat.succ 0).succ)) ⋯ ∘ Fin.funPredPredAbove 1 2 ⋯ (Fin.append (Fin.castAdd 1 ∘ ![1, 0]) (Fin.natAdd (Nat.succ 0).succ)) ⋯) ⋯) ((permT (id ∘ id) ⋯) x) = (permT id ⋯) x conv_lhs => 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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cx:S.Tensor ![S.τ c]| (permT ((id ∘ id) ∘ (Fin.append (Fin.castAdd 1 ∘ ![1, 0]) (Fin.natAdd (Nat.succ 0).succ) 1).funPredPredAbove (Fin.append (Fin.castAdd 1 ∘ ![1, 0]) (Fin.natAdd (Nat.succ 0).succ) 2) ⋯ (Fin.append (Fin.natAdd 1) (Fin.castAdd (Nat.succ 0).succ)) ⋯ ∘ Fin.funPredPredAbove 1 2 ⋯ (Fin.append (Fin.castAdd 1 ∘ ![1, 0]) (Fin.natAdd (Nat.succ 0).succ)) ⋯) ⋯) 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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cx:S.Tensor ![S.τ c]⊢ (id ∘ id) ∘ (Fin.append (Fin.castAdd 1 ∘ ![1, 0]) (Fin.natAdd (Nat.succ 0).succ) 1).funPredPredAbove (Fin.append (Fin.castAdd 1 ∘ ![1, 0]) (Fin.natAdd (Nat.succ 0).succ) 2) ⋯ (Fin.append (Fin.natAdd 1) (Fin.castAdd (Nat.succ 0).succ)) ⋯ ∘ Fin.funPredPredAbove 1 2 ⋯ (Fin.append (Fin.castAdd 1 ∘ ![1, 0]) (Fin.natAdd (Nat.succ 0).succ)) ⋯ = idk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cx:S.Tensor ![S.τ c]⊢ x = 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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cx:S.Tensor ![S.τ c]⊢ (id ∘ id) ∘ (Fin.append (Fin.castAdd 1 ∘ ![1, 0]) (Fin.natAdd (Nat.succ 0).succ) 1).funPredPredAbove (Fin.append (Fin.castAdd 1 ∘ ![1, 0]) (Fin.natAdd (Nat.succ 0).succ) 2) ⋯ (Fin.append (Fin.natAdd 1) (Fin.castAdd (Nat.succ 0).succ)) ⋯ ∘ Fin.funPredPredAbove 1 2 ⋯ (Fin.append (Fin.castAdd 1 ∘ ![1, 0]) (Fin.natAdd (Nat.succ 0).succ)) ⋯ = 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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cx:S.Tensor ![S.τ c]i:Fin 1⊢ ↑(((id ∘ id) ∘ (Fin.append (Fin.castAdd 1 ∘ ![1, 0]) (Fin.natAdd (Nat.succ 0).succ) 1).funPredPredAbove (Fin.append (Fin.castAdd 1 ∘ ![1, 0]) (Fin.natAdd (Nat.succ 0).succ) 2) ⋯ (Fin.append (Fin.natAdd 1) (Fin.castAdd (Nat.succ 0).succ)) ⋯ ∘ Fin.funPredPredAbove 1 2 ⋯ (Fin.append (Fin.castAdd 1 ∘ ![1, 0]) (Fin.natAdd (Nat.succ 0).succ)) ⋯) i) = ↑(id 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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cx:S.Tensor ![S.τ c]⊢ ↑(((id ∘ id) ∘ (Fin.append (Fin.castAdd 1 ∘ ![1, 0]) (Fin.natAdd (Nat.succ 0).succ) 1).funPredPredAbove (Fin.append (Fin.castAdd 1 ∘ ![1, 0]) (Fin.natAdd (Nat.succ 0).succ) 2) ⋯ (Fin.append (Fin.natAdd 1) (Fin.castAdd (Nat.succ 0).succ)) ⋯ ∘ Fin.funPredPredAbove 1 2 ⋯ (Fin.append (Fin.castAdd 1 ∘ ![1, 0]) (Fin.natAdd (Nat.succ 0).succ)) ⋯) ((fun i => i) ⟨0, ⋯⟩)) = ↑(id ((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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Cx:S.Tensor ![S.τ c]⊢ x = x All goals completed! 🐙All goals completed! 🐙