DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix: Correct tensor evaluation

Browse source
This commit is contained in:
jstoobysmith 2024-10-21 14:28:02 +00:00
parent 7fc850cc38
commit baf5169171
2 changed files with 18 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

1
HepLean/Tensors/Tree/Basic.lean
View file

@ -448,6 +448,7 @@ noncomputable section
Note: This function is not fully defined yet. -/
def tensor : ∀ {n : ℕ} {c : Fin n → S.C}, TensorTree S c → S.F.obj (OverColor.mk c) := fun
| tensorNode t => t
| twoNode t => (OverColor.Discrete.pairIsoSep S.FDiscrete).hom.hom t
| constTwoNode t => (OverColor.Discrete.pairIsoSep S.FDiscrete).hom.hom (t.hom (1 : S.k))
| add t1 t2 => t1.tensor + t2.tensor
| perm σ t => (S.F.map σ).hom t.tensor