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

fix: Doc on Tensor Species

Browse source
This commit is contained in:
jstoobysmith 2024-11-04 11:43:36 +00:00
parent 72a468333b
commit 718583ff49
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -50,8 +50,8 @@ structure TensorSpecies where
G_group : Group G
/-- The colors of indices e.g. up or down. -/
C : Type
/-- A `MonoidalFunctor` from `OverColor C` giving the rep corresponding to a map of colors
`X → C`. -/
/-- A functor from `C` to `Rep k G` giving our building block representations.
Equivalently a function `C → Re k G`. -/
FDiscrete : Discrete C ⥤ Rep k G
/-- A specification of the dimension of each color in C. This will be used for explicit
evaluation of tensors. -/