doc: Curated notes for tensors

PhysLean/Relativity/Tensors/TensorSpecies/Basic.lean

@@ -20,8 +20,9 @@ open IndexNotation
 open CategoryTheory
 open MonoidalCategory
 
-/-- The structure of a type of tensors e.g. Lorentz tensors, ordinary tensors
-  (vectors and matrices), complex Lorentz tensors. -/
+/-- The structure `TensorSpecies` contains the necessary structure needed to define
+  a system of tensors with index notation. Examples of `TensorSpecies` include real Lorentz tensors,
+  complex Lorentz tensors, and ordinary Euclidean tensors.-/
 structure TensorSpecies where
   /-- The commutative ring over which we want to consider the tensors to live in,
     usually `ℝ` or `ℂ`. -/

PhysLean/Relativity/Tensors/Tree/Elab.lean

@@ -346,7 +346,7 @@ def getIndicesLeftEq (stx : Syntax) : TermElabM (List (TSyntax `indexExpr)) := d
   | `(tensorExpr| $a:tensorExpr = $_:tensorExpr) => do
       return (← getIndicesFull a)
   | _ =>
-    throwError "Unsupported tensor expression syntax in getIndicesProd: {stx}"
+    throwError "Unsupported tensor expression syntax in getIndicesLeftEq: {stx}"
 
 /-- Gets the indices associated with the RHS of an equality. -/
 def getIndicesRightEq (stx : Syntax) : TermElabM (List (TSyntax `indexExpr)) := do
@@ -354,7 +354,7 @@ def getIndicesRightEq (stx : Syntax) : TermElabM (List (TSyntax `indexExpr)) :=
   | `(tensorExpr| $_:tensorExpr = $a:tensorExpr) => do
       return (← getIndicesFull a)
   | _ =>
-    throwError "Unsupported tensor expression syntax in getIndicesProd: {stx}"
+    throwError "Unsupported tensor expression syntax in getIndicesRightEq: {stx}"
 
 /-!
 

docs/CuratedNotes/Tensors.html

@@ -0,0 +1,4 @@
+---
+layout: curatedNote
+data_source: tensors
+---

docs/CuratedNotes/index.html

@@ -25,6 +25,13 @@ layout: default
       <a href="HiggsPotential" class="note-link">Read More →</a>
     </div>
     <!-- End Wick's theorem -->
+     <!-- Tensors -->
+    <div class="note-card">
+      <h2 style="text-align: center;">Tensors 🚧</h2>
+      <p class="description">The formalization of tensors and index notation.</p>
+      <a href="Tensors" class="note-link">Read More →</a>
+    </div>
+    <!-- End Wick's theorem -->
   </div>
 </div>
 

scripts/MetaPrograms/notes.lean

@@ -373,10 +373,32 @@ def higgsPotential : Note where
     .name ``StandardModel.HiggsField.Potential.isMinOn_iff_field_of_𝓵_pos .complete,
   ]
 
+def tensors : Note where
+  title := "Tensors and index notation 🚧"
+  curators := ["Joseph Tooby-Smith"]
+  parts := [
+    .warning "This note is a work in progress. (5th March 2025)",
+    .h1 "Introduction",
+    .p "This note is related to: https://arxiv.org/pdf/2411.07667, and concerns the
+      implmentation of tensors and index notation into PhysLean, and
+      its mathematical structure.",
+    .p  "This note is not intended to be a first-introduction to tensors and index notation.",
+    .h1 "Tensor Species",
+    .name ``TensorSpecies .incomplete,
+    .h2 "Example: Complex Lorentz tensors",
+    .h1 "Tensor trees",
+    .name ``TensorTree .incomplete,
+    .name ``TensorTree.tensor .incomplete,
+    .h2 "Node identities",
+    .h1 "Elaboration",
+    .h1 "Example use: Pauli matrices"
+  ]
+
 def notesToMake : List (Note × String) := [
     (perturbationTheory, "perturbationTheory"),
     (harmonicOscillator, "harmonicOscillator"),
-    (higgsPotential, "higgsPotential")]
+    (higgsPotential, "higgsPotential"),
+    (tensors, "tensors")]
 
 def makeYML (nt : Note × String) : IO UInt32 := do
   let n := nt.1