feat: Add informal superalgebra

HepLean/Mathematics/SuperAlgebra/Basic.lean

@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+import Mathlib.RingTheory.GradedAlgebra.Basic
+import HepLean.Meta.Informal
+/-!
+
+# Super Algebras
+
+A super algebra is a special type of graded algebra.
+
+It is used in physics to model the commutator of fermionic operators among themselves,
+aswell as among bosonic operators.
+
+-/
+
+informal_definition SuperAlgebra where
+  math :≈ "A super algebra is a graded algebra A with a ℤ₂ grading."
+  physics :≈ "A super algebra is used to model the commutator of fermionic operators among
+    themselves, aswell as among bosonic operators."
+  ref :≈ "https://en.wikipedia.org/wiki/Superalgebra"

HepLean/PerturbationTheory/Wick/Algebra.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.PerturbationTheory.Wick.Species
+import HepLean.Mathematics.SuperAlgebra.Basic
 /-!
 
 # Operator algebra
@@ -28,7 +29,7 @@ informal_definition WickAlgebra where
   math :≈ "
     Modifications of this may be needed.
     A structure with the following data:
-    - A ℤ₂-graded algebra A.
+    - A super algebra A.
     - A map from `ψ : 𝓔 × SpaceTime → A` where 𝓔 are field colors.
     - A map `ψc : 𝓔 × SpaceTime → A`.
     - A map `ψd : 𝓔 × SpaceTime → A`.
@@ -47,6 +48,7 @@ informal_definition WickAlgebra where
   physics :≈ "This is defined to be an
     abstraction of the notion of an operator algebra."
   ref :≈ "https://physics.stackexchange.com/questions/24157/"
+  deps :≈ [``SuperAlgebra]
 
 informal_definition WickMonomial where
   math :≈ "The type of elements of the Wick algebra which is a product of fields."

HepLean/PerturbationTheory/Wick/Species.lean

@@ -22,8 +22,7 @@ namespace Wick
 /-- The basic structure needed to write down Wick contractions for a theory and
   calculate the corresponding Feynman diagrams.
 
-  WARNING: This definition is not yet complete.
-  -/
+  WARNING: This definition is not yet complete. -/
 structure Species where
   /-- The color of Field operators which appear in a theory.
     One may wish to call these `half-edges`, however we restrict this terminology