From 88b2d28431c5ba3507598e43a7e697364bdacb7a Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Tue, 26 Nov 2024 12:35:52 +0000
Subject: [PATCH] docs: Colors of Lorentz tensors

---
 HepLean/Lorentz/ComplexTensor/Basic.lean | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/HepLean/Lorentz/ComplexTensor/Basic.lean b/HepLean/Lorentz/ComplexTensor/Basic.lean
index e331cd5..50b28e9 100644
--- a/HepLean/Lorentz/ComplexTensor/Basic.lean
+++ b/HepLean/Lorentz/ComplexTensor/Basic.lean
@@ -30,11 +30,17 @@ namespace complexLorentzTensor
 
 /-- The colors associated with complex representations of SL(2, ℂ) of intrest to physics. -/
 inductive Color
+  /-- The color associated with Left handed fermions. -/
   | upL : Color
+  /-- The color associated with alt-Left handed fermions. -/
   | downL : Color
+  /-- The color associated with Right handed fermions. -/
   | upR : Color
+  /-- The color associated with alt-Right handed fermions. -/
   | downR : Color
+  /-- The color associated with contravariant Lorentz vectors. -/
   | up : Color
+  /-- The color associated with covariant Lorentz vectors. -/
   | down : Color
 
 /-- Color for complex Lorentz tensors is decidable. -/