feat: More informal def and lemma

HepLean/SpaceTime/WeylFermion/Basic.lean

@@ -14,6 +14,9 @@ import HepLean.Meta.Informal
 
 ## The definition of Weyl fermion vector spaces.
 
+We define the vector spaces corresponding to different types of Weyl fermions.
+
+Note: We should prevent casting between these vector spaces.
 -/
 
 informal_definition leftHandedWeylFermion where
@@ -76,10 +79,27 @@ informal_definition leftAltWeylFermionContraction where
     standard basis (i.e. the dot product)."
   physics :≈ "The contraction of a left-handed Weyl fermion with a right-handed Weyl fermion.
     In index notation this is ψ_a φ^a."
-  ref :≈ "https://particle.physics.ucdavis.edu/modernsusy/slides/slideimages/spinorfeynrules.pdf"
   deps :≈ [``leftHandedWeylFermion, ``altLeftHandedWeylFermion]
 
 informal_lemma leftAltWeylFermionContraction_invariant where
   math :≈ "The contraction leftAltWeylFermionContraction is invariant with respect to
     the action of SL(2,C) on leftHandedWeylFermion and altLeftHandedWeylFermion."
-  deps :≈ [`leftAltWeylFermionContraction]
+  deps :≈ [``leftAltWeylFermionContraction]
+
+informal_definition altLeftWeylFermionContraction where
+  math :≈ "The linear map from altLeftHandedWeylFermion ⊗ leftHandedWeylFermion  to ℂ given by
+    summing over components of altLeftHandedWeylFermion and leftHandedWeylFermion  in the
+    standard basis (i.e. the dot product)."
+  physics :≈ "The contraction of a left-handed Weyl fermion with a right-handed Weyl fermion.
+    In index notation this is φ^a ψ_a ."
+  deps :≈ [``leftHandedWeylFermion, ``altLeftHandedWeylFermion]
+
+informal_lemma leftAltWeylFermionContraction_symm_altLeftWeylFermionContraction where
+  math :≈ "The linear map altLeftWeylFermionContraction is leftAltWeylFermionContraction composed
+    with the braiding of the tensor product."
+  deps :≈ [``leftAltWeylFermionContraction, ``altLeftWeylFermionContraction]
+
+informal_lemma altLeftWeylFermionContraction_invariant where
+  math :≈ "The contraction altLeftWeylFermionContraction is invariant with respect to
+    the action of SL(2,C) on leftHandedWeylFermion and altLeftHandedWeylFermion."
+  deps :≈ [``altLeftWeylFermionContraction]