feat: More informal lemmas

HepLean/Tensors/ComplexLorentz/Metrics/Lemmas.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.Tensors.ComplexLorentz.Metrics.Basis
+import HepLean.Tensors.ComplexLorentz.Units.Basic
 import HepLean.Tensors.ComplexLorentz.Basis
 /-!
 
@@ -55,6 +56,46 @@ informal_lemma altRightMetric_antisymm where
   math :≈ "The alt-right metric is antisymmetric {εR' | β β' = - εR' | β' β}ᵀ"
   deps :≈ [``altRightMetric]
 
+/-!
+
+## Contractions with each other
+
+-/
+
+informal_lemma coMetric_contr_contrMetric where
+  math :≈ "The contraction of the covariant metric with the contravariant metric is the unit
+        {η' | μ ρ ⊗ η | ρ ν = δ' | μ ν}ᵀ"
+  deps :≈ [``coMetric, ``contrMetric, ``coContrUnit]
+
+informal_lemma contrMetric_contr_coMetric where
+  math :≈ "The contraction of the contravariant metric with the covariant metric is the unit
+        {η | μ ρ ⊗ η' | ρ ν = δ | μ ν}ᵀ"
+  deps :≈ [``contrMetric, ``coMetric, ``contrCoUnit]
+
+informal_lemma leftMetric_contr_altLeftMetric where
+  math :≈ "The contraction of the left metric with the alt-left metric is the unit
+        {εL | α β ⊗ εL' | β γ = δL | α γ}ᵀ"
+  deps :≈ [``leftMetric, ``altLeftMetric, ``leftAltLeftUnit]
+
+informal_lemma rightMetric_contr_altRightMetric where
+  math :≈ "The contraction of the right metric with the alt-right metric is the unit
+        {εR | α β ⊗ εR' | β γ = δR | α γ}ᵀ"
+  deps :≈ [``rightMetric, ``altRightMetric, ``rightAltRightUnit]
+
+informal_lemma altLeftMetric_contr_leftMetric where
+  math :≈ "The contraction of the alt-left metric with the left metric is the unit
+        {εL' | α β ⊗ εL | β γ = δL' | α γ}ᵀ"
+  deps :≈ [``altLeftMetric, ``leftMetric, ``altLeftLeftUnit]
+
+informal_lemma altRightMetric_contr_rightMetric where
+  math :≈ "The contraction of the alt-right metric with the right metric is the unit
+        {εR' | α β ⊗ εR | β γ = δR' | α γ}ᵀ"
+  deps :≈ [``altRightMetric, ``rightMetric, ``altRightRightUnit]
+/-!
+
+## Other relations
+
+-/
 /-- The map to color one gets when multiplying left and right metrics. -/
 def leftMetricMulRightMap := (Sum.elim ![Color.upL, Color.upL] ![Color.upR, Color.upR]) ∘
   finSumFinEquiv.symm

HepLean/Tensors/ComplexLorentz/Units/Basic.lean

@@ -129,38 +129,32 @@ lemma tensorNode_rightAltRightUnit: {δR | μ ν}ᵀ.tensor = (TensorTree.constT
 
 /-- The tensor `coContrUnit` is invariant under the action of `SL(2,ℂ)`. -/
 lemma action_coContrUnit (g : SL(2,ℂ)) : {g •ₐ δ' | μ ν}ᵀ.tensor = {δ' | μ ν}ᵀ.tensor := by
-  rw [tensorNode_coContrUnit, constTwoNodeE]
+  rw [tensorNode_coContrUnit, constTwoNodeE, ← action_constTwoNode _ g]
-  rw [← action_constTwoNode _ g]
   rfl
 
 /-- The tensor `contrCoUnit` is invariant under the action of `SL(2,ℂ)`. -/
 lemma action_contrCoUnit (g : SL(2,ℂ)) : {g •ₐ δ | μ ν}ᵀ.tensor = {δ | μ ν}ᵀ.tensor := by
-  rw [tensorNode_contrCoUnit, constTwoNodeE]
+  rw [tensorNode_contrCoUnit, constTwoNodeE, ← action_constTwoNode _ g]
-  rw [← action_constTwoNode _ g]
   rfl
 
 /-- The tensor `altLeftLeftUnit` is invariant under the action of `SL(2,ℂ)`. -/
 lemma action_altLeftLeftUnit (g : SL(2,ℂ)) : {g •ₐ δL' | μ ν}ᵀ.tensor = {δL' | μ ν}ᵀ.tensor := by
-  rw [tensorNode_altLeftLeftUnit, constTwoNodeE]
+  rw [tensorNode_altLeftLeftUnit, constTwoNodeE, ← action_constTwoNode _ g]
-  rw [← action_constTwoNode _ g]
   rfl
 
 /-- The tensor `leftAltLeftUnit` is invariant under the action of `SL(2,ℂ)`. -/
 lemma action_leftAltLeftUnit (g : SL(2,ℂ)) : {g •ₐ δL | μ ν}ᵀ.tensor = {δL | μ ν}ᵀ.tensor := by
-  rw [tensorNode_leftAltLeftUnit, constTwoNodeE]
+  rw [tensorNode_leftAltLeftUnit, constTwoNodeE, ← action_constTwoNode _ g]
-  rw [← action_constTwoNode _ g]
   rfl
 
 /-- The tensor `altRightRightUnit` is invariant under the action of `SL(2,ℂ)`. -/
 lemma action_altRightRightUnit (g : SL(2,ℂ)) : {g •ₐ δR' | μ ν}ᵀ.tensor = {δR' | μ ν}ᵀ.tensor := by
-  rw [tensorNode_altRightRightUnit, constTwoNodeE]
+  rw [tensorNode_altRightRightUnit, constTwoNodeE, ← action_constTwoNode _ g]
-  rw [← action_constTwoNode _ g]
   rfl
 
 /-- The tensor `rightAltRightUnit` is invariant under the action of `SL(2,ℂ)`. -/
 lemma action_rightAltRightUnit (g : SL(2,ℂ)) : {g •ₐ δR | μ ν}ᵀ.tensor = {δR | μ ν}ᵀ.tensor := by
-  rw [tensorNode_rightAltRightUnit, constTwoNodeE]
+  rw [tensorNode_rightAltRightUnit, constTwoNodeE, ← action_constTwoNode _ g]
-  rw [← action_constTwoNode _ g]
   rfl
 
 end complexLorentzTensor