docs: metric-lemmas

HepLean/Lorentz/ComplexTensor/Metrics/Basis.lean

@@ -87,6 +87,8 @@ lemma contrMatrix_basis_expand : {η | μ ν}ᵀ.tensor =
       simp only [Fin.isValue, Lorentz.complexContrBasisFin4, Basis.coe_reindex, Function.comp_apply]
       rfl
 
+/-- The expansion of the Lorentz contrvariant metric in terms of basis vectors as
+  a structured tensor tree. -/
 lemma contrMatrix_basis_expand_tree : {η | μ ν}ᵀ.tensor =
     (TensorTree.add (tensorNode (basisVector ![Color.up, Color.up] (fun _ => 0))) <|
     TensorTree.add (smul (-1) (tensorNode (basisVector ![Color.up, Color.up] (fun _ => 1)))) <|
@@ -94,6 +96,7 @@ lemma contrMatrix_basis_expand_tree : {η | μ ν}ᵀ.tensor =
     (smul (-1) (tensorNode (basisVector ![Color.up, Color.up] (fun _ => 3))))).tensor :=
   contrMatrix_basis_expand
 
+/-- The expansion of the Fermionic left metric in terms of basis vectors. -/
 lemma leftMetric_expand : {εL | α β}ᵀ.tensor =
     - basisVector ![Color.upL, Color.upL] (fun | 0 => 0 | 1 => 1)
     + basisVector ![Color.upL, Color.upL] (fun | 0 => 1 | 1 => 0) := by
@@ -112,12 +115,15 @@ lemma leftMetric_expand : {εL | α β}ᵀ.tensor =
     · rfl
     · rfl
 
+/-- The expansion of the Fermionic left metric in terms of basis vectors as a structured
+  tensor tree. -/
 lemma leftMetric_expand_tree : {εL | α β}ᵀ.tensor =
     (TensorTree.add (smul (-1) (tensorNode (basisVector ![Color.upL, Color.upL]
     (fun | 0 => 0 | 1 => 1)))) <|
     (tensorNode (basisVector ![Color.upL, Color.upL] (fun | 0 => 1 | 1 => 0)))).tensor :=
   leftMetric_expand
 
+/-- The expansion of the Fermionic alt-left metric in terms of basis vectors. -/
 lemma altLeftMetric_expand : {εL' | α β}ᵀ.tensor =
     basisVector ![Color.downL, Color.downL] (fun | 0 => 0 | 1 => 1)
     - basisVector ![Color.downL, Color.downL] (fun | 0 => 1 | 1 => 0) := by
@@ -135,6 +141,8 @@ lemma altLeftMetric_expand : {εL' | α β}ᵀ.tensor =
     · rfl
     · rfl
 
+/-- The expansion of the Fermionic alt-left metric in terms of basis vectors as a
+  structured tensor tree. -/
 lemma altLeftMetric_expand_tree : {εL' | α β}ᵀ.tensor =
     (TensorTree.add (tensorNode (basisVector ![Color.downL, Color.downL]
     (fun | 0 => 0 | 1 => 1))) <|
@@ -142,6 +150,7 @@ lemma altLeftMetric_expand_tree : {εL' | α β}ᵀ.tensor =
     (fun | 0 => 1 | 1 => 0))))).tensor :=
   altLeftMetric_expand
 
+/-- The expansion of the Fermionic right metric in terms of basis vectors. -/
 lemma rightMetric_expand : {εR | α β}ᵀ.tensor =
     - basisVector ![Color.upR, Color.upR] (fun | 0 => 0 | 1 => 1)
     + basisVector ![Color.upR, Color.upR] (fun | 0 => 1 | 1 => 0) := by
@@ -160,12 +169,15 @@ lemma rightMetric_expand : {εR | α β}ᵀ.tensor =
     · rfl
     · rfl
 
+/-- The expansion of the Fermionic right metric in terms of basis vectors as a
+  structured tensor tree. -/
 lemma rightMetric_expand_tree : {εR | α β}ᵀ.tensor =
     (TensorTree.add (smul (-1) (tensorNode (basisVector ![Color.upR, Color.upR]
     (fun | 0 => 0 | 1 => 1)))) <|
     (tensorNode (basisVector ![Color.upR, Color.upR] (fun | 0 => 1 | 1 => 0)))).tensor :=
   rightMetric_expand
 
+/-- The expansion of the Fermionic alt-right metric in terms of basis vectors. -/
 lemma altRightMetric_expand : {εR' | α β}ᵀ.tensor =
     basisVector ![Color.downR, Color.downR] (fun | 0 => 0 | 1 => 1)
     - basisVector ![Color.downR, Color.downR] (fun | 0 => 1 | 1 => 0) := by
@@ -183,6 +195,8 @@ lemma altRightMetric_expand : {εR' | α β}ᵀ.tensor =
     · rfl
     · rfl
 
+/-- The expansion of the Fermionic alt-right metric in terms of basis vectors as a
+  structured tensor tree. -/
 lemma altRightMetric_expand_tree : {εR' | α β}ᵀ.tensor =
     (TensorTree.add (tensorNode (basisVector
     ![Color.downR, Color.downR] (fun | 0 => 0 | 1 => 1))) <|

HepLean/Lorentz/ComplexTensor/Metrics/Lemmas.lean

@@ -101,7 +101,7 @@ informal_lemma altRightMetric_contr_rightMetric where
 def leftMetricMulRightMap := (Sum.elim ![Color.upL, Color.upL] ![Color.upR, Color.upR]) ∘
   finSumFinEquiv.symm
 
-/- Expansion of the product of `εL` and `εR` in terms of a basis. -/
+/-- Expansion of the product of `εL` and `εR` in terms of a basis. -/
 lemma leftMetric_prod_rightMetric : {εL | α α' ⊗ εR | β β'}ᵀ.tensor
     = basisVector leftMetricMulRightMap (fun | 0 => 0 | 1 => 1 | 2 => 0 | 3 => 1)
     - basisVector leftMetricMulRightMap (fun | 0 => 0 | 1 => 1 | 2 => 1 | 3 => 0)
@@ -134,7 +134,7 @@ lemma leftMetric_prod_rightMetric : {εL | α α' ⊗ εR | β β'}ᵀ.tensor
     funext x
     fin_cases x <;> rfl
 
-/- Expansion of the product of `εL` and `εR` in terms of a basis, as a tensor tree. -/
+/-- Expansion of the product of `εL` and `εR` in terms of a basis, as a tensor tree. -/
 lemma leftMetric_prod_rightMetric_tree : {εL | α α' ⊗ εR | β β'}ᵀ.tensor
     = (TensorTree.add (tensorNode
         (basisVector leftMetricMulRightMap (fun | 0 => 0 | 1 => 1 | 2 => 0 | 3 => 1))) <|

HepLean/Lorentz/Weyl/Metric.lean

@@ -30,6 +30,8 @@ open CategoryTheory.MonoidalCategory
 /-- The raw `2x2` matrix corresponding to the metric for fermions. -/
 def metricRaw : Matrix (Fin 2) (Fin 2) ℂ := !![0, 1; -1, 0]
 
+/-- Multiplying an element of `SL(2, ℂ)` on the left with the metric `𝓔` is equivalent
+  to multiplying the inverse-transpose of that element on the right with the metric. -/
 lemma comm_metricRaw (M : SL(2,ℂ)) : M.1 * metricRaw = metricRaw * (M.1⁻¹)ᵀ := by
   rw [metricRaw]
   rw [Lorentz.SL2C.inverse_coe, eta_fin_two M.1]