1. Physlib
  2. Relativity
  3. Fermions
  4. Weyl
  5. Metric
Imports
/- 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 -/ module public import Physlib.Relativity.Fermions.Weyl.Unit

Metrics of Weyl fermions

We define the metrics for Weyl fermions, often denoted ε in the literature. These allow us to go from left-handed to dual-left-handed Weyl fermions and back, and from right-handed to dual-right-handed Weyl fermions and back.

@[expose] public section

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.

M:SL(2, ℂ)⊢ !![↑M 0 0 * 0 + ↑M 0 1 * -1, ↑M 0 0 * 1 + ↑M 0 1 * 0; ↑M 1 0 * 0 + ↑M 1 1 * -1, ↑M 1 0 * 1 + ↑M 1 1 * 0] = !![0, 1; -1, 0] * !![!![↑M 1 1, -↑M 0 1; -↑M 1 0, ↑M 0 0]ᵀ 0 0, !![↑M 1 1, -↑M 0 1; -↑M 1 0, ↑M 0 0]ᵀ 0 1; !![↑M 1 1, -↑M 0 1; -↑M 1 0, ↑M 0 0]ᵀ 1 0, !![↑M 1 1, -↑M 0 1; -↑M 1 0, ↑M 0 0]ᵀ 1 1] All goals completed! 🐙
M:SL(2, ℂ)⊢ !![0 * ↑M 0 0 + 1 * ↑M 1 0, 0 * ↑M 0 1 + 1 * ↑M 1 1; -1 * ↑M 0 0 + 0 * ↑M 1 0, -1 * ↑M 0 1 + 0 * ↑M 1 1] = !![!![↑M 1 1, -↑M 0 1; -↑M 1 0, ↑M 0 0]ᵀ 0 0, !![↑M 1 1, -↑M 0 1; -↑M 1 0, ↑M 0 0]ᵀ 0 1; !![↑M 1 1, -↑M 0 1; -↑M 1 0, ↑M 0 0]ᵀ 1 0, !![↑M 1 1, -↑M 0 1; -↑M 1 0, ↑M 0 0]ᵀ 1 1] * !![0, 1; -1, 0] All goals completed! 🐙M:SL(2, ℂ)⊢ !![!![↑M 0 0, ↑M 0 1; ↑M 1 0, ↑M 1 1].map star 0 0, !![↑M 0 0, ↑M 0 1; ↑M 1 0, ↑M 1 1].map star 0 1; !![↑M 0 0, ↑M 0 1; ↑M 1 0, ↑M 1 1].map star 1 0, !![↑M 0 0, ↑M 0 1; ↑M 1 0, ↑M 1 1].map star 1 1] * !![0, 1; -1, 0] = !![0, 1; -1, 0] * !![!![↑M 1 1, -↑M 0 1; -↑M 1 0, ↑M 0 0]ᴴ 0 0, !![↑M 1 1, -↑M 0 1; -↑M 1 0, ↑M 0 0]ᴴ 0 1; !![↑M 1 1, -↑M 0 1; -↑M 1 0, ↑M 0 0]ᴴ 1 0, !![↑M 1 1, -↑M 0 1; -↑M 1 0, ↑M 0 0]ᴴ 1 1] All goals completed! 🐙M:SL(2, ℂ)⊢ !![0, 1; -1, 0] * !![!![↑M 0 0, ↑M 0 1; ↑M 1 0, ↑M 1 1].map star 0 0, !![↑M 0 0, ↑M 0 1; ↑M 1 0, ↑M 1 1].map star 0 1; !![↑M 0 0, ↑M 0 1; ↑M 1 0, ↑M 1 1].map star 1 0, !![↑M 0 0, ↑M 0 1; ↑M 1 0, ↑M 1 1].map star 1 1] = !![!![↑M 1 1, -↑M 0 1; -↑M 1 0, ↑M 0 0]ᴴ 0 0, !![↑M 1 1, -↑M 0 1; -↑M 1 0, ↑M 0 0]ᴴ 0 1; !![↑M 1 1, -↑M 0 1; -↑M 1 0, ↑M 0 0]ᴴ 1 0, !![↑M 1 1, -↑M 0 1; -↑M 1 0, ↑M 0 0]ᴴ 1 1] * !![0, 1; -1, 0] All goals completed! 🐙

The metric εᵃᵃ as an element of (leftHanded ⊗ leftHanded).V.

def leftMetricVal : LeftHandedWeyl ⊗[ℂ] LeftHandedWeyl := leftLeftToMatrix.symm (- metricRaw)

Expansion of leftMetricVal into the left basis.

set_option backward.isDefEq.respectTransparency false in⊢ ∑ i, ∑ j, (-metricRaw) i j • LeftHandedWeyl.basis i ⊗ₜ[ℂ] LeftHandedWeyl.basis j = -LeftHandedWeyl.basis 0 ⊗ₜ[ℂ] LeftHandedWeyl.basis 1 + LeftHandedWeyl.basis 1 ⊗ₜ[ℂ] LeftHandedWeyl.basis 0 ⊢ -1 • LeftHandedWeyl.basis 0 ⊗ₜ[ℂ] LeftHandedWeyl.basis 1 = -LeftHandedWeyl.basis 0 ⊗ₜ[ℂ] LeftHandedWeyl.basis 1 All goals completed! 🐙
⊢ -LeftHandedWeyl.basis 0 ⊗ₜ[ℂ] LeftHandedWeyl.basis 1 + LeftHandedWeyl.basis 1 ⊗ₜ[ℂ] LeftHandedWeyl.basis 0 = LeftHandedWeyl.basis 1 ⊗ₜ[ℂ] LeftHandedWeyl.basis 0 - LeftHandedWeyl.basis 0 ⊗ₜ[ℂ] LeftHandedWeyl.basis 1; All goals completed! 🐙

The metric εᵃᵃ as a morphism 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ leftHanded ⊗ leftHanded, making manifest its invariance under the action of SL(2,ℂ).

M:SL(2, ℂ)x:ℂ⊢ metricRaw = metricRaw * (↑M * (↑M)⁻¹)ᵀ All goals completed! 🐙
lemma leftMetric_apply_one : leftMetric (1 : ℂ) = leftMetricVal := ⊢ leftMetric 1 = leftMetricVal ⊢ 1 • leftMetricVal = leftMetricVal All goals completed! 🐙

The metric εₐₐ as an element of (dualLeftHanded ⊗ dualLeftHanded).V.

def dualLeftMetricVal : (DualLeftHandedWeyl ⊗[ℂ] DualLeftHandedWeyl) := dualLeftdualLeftToMatrix.symm metricRaw

Expansion of dualLeftMetricVal into the left basis.

set_option backward.isDefEq.respectTransparency false in⊢ ∑ i, ∑ j, metricRaw i j • DualLeftHandedWeyl.basis i ⊗ₜ[ℂ] DualLeftHandedWeyl.basis j = DualLeftHandedWeyl.basis 0 ⊗ₜ[ℂ] DualLeftHandedWeyl.basis 1 - DualLeftHandedWeyl.basis 1 ⊗ₜ[ℂ] DualLeftHandedWeyl.basis 0 ⊢ DualLeftHandedWeyl.basis 0 ⊗ₜ[ℂ] DualLeftHandedWeyl.basis 1 + -1 • DualLeftHandedWeyl.basis 1 ⊗ₜ[ℂ] DualLeftHandedWeyl.basis 0 = DualLeftHandedWeyl.basis 0 ⊗ₜ[ℂ] DualLeftHandedWeyl.basis 1 - DualLeftHandedWeyl.basis 1 ⊗ₜ[ℂ] DualLeftHandedWeyl.basis 0 All goals completed! 🐙

The metric εₐₐ as a morphism 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ dualLeftHanded ⊗ dualLeftHanded, making manifest its invariance under the action of SL(2,ℂ).

M:SL(2, ℂ)x:ℂ⊢ metricRaw = metricRaw * (↑M * (↑M)⁻¹) All goals completed! 🐙
lemma dualLeftMetric_apply_one : dualLeftMetric (1 : ℂ) = dualLeftMetricVal := ⊢ dualLeftMetric 1 = dualLeftMetricVal ⊢ 1 • dualLeftMetricVal = dualLeftMetricVal All goals completed! 🐙

The metric ε^{dot a}^{dot a} as an element of (rightHanded ⊗ rightHanded).V.

def rightMetricVal : (RightHandedWeyl ⊗[ℂ] RightHandedWeyl) := rightRightToMatrix.symm (- metricRaw)

Expansion of rightMetricVal into the left basis.

set_option backward.isDefEq.respectTransparency false in⊢ ∑ i, ∑ j, (-metricRaw) i j • RightHandedWeyl.basis i ⊗ₜ[ℂ] RightHandedWeyl.basis j = -RightHandedWeyl.basis 0 ⊗ₜ[ℂ] RightHandedWeyl.basis 1 + RightHandedWeyl.basis 1 ⊗ₜ[ℂ] RightHandedWeyl.basis 0 ⊢ -1 • RightHandedWeyl.basis 0 ⊗ₜ[ℂ] RightHandedWeyl.basis 1 = -RightHandedWeyl.basis 0 ⊗ₜ[ℂ] RightHandedWeyl.basis 1 All goals completed! 🐙
⊢ -RightHandedWeyl.basis 0 ⊗ₜ[ℂ] RightHandedWeyl.basis 1 + RightHandedWeyl.basis 1 ⊗ₜ[ℂ] RightHandedWeyl.basis 0 = RightHandedWeyl.basis 1 ⊗ₜ[ℂ] RightHandedWeyl.basis 0 - RightHandedWeyl.basis 0 ⊗ₜ[ℂ] RightHandedWeyl.basis 1 All goals completed! 🐙

The metric ε^{dot a}^{dot a} as a morphism 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ rightHanded ⊗ rightHanded, making manifest its invariance under the action of SL(2,ℂ).

All goals completed! 🐙
lemma rightMetric_apply_one : rightMetric (1 : ℂ) = rightMetricVal := ⊢ rightMetric 1 = rightMetricVal ⊢ 1 • rightMetricVal = rightMetricVal All goals completed! 🐙

The metric ε_{dot a}_{dot a} as an element of (dualRightHanded ⊗ dualRightHanded).V.

def dualRightMetricVal : DualRightHandedWeyl ⊗[ℂ] DualRightHandedWeyl := dualRightDualRightToMatrix.symm (metricRaw)

Expansion of rightMetricVal into the left basis.

set_option backward.isDefEq.respectTransparency false in⊢ ∑ i, ∑ j, metricRaw i j • DualRightHandedWeyl.basis i ⊗ₜ[ℂ] DualRightHandedWeyl.basis j = DualRightHandedWeyl.basis 0 ⊗ₜ[ℂ] DualRightHandedWeyl.basis 1 - DualRightHandedWeyl.basis 1 ⊗ₜ[ℂ] DualRightHandedWeyl.basis 0 ⊢ DualRightHandedWeyl.basis 0 ⊗ₜ[ℂ] DualRightHandedWeyl.basis 1 + -1 • DualRightHandedWeyl.basis 1 ⊗ₜ[ℂ] DualRightHandedWeyl.basis 0 = DualRightHandedWeyl.basis 0 ⊗ₜ[ℂ] DualRightHandedWeyl.basis 1 - DualRightHandedWeyl.basis 1 ⊗ₜ[ℂ] DualRightHandedWeyl.basis 0 All goals completed! 🐙

The metric ε_{dot a}_{dot a} as a morphism 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ dualRightHanded ⊗ dualRightHanded, making manifest its invariance under the action of SL(2,ℂ).

M:SL(2, ℂ)x:ℂ⊢ (TensorProduct.map (DualRightHandedWeyl.rep M) (DualRightHandedWeyl.rep M)) (dualRightDualRightToMatrix.symm metricRaw) = (TensorProduct.map (DualRightHandedWeyl.rep M) (DualRightHandedWeyl.rep M)) dualRightMetricVal All goals completed! 🐙
lemma dualRightMetric_apply_one : dualRightMetric (1 : ℂ) = dualRightMetricVal := ⊢ dualRightMetric 1 = dualRightMetricVal ⊢ 1 • dualRightMetricVal = dualRightMetricVal All goals completed! 🐙

Contraction of metrics

⊢ DualLeftHandedWeyl.basis 1 ⊗ₜ[ℂ] LeftHandedWeyl.basis 1 - 0 • DualLeftHandedWeyl.basis 1 ⊗ₜ[ℂ] LeftHandedWeyl.basis 0 - (0 • DualLeftHandedWeyl.basis 0 ⊗ₜ[ℂ] LeftHandedWeyl.basis 1 - DualLeftHandedWeyl.basis 0 ⊗ₜ[ℂ] LeftHandedWeyl.basis 0) = DualLeftHandedWeyl.basis 1 ⊗ₜ[ℂ] LeftHandedWeyl.basis 1 + DualLeftHandedWeyl.basis 0 ⊗ₜ[ℂ] LeftHandedWeyl.basis 0 All goals completed! 🐙All goals completed! 🐙⊢ DualRightHandedWeyl.basis 1 ⊗ₜ[ℂ] RightHandedWeyl.basis 1 - 0 • DualRightHandedWeyl.basis 1 ⊗ₜ[ℂ] RightHandedWeyl.basis 0 - (0 • DualRightHandedWeyl.basis 0 ⊗ₜ[ℂ] RightHandedWeyl.basis 1 - DualRightHandedWeyl.basis 0 ⊗ₜ[ℂ] RightHandedWeyl.basis 0) = DualRightHandedWeyl.basis 1 ⊗ₜ[ℂ] RightHandedWeyl.basis 1 + DualRightHandedWeyl.basis 0 ⊗ₜ[ℂ] RightHandedWeyl.basis 0 All goals completed! 🐙All goals completed! 🐙