Physlib.Relativity.Tensors.RealTensor.Metrics.Pre

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.Tensors.RealTensor.Units.Pre

Metric for real Lorentz vectors

@[expose] public section

The metric ηᵃᵃ as an element of (ContrMod d ⊗[ℝ] ContrMod d).

def preContrMetricVal (d : ℕ := 3) : ContrMod d ⊗[ℝ] ContrMod d :=
  contrContrToMatrixRe.symm ((@minkowskiMatrix d))



lemma preContrMetricVal_expand_tmul_minkowskiMatrix {d : ℕ} : preContrMetricVal d =
    ∑ i, (minkowskiMatrix i i) • (contrBasis d i ⊗ₜ[ℝ] contrBasis d i) := byd:ℕ⊢ preContrMetricVal d = ∑ i, minkowskiMatrix i i • (contrBasis d) i ⊗ₜ[ℝ] (contrBasis d) i
  rw [preContrMetricVal,d:ℕ⊢ contrContrToMatrixRe.symm minkowskiMatrix = ∑ i, minkowskiMatrix i i • (contrBasis d) i ⊗ₜ[ℝ] (contrBasis d) id:ℕ⊢ ∑ i, ∑ j, minkowskiMatrix i j • (contrBasis d) i ⊗ₜ[ℝ] (contrBasis d) j =
  ∑ i, minkowskiMatrix i i • (contrBasis d) i ⊗ₜ[ℝ] (contrBasis d) i contrContrToMatrixRe_symm_expand_tmuld:ℕ⊢ ∑ i, ∑ j, minkowskiMatrix i j • (contrBasis d) i ⊗ₜ[ℝ] (contrBasis d) j =
  ∑ i, minkowskiMatrix i i • (contrBasis d) i ⊗ₜ[ℝ] (contrBasis d) id:ℕ⊢ ∑ i, ∑ j, minkowskiMatrix i j • (contrBasis d) i ⊗ₜ[ℝ] (contrBasis d) j =
  ∑ i, minkowskiMatrix i i • (contrBasis d) i ⊗ₜ[ℝ] (contrBasis d) i]d:ℕ⊢ ∑ i, ∑ j, minkowskiMatrix i j • (contrBasis d) i ⊗ₜ[ℝ] (contrBasis d) j =
  ∑ i, minkowskiMatrix i i • (contrBasis d) i ⊗ₜ[ℝ] (contrBasis d) i
  exact Finset.sum_congr rfl fun i _ => Finset.sum_eq_single_of_mem i (Finset.mem_univ i)
    fun j _ hj => smul_eq_zero_of_left (minkowskiMatrix.off_diag_zero hj.symm) _All goals completed! 🐙

Expansion of preContrMetricVal into basis.


lemma preContrMetricVal_expand_tmul {d : ℕ} : preContrMetricVal d =
    contrBasis d (Sum.inl 0) ⊗ₜ[ℝ] contrBasis d (Sum.inl 0) -
    ∑ i, contrBasis d (Sum.inr i) ⊗ₜ[ℝ] contrBasis d (Sum.inr i) := byd:ℕ⊢ preContrMetricVal d =
  (contrBasis d) (Sum.inl 0) ⊗ₜ[ℝ] (contrBasis d) (Sum.inl 0) -
    ∑ i, (contrBasis d) (Sum.inr i) ⊗ₜ[ℝ] (contrBasis d) (Sum.inr i)
  rw [preContrMetricVal_expand_tmul_minkowskiMatrixd:ℕ⊢ ∑ i, minkowskiMatrix i i • (contrBasis d) i ⊗ₜ[ℝ] (contrBasis d) i =
  (contrBasis d) (Sum.inl 0) ⊗ₜ[ℝ] (contrBasis d) (Sum.inl 0) -
    ∑ i, (contrBasis d) (Sum.inr i) ⊗ₜ[ℝ] (contrBasis d) (Sum.inr i)d:ℕ⊢ ∑ i, minkowskiMatrix i i • (contrBasis d) i ⊗ₜ[ℝ] (contrBasis d) i =
  (contrBasis d) (Sum.inl 0) ⊗ₜ[ℝ] (contrBasis d) (Sum.inl 0) -
    ∑ i, (contrBasis d) (Sum.inr i) ⊗ₜ[ℝ] (contrBasis d) (Sum.inr i)]d:ℕ⊢ ∑ i, minkowskiMatrix i i • (contrBasis d) i ⊗ₜ[ℝ] (contrBasis d) i =
  (contrBasis d) (Sum.inl 0) ⊗ₜ[ℝ] (contrBasis d) (Sum.inl 0) -
    ∑ i, (contrBasis d) (Sum.inr i) ⊗ₜ[ℝ] (contrBasis d) (Sum.inr i)
  simp [Fintype.sum_sum_type, minkowskiMatrix.inl_0_inl_0, minkowskiMatrix.inr_i_inr_i,
    sub_eq_add_neg]All goals completed! 🐙

The metric ηᵃᵃ as a morphism 𝟙_ (Rep ℝ (LorentzGroup d)) ⟶ ContrMod.rep ⊗ ContrMod.rep, making its invariance under the action of LorentzGroup d.

set_option backward.isDefEq.respectTransparency false in

def preContrMetric (d : ℕ := 3) :
    (Representation.trivial ℝ (LorentzGroup d) ℝ).IntertwiningMap
    ((ContrMod.rep).tprod (ContrMod.rep)) where
  toFun := fun a => a • (preContrMetricVal d)
  map_add' := fun x y => add_smul x y _
  map_smul' := fun m x => mul_smul m x _
  isIntertwining' M := byd:ℕM:↑(LorentzGroup d)⊢ { toFun := fun a => a • preContrMetricVal d, map_add' := ⋯, map_smul' := ⋯ } ∘ₗ
    (Representation.trivial ℝ ↑(LorentzGroup d) ℝ) M =
  (ContrMod.rep.tprod ContrMod.rep) M ∘ₗ { toFun := fun a => a • preContrMetricVal d, map_add' := ⋯, map_smul' := ⋯ }
    refine LinearMap.ext fun x : ℝ => ?_d:ℕM:↑(LorentzGroup d)x:ℝ⊢ ({ toFun := fun a => a • preContrMetricVal d, map_add' := ⋯, map_smul' := ⋯ } ∘ₗ
      (Representation.trivial ℝ ↑(LorentzGroup d) ℝ) M)
    x =
  ((ContrMod.rep.tprod ContrMod.rep) M ∘ₗ { toFun := fun a => a • preContrMetricVal d, map_add' := ⋯, map_smul' := ⋯ })
    x
    simp only [LinearMap.coe_comp, Function.comp_apply]d:ℕM:↑(LorentzGroup d)x:ℝ⊢ { toFun := fun a => a • preContrMetricVal d, map_add' := ⋯, map_smul' := ⋯ }
    (((Representation.trivial ℝ ↑(LorentzGroup d) ℝ) M) x) =
  ((ContrMod.rep.tprod ContrMod.rep) M) ({ toFun := fun a => a • preContrMetricVal d, map_add' := ⋯, map_smul' := ⋯ } x)
    change x • (preContrMetricVal d) =
      (TensorProduct.map (ContrMod.rep M) (ContrMod.rep M)) (x • (preContrMetricVal d))d:ℕM:↑(LorentzGroup d)x:ℝ⊢ x • preContrMetricVal d = (TensorProduct.map (ContrMod.rep M) (ContrMod.rep M)) (x • preContrMetricVal d)
    simp only [map_smul]d:ℕM:↑(LorentzGroup d)x:ℝ⊢ x • preContrMetricVal d = x • (TensorProduct.map (ContrMod.rep M) (ContrMod.rep M)) (preContrMetricVal d)
    apply congrArgd:ℕM:↑(LorentzGroup d)x:ℝ⊢ preContrMetricVal d = (TensorProduct.map (ContrMod.rep M) (ContrMod.rep M)) (preContrMetricVal d)
    simp only [preContrMetricVal]d:ℕM:↑(LorentzGroup d)x:ℝ⊢ contrContrToMatrixRe.symm minkowskiMatrix =
  (TensorProduct.map (ContrMod.rep M) (ContrMod.rep M)) (contrContrToMatrixRe.symm minkowskiMatrix)
    conv_rhs =>
      rw [contrContrToMatrixRe_ρ_symm]d:ℕM:↑(LorentzGroup d)x:ℝ| contrContrToMatrixRe.symm (↑M * minkowskiMatrix * (↑M)ᵀ)
    apply congrArgd:ℕM:↑(LorentzGroup d)x:ℝ⊢ minkowskiMatrix = ↑M * minkowskiMatrix * (↑M)ᵀ
    simpAll goals completed! 🐙

lemma preContrMetric_apply_one {d : ℕ} : (preContrMetric d) (1 : ℝ) = preContrMetricVal d :=
  one_smul ℝ _

The metric ηᵢᵢ as an element of (CoMod d ⊗[ℝ] CoMod d).

def preCoMetricVal (d : ℕ := 3) : CoMod d ⊗[ℝ] CoMod d :=
  coCoToMatrixRe.symm ((@minkowskiMatrix d))



lemma preCoMetricVal_expand_tmul_minkowskiMatrix {d : ℕ} : preCoMetricVal d =
    ∑ i, (minkowskiMatrix i i) • (coBasis d i ⊗ₜ[ℝ] coBasis d i) := byd:ℕ⊢ preCoMetricVal d = ∑ i, minkowskiMatrix i i • (coBasis d) i ⊗ₜ[ℝ] (coBasis d) i
  rw [preCoMetricVal,d:ℕ⊢ coCoToMatrixRe.symm minkowskiMatrix = ∑ i, minkowskiMatrix i i • (coBasis d) i ⊗ₜ[ℝ] (coBasis d) id:ℕ⊢ ∑ i, ∑ j, minkowskiMatrix i j • (coBasis d) i ⊗ₜ[ℝ] (coBasis d) j =
  ∑ i, minkowskiMatrix i i • (coBasis d) i ⊗ₜ[ℝ] (coBasis d) i coCoToMatrixRe_symm_expand_tmuld:ℕ⊢ ∑ i, ∑ j, minkowskiMatrix i j • (coBasis d) i ⊗ₜ[ℝ] (coBasis d) j =
  ∑ i, minkowskiMatrix i i • (coBasis d) i ⊗ₜ[ℝ] (coBasis d) id:ℕ⊢ ∑ i, ∑ j, minkowskiMatrix i j • (coBasis d) i ⊗ₜ[ℝ] (coBasis d) j =
  ∑ i, minkowskiMatrix i i • (coBasis d) i ⊗ₜ[ℝ] (coBasis d) i]d:ℕ⊢ ∑ i, ∑ j, minkowskiMatrix i j • (coBasis d) i ⊗ₜ[ℝ] (coBasis d) j =
  ∑ i, minkowskiMatrix i i • (coBasis d) i ⊗ₜ[ℝ] (coBasis d) i
  exact Finset.sum_congr rfl fun i _ => Finset.sum_eq_single_of_mem i (Finset.mem_univ i)
    fun j _ hj => smul_eq_zero_of_left (minkowskiMatrix.off_diag_zero hj.symm) _All goals completed! 🐙

Expansion of preContrMetricVal into basis.


lemma preCoMetricVal_expand_tmul {d : ℕ} : preCoMetricVal d =
    coBasis d (Sum.inl 0) ⊗ₜ[ℝ] coBasis d (Sum.inl 0) -
    ∑ i, coBasis d (Sum.inr i) ⊗ₜ[ℝ] coBasis d (Sum.inr i) := byd:ℕ⊢ preCoMetricVal d =
  (coBasis d) (Sum.inl 0) ⊗ₜ[ℝ] (coBasis d) (Sum.inl 0) - ∑ i, (coBasis d) (Sum.inr i) ⊗ₜ[ℝ] (coBasis d) (Sum.inr i)
  rw [preCoMetricVal_expand_tmul_minkowskiMatrixd:ℕ⊢ ∑ i, minkowskiMatrix i i • (coBasis d) i ⊗ₜ[ℝ] (coBasis d) i =
  (coBasis d) (Sum.inl 0) ⊗ₜ[ℝ] (coBasis d) (Sum.inl 0) - ∑ i, (coBasis d) (Sum.inr i) ⊗ₜ[ℝ] (coBasis d) (Sum.inr i)d:ℕ⊢ ∑ i, minkowskiMatrix i i • (coBasis d) i ⊗ₜ[ℝ] (coBasis d) i =
  (coBasis d) (Sum.inl 0) ⊗ₜ[ℝ] (coBasis d) (Sum.inl 0) - ∑ i, (coBasis d) (Sum.inr i) ⊗ₜ[ℝ] (coBasis d) (Sum.inr i)]d:ℕ⊢ ∑ i, minkowskiMatrix i i • (coBasis d) i ⊗ₜ[ℝ] (coBasis d) i =
  (coBasis d) (Sum.inl 0) ⊗ₜ[ℝ] (coBasis d) (Sum.inl 0) - ∑ i, (coBasis d) (Sum.inr i) ⊗ₜ[ℝ] (coBasis d) (Sum.inr i)
  simp [Fintype.sum_sum_type, minkowskiMatrix.inl_0_inl_0, minkowskiMatrix.inr_i_inr_i,
    sub_eq_add_neg]All goals completed! 🐙

The metric ηᵢᵢ as a morphism 𝟙_ (Rep ℂ (LorentzGroup d))) ⟶ CoMod.rep ⊗ CoMod.rep, making its invariance under the action of LorentzGroup d.

set_option backward.isDefEq.respectTransparency false in


def preCoMetric (d : ℕ := 3) : (Representation.trivial ℝ (LorentzGroup d) ℝ).IntertwiningMap
    ((CoMod.rep).tprod (CoMod.rep)) where
  toFun := fun a => a • preCoMetricVal d
  map_add' := fun x y => add_smul x y _
  map_smul' := fun m x => mul_smul m x _
  isIntertwining' M := byd:ℕM:↑(LorentzGroup d)⊢ { toFun := fun a => a • preCoMetricVal d, map_add' := ⋯, map_smul' := ⋯ } ∘ₗ
    (Representation.trivial ℝ ↑(LorentzGroup d) ℝ) M =
  (CoMod.rep.tprod CoMod.rep) M ∘ₗ { toFun := fun a => a • preCoMetricVal d, map_add' := ⋯, map_smul' := ⋯ }
    refine LinearMap.ext fun x : ℝ => ?_d:ℕM:↑(LorentzGroup d)x:ℝ⊢ ({ toFun := fun a => a • preCoMetricVal d, map_add' := ⋯, map_smul' := ⋯ } ∘ₗ
      (Representation.trivial ℝ ↑(LorentzGroup d) ℝ) M)
    x =
  ((CoMod.rep.tprod CoMod.rep) M ∘ₗ { toFun := fun a => a • preCoMetricVal d, map_add' := ⋯, map_smul' := ⋯ }) x
    simp only [LinearMap.coe_comp, Function.comp_apply]d:ℕM:↑(LorentzGroup d)x:ℝ⊢ { toFun := fun a => a • preCoMetricVal d, map_add' := ⋯, map_smul' := ⋯ }
    (((Representation.trivial ℝ ↑(LorentzGroup d) ℝ) M) x) =
  ((CoMod.rep.tprod CoMod.rep) M) ({ toFun := fun a => a • preCoMetricVal d, map_add' := ⋯, map_smul' := ⋯ } x)
    change x • preCoMetricVal d =
      (TensorProduct.map (CoMod.rep M) (CoMod.rep M)) (x • preCoMetricVal d)d:ℕM:↑(LorentzGroup d)x:ℝ⊢ x • preCoMetricVal d = (TensorProduct.map (CoMod.rep M) (CoMod.rep M)) (x • preCoMetricVal d)
    simp only [_root_.map_smul]d:ℕM:↑(LorentzGroup d)x:ℝ⊢ x • preCoMetricVal d = x • (TensorProduct.map (CoMod.rep M) (CoMod.rep M)) (preCoMetricVal d)
    apply congrArgd:ℕM:↑(LorentzGroup d)x:ℝ⊢ preCoMetricVal d = (TensorProduct.map (CoMod.rep M) (CoMod.rep M)) (preCoMetricVal d)
    simp only [preCoMetricVal]d:ℕM:↑(LorentzGroup d)x:ℝ⊢ coCoToMatrixRe.symm minkowskiMatrix =
  (TensorProduct.map (CoMod.rep M) (CoMod.rep M)) (coCoToMatrixRe.symm minkowskiMatrix)
    rw [coCoToMatrixRe_ρ_symmd:ℕM:↑(LorentzGroup d)x:ℝ⊢ coCoToMatrixRe.symm minkowskiMatrix = coCoToMatrixRe.symm ((↑M)⁻¹ᵀ * minkowskiMatrix * (↑M)⁻¹)d:ℕM:↑(LorentzGroup d)x:ℝ⊢ coCoToMatrixRe.symm minkowskiMatrix = coCoToMatrixRe.symm ((↑M)⁻¹ᵀ * minkowskiMatrix * (↑M)⁻¹)]d:ℕM:↑(LorentzGroup d)x:ℝ⊢ coCoToMatrixRe.symm minkowskiMatrix = coCoToMatrixRe.symm ((↑M)⁻¹ᵀ * minkowskiMatrix * (↑M)⁻¹)
    apply congrArgd:ℕM:↑(LorentzGroup d)x:ℝ⊢ minkowskiMatrix = (↑M)⁻¹ᵀ * minkowskiMatrix * (↑M)⁻¹
    rw [← LorentzGroup.coe_inv,d:ℕM:↑(LorentzGroup d)x:ℝ⊢ minkowskiMatrix = (↑M⁻¹)ᵀ * minkowskiMatrix * ↑M⁻¹All goals completed! 🐙 LorentzGroup.transpose_mul_minkowskiMatrix_mul_selfd:ℕM:↑(LorentzGroup d)x:ℝ⊢ minkowskiMatrix = minkowskiMatrixAll goals completed! 🐙]All goals completed! 🐙

lemma preCoMetric_apply_one {d : ℕ} : (preCoMetric d) (1 : ℝ) = preCoMetricVal d :=
  one_smul ℝ _

Metric for real Lorentz vectors

Contraction of metrics