Physlib.Relativity.Tensors.RealTensor.Metrics.Basic

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.Basic
public import Physlib.Relativity.Tensors.MetricTensor

Metrics as real Lorentz tensors

@[expose] public section

Definitions.

The metric ηᵢᵢ as a complex Lorentz tensor.

abbrev coMetric (d : ℕ := 3) : ℝT[d, .down, .down] :=
  (realLorentzTensor d).metricTensor .down

The metric ηⁱⁱ as a complex Lorentz tensor.

abbrev contrMetric (d : ℕ := 3) : ℝT[d, .up, .up] :=
  (realLorentzTensor d).metricTensor .up

Notation

The metric ηᵢᵢ as a complex Lorentz tensors.

scoped[realLorentzTensor] notation "η'" => @coMetric

The metric ηⁱⁱ as a complex Lorentz tensors.

scoped[realLorentzTensor] notation "η" => @contrMetric

Equivalent forms of the metrics

              lemma coMetric_eq_fromConstPair {d : ℕ} :
    η' d = fromConstPair (S := realLorentzTensor d) (c1 := .down) (c2 := .down)
      (Lorentz.preCoMetric d) := byd:ℕ⊢ coMetric d = fromConstPair (Lorentz.preCoMetric d)
  rflAll goals completed! 🐙lemma contrMetric_eq_fromConstPair {d : ℕ} :
    η d = fromConstPair (S := realLorentzTensor d)
      (c1 := .up) (c2 := .up) (Lorentz.preContrMetric d) := byd:ℕ⊢ contrMetric d = fromConstPair (Lorentz.preContrMetric d)
  rflAll goals completed! 🐙

lemma coMetric_eq_fromPairT {d : ℕ} :
    η' d = fromPairT (S := realLorentzTensor d) (c1 := .down) (c2 := .down)
      (Lorentz.preCoMetricVal d) := byd:ℕ⊢ coMetric d = fromPairT (Lorentz.preCoMetricVal d)
  rw [coMetric_eq_fromConstPair,d:ℕ⊢ fromConstPair (Lorentz.preCoMetric d) = fromPairT (Lorentz.preCoMetricVal d)All goals completed! 🐙 fromConstPair,d:ℕ⊢ fromPairT ((Lorentz.preCoMetric d) 1) = fromPairT (Lorentz.preCoMetricVal d)All goals completed! 🐙 Lorentz.preCoMetric_apply_oned:ℕ⊢ fromPairT (Lorentz.preCoMetricVal d) = fromPairT (Lorentz.preCoMetricVal d)All goals completed! 🐙]All goals completed! 🐙

lemma contrMetric_eq_fromPairT {d : ℕ} :
    η d = fromPairT (S := realLorentzTensor d) (c1 := .up) (c2 := .up)
        (Lorentz.preContrMetricVal d) := byd:ℕ⊢ contrMetric d = fromPairT (Lorentz.preContrMetricVal d)
  rw [contrMetric_eq_fromConstPair,d:ℕ⊢ fromConstPair (Lorentz.preContrMetric d) = fromPairT (Lorentz.preContrMetricVal d)All goals completed! 🐙 fromConstPair,d:ℕ⊢ fromPairT ((Lorentz.preContrMetric d) 1) = fromPairT (Lorentz.preContrMetricVal d)All goals completed! 🐙 Lorentz.preContrMetric_apply_oned:ℕ⊢ fromPairT (Lorentz.preContrMetricVal d) = fromPairT (Lorentz.preContrMetricVal d)All goals completed! 🐙]All goals completed! 🐙

The tensor coMetric is invariant under the action of LorentzGroup d.

@[simp]
lemma actionT_coMetric {d : ℕ} (g : LorentzGroup d) :
    g • η' d = η' d:= byd:ℕg:↑(LorentzGroup d)⊢ g • coMetric d = coMetric d
  erw [TensorSpecies.metricTensor_invariantd:ℕg:↑(LorentzGroup d)⊢ metricTensor Color.down = coMetric d]All goals completed! 🐙

The tensor contrMetric is invariant under the action of LorentzGroup d.

@[simp]
lemma actionT_contrMetric {d} (g : LorentzGroup d) : g • η d = η d := byd:ℕg:↑(LorentzGroup d)⊢ g • contrMetric d = contrMetric d
  erw [TensorSpecies.metricTensor_invariantd:ℕg:↑(LorentzGroup d)⊢ metricTensor Color.up = contrMetric d]All goals completed! 🐙



/-

## There value with respect to a basis

-/

lemma coMetric_repr_apply_eq_minkowskiMatrix {d : ℕ}
    (b : ComponentIdx (S := realLorentzTensor d) ![Color.down, Color.down]) :
    (Tensor.basis _).repr (coMetric d) b =
    minkowskiMatrix (b 0) (b 1) := byd:ℕb:ComponentIdx ![Color.down, Color.down]⊢ ((basis ![Color.down, Color.down]).repr (coMetric d)) b = minkowskiMatrix (b 0) (b 1)
  rw [coMetric_eq_fromPairT,d:ℕb:ComponentIdx ![Color.down, Color.down]⊢ ((basis ![Color.down, Color.down]).repr (fromPairT (Lorentz.preCoMetricVal d))) b = minkowskiMatrix (b 0) (b 1)d:ℕb:ComponentIdx ![Color.down, Color.down]⊢ (((match Color.down with
            | Color.up => Lorentz.contrBasis d
            | Color.down => Lorentz.coBasis d).tensorProduct
          (match Color.down with
          | Color.up => Lorentz.contrBasis d
          | Color.down => Lorentz.coBasis d)).repr
      (∑ i, minkowskiMatrix i i • (Lorentz.coBasis d) i ⊗ₜ[ℝ] (Lorentz.coBasis d) i))
    (b 0, b 1) =
  minkowskiMatrix (b 0) (b 1) fromPairT_basis_repr,d:ℕb:ComponentIdx ![Color.down, Color.down]⊢ (((match Color.down with
            | Color.up => Lorentz.contrBasis d
            | Color.down => Lorentz.coBasis d).tensorProduct
          (match Color.down with
          | Color.up => Lorentz.contrBasis d
          | Color.down => Lorentz.coBasis d)).repr
      (Lorentz.preCoMetricVal d))
    (b 0, b 1) =
  minkowskiMatrix (b 0) (b 1)d:ℕb:ComponentIdx ![Color.down, Color.down]⊢ (((match Color.down with
            | Color.up => Lorentz.contrBasis d
            | Color.down => Lorentz.coBasis d).tensorProduct
          (match Color.down with
          | Color.up => Lorentz.contrBasis d
          | Color.down => Lorentz.coBasis d)).repr
      (∑ i, minkowskiMatrix i i • (Lorentz.coBasis d) i ⊗ₜ[ℝ] (Lorentz.coBasis d) i))
    (b 0, b 1) =
  minkowskiMatrix (b 0) (b 1)
    Lorentz.preCoMetricVal_expand_tmul_minkowskiMatrixd:ℕb:ComponentIdx ![Color.down, Color.down]⊢ (((match Color.down with
            | Color.up => Lorentz.contrBasis d
            | Color.down => Lorentz.coBasis d).tensorProduct
          (match Color.down with
          | Color.up => Lorentz.contrBasis d
          | Color.down => Lorentz.coBasis d)).repr
      (∑ i, minkowskiMatrix i i • (Lorentz.coBasis d) i ⊗ₜ[ℝ] (Lorentz.coBasis d) i))
    (b 0, b 1) =
  minkowskiMatrix (b 0) (b 1)d:ℕb:ComponentIdx ![Color.down, Color.down]⊢ (((match Color.down with
            | Color.up => Lorentz.contrBasis d
            | Color.down => Lorentz.coBasis d).tensorProduct
          (match Color.down with
          | Color.up => Lorentz.contrBasis d
          | Color.down => Lorentz.coBasis d)).repr
      (∑ i, minkowskiMatrix i i • (Lorentz.coBasis d) i ⊗ₜ[ℝ] (Lorentz.coBasis d) i))
    (b 0, b 1) =
  minkowskiMatrix (b 0) (b 1)]d:ℕb:ComponentIdx ![Color.down, Color.down]⊢ (((match Color.down with
            | Color.up => Lorentz.contrBasis d
            | Color.down => Lorentz.coBasis d).tensorProduct
          (match Color.down with
          | Color.up => Lorentz.contrBasis d
          | Color.down => Lorentz.coBasis d)).repr
      (∑ i, minkowskiMatrix i i • (Lorentz.coBasis d) i ⊗ₜ[ℝ] (Lorentz.coBasis d) i))
    (b 0, b 1) =
  minkowskiMatrix (b 0) (b 1)
  simp only [map_sum, Finsupp.coe_finsetSum, Finset.sum_apply, map_smul, Finsupp.coe_smul,
    Pi.smul_apply, Basis.tensorProduct_repr_tmul_apply, Basis.repr_self, Finsupp.single_apply,
    smul_eq_mul]d:ℕb:ComponentIdx ![Color.down, Color.down]⊢ ∑ x, minkowskiMatrix x x * ((if x = b 1 then 1 else 0) * if x = b 0 then 1 else 0) = minkowskiMatrix (b 0) (b 1)
  rw [Finset.sum_eq_single (b 0)d:ℕb:ComponentIdx ![Color.down, Color.down]⊢ minkowskiMatrix (b 0) (b 0) * ((if b 0 = b 1 then 1 else 0) * if b 0 = b 0 then 1 else 0) = minkowskiMatrix (b 0) (b 1)h₀d:ℕb:ComponentIdx ![Color.down, Color.down]⊢ ∀ b_1 ∈ Finset.univ,
  b_1 ≠ b 0 → minkowskiMatrix b_1 b_1 * ((if b_1 = b 1 then 1 else 0) * if b_1 = b 0 then 1 else 0) = 0h₁d:ℕb:ComponentIdx ![Color.down, Color.down]⊢ b 0 ∉ Finset.univ → minkowskiMatrix (b 0) (b 0) * ((if b 0 = b 1 then 1 else 0) * if b 0 = b 0 then 1 else 0) = 0d:ℕb:ComponentIdx ![Color.down, Color.down]⊢ minkowskiMatrix (b 0) (b 0) * ((if b 0 = b 1 then 1 else 0) * if b 0 = b 0 then 1 else 0) = minkowskiMatrix (b 0) (b 1)h₀d:ℕb:ComponentIdx ![Color.down, Color.down]⊢ ∀ b_1 ∈ Finset.univ,
  b_1 ≠ b 0 → minkowskiMatrix b_1 b_1 * ((if b_1 = b 1 then 1 else 0) * if b_1 = b 0 then 1 else 0) = 0h₁d:ℕb:ComponentIdx ![Color.down, Color.down]⊢ b 0 ∉ Finset.univ → minkowskiMatrix (b 0) (b 0) * ((if b 0 = b 1 then 1 else 0) * if b 0 = b 0 then 1 else 0) = 0]d:ℕb:ComponentIdx ![Color.down, Color.down]⊢ minkowskiMatrix (b 0) (b 0) * ((if b 0 = b 1 then 1 else 0) * if b 0 = b 0 then 1 else 0) = minkowskiMatrix (b 0) (b 1)h₀d:ℕb:ComponentIdx ![Color.down, Color.down]⊢ ∀ b_1 ∈ Finset.univ,
  b_1 ≠ b 0 → minkowskiMatrix b_1 b_1 * ((if b_1 = b 1 then 1 else 0) * if b_1 = b 0 then 1 else 0) = 0h₁d:ℕb:ComponentIdx ![Color.down, Color.down]⊢ b 0 ∉ Finset.univ → minkowskiMatrix (b 0) (b 0) * ((if b 0 = b 1 then 1 else 0) * if b 0 = b 0 then 1 else 0) = 0 <;>d:ℕb:ComponentIdx ![Color.down, Color.down]⊢ minkowskiMatrix (b 0) (b 0) * ((if b 0 = b 1 then 1 else 0) * if b 0 = b 0 then 1 else 0) = minkowskiMatrix (b 0) (b 1)h₀d:ℕb:ComponentIdx ![Color.down, Color.down]⊢ ∀ b_1 ∈ Finset.univ,
  b_1 ≠ b 0 → minkowskiMatrix b_1 b_1 * ((if b_1 = b 1 then 1 else 0) * if b_1 = b 0 then 1 else 0) = 0h₁d:ℕb:ComponentIdx ![Color.down, Color.down]⊢ b 0 ∉ Finset.univ → minkowskiMatrix (b 0) (b 0) * ((if b 0 = b 1 then 1 else 0) * if b 0 = b 0 then 1 else 0) = 0
    simp +contextual [minkowskiMatrix.as_diagonal, Matrix.diagonal_apply]All goals completed! 🐙



lemma contrMetric_repr_apply_eq_minkowskiMatrix {d : ℕ}
    (b : ComponentIdx (S := realLorentzTensor d) ![Color.up, Color.up]) :
    (Tensor.basis _).repr (contrMetric d) b =
    minkowskiMatrix (b 0) (b 1) := byd:ℕb:ComponentIdx ![Color.up, Color.up]⊢ ((basis ![Color.up, Color.up]).repr (contrMetric d)) b = minkowskiMatrix (b 0) (b 1)
  rw [contrMetric_eq_fromPairT,d:ℕb:ComponentIdx ![Color.up, Color.up]⊢ ((basis ![Color.up, Color.up]).repr (fromPairT (Lorentz.preContrMetricVal d))) b = minkowskiMatrix (b 0) (b 1)d:ℕb:ComponentIdx ![Color.up, Color.up]⊢ (((match Color.up with
            | Color.up => Lorentz.contrBasis d
            | Color.down => Lorentz.coBasis d).tensorProduct
          (match Color.up with
          | Color.up => Lorentz.contrBasis d
          | Color.down => Lorentz.coBasis d)).repr
      (∑ i, minkowskiMatrix i i • (Lorentz.contrBasis d) i ⊗ₜ[ℝ] (Lorentz.contrBasis d) i))
    (b 0, b 1) =
  minkowskiMatrix (b 0) (b 1) fromPairT_basis_repr,d:ℕb:ComponentIdx ![Color.up, Color.up]⊢ (((match Color.up with
            | Color.up => Lorentz.contrBasis d
            | Color.down => Lorentz.coBasis d).tensorProduct
          (match Color.up with
          | Color.up => Lorentz.contrBasis d
          | Color.down => Lorentz.coBasis d)).repr
      (Lorentz.preContrMetricVal d))
    (b 0, b 1) =
  minkowskiMatrix (b 0) (b 1)d:ℕb:ComponentIdx ![Color.up, Color.up]⊢ (((match Color.up with
            | Color.up => Lorentz.contrBasis d
            | Color.down => Lorentz.coBasis d).tensorProduct
          (match Color.up with
          | Color.up => Lorentz.contrBasis d
          | Color.down => Lorentz.coBasis d)).repr
      (∑ i, minkowskiMatrix i i • (Lorentz.contrBasis d) i ⊗ₜ[ℝ] (Lorentz.contrBasis d) i))
    (b 0, b 1) =
  minkowskiMatrix (b 0) (b 1)
    Lorentz.preContrMetricVal_expand_tmul_minkowskiMatrixd:ℕb:ComponentIdx ![Color.up, Color.up]⊢ (((match Color.up with
            | Color.up => Lorentz.contrBasis d
            | Color.down => Lorentz.coBasis d).tensorProduct
          (match Color.up with
          | Color.up => Lorentz.contrBasis d
          | Color.down => Lorentz.coBasis d)).repr
      (∑ i, minkowskiMatrix i i • (Lorentz.contrBasis d) i ⊗ₜ[ℝ] (Lorentz.contrBasis d) i))
    (b 0, b 1) =
  minkowskiMatrix (b 0) (b 1)d:ℕb:ComponentIdx ![Color.up, Color.up]⊢ (((match Color.up with
            | Color.up => Lorentz.contrBasis d
            | Color.down => Lorentz.coBasis d).tensorProduct
          (match Color.up with
          | Color.up => Lorentz.contrBasis d
          | Color.down => Lorentz.coBasis d)).repr
      (∑ i, minkowskiMatrix i i • (Lorentz.contrBasis d) i ⊗ₜ[ℝ] (Lorentz.contrBasis d) i))
    (b 0, b 1) =
  minkowskiMatrix (b 0) (b 1)]d:ℕb:ComponentIdx ![Color.up, Color.up]⊢ (((match Color.up with
            | Color.up => Lorentz.contrBasis d
            | Color.down => Lorentz.coBasis d).tensorProduct
          (match Color.up with
          | Color.up => Lorentz.contrBasis d
          | Color.down => Lorentz.coBasis d)).repr
      (∑ i, minkowskiMatrix i i • (Lorentz.contrBasis d) i ⊗ₜ[ℝ] (Lorentz.contrBasis d) i))
    (b 0, b 1) =
  minkowskiMatrix (b 0) (b 1)
  simp only [map_sum, Finsupp.coe_finsetSum, Finset.sum_apply, map_smul, Finsupp.coe_smul,
    Pi.smul_apply, Basis.tensorProduct_repr_tmul_apply, Basis.repr_self, Finsupp.single_apply,
    smul_eq_mul]d:ℕb:ComponentIdx ![Color.up, Color.up]⊢ ∑ x, minkowskiMatrix x x * ((if x = b 1 then 1 else 0) * if x = b 0 then 1 else 0) = minkowskiMatrix (b 0) (b 1)
  rw [Finset.sum_eq_single (b 0)d:ℕb:ComponentIdx ![Color.up, Color.up]⊢ minkowskiMatrix (b 0) (b 0) * ((if b 0 = b 1 then 1 else 0) * if b 0 = b 0 then 1 else 0) = minkowskiMatrix (b 0) (b 1)h₀d:ℕb:ComponentIdx ![Color.up, Color.up]⊢ ∀ b_1 ∈ Finset.univ,
  b_1 ≠ b 0 → minkowskiMatrix b_1 b_1 * ((if b_1 = b 1 then 1 else 0) * if b_1 = b 0 then 1 else 0) = 0h₁d:ℕb:ComponentIdx ![Color.up, Color.up]⊢ b 0 ∉ Finset.univ → minkowskiMatrix (b 0) (b 0) * ((if b 0 = b 1 then 1 else 0) * if b 0 = b 0 then 1 else 0) = 0d:ℕb:ComponentIdx ![Color.up, Color.up]⊢ minkowskiMatrix (b 0) (b 0) * ((if b 0 = b 1 then 1 else 0) * if b 0 = b 0 then 1 else 0) = minkowskiMatrix (b 0) (b 1)h₀d:ℕb:ComponentIdx ![Color.up, Color.up]⊢ ∀ b_1 ∈ Finset.univ,
  b_1 ≠ b 0 → minkowskiMatrix b_1 b_1 * ((if b_1 = b 1 then 1 else 0) * if b_1 = b 0 then 1 else 0) = 0h₁d:ℕb:ComponentIdx ![Color.up, Color.up]⊢ b 0 ∉ Finset.univ → minkowskiMatrix (b 0) (b 0) * ((if b 0 = b 1 then 1 else 0) * if b 0 = b 0 then 1 else 0) = 0]d:ℕb:ComponentIdx ![Color.up, Color.up]⊢ minkowskiMatrix (b 0) (b 0) * ((if b 0 = b 1 then 1 else 0) * if b 0 = b 0 then 1 else 0) = minkowskiMatrix (b 0) (b 1)h₀d:ℕb:ComponentIdx ![Color.up, Color.up]⊢ ∀ b_1 ∈ Finset.univ,
  b_1 ≠ b 0 → minkowskiMatrix b_1 b_1 * ((if b_1 = b 1 then 1 else 0) * if b_1 = b 0 then 1 else 0) = 0h₁d:ℕb:ComponentIdx ![Color.up, Color.up]⊢ b 0 ∉ Finset.univ → minkowskiMatrix (b 0) (b 0) * ((if b 0 = b 1 then 1 else 0) * if b 0 = b 0 then 1 else 0) = 0 <;>d:ℕb:ComponentIdx ![Color.up, Color.up]⊢ minkowskiMatrix (b 0) (b 0) * ((if b 0 = b 1 then 1 else 0) * if b 0 = b 0 then 1 else 0) = minkowskiMatrix (b 0) (b 1)h₀d:ℕb:ComponentIdx ![Color.up, Color.up]⊢ ∀ b_1 ∈ Finset.univ,
  b_1 ≠ b 0 → minkowskiMatrix b_1 b_1 * ((if b_1 = b 1 then 1 else 0) * if b_1 = b 0 then 1 else 0) = 0h₁d:ℕb:ComponentIdx ![Color.up, Color.up]⊢ b 0 ∉ Finset.univ → minkowskiMatrix (b 0) (b 0) * ((if b 0 = b 1 then 1 else 0) * if b 0 = b 0 then 1 else 0) = 0
    simp +contextual [minkowskiMatrix.as_diagonal, Matrix.diagonal_apply]All goals completed! 🐙