Metrics as real Lorentz tensors

Definitions.

@[reducible, inline]

abbrev realLorentzTensor.coMetric (d : ℕ := 3) : (realLorentzTensor d).Tensor ![Color.down, Color.down]

The metric ηᵢᵢ as a complex Lorentz tensor.

Equations

• realLorentzTensor.coMetric d = TensorSpecies.metricTensor realLorentzTensor.Color.down

@[reducible, inline]

abbrev realLorentzTensor.contrMetric (d : ℕ := 3) : (realLorentzTensor d).Tensor ![Color.up, Color.up]

The metric ηⁱⁱ as a complex Lorentz tensor.

Equations

• realLorentzTensor.contrMetric d = TensorSpecies.metricTensor realLorentzTensor.Color.up

Notation

def realLorentzTensor.termη' : Lean.ParserDescr

The metric ηᵢᵢ as a complex Lorentz tensors.

Equations

• realLorentzTensor.termη' = Lean.ParserDescr.node `realLorentzTensor.termη' 1024 (Lean.ParserDescr.symbol "η'")

def realLorentzTensor.termη : Lean.ParserDescr

The metric ηⁱⁱ as a complex Lorentz tensors.

Equations

• realLorentzTensor.termη = Lean.ParserDescr.node `realLorentzTensor.termη 1024 (Lean.ParserDescr.symbol "η")

Equivalent forms of the metrics

theorem realLorentzTensor.coMetric_eq_fromConstPair {d : ℕ} : coMetric d = TensorSpecies.Tensor.fromConstPair (Lorentz.preCoMetric d)

theorem realLorentzTensor.contrMetric_eq_fromConstPair {d : ℕ} : contrMetric d = TensorSpecies.Tensor.fromConstPair (Lorentz.preContrMetric d)

theorem realLorentzTensor.coMetric_eq_fromPairT {d : ℕ} : coMetric d = TensorSpecies.Tensor.fromPairT (Lorentz.preCoMetricVal d)

theorem realLorentzTensor.contrMetric_eq_fromPairT {d : ℕ} : contrMetric d = TensorSpecies.Tensor.fromPairT (Lorentz.preContrMetricVal d)

@[simp]

theorem realLorentzTensor.actionT_coMetric {d : ℕ} (g : ↑(LorentzGroup d)) : g • coMetric d = coMetric d

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

@[simp]

theorem realLorentzTensor.actionT_contrMetric {d : ℕ} (g : ↑(LorentzGroup d)) : g • contrMetric d = contrMetric d

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

theorem realLorentzTensor.coMetric_repr_apply_eq_minkowskiMatrix {d : ℕ} (b : TensorSpecies.Tensor.ComponentIdx ![Color.down, Color.down]) : ((TensorSpecies.Tensor.basis ![Color.down, Color.down]).repr (coMetric d)) b = minkowskiMatrix (finSumFinEquiv.symm (b 0)) (finSumFinEquiv.symm (b 1))

theorem realLorentzTensor.contrMetric_repr_apply_eq_minkowskiMatrix {d : ℕ} (b : TensorSpecies.Tensor.ComponentIdx ![Color.up, Color.up]) : ((TensorSpecies.Tensor.basis ![Color.up, Color.up]).repr (contrMetric d)) b = minkowskiMatrix (finSumFinEquiv.symm (b 0)) (finSumFinEquiv.symm (b 1))