Metrics as complex Lorentz tensors

Definitions.

@[reducible, inline]

abbrev complexLorentzTensor.coMetric : complexLorentzTensor.Tensor ![Color.down, Color.down]

The metric ηᵢᵢ as a complex Lorentz tensor.

Equations

• complexLorentzTensor.coMetric = TensorSpecies.metricTensor complexLorentzTensor.Color.down

@[reducible, inline]

abbrev complexLorentzTensor.contrMetric : complexLorentzTensor.Tensor ![Color.up, Color.up]

The metric ηⁱⁱ as a complex Lorentz tensor.

Equations

• complexLorentzTensor.contrMetric = TensorSpecies.metricTensor complexLorentzTensor.Color.up

@[reducible, inline]

abbrev complexLorentzTensor.leftMetric : complexLorentzTensor.Tensor ![Color.upL, Color.upL]

The metric εᵃᵃ as a complex Lorentz tensor.

Equations

• complexLorentzTensor.leftMetric = TensorSpecies.metricTensor complexLorentzTensor.Color.upL

@[reducible, inline]

abbrev complexLorentzTensor.rightMetric : complexLorentzTensor.Tensor ![Color.upR, Color.upR]

The metric ε^{dot a}^{dot a} as a complex Lorentz tensor.

Equations

• complexLorentzTensor.rightMetric = TensorSpecies.metricTensor complexLorentzTensor.Color.upR

@[reducible, inline]

abbrev complexLorentzTensor.altLeftMetric : complexLorentzTensor.Tensor ![Color.downL, Color.downL]

The metric εₐₐ as a complex Lorentz tensor.

Equations

• complexLorentzTensor.altLeftMetric = TensorSpecies.metricTensor complexLorentzTensor.Color.downL

@[reducible, inline]

abbrev complexLorentzTensor.altRightMetric : complexLorentzTensor.Tensor ![Color.downR, Color.downR]

The metric ε_{dot a}_{dot a} as a complex Lorentz tensor.

Equations

• complexLorentzTensor.altRightMetric = TensorSpecies.metricTensor complexLorentzTensor.Color.downR

Notation

def complexLorentzTensor.termη' : Lean.ParserDescr

The metric ηᵢᵢ as a complex Lorentz tensors.

Equations

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

def complexLorentzTensor.termη : Lean.ParserDescr

The metric ηⁱⁱ as a complex Lorentz tensors.

Equations

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

def complexLorentzTensor.termεL : Lean.ParserDescr

The metric εᵃᵃ as a complex Lorentz tensors.

Equations

• complexLorentzTensor.termεL = Lean.ParserDescr.node `complexLorentzTensor.termεL 1024 (Lean.ParserDescr.symbol "εL")

def complexLorentzTensor.termεR : Lean.ParserDescr

The metric ε^{dot a}^{dot a} as a complex Lorentz tensors.

Equations

• complexLorentzTensor.termεR = Lean.ParserDescr.node `complexLorentzTensor.termεR 1024 (Lean.ParserDescr.symbol "εR")

def complexLorentzTensor.termεL' : Lean.ParserDescr

The metric εₐₐ as a complex Lorentz tensors.

Equations

• complexLorentzTensor.termεL' = Lean.ParserDescr.node `complexLorentzTensor.termεL' 1024 (Lean.ParserDescr.symbol "εL'")

def complexLorentzTensor.termεR' : Lean.ParserDescr

The metric ε_{dot a}_{dot a} as a complex Lorentz tensors.

Equations

• complexLorentzTensor.termεR' = Lean.ParserDescr.node `complexLorentzTensor.termεR' 1024 (Lean.ParserDescr.symbol "εR'")

Other forms

fromConstPair

theorem complexLorentzTensor.coMetric_eq_fromConstPair : coMetric = TensorSpecies.Tensor.fromConstPair Lorentz.coMetric

theorem complexLorentzTensor.contrMetric_eq_fromConstPair : contrMetric = TensorSpecies.Tensor.fromConstPair Lorentz.contrMetric

theorem complexLorentzTensor.leftMetric_eq_fromConstPair : leftMetric = TensorSpecies.Tensor.fromConstPair Fermion.leftMetric

theorem complexLorentzTensor.rightMetric_eq_fromConstPair : rightMetric = TensorSpecies.Tensor.fromConstPair Fermion.rightMetric

theorem complexLorentzTensor.altLeftMetric_eq_fromConstPair : altLeftMetric = TensorSpecies.Tensor.fromConstPair Fermion.altLeftMetric

theorem complexLorentzTensor.altRightMetric_eq_fromConstPair : altRightMetric = TensorSpecies.Tensor.fromConstPair Fermion.altRightMetric

fromPairT

theorem complexLorentzTensor.coMetric_eq_fromPairT : coMetric = TensorSpecies.Tensor.fromPairT Lorentz.coMetricVal

theorem complexLorentzTensor.contrMetric_eq_fromPairT : contrMetric = TensorSpecies.Tensor.fromPairT Lorentz.contrMetricVal

theorem complexLorentzTensor.leftMetric_eq_fromPairT : leftMetric = TensorSpecies.Tensor.fromPairT Fermion.leftMetricVal

theorem complexLorentzTensor.rightMetric_eq_fromPairT : rightMetric = TensorSpecies.Tensor.fromPairT Fermion.rightMetricVal

theorem complexLorentzTensor.altLeftMetric_eq_fromPairT : altLeftMetric = TensorSpecies.Tensor.fromPairT Fermion.altLeftMetricVal

theorem complexLorentzTensor.altRightMetric_eq_fromPairT : altRightMetric = TensorSpecies.Tensor.fromPairT Fermion.altRightMetricVal

complexCoBasis etc.

theorem complexLorentzTensor.coMetric_eq_complexCoBasis : coMetric = TensorSpecies.Tensor.fromPairT (Lorentz.complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] Lorentz.complexCoBasis (Sum.inl 0)) - TensorSpecies.Tensor.fromPairT (Lorentz.complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] Lorentz.complexCoBasis (Sum.inr 0)) - TensorSpecies.Tensor.fromPairT (Lorentz.complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] Lorentz.complexCoBasis (Sum.inr 1)) - TensorSpecies.Tensor.fromPairT (Lorentz.complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] Lorentz.complexCoBasis (Sum.inr 2))

theorem complexLorentzTensor.coMetric_eq_complexCoBasisFin4 : coMetric = TensorSpecies.Tensor.fromPairT (Lorentz.complexCoBasisFin4 0 ⊗ₜ[ℂ] Lorentz.complexCoBasisFin4 0) - TensorSpecies.Tensor.fromPairT (Lorentz.complexCoBasisFin4 1 ⊗ₜ[ℂ] Lorentz.complexCoBasisFin4 1) - TensorSpecies.Tensor.fromPairT (Lorentz.complexCoBasisFin4 2 ⊗ₜ[ℂ] Lorentz.complexCoBasisFin4 2) - TensorSpecies.Tensor.fromPairT (Lorentz.complexCoBasisFin4 3 ⊗ₜ[ℂ] Lorentz.complexCoBasisFin4 3)

theorem complexLorentzTensor.contrMetric_eq_complexContrBasis : contrMetric = TensorSpecies.Tensor.fromPairT (Lorentz.complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] Lorentz.complexContrBasis (Sum.inl 0)) - TensorSpecies.Tensor.fromPairT (Lorentz.complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] Lorentz.complexContrBasis (Sum.inr 0)) - TensorSpecies.Tensor.fromPairT (Lorentz.complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] Lorentz.complexContrBasis (Sum.inr 1)) - TensorSpecies.Tensor.fromPairT (Lorentz.complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] Lorentz.complexContrBasis (Sum.inr 2))

theorem complexLorentzTensor.contrMetric_eq_complexContrBasisFin4 : contrMetric = TensorSpecies.Tensor.fromPairT (Lorentz.complexContrBasisFin4 0 ⊗ₜ[ℂ] Lorentz.complexContrBasisFin4 0) - TensorSpecies.Tensor.fromPairT (Lorentz.complexContrBasisFin4 1 ⊗ₜ[ℂ] Lorentz.complexContrBasisFin4 1) - TensorSpecies.Tensor.fromPairT (Lorentz.complexContrBasisFin4 2 ⊗ₜ[ℂ] Lorentz.complexContrBasisFin4 2) - TensorSpecies.Tensor.fromPairT (Lorentz.complexContrBasisFin4 3 ⊗ₜ[ℂ] Lorentz.complexContrBasisFin4 3)

theorem complexLorentzTensor.leftMetric_eq_leftBasis : leftMetric = -TensorSpecies.Tensor.fromPairT (Fermion.leftBasis 0 ⊗ₜ[ℂ] Fermion.leftBasis 1) + TensorSpecies.Tensor.fromPairT (Fermion.leftBasis 1 ⊗ₜ[ℂ] Fermion.leftBasis 0)

theorem complexLorentzTensor.altLeftMetric_eq_altLeftBasis : altLeftMetric = TensorSpecies.Tensor.fromPairT (Fermion.altLeftBasis 0 ⊗ₜ[ℂ] Fermion.altLeftBasis 1) - TensorSpecies.Tensor.fromPairT (Fermion.altLeftBasis 1 ⊗ₜ[ℂ] Fermion.altLeftBasis 0)

theorem complexLorentzTensor.rightMetric_eq_rightBasis : rightMetric = -TensorSpecies.Tensor.fromPairT (Fermion.rightBasis 0 ⊗ₜ[ℂ] Fermion.rightBasis 1) + TensorSpecies.Tensor.fromPairT (Fermion.rightBasis 1 ⊗ₜ[ℂ] Fermion.rightBasis 0)

theorem complexLorentzTensor.altRightMetric_eq_altRightBasis : altRightMetric = TensorSpecies.Tensor.fromPairT (Fermion.altRightBasis 0 ⊗ₜ[ℂ] Fermion.altRightBasis 1) - TensorSpecies.Tensor.fromPairT (Fermion.altRightBasis 1 ⊗ₜ[ℂ] Fermion.altRightBasis 0)

basis

theorem complexLorentzTensor.coMetric_eq_basis : coMetric = ((((TensorSpecies.Tensor.basis ![Color.down, Color.down]) fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => 0 | 1 => 0) - (TensorSpecies.Tensor.basis ![Color.down, Color.down]) fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => 1 | 1 => 1) - (TensorSpecies.Tensor.basis ![Color.down, Color.down]) fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => 2 | 1 => 2) - (TensorSpecies.Tensor.basis ![Color.down, Color.down]) fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => 3 | 1 => 3

theorem complexLorentzTensor.contrMetric_eq_basis : contrMetric = ((((TensorSpecies.Tensor.basis ![Color.up, Color.up]) fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => 0 | 1 => 0) - (TensorSpecies.Tensor.basis ![Color.up, Color.up]) fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => 1 | 1 => 1) - (TensorSpecies.Tensor.basis ![Color.up, Color.up]) fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => 2 | 1 => 2) - (TensorSpecies.Tensor.basis ![Color.up, Color.up]) fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => 3 | 1 => 3

theorem complexLorentzTensor.leftMetric_eq_basis : leftMetric = (-(TensorSpecies.Tensor.basis ![Color.upL, Color.upL]) fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => 0 | 1 => 1) + (TensorSpecies.Tensor.basis ![Color.upL, Color.upL]) fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => 1 | 1 => 0

theorem complexLorentzTensor.altLeftMetric_eq_basis : altLeftMetric = ((TensorSpecies.Tensor.basis ![Color.downL, Color.downL]) fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => 0 | 1 => 1) - (TensorSpecies.Tensor.basis ![Color.downL, Color.downL]) fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => 1 | 1 => 0

theorem complexLorentzTensor.rightMetric_eq_basis : rightMetric = (-(TensorSpecies.Tensor.basis ![Color.upR, Color.upR]) fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => 0 | 1 => 1) + (TensorSpecies.Tensor.basis ![Color.upR, Color.upR]) fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => 1 | 1 => 0

theorem complexLorentzTensor.altRightMetric_eq_basis : altRightMetric = ((TensorSpecies.Tensor.basis ![Color.downR, Color.downR]) fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => 0 | 1 => 1) - (TensorSpecies.Tensor.basis ![Color.downR, Color.downR]) fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => 1 | 1 => 0

ofRat

theorem complexLorentzTensor.coMetric_eq_ofRat : coMetric = ofRat fun (f : TensorSpecies.Tensor.ComponentIdx ![Color.down, Color.down]) => if f 0 = 0 ∧ f 1 = 0 then 1 else if f 0 = f 1 then -1 else 0

theorem complexLorentzTensor.contrMetric_eq_ofRat : contrMetric = ofRat fun (f : TensorSpecies.Tensor.ComponentIdx ![Color.up, Color.up]) => if f 0 = 0 ∧ f 1 = 0 then 1 else if f 0 = f 1 then -1 else 0

theorem complexLorentzTensor.leftMetric_eq_ofRat : leftMetric = ofRat fun (f : TensorSpecies.Tensor.ComponentIdx ![Color.upL, Color.upL]) => if f 0 = 0 ∧ f 1 = 1 then -1 else if f 1 = 0 ∧ f 0 = 1 then 1 else 0

theorem complexLorentzTensor.altLeftMetric_eq_ofRat : altLeftMetric = ofRat fun (f : TensorSpecies.Tensor.ComponentIdx ![Color.downL, Color.downL]) => if f 0 = 0 ∧ f 1 = 1 then 1 else if f 1 = 0 ∧ f 0 = 1 then -1 else 0

theorem complexLorentzTensor.rightMetric_eq_ofRat : rightMetric = ofRat fun (f : TensorSpecies.Tensor.ComponentIdx ![Color.upR, Color.upR]) => if f 0 = 0 ∧ f 1 = 1 then -1 else if f 1 = 0 ∧ f 0 = 1 then 1 else 0

theorem complexLorentzTensor.altRightMetric_eq_ofRat : altRightMetric = ofRat fun (f : TensorSpecies.Tensor.ComponentIdx ![Color.downR, Color.downR]) => if f 0 = 0 ∧ f 1 = 1 then 1 else if f 1 = 0 ∧ f 0 = 1 then -1 else 0

Group actions

theorem complexLorentzTensor.actionT_coMetric (g : Matrix.SpecialLinearGroup (Fin 2) ℂ) : g • coMetric = coMetric

The tensor coMetric is invariant under the action of SL(2,ℂ).

theorem complexLorentzTensor.actionT_contrMetric (g : Matrix.SpecialLinearGroup (Fin 2) ℂ) : g • contrMetric = contrMetric

The tensor contrMetric is invariant under the action of SL(2,ℂ).

theorem complexLorentzTensor.actionT_leftMetric (g : Matrix.SpecialLinearGroup (Fin 2) ℂ) : g • leftMetric = leftMetric

The tensor leftMetric is invariant under the action of SL(2,ℂ).

theorem complexLorentzTensor.actionT_rightMetric (g : Matrix.SpecialLinearGroup (Fin 2) ℂ) : g • rightMetric = rightMetric

The tensor rightMetric is invariant under the action of SL(2,ℂ).

theorem complexLorentzTensor.actionT_altLeftMetric (g : Matrix.SpecialLinearGroup (Fin 2) ℂ) : g • altLeftMetric = altLeftMetric

The tensor altLeftMetric is invariant under the action of SL(2,ℂ).

theorem complexLorentzTensor.actionT_altRightMetric (g : Matrix.SpecialLinearGroup (Fin 2) ℂ) : g • altRightMetric = altRightMetric

The tensor altRightMetric is invariant under the action of SL(2,ℂ).