Metrics as complex Lorentz tensors

Definitions.

def complexLorentzTensor.coMetric : CoeSort.coe (complexLorentzTensor.F.obj (IndexNotation.OverColor.mk ![complexLorentzTensor.Color.down, complexLorentzTensor.Color.down]))

The metric ηᵢᵢ as a complex Lorentz tensor.

Equations

• complexLorentzTensor.coMetric = (TensorTree.constTwoNodeE complexLorentzTensor complexLorentzTensor.Color.down complexLorentzTensor.Color.down Lorentz.coMetric).tensor

def complexLorentzTensor.contrMetric : CoeSort.coe (complexLorentzTensor.F.obj (IndexNotation.OverColor.mk ![complexLorentzTensor.Color.up, complexLorentzTensor.Color.up]))

The metric ηⁱⁱ as a complex Lorentz tensor.

Equations

• complexLorentzTensor.contrMetric = (TensorTree.constTwoNodeE complexLorentzTensor complexLorentzTensor.Color.up complexLorentzTensor.Color.up Lorentz.contrMetric).tensor

def complexLorentzTensor.leftMetric : CoeSort.coe (complexLorentzTensor.F.obj (IndexNotation.OverColor.mk ![complexLorentzTensor.Color.upL, complexLorentzTensor.Color.upL]))

The metric εᵃᵃ as a complex Lorentz tensor.

Equations

• complexLorentzTensor.leftMetric = (TensorTree.constTwoNodeE complexLorentzTensor complexLorentzTensor.Color.upL complexLorentzTensor.Color.upL Fermion.leftMetric).tensor

def complexLorentzTensor.rightMetric : CoeSort.coe (complexLorentzTensor.F.obj (IndexNotation.OverColor.mk ![complexLorentzTensor.Color.upR, complexLorentzTensor.Color.upR]))

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

Equations

• complexLorentzTensor.rightMetric = (TensorTree.constTwoNodeE complexLorentzTensor complexLorentzTensor.Color.upR complexLorentzTensor.Color.upR Fermion.rightMetric).tensor

def complexLorentzTensor.altLeftMetric : CoeSort.coe (complexLorentzTensor.F.obj (IndexNotation.OverColor.mk ![complexLorentzTensor.Color.downL, complexLorentzTensor.Color.downL]))

The metric εₐₐ as a complex Lorentz tensor.

Equations

• complexLorentzTensor.altLeftMetric = (TensorTree.constTwoNodeE complexLorentzTensor complexLorentzTensor.Color.downL complexLorentzTensor.Color.downL Fermion.altLeftMetric).tensor

def complexLorentzTensor.altRightMetric : CoeSort.coe (complexLorentzTensor.F.obj (IndexNotation.OverColor.mk ![complexLorentzTensor.Color.downR, complexLorentzTensor.Color.downR]))

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

Equations

• complexLorentzTensor.altRightMetric = (TensorTree.constTwoNodeE complexLorentzTensor complexLorentzTensor.Color.downR complexLorentzTensor.Color.downR Fermion.altRightMetric).tensor

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'")

Tensor nodes.

theorem complexLorentzTensor.tensorNode_coMetric : (TensorTree.tensorNode complexLorentzTensor.coMetric).tensor = (TensorTree.constTwoNodeE complexLorentzTensor complexLorentzTensor.Color.down complexLorentzTensor.Color.down Lorentz.coMetric).tensor

The definitional tensor node relation for coMetric.

theorem complexLorentzTensor.tensorNode_contrMetric : (TensorTree.tensorNode complexLorentzTensor.contrMetric).tensor = (TensorTree.constTwoNodeE complexLorentzTensor complexLorentzTensor.Color.up complexLorentzTensor.Color.up Lorentz.contrMetric).tensor

The definitional tensor node relation for contrMetric.

theorem complexLorentzTensor.tensorNode_leftMetric : (TensorTree.tensorNode complexLorentzTensor.leftMetric).tensor = (TensorTree.constTwoNodeE complexLorentzTensor complexLorentzTensor.Color.upL complexLorentzTensor.Color.upL Fermion.leftMetric).tensor

The definitional tensor node relation for leftMetric.

theorem complexLorentzTensor.tensorNode_rightMetric : (TensorTree.tensorNode complexLorentzTensor.rightMetric).tensor = (TensorTree.constTwoNodeE complexLorentzTensor complexLorentzTensor.Color.upR complexLorentzTensor.Color.upR Fermion.rightMetric).tensor

The definitional tensor node relation for rightMetric.

theorem complexLorentzTensor.tensorNode_altLeftMetric : (TensorTree.tensorNode complexLorentzTensor.altLeftMetric).tensor = (TensorTree.constTwoNodeE complexLorentzTensor complexLorentzTensor.Color.downL complexLorentzTensor.Color.downL Fermion.altLeftMetric).tensor

The definitional tensor node relation for altLeftMetric.

theorem complexLorentzTensor.tensorNode_altRightMetric : (TensorTree.tensorNode complexLorentzTensor.altRightMetric).tensor = (TensorTree.constTwoNodeE complexLorentzTensor complexLorentzTensor.Color.downR complexLorentzTensor.Color.downR Fermion.altRightMetric).tensor

The definitional tensor node relation for altRightMetric.

Group actions

theorem complexLorentzTensor.action_coMetric (g : Matrix.SpecialLinearGroup (Fin 2) ℂ) : (TensorTree.action g (TensorTree.tensorNode complexLorentzTensor.coMetric)).tensor = (TensorTree.tensorNode complexLorentzTensor.coMetric).tensor

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

theorem complexLorentzTensor.action_contrMetric (g : Matrix.SpecialLinearGroup (Fin 2) ℂ) : (TensorTree.action g (TensorTree.tensorNode complexLorentzTensor.contrMetric)).tensor = (TensorTree.tensorNode complexLorentzTensor.contrMetric).tensor

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

theorem complexLorentzTensor.action_leftMetric (g : Matrix.SpecialLinearGroup (Fin 2) ℂ) : (TensorTree.action g (TensorTree.tensorNode complexLorentzTensor.leftMetric)).tensor = (TensorTree.tensorNode complexLorentzTensor.leftMetric).tensor

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

theorem complexLorentzTensor.action_rightMetric (g : Matrix.SpecialLinearGroup (Fin 2) ℂ) : (TensorTree.action g (TensorTree.tensorNode complexLorentzTensor.rightMetric)).tensor = (TensorTree.tensorNode complexLorentzTensor.rightMetric).tensor

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

theorem complexLorentzTensor.action_altLeftMetric (g : Matrix.SpecialLinearGroup (Fin 2) ℂ) : (TensorTree.action g (TensorTree.tensorNode complexLorentzTensor.altLeftMetric)).tensor = (TensorTree.tensorNode complexLorentzTensor.altLeftMetric).tensor

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

theorem complexLorentzTensor.action_altRightMetric (g : Matrix.SpecialLinearGroup (Fin 2) ℂ) : (TensorTree.action g (TensorTree.tensorNode complexLorentzTensor.altRightMetric)).tensor = (TensorTree.tensorNode complexLorentzTensor.altRightMetric).tensor

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