Metrics as complex Lorentz tensors

Definitions.

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

The unit δᵢⁱ as a complex Lorentz tensor.

Equations

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

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

The unit δⁱᵢ as a complex Lorentz tensor.

Equations

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

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

The unit δₐᵃ as a complex Lorentz tensor.

Equations

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

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

The unit δᵃₐ as a complex Lorentz tensor.

Equations

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

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

The unit δ_{dot a}^{dot a} as a complex Lorentz tensor.

Equations

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

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

The unit δ^{dot a}_{dot a} as a complex Lorentz tensor.

Equations

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

Notation

def complexLorentzTensor.termδ' : Lean.ParserDescr

The unit δᵢⁱ as a complex Lorentz tensor.

Equations

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

def complexLorentzTensor.termδ : Lean.ParserDescr

The unit δⁱᵢ as a complex Lorentz tensor.

Equations

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

def complexLorentzTensor.termδL' : Lean.ParserDescr

The unit δₐᵃ as a complex Lorentz tensor.

Equations

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

def complexLorentzTensor.termδL : Lean.ParserDescr

The unit δᵃₐ as a complex Lorentz tensor.

Equations

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

def complexLorentzTensor.termδR' : Lean.ParserDescr

The unit δ_{dot a}^{dot a} as a complex Lorentz tensor.

Equations

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

def complexLorentzTensor.termδR : Lean.ParserDescr

The unit δ^{dot a}_{dot a} as a complex Lorentz tensor.

Equations

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

Tensor nodes.

theorem complexLorentzTensor.tensorNode_coContrUnit : (TensorTree.tensorNode complexLorentzTensor.coContrUnit).tensor = (TensorTree.constTwoNodeE complexLorentzTensor complexLorentzTensor.Color.down complexLorentzTensor.Color.up Lorentz.coContrUnit).tensor

The definitional tensor node relation for coContrUnit.

theorem complexLorentzTensor.tensorNode_contrCoUnit : (TensorTree.tensorNode complexLorentzTensor.contrCoUnit).tensor = (TensorTree.constTwoNodeE complexLorentzTensor complexLorentzTensor.Color.up complexLorentzTensor.Color.down Lorentz.contrCoUnit).tensor

The definitional tensor node relation for contrCoUnit.

theorem complexLorentzTensor.tensorNode_altLeftLeftUnit : (TensorTree.tensorNode complexLorentzTensor.altLeftLeftUnit).tensor = (TensorTree.constTwoNodeE complexLorentzTensor complexLorentzTensor.Color.downL complexLorentzTensor.Color.upL Fermion.altLeftLeftUnit).tensor

The definitional tensor node relation for altLeftLeftUnit.

theorem complexLorentzTensor.tensorNode_leftAltLeftUnit : (TensorTree.tensorNode complexLorentzTensor.leftAltLeftUnit).tensor = (TensorTree.constTwoNodeE complexLorentzTensor complexLorentzTensor.Color.upL complexLorentzTensor.Color.downL Fermion.leftAltLeftUnit).tensor

The definitional tensor node relation for leftAltLeftUnit.

theorem complexLorentzTensor.tensorNode_altRightRightUnit : (TensorTree.tensorNode complexLorentzTensor.altRightRightUnit).tensor = (TensorTree.constTwoNodeE complexLorentzTensor complexLorentzTensor.Color.downR complexLorentzTensor.Color.upR Fermion.altRightRightUnit).tensor

The definitional tensor node relation for altRightRightUnit.

theorem complexLorentzTensor.tensorNode_rightAltRightUnit : (TensorTree.tensorNode complexLorentzTensor.rightAltRightUnit).tensor = (TensorTree.constTwoNodeE complexLorentzTensor complexLorentzTensor.Color.upR complexLorentzTensor.Color.downR Fermion.rightAltRightUnit).tensor

The definitional tensor node relation for rightAltRightUnit.

Group actions

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

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

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

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

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

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

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

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

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

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

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

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