Unit tensors for complex Lorentz tensors

Definitions.

@[reducible, inline]

abbrev complexLorentzTensor.coContrUnit : complexLorentzTensor.Tensor ![Color.down, Color.up]

The unit δᵢⁱ as a complex Lorentz tensor.

Equations

• complexLorentzTensor.coContrUnit = TensorSpecies.unitTensor complexLorentzTensor.Color.up

@[reducible, inline]

abbrev complexLorentzTensor.contrCoUnit : complexLorentzTensor.Tensor ![Color.up, Color.down]

The unit δⁱᵢ as a complex Lorentz tensor.

Equations

• complexLorentzTensor.contrCoUnit = TensorSpecies.unitTensor complexLorentzTensor.Color.down

@[reducible, inline]

abbrev complexLorentzTensor.altLeftLeftUnit : complexLorentzTensor.Tensor ![Color.downL, Color.upL]

The unit δₐᵃ as a complex Lorentz tensor.

Equations

• complexLorentzTensor.altLeftLeftUnit = TensorSpecies.unitTensor complexLorentzTensor.Color.upL

@[reducible, inline]

abbrev complexLorentzTensor.leftAltLeftUnit : complexLorentzTensor.Tensor ![Color.upL, Color.downL]

The unit δᵃₐ as a complex Lorentz tensor.

Equations

• complexLorentzTensor.leftAltLeftUnit = TensorSpecies.unitTensor complexLorentzTensor.Color.downL

@[reducible, inline]

abbrev complexLorentzTensor.altRightRightUnit : complexLorentzTensor.Tensor ![Color.downR, Color.upR]

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

Equations

• complexLorentzTensor.altRightRightUnit = TensorSpecies.unitTensor complexLorentzTensor.Color.upR

@[reducible, inline]

abbrev complexLorentzTensor.rightAltRightUnit : complexLorentzTensor.Tensor ![Color.upR, Color.downR]

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

Equations

• complexLorentzTensor.rightAltRightUnit = TensorSpecies.unitTensor complexLorentzTensor.Color.downR

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

Other forms

fromConstPair

theorem complexLorentzTensor.coContrUnit_eq_fromConstPair : coContrUnit = TensorSpecies.Tensor.fromConstPair Lorentz.coContrUnit

theorem complexLorentzTensor.contrCoUnit_eq_fromConstPair : contrCoUnit = TensorSpecies.Tensor.fromConstPair Lorentz.contrCoUnit

theorem complexLorentzTensor.altLeftLeftUnit_eq_fromConstPair : altLeftLeftUnit = TensorSpecies.Tensor.fromConstPair Fermion.altLeftLeftUnit

theorem complexLorentzTensor.leftAltLeftUnit_eq_fromConstPair : leftAltLeftUnit = TensorSpecies.Tensor.fromConstPair Fermion.leftAltLeftUnit

theorem complexLorentzTensor.altRightRightUnit_eq_fromConstPair : altRightRightUnit = TensorSpecies.Tensor.fromConstPair Fermion.altRightRightUnit

theorem complexLorentzTensor.rightAltRightUnit_eq_fromConstPair : rightAltRightUnit = TensorSpecies.Tensor.fromConstPair Fermion.rightAltRightUnit

fromPairT

theorem complexLorentzTensor.coContrUnit_eq_fromPairT : coContrUnit = TensorSpecies.Tensor.fromPairT Lorentz.coContrUnitVal

theorem complexLorentzTensor.contrCoUnit_eq_fromPairT : contrCoUnit = TensorSpecies.Tensor.fromPairT Lorentz.contrCoUnitVal

theorem complexLorentzTensor.altLeftLeftUnit_eq_fromPairT : altLeftLeftUnit = TensorSpecies.Tensor.fromPairT Fermion.altLeftLeftUnitVal

theorem complexLorentzTensor.leftAltLeftUnit_eq_fromPairT : leftAltLeftUnit = TensorSpecies.Tensor.fromPairT Fermion.leftAltLeftUnitVal

theorem complexLorentzTensor.altRightRightUnit_eq_fromPairT : altRightRightUnit = TensorSpecies.Tensor.fromPairT Fermion.altRightRightUnitVal

theorem complexLorentzTensor.rightAltRightUnit_eq_fromPairT : rightAltRightUnit = TensorSpecies.Tensor.fromPairT Fermion.rightAltRightUnitVal

complexCoBasis etc.

theorem complexLorentzTensor.coContrUnit_eq_complexCoBasis_complexContrBasis : coContrUnit = ∑ i : Fin 1 ⊕ Fin 3, TensorSpecies.Tensor.fromPairT (Lorentz.complexCoBasis i ⊗ₜ[ℂ] Lorentz.complexContrBasis i)

theorem complexLorentzTensor.coContrUnit_eq_complexCoBasisFin4_complexContrBasisFin4 : coContrUnit = ∑ i : Fin 4, TensorSpecies.Tensor.fromPairT (Lorentz.complexCoBasisFin4 i ⊗ₜ[ℂ] Lorentz.complexContrBasisFin4 i)

theorem complexLorentzTensor.contrCoUnit_eq_complexContrBasis_complexCoBasis : contrCoUnit = ∑ i : Fin 1 ⊕ Fin 3, TensorSpecies.Tensor.fromPairT (Lorentz.complexContrBasis i ⊗ₜ[ℂ] Lorentz.complexCoBasis i)

theorem complexLorentzTensor.contrCoUnit_eq_complexContrBasisFin4_complexCoBasisFin4 : contrCoUnit = ∑ i : Fin 4, TensorSpecies.Tensor.fromPairT (Lorentz.complexContrBasisFin4 i ⊗ₜ[ℂ] Lorentz.complexCoBasisFin4 i)

theorem complexLorentzTensor.altLeftLeftUnit_eq_altLeftBasis_leftBasis : altLeftLeftUnit = ∑ i : Fin 2, TensorSpecies.Tensor.fromPairT (Fermion.altLeftBasis i ⊗ₜ[ℂ] Fermion.leftBasis i)

theorem complexLorentzTensor.leftAltLeftUnit_eq_leftBasis_altLeftBasis : leftAltLeftUnit = ∑ i : Fin 2, TensorSpecies.Tensor.fromPairT (Fermion.leftBasis i ⊗ₜ[ℂ] Fermion.altLeftBasis i)

theorem complexLorentzTensor.altRightRightUnit_eq_altRightBasis_rightBasis : altRightRightUnit = ∑ i : Fin 2, TensorSpecies.Tensor.fromPairT (Fermion.altRightBasis i ⊗ₜ[ℂ] Fermion.rightBasis i)

theorem complexLorentzTensor.rightAltRightUnit_eq_rightBasis_altRightBasis : rightAltRightUnit = ∑ i : Fin 2, TensorSpecies.Tensor.fromPairT (Fermion.rightBasis i ⊗ₜ[ℂ] Fermion.altRightBasis i)

basis

theorem complexLorentzTensor.coContrUnit_eq_basis : coContrUnit = ∑ i : Fin (complexLorentzTensor.repDim (![Color.down, Color.up] 0)), (TensorSpecies.Tensor.basis ![Color.down, Color.up]) fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => i | 1 => i

theorem complexLorentzTensor.contrCoUnit_eq_basis : contrCoUnit = ∑ i : Fin (complexLorentzTensor.repDim (![Color.up, Color.down] 0)), (TensorSpecies.Tensor.basis ![Color.up, Color.down]) fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => i | 1 => i

theorem complexLorentzTensor.altLeftLeftUnit_eq_basis : altLeftLeftUnit = ∑ i : Fin (complexLorentzTensor.repDim (![Color.downL, Color.upL] 0)), (TensorSpecies.Tensor.basis ![Color.downL, Color.upL]) fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => i | 1 => i

theorem complexLorentzTensor.leftAltLeftUnit_eq_basis : leftAltLeftUnit = ∑ i : Fin (complexLorentzTensor.repDim (![Color.upL, Color.downL] 0)), (TensorSpecies.Tensor.basis ![Color.upL, Color.downL]) fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => i | 1 => i

theorem complexLorentzTensor.altRightRightUnit_eq_basis : altRightRightUnit = ∑ i : Fin (complexLorentzTensor.repDim (![Color.downR, Color.upR] 0)), (TensorSpecies.Tensor.basis ![Color.downR, Color.upR]) fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => i | 1 => i

theorem complexLorentzTensor.rightAltRightUnit_eq_basis : rightAltRightUnit = ∑ i : Fin (complexLorentzTensor.repDim (![Color.upR, Color.downR] 0)), (TensorSpecies.Tensor.basis ![Color.upR, Color.downR]) fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => i | 1 => i

ofRat

theorem complexLorentzTensor.coContrUnit_eq_ofRat : coContrUnit = ofRat fun (f : TensorSpecies.Tensor.ComponentIdx ![Color.down, Color.up]) => if f 0 = f 1 then 1 else 0

theorem complexLorentzTensor.contrCoUnit_eq_ofRat : contrCoUnit = ofRat fun (f : TensorSpecies.Tensor.ComponentIdx ![Color.up, Color.down]) => if f 0 = f 1 then 1 else 0

theorem complexLorentzTensor.altLeftLeftUnit_eq_ofRat : altLeftLeftUnit = ofRat fun (f : TensorSpecies.Tensor.ComponentIdx ![Color.downL, Color.upL]) => if f 0 = f 1 then 1 else 0

theorem complexLorentzTensor.leftAltLeftUnit_eq_ofRat : leftAltLeftUnit = ofRat fun (f : TensorSpecies.Tensor.ComponentIdx ![Color.upL, Color.downL]) => if f 0 = f 1 then 1 else 0

theorem complexLorentzTensor.altRightRightUnit_eq_ofRat : altRightRightUnit = ofRat fun (f : TensorSpecies.Tensor.ComponentIdx ![Color.downR, Color.upR]) => if f 0 = f 1 then 1 else 0

theorem complexLorentzTensor.rightAltRightUnit_eq_ofRat : rightAltRightUnit = ofRat fun (f : TensorSpecies.Tensor.ComponentIdx ![Color.upR, Color.downR]) => if f 0 = f 1 then 1 else 0

Group actions

theorem complexLorentzTensor.actionT_coContrUnit (g : Matrix.SpecialLinearGroup (Fin 2) ℂ) : g • coContrUnit = coContrUnit

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

theorem complexLorentzTensor.actionT_contrCoUnit (g : Matrix.SpecialLinearGroup (Fin 2) ℂ) : g • contrCoUnit = contrCoUnit

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

theorem complexLorentzTensor.actionT_altLeftLeftUnit (g : Matrix.SpecialLinearGroup (Fin 2) ℂ) : g • altLeftLeftUnit = altLeftLeftUnit

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

theorem complexLorentzTensor.actionT_leftAltLeftUnit (g : Matrix.SpecialLinearGroup (Fin 2) ℂ) : g • leftAltLeftUnit = leftAltLeftUnit

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

theorem complexLorentzTensor.actionT_altRightRightUnit (g : Matrix.SpecialLinearGroup (Fin 2) ℂ) : g • altRightRightUnit = altRightRightUnit

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

theorem complexLorentzTensor.actionT_rightAltRightUnit (g : Matrix.SpecialLinearGroup (Fin 2) ℂ) : g • rightAltRightUnit = rightAltRightUnit

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