Basis of units

Expansion of units in terms of the tensor basis.

theorem complexLorentzTensor.coContrUnit_tensorBasis : coContrUnit = ((((complexLorentzTensor.tensorBasis ![Color.down, Color.up]) fun (x : Fin (Nat.succ 0).succ) => 0) + (complexLorentzTensor.tensorBasis ![Color.down, Color.up]) fun (x : Fin (Nat.succ 0).succ) => 1) + (complexLorentzTensor.tensorBasis ![Color.down, Color.up]) fun (x : Fin (Nat.succ 0).succ) => 2) + (complexLorentzTensor.tensorBasis ![Color.down, Color.up]) fun (x : Fin (Nat.succ 0).succ) => 3

theorem complexLorentzTensor.contrCoUnit_tensorBasis : contrCoUnit = ((((complexLorentzTensor.tensorBasis ![Color.up, Color.down]) fun (x : Fin (Nat.succ 0).succ) => 0) + (complexLorentzTensor.tensorBasis ![Color.up, Color.down]) fun (x : Fin (Nat.succ 0).succ) => 1) + (complexLorentzTensor.tensorBasis ![Color.up, Color.down]) fun (x : Fin (Nat.succ 0).succ) => 2) + (complexLorentzTensor.tensorBasis ![Color.up, Color.down]) fun (x : Fin (Nat.succ 0).succ) => 3

theorem complexLorentzTensor.altLeftLeftUnit_tensorBasis : altLeftLeftUnit = ((complexLorentzTensor.tensorBasis ![Color.downL, Color.upL]) fun (x : Fin (Nat.succ 0).succ) => 0) + (complexLorentzTensor.tensorBasis ![Color.downL, Color.upL]) fun (x : Fin (Nat.succ 0).succ) => 1

theorem complexLorentzTensor.leftAltLeftUnit_tensorBasis : leftAltLeftUnit = ((complexLorentzTensor.tensorBasis ![Color.upL, Color.downL]) fun (x : Fin (Nat.succ 0).succ) => 0) + (complexLorentzTensor.tensorBasis ![Color.upL, Color.downL]) fun (x : Fin (Nat.succ 0).succ) => 1

theorem complexLorentzTensor.altRightRightUnit_tensorBasis : altRightRightUnit = ((complexLorentzTensor.tensorBasis ![Color.downR, Color.upR]) fun (x : Fin (Nat.succ 0).succ) => 0) + (complexLorentzTensor.tensorBasis ![Color.downR, Color.upR]) fun (x : Fin (Nat.succ 0).succ) => 1

theorem complexLorentzTensor.rightAltRightUnit_tensorBasis : rightAltRightUnit = ((complexLorentzTensor.tensorBasis ![Color.upR, Color.downR]) fun (x : Fin (Nat.succ 0).succ) => 0) + (complexLorentzTensor.tensorBasis ![Color.upR, Color.downR]) fun (x : Fin (Nat.succ 0).succ) => 1

As rationals tensors

theorem complexLorentzTensor.coContrUnit_eq_ofRat : coContrUnit = ofRat fun (f : (j : Fin (Nat.succ 0).succ) → Fin (complexLorentzTensor.repDim (![Color.down, Color.up] j))) => if f 0 = f 1 then 1 else 0

theorem complexLorentzTensor.contrCoUnit_eq_ofRat : contrCoUnit = ofRat fun (f : (j : Fin (Nat.succ 0).succ) → Fin (complexLorentzTensor.repDim (![Color.up, Color.down] j))) => if f 0 = f 1 then 1 else 0

theorem complexLorentzTensor.altLeftLeftUnit_eq_ofRat : altLeftLeftUnit = ofRat fun (f : (j : Fin (Nat.succ 0).succ) → Fin (complexLorentzTensor.repDim (![Color.downL, Color.upL] j))) => if f 0 = f 1 then 1 else 0

theorem complexLorentzTensor.leftAltLeftUnit_eq_ofRat : leftAltLeftUnit = ofRat fun (f : (j : Fin (Nat.succ 0).succ) → Fin (complexLorentzTensor.repDim (![Color.upL, Color.downL] j))) => if f 0 = f 1 then 1 else 0

theorem complexLorentzTensor.altRightRightUnit_eq_ofRat : altRightRightUnit = ofRat fun (f : (j : Fin (Nat.succ 0).succ) → Fin (complexLorentzTensor.repDim (![Color.downR, Color.upR] j))) => if f 0 = f 1 then 1 else 0

theorem complexLorentzTensor.rightAltRightUnit_eq_ofRat : rightAltRightUnit = ofRat fun (f : (j : Fin (Nat.succ 0).succ) → Fin (complexLorentzTensor.repDim (![Color.upR, Color.downR] j))) => if f 0 = f 1 then 1 else 0