Metrics and basis expansions

theorem complexLorentzTensor.coMetric_basis_expand : (TensorTree.tensorNode coMetric).tensor = (((basisVector ![Color.down, Color.down] fun (x : Fin (Nat.succ 0).succ) => 0) - basisVector ![Color.down, Color.down] fun (x : Fin (Nat.succ 0).succ) => 1) - basisVector ![Color.down, Color.down] fun (x : Fin (Nat.succ 0).succ) => 2) - basisVector ![Color.down, Color.down] fun (x : Fin (Nat.succ 0).succ) => 3

The expansion of the Lorentz covariant metric in terms of basis vectors.

theorem complexLorentzTensor.coMetric_tensorBasis : coMetric = ((((complexLorentzTensor.tensorBasis ![Color.down, Color.down]) fun (x : Fin (Nat.succ 0).succ) => 0) - (complexLorentzTensor.tensorBasis ![Color.down, Color.down]) fun (x : Fin (Nat.succ 0).succ) => 1) - (complexLorentzTensor.tensorBasis ![Color.down, Color.down]) fun (x : Fin (Nat.succ 0).succ) => 2) - (complexLorentzTensor.tensorBasis ![Color.down, Color.down]) fun (x : Fin (Nat.succ 0).succ) => 3

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

theorem complexLorentzTensor.coMetric_basis_expand_tree : (TensorTree.tensorNode coMetric).tensor = ((TensorTree.tensorNode (basisVector ![Color.down, Color.down] fun (x : Fin (Nat.succ 0).succ) => 0)).add ((TensorTree.smul (-1) (TensorTree.tensorNode (basisVector ![Color.down, Color.down] fun (x : Fin (Nat.succ 0).succ) => 1))).add ((TensorTree.smul (-1) (TensorTree.tensorNode (basisVector ![Color.down, Color.down] fun (x : Fin (Nat.succ 0).succ) => 2))).add (TensorTree.smul (-1) (TensorTree.tensorNode (basisVector ![Color.down, Color.down] fun (x : Fin (Nat.succ 0).succ) => 3)))))).tensor

Provides the explicit expansion of the co-metric tensor in terms of the basis elements, as a tensor tree.

contrMetric

theorem complexLorentzTensor.contrMetric_basis_expand : (TensorTree.tensorNode contrMetric).tensor = (((basisVector ![Color.up, Color.up] fun (x : Fin (Nat.succ 0).succ) => 0) - basisVector ![Color.up, Color.up] fun (x : Fin (Nat.succ 0).succ) => 1) - basisVector ![Color.up, Color.up] fun (x : Fin (Nat.succ 0).succ) => 2) - basisVector ![Color.up, Color.up] fun (x : Fin (Nat.succ 0).succ) => 3

The expansion of the Lorentz contravariant metric in terms of basis vectors.

theorem complexLorentzTensor.contrMetric_tensorBasis : contrMetric = ((((complexLorentzTensor.tensorBasis ![Color.up, Color.up]) fun (x : Fin (Nat.succ 0).succ) => 0) - (complexLorentzTensor.tensorBasis ![Color.up, Color.up]) fun (x : Fin (Nat.succ 0).succ) => 1) - (complexLorentzTensor.tensorBasis ![Color.up, Color.up]) fun (x : Fin (Nat.succ 0).succ) => 2) - (complexLorentzTensor.tensorBasis ![Color.up, Color.up]) fun (x : Fin (Nat.succ 0).succ) => 3

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

theorem complexLorentzTensor.contrMetric_basis_expand_tree : (TensorTree.tensorNode contrMetric).tensor = ((TensorTree.tensorNode (basisVector ![Color.up, Color.up] fun (x : Fin (Nat.succ 0).succ) => 0)).add ((TensorTree.smul (-1) (TensorTree.tensorNode (basisVector ![Color.up, Color.up] fun (x : Fin (Nat.succ 0).succ) => 1))).add ((TensorTree.smul (-1) (TensorTree.tensorNode (basisVector ![Color.up, Color.up] fun (x : Fin (Nat.succ 0).succ) => 2))).add (TensorTree.smul (-1) (TensorTree.tensorNode (basisVector ![Color.up, Color.up] fun (x : Fin (Nat.succ 0).succ) => 3)))))).tensor

The expansion of the Lorentz contravariant metric in terms of basis vectors as a structured tensor tree.

theorem complexLorentzTensor.leftMetric_expand : (TensorTree.tensorNode leftMetric).tensor = (-basisVector ![Color.upL, Color.upL] fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => 0 | 1 => 1) + basisVector ![Color.upL, Color.upL] fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => 1 | 1 => 0

The expansion of the Fermionic left metric in terms of basis vectors.

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

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

theorem complexLorentzTensor.leftMetric_expand_tree : (TensorTree.tensorNode leftMetric).tensor = ((TensorTree.smul (-1) (TensorTree.tensorNode (basisVector ![Color.upL, Color.upL] fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => 0 | 1 => 1))).add (TensorTree.tensorNode (basisVector ![Color.upL, Color.upL] fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => 1 | 1 => 0))).tensor

The expansion of the Fermionic left metric in terms of basis vectors as a structured tensor tree.

theorem complexLorentzTensor.altLeftMetric_expand : (TensorTree.tensorNode altLeftMetric).tensor = (basisVector ![Color.downL, Color.downL] fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => 0 | 1 => 1) - basisVector ![Color.downL, Color.downL] fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => 1 | 1 => 0

The expansion of the Fermionic alt-left metric in terms of basis vectors.

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

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

theorem complexLorentzTensor.altLeftMetric_expand_tree : (TensorTree.tensorNode altLeftMetric).tensor = ((TensorTree.tensorNode (basisVector ![Color.downL, Color.downL] fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => 0 | 1 => 1)).add (TensorTree.smul (-1) (TensorTree.tensorNode (basisVector ![Color.downL, Color.downL] fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => 1 | 1 => 0)))).tensor

The expansion of the Fermionic alt-left metric in terms of basis vectors as a structured tensor tree.

theorem complexLorentzTensor.rightMetric_expand : (TensorTree.tensorNode rightMetric).tensor = (-basisVector ![Color.upR, Color.upR] fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => 0 | 1 => 1) + basisVector ![Color.upR, Color.upR] fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => 1 | 1 => 0

The expansion of the Fermionic right metric in terms of basis vectors.

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

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

theorem complexLorentzTensor.rightMetric_expand_tree : (TensorTree.tensorNode rightMetric).tensor = ((TensorTree.smul (-1) (TensorTree.tensorNode (basisVector ![Color.upR, Color.upR] fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => 0 | 1 => 1))).add (TensorTree.tensorNode (basisVector ![Color.upR, Color.upR] fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => 1 | 1 => 0))).tensor

The expansion of the Fermionic right metric in terms of basis vectors as a structured tensor tree.

theorem complexLorentzTensor.altRightMetric_expand : (TensorTree.tensorNode altRightMetric).tensor = (basisVector ![Color.downR, Color.downR] fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => 0 | 1 => 1) - basisVector ![Color.downR, Color.downR] fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => 1 | 1 => 0

The expansion of the Fermionic alt-right metric in terms of basis vectors.

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

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

theorem complexLorentzTensor.altRightMetric_expand_tree : (TensorTree.tensorNode altRightMetric).tensor = ((TensorTree.tensorNode (basisVector ![Color.downR, Color.downR] fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => 0 | 1 => 1)).add (TensorTree.smul (-1) (TensorTree.tensorNode (basisVector ![Color.downR, Color.downR] fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => 1 | 1 => 0)))).tensor

The expansion of the Fermionic alt-right metric in terms of basis vectors as a structured tensor tree.