PhysLean Documentation

PhysLean.Relativity.Lorentz.ComplexTensor.Metrics.Lemmas

Basic lemmas regarding metrics #

Symmetry properties #

theorem complexLorentzTensor.coMetric_symm :

(TensorTree.tensorNode coMetric).tensor = (TensorTree.perm (IndexNotation.OverColor.equivToHomEq (PhysLean.Fin.finMapToEquiv ![1, 0] ![1, 0] ⋯ ⋯) ⋯) (TensorTree.tensorNode coMetric)).tensor

The covariant metric is symmetric {η' | μ ν = η' | ν μ}ᵀ.

theorem complexLorentzTensor.contrMetric_symm :

(TensorTree.tensorNode contrMetric).tensor = (TensorTree.perm (IndexNotation.OverColor.equivToHomEq (PhysLean.Fin.finMapToEquiv ![1, 0] ![1, 0] ⋯ ⋯) ⋯) (TensorTree.tensorNode contrMetric)).tensor

The contravariant metric is symmetric {η | μ ν = η | ν μ}ᵀ.

theorem complexLorentzTensor.leftMetric_antisymm :

(TensorTree.tensorNode leftMetric).tensor = (TensorTree.perm (IndexNotation.OverColor.equivToHomEq (PhysLean.Fin.finMapToEquiv ![1, 0] ![1, 0] ⋯ ⋯) ⋯) (TensorTree.tensorNode leftMetric).neg).tensor

The left metric is antisymmetric {εL | α α' = - εL | α' α}ᵀ.

theorem complexLorentzTensor.rightMetric_antisymm :

(TensorTree.tensorNode rightMetric).tensor = (TensorTree.perm (IndexNotation.OverColor.equivToHomEq (PhysLean.Fin.finMapToEquiv ![1, 0] ![1, 0] ⋯ ⋯) ⋯) (TensorTree.tensorNode rightMetric).neg).tensor

The right metric is antisymmetric {εR | β β' = - εR | β' β}ᵀ.

theorem complexLorentzTensor.altLeftMetric_antisymm :

(TensorTree.tensorNode altLeftMetric).tensor = (TensorTree.perm (IndexNotation.OverColor.equivToHomEq (PhysLean.Fin.finMapToEquiv ![1, 0] ![1, 0] ⋯ ⋯) ⋯) (TensorTree.tensorNode altLeftMetric).neg).tensor

The alt-left metric is antisymmetric {εL' | α α' = - εL' | α' α}ᵀ.

theorem complexLorentzTensor.altRightMetric_antisymm :

(TensorTree.tensorNode altRightMetric).tensor = (TensorTree.perm (IndexNotation.OverColor.equivToHomEq (PhysLean.Fin.finMapToEquiv ![1, 0] ![1, 0] ⋯ ⋯) ⋯) (TensorTree.tensorNode altRightMetric).neg).tensor

The alt-right metric is antisymmetric {εR' | β β' = - εR' | β' β}ᵀ.

Contractions with each other #

theorem complexLorentzTensor.coMetric_contr_contrMetric :

(TensorTree.contr 1 1 ⋯ ((TensorTree.tensorNode coMetric).prod (TensorTree.tensorNode contrMetric))).tensor = (TensorTree.perm (IndexNotation.OverColor.equivToHomEq (PhysLean.Fin.finMapToEquiv ![0, 1] ![0, 1] ⋯ ⋯) ⋯) (TensorTree.tensorNode coContrUnit)).tensor

The contraction of the covariant metric with the contravariant metric is the unit {η' | μ ρ ⊗ η | ρ ν = δ' | μ ν}ᵀ.

theorem complexLorentzTensor.contrMetric_contr_coMetric :

(TensorTree.contr 1 1 ⋯ ((TensorTree.tensorNode contrMetric).prod (TensorTree.tensorNode coMetric))).tensor = (TensorTree.perm (IndexNotation.OverColor.equivToHomEq (PhysLean.Fin.finMapToEquiv ![0, 1] ![0, 1] ⋯ ⋯) ⋯) (TensorTree.tensorNode contrCoUnit)).tensor

The contraction of the contravariant metric with the covariant metric is the unit {η | μ ρ ⊗ η' | ρ ν = δ | μ ν}ᵀ.

theorem complexLorentzTensor.leftMetric_contr_altLeftMetric :

(TensorTree.contr 1 1 ⋯ ((TensorTree.tensorNode leftMetric).prod (TensorTree.tensorNode altLeftMetric))).tensor = (TensorTree.perm (IndexNotation.OverColor.equivToHomEq (PhysLean.Fin.finMapToEquiv ![0, 1] ![0, 1] ⋯ ⋯) ⋯) (TensorTree.tensorNode leftAltLeftUnit)).tensor

The contraction of the left metric with the alt-left metric is the unit {εL | α β ⊗ εL' | β γ = δL | α γ}ᵀ.

The contraction of the right metric with the alt-right metric is the unit {εR | α β ⊗ εR' | β γ = δR | α γ}ᵀ.

theorem complexLorentzTensor.altLeftMetric_contr_leftMetric :

(TensorTree.contr 1 1 ⋯ ((TensorTree.tensorNode altLeftMetric).prod (TensorTree.tensorNode leftMetric))).tensor = (TensorTree.perm (IndexNotation.OverColor.equivToHomEq (PhysLean.Fin.finMapToEquiv ![0, 1] ![0, 1] ⋯ ⋯) ⋯) (TensorTree.tensorNode altLeftLeftUnit)).tensor

The contraction of the alt-left metric with the left metric is the unit {εL' | α β ⊗ εL | β γ = δL' | α γ}ᵀ.

The contraction of the alt-right metric with the right metric is the unit {εR' | α β ⊗ εR | β γ = δR' | α γ}ᵀ.

Other relations #

def complexLorentzTensor.leftMetricMulRightMap :

Fin ((Nat.succ 0).succ + (Nat.succ 0).succ) → Color

The map to color one gets when multiplying left and right metrics.

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem complexLorentzTensor.leftMetric_prod_rightMetric :

((TensorTree.tensorNode leftMetric).prod (TensorTree.tensorNode rightMetric)).tensor = (((basisVector leftMetricMulRightMap fun (x : Fin ((Nat.succ 0).succ + (Nat.succ 0).succ)) => match x with | 0 => 0 | 1 => 1 | 2 => 0 | 3 => 1) - basisVector leftMetricMulRightMap fun (x : Fin ((Nat.succ 0).succ + (Nat.succ 0).succ)) => match x with | 0 => 0 | 1 => 1 | 2 => 1 | 3 => 0) - basisVector leftMetricMulRightMap fun (x : Fin ((Nat.succ 0).succ + (Nat.succ 0).succ)) => match x with | 0 => 1 | 1 => 0 | 2 => 0 | 3 => 1) + basisVector leftMetricMulRightMap fun (x : Fin ((Nat.succ 0).succ + (Nat.succ 0).succ)) => match x with | 0 => 1 | 1 => 0 | 2 => 1 | 3 => 0

Expansion of the product of εL and εR in terms of a basis.

theorem complexLorentzTensor.leftMetric_prod_rightMetric_tree :

((TensorTree.tensorNode leftMetric).prod (TensorTree.tensorNode rightMetric)).tensor = ((TensorTree.tensorNode (basisVector leftMetricMulRightMap fun (x : Fin ((Nat.succ 0).succ + (Nat.succ 0).succ)) => match x with | 0 => 0 | 1 => 1 | 2 => 0 | 3 => 1)).add ((TensorTree.smul (-1) (TensorTree.tensorNode (basisVector leftMetricMulRightMap fun (x : Fin ((Nat.succ 0).succ + (Nat.succ 0).succ)) => match x with | 0 => 0 | 1 => 1 | 2 => 1 | 3 => 0))).add ((TensorTree.smul (-1) (TensorTree.tensorNode (basisVector leftMetricMulRightMap fun (x : Fin ((Nat.succ 0).succ + (Nat.succ 0).succ)) => match x with | 0 => 1 | 1 => 0 | 2 => 0 | 3 => 1))).add (TensorTree.tensorNode (basisVector leftMetricMulRightMap fun (x : Fin ((Nat.succ 0).succ + (Nat.succ 0).succ)) => match x with | 0 => 1 | 1 => 0 | 2 => 1 | 3 => 0))))).tensor

Expansion of the product of εL and εR in terms of a basis, as a tensor tree.