PhysLean.Relativity.Tensors.ComplexTensor.Metrics.Lemmas

Basic lemmas regarding metrics #

Symmetry properties #

source

theorem complexLorentzTensor.coMetric_symm :

coMetric = (TensorSpecies.Tensor.permT ![1, 0] ⋯) coMetric

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

source

theorem complexLorentzTensor.contrMetric_symm :

contrMetric = (TensorSpecies.Tensor.permT ![1, 0] ⋯) contrMetric

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

source

theorem complexLorentzTensor.leftMetric_antisymm :

leftMetric = (TensorSpecies.Tensor.permT ![1, 0] ⋯) (-leftMetric)

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

source

theorem complexLorentzTensor.rightMetric_antisymm :

rightMetric = (TensorSpecies.Tensor.permT ![1, 0] ⋯) (-rightMetric)

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

source

theorem complexLorentzTensor.altLeftMetric_antisymm :

altLeftMetric = (TensorSpecies.Tensor.permT ![1, 0] ⋯) (-altLeftMetric)

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

source

theorem complexLorentzTensor.altRightMetric_antisymm :

altRightMetric = (TensorSpecies.Tensor.permT ![1, 0] ⋯) (-altRightMetric)

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

Contractions with each other #

source

theorem complexLorentzTensor.coMetric_contr_contrMetric :

(TensorSpecies.Tensor.contrT 2 1 2 ⋯) ((TensorSpecies.Tensor.prodT coMetric) contrMetric) = (TensorSpecies.Tensor.permT ![0, 1] ⋯) coContrUnit

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

source

theorem complexLorentzTensor.contrMetric_contr_coMetric :

(TensorSpecies.Tensor.contrT 2 1 2 ⋯) ((TensorSpecies.Tensor.prodT contrMetric) coMetric) = (TensorSpecies.Tensor.permT ![0, 1] ⋯) contrCoUnit

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

source

theorem complexLorentzTensor.leftMetric_contr_altLeftMetric :

(TensorSpecies.Tensor.contrT 2 1 2 ⋯) ((TensorSpecies.Tensor.prodT leftMetric) altLeftMetric) = (TensorSpecies.Tensor.permT ![0, 1] ⋯) leftAltLeftUnit

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

source

theorem complexLorentzTensor.rightMetric_contr_altRightMetric :

(TensorSpecies.Tensor.contrT 2 1 2 ⋯) ((TensorSpecies.Tensor.prodT rightMetric) altRightMetric) = (TensorSpecies.Tensor.permT ![0, 1] ⋯) rightAltRightUnit

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

source

theorem complexLorentzTensor.altLeftMetric_contr_leftMetric :

(TensorSpecies.Tensor.contrT 2 1 2 ⋯) ((TensorSpecies.Tensor.prodT altLeftMetric) leftMetric) = (TensorSpecies.Tensor.permT ![0, 1] ⋯) altLeftLeftUnit

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

source

theorem complexLorentzTensor.altRightMetric_contr_rightMetric :

(TensorSpecies.Tensor.contrT 2 1 2 ⋯) ((TensorSpecies.Tensor.prodT altRightMetric) rightMetric) = (TensorSpecies.Tensor.permT ![0, 1] ⋯) altRightRightUnit

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

PhysLean Documentation