PhysLean Documentation

PhysLean.Relativity.Lorentz.ComplexTensor.Units.Symm

Symmetry lemmas relating to units #

Symmetry properties #

source
theorem complexLorentzTensor.coContrUnit_symm :
(TensorTree.tensorNode coContrUnit).tensor = (TensorTree.perm (IndexNotation.OverColor.equivToHomEq (PhysLean.Fin.finMapToEquiv ![1, 0] ![1, 0] ⋯ ⋯) ⋯) (TensorTree.tensorNode contrCoUnit)).tensor

Swapping indices of coContrUnit returns contrCoUnit: {δ' | μ ν = δ | ν μ}ᵀ.

source
theorem complexLorentzTensor.contrCoUnit_symm :
(TensorTree.tensorNode contrCoUnit).tensor = (TensorTree.perm (IndexNotation.OverColor.equivToHomEq (PhysLean.Fin.finMapToEquiv ![1, 0] ![1, 0] ⋯ ⋯) ⋯) (TensorTree.tensorNode coContrUnit)).tensor

Swapping indices of contrCoUnit returns coContrUnit: {δ | μ ν = δ' | ν μ}ᵀ.

source
theorem complexLorentzTensor.altLeftLeftUnit_symm :
(TensorTree.tensorNode altLeftLeftUnit).tensor = (TensorTree.perm (IndexNotation.OverColor.equivToHomEq (PhysLean.Fin.finMapToEquiv ![1, 0] ![1, 0] ⋯ ⋯) ⋯) (TensorTree.tensorNode leftAltLeftUnit)).tensor

Swapping indices of altLeftLeftUnit returns leftAltLeftUnit: {δL' | α α' = δL | α' α}ᵀ.

source
theorem complexLorentzTensor.leftAltLeftUnit_symm :
(TensorTree.tensorNode leftAltLeftUnit).tensor = (TensorTree.perm (IndexNotation.OverColor.equivToHomEq (PhysLean.Fin.finMapToEquiv ![1, 0] ![1, 0] ⋯ ⋯) ⋯) (TensorTree.tensorNode altLeftLeftUnit)).tensor

Swapping indices of leftAltLeftUnit returns altLeftLeftUnit: {δL | α α' = δL' | α' α}ᵀ.

source
theorem complexLorentzTensor.altRightRightUnit_symm :
(TensorTree.tensorNode altRightRightUnit).tensor = (TensorTree.perm (IndexNotation.OverColor.equivToHomEq (PhysLean.Fin.finMapToEquiv ![1, 0] ![1, 0] ⋯ ⋯) ⋯) (TensorTree.tensorNode rightAltRightUnit)).tensor

Swapping indices of altRightRightUnit returns rightAltRightUnit: {δR' | β β' = δR | β' β}ᵀ.

source
theorem complexLorentzTensor.rightAltRightUnit_symm :
(TensorTree.tensorNode rightAltRightUnit).tensor = (TensorTree.perm (IndexNotation.OverColor.equivToHomEq (PhysLean.Fin.finMapToEquiv ![1, 0] ![1, 0] ⋯ ⋯) ⋯) (TensorTree.tensorNode altRightRightUnit)).tensor

Swapping indices of rightAltRightUnit returns altRightRightUnit: {δR | β β' = δR' | β' β}ᵀ.