Physlib.Relativity.Tensors.ComplexTensor.Units.Symm

Imports

/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Physlib.Relativity.Tensors.ComplexTensor.Units.Basic

Symmetry lemmas relating to units

@[expose] public section

Symmetry properties

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


lemma coContrUnit_symm : {δ' | μ ν = δ | ν μ}ᵀ := by⊢ δ' = (permT ![1, 0] ⋯) δ
  rw [coContrUnit,⊢ unitTensor Color.up = (permT ![1, 0] ⋯) δ⊢ (permT ![1, 0] ⋯) (unitTensor (complexLorentzTensor.τ Color.up)) = (permT ![1, 0] ⋯) δ unitTensor_eq_permT_dual⊢ (permT ![1, 0] ⋯) (unitTensor (complexLorentzTensor.τ Color.up)) = (permT ![1, 0] ⋯) δ⊢ (permT ![1, 0] ⋯) (unitTensor (complexLorentzTensor.τ Color.up)) = (permT ![1, 0] ⋯) δ]⊢ (permT ![1, 0] ⋯) (unitTensor (complexLorentzTensor.τ Color.up)) = (permT ![1, 0] ⋯) δ
  rflAll goals completed! 🐙

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


lemma contrCoUnit_symm : {δ | μ ν = δ' | ν μ}ᵀ := by⊢ δ = (permT ![1, 0] ⋯) δ'
  rw [contrCoUnit,⊢ unitTensor Color.down = (permT ![1, 0] ⋯) δ'⊢ (permT ![1, 0] ⋯) (unitTensor (complexLorentzTensor.τ Color.down)) = (permT ![1, 0] ⋯) δ' unitTensor_eq_permT_dual⊢ (permT ![1, 0] ⋯) (unitTensor (complexLorentzTensor.τ Color.down)) = (permT ![1, 0] ⋯) δ'⊢ (permT ![1, 0] ⋯) (unitTensor (complexLorentzTensor.τ Color.down)) = (permT ![1, 0] ⋯) δ']⊢ (permT ![1, 0] ⋯) (unitTensor (complexLorentzTensor.τ Color.down)) = (permT ![1, 0] ⋯) δ'
  rflAll goals completed! 🐙

Swapping indices of dualLeftLeftUnit returns leftDualLeftUnit: {δL' | α α' = δL | α' α}ᵀ.


lemma dualLeftLeftUnit_symm : {δL' | α α' = δL | α' α}ᵀ := by⊢ δL' = (permT ![1, 0] ⋯) δL
  rw [dualLeftLeftUnit,⊢ unitTensor Color.upL = (permT ![1, 0] ⋯) δL⊢ (permT ![1, 0] ⋯) (unitTensor (complexLorentzTensor.τ Color.upL)) = (permT ![1, 0] ⋯) δL unitTensor_eq_permT_dual⊢ (permT ![1, 0] ⋯) (unitTensor (complexLorentzTensor.τ Color.upL)) = (permT ![1, 0] ⋯) δL⊢ (permT ![1, 0] ⋯) (unitTensor (complexLorentzTensor.τ Color.upL)) = (permT ![1, 0] ⋯) δL]⊢ (permT ![1, 0] ⋯) (unitTensor (complexLorentzTensor.τ Color.upL)) = (permT ![1, 0] ⋯) δL
  rflAll goals completed! 🐙

Swapping indices of leftDualLeftUnit returns dualLeftLeftUnit: {δL | α α' = δL' | α' α}ᵀ.


lemma leftDualLeftUnit_symm : {δL | α α' = δL' | α' α}ᵀ := by⊢ δL = (permT ![1, 0] ⋯) δL'
  rw [leftDualLeftUnit,⊢ unitTensor Color.downL = (permT ![1, 0] ⋯) δL'⊢ (permT ![1, 0] ⋯) (unitTensor (complexLorentzTensor.τ Color.downL)) = (permT ![1, 0] ⋯) δL' unitTensor_eq_permT_dual⊢ (permT ![1, 0] ⋯) (unitTensor (complexLorentzTensor.τ Color.downL)) = (permT ![1, 0] ⋯) δL'⊢ (permT ![1, 0] ⋯) (unitTensor (complexLorentzTensor.τ Color.downL)) = (permT ![1, 0] ⋯) δL']⊢ (permT ![1, 0] ⋯) (unitTensor (complexLorentzTensor.τ Color.downL)) = (permT ![1, 0] ⋯) δL'
  rflAll goals completed! 🐙

Swapping indices of dualRightRightUnit returns rightDualRightUnit: {δR' | β β' = δR | β' β}ᵀ.


lemma dualRightRightUnit_symm : {δR' | β β' = δR | β' β}ᵀ := by⊢ δR' = (permT ![1, 0] ⋯) δR
  rw [dualRightRightUnit,⊢ unitTensor Color.upR = (permT ![1, 0] ⋯) δR⊢ (permT ![1, 0] ⋯) (unitTensor (complexLorentzTensor.τ Color.upR)) = (permT ![1, 0] ⋯) δR unitTensor_eq_permT_dual⊢ (permT ![1, 0] ⋯) (unitTensor (complexLorentzTensor.τ Color.upR)) = (permT ![1, 0] ⋯) δR⊢ (permT ![1, 0] ⋯) (unitTensor (complexLorentzTensor.τ Color.upR)) = (permT ![1, 0] ⋯) δR]⊢ (permT ![1, 0] ⋯) (unitTensor (complexLorentzTensor.τ Color.upR)) = (permT ![1, 0] ⋯) δR
  rflAll goals completed! 🐙

Swapping indices of rightDualRightUnit returns dualRightRightUnit: {δR | β β' = δR' | β' β}ᵀ.


lemma rightDualRightUnit_symm : {δR | β β' = δR' | β' β}ᵀ := by⊢ δR = (permT ![1, 0] ⋯) δR'
  rw [rightDualRightUnit,⊢ unitTensor Color.downR = (permT ![1, 0] ⋯) δR'⊢ (permT ![1, 0] ⋯) (unitTensor (complexLorentzTensor.τ Color.downR)) = (permT ![1, 0] ⋯) δR' unitTensor_eq_permT_dual⊢ (permT ![1, 0] ⋯) (unitTensor (complexLorentzTensor.τ Color.downR)) = (permT ![1, 0] ⋯) δR'⊢ (permT ![1, 0] ⋯) (unitTensor (complexLorentzTensor.τ Color.downR)) = (permT ![1, 0] ⋯) δR']⊢ (permT ![1, 0] ⋯) (unitTensor (complexLorentzTensor.τ Color.downR)) = (permT ![1, 0] ⋯) δR'
  rflAll goals completed! 🐙