1. Physlib
  2. Relativity
  3. Tensors
  4. ComplexTensor
  5. Metrics
  6. Lemmas
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.Metrics.Basic public import Physlib.Relativity.Tensors.ComplexTensor.Units.Basic

Basic lemmas regarding metrics

@[expose] public section

Symmetry properties

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

b:ComponentIdx ![Color.down, Color.down]⊢ Physlib.RatComplexNum.toComplexNum (if b 0 = Fin.cast coMetric_eq_ofRat._proof_1 0 ∧ b 1 = Fin.cast coMetric_eq_ofRat._proof_2 0 then 1 else if b 0 = b 1 then -1 else 0) = Physlib.RatComplexNum.toComplexNum (if (fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ i))) 0 = Fin.cast coMetric_eq_ofRat._proof_1 0 ∧ (fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ i))) 1 = Fin.cast coMetric_eq_ofRat._proof_2 0 then 1 else if (fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ i))) 0 = (fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ i))) 1 then -1 else 0) b:ComponentIdx ![Color.down, Color.down]⊢ (if b 0 = Fin.cast coMetric_eq_ofRat._proof_1 0 ∧ b 1 = Fin.cast coMetric_eq_ofRat._proof_2 0 then 1 else if b 0 = b 1 then -1 else 0) = if (fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ i))) 0 = Fin.cast coMetric_eq_ofRat._proof_1 0 ∧ (fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ i))) 1 = Fin.cast coMetric_eq_ofRat._proof_2 0 then 1 else if (fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ i))) 0 = (fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ i))) 1 then -1 else 0 ⊢ ∀ (b : ComponentIdx ![Color.down, Color.down]), (if b 0 = Fin.cast coMetric_eq_ofRat._proof_1 0 ∧ b 1 = Fin.cast coMetric_eq_ofRat._proof_2 0 then 1 else if b 0 = b 1 then -1 else 0) = if (fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ i))) 0 = Fin.cast coMetric_eq_ofRat._proof_1 0 ∧ (fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ i))) 1 = Fin.cast coMetric_eq_ofRat._proof_2 0 then 1 else if (fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ i))) 0 = (fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ i))) 1 then -1 else 0 All goals completed! 🐙

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

b:ComponentIdx ![Color.up, Color.up]⊢ Physlib.RatComplexNum.toComplexNum (if b 0 = Fin.cast contrMetric_eq_ofRat._proof_1 0 ∧ b 1 = Fin.cast contrMetric_eq_ofRat._proof_2 0 then 1 else if b 0 = b 1 then -1 else 0) = Physlib.RatComplexNum.toComplexNum (if (fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ i))) 0 = Fin.cast contrMetric_eq_ofRat._proof_1 0 ∧ (fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ i))) 1 = Fin.cast contrMetric_eq_ofRat._proof_2 0 then 1 else if (fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ i))) 0 = (fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ i))) 1 then -1 else 0) b:ComponentIdx ![Color.up, Color.up]⊢ (if b 0 = Fin.cast contrMetric_eq_ofRat._proof_1 0 ∧ b 1 = Fin.cast contrMetric_eq_ofRat._proof_2 0 then 1 else if b 0 = b 1 then -1 else 0) = if (fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ i))) 0 = Fin.cast contrMetric_eq_ofRat._proof_1 0 ∧ (fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ i))) 1 = Fin.cast contrMetric_eq_ofRat._proof_2 0 then 1 else if (fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ i))) 0 = (fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ i))) 1 then -1 else 0 ⊢ ∀ (b : ComponentIdx ![Color.up, Color.up]), (if b 0 = Fin.cast contrMetric_eq_ofRat._proof_1 0 ∧ b 1 = Fin.cast contrMetric_eq_ofRat._proof_2 0 then 1 else if b 0 = b 1 then -1 else 0) = if (fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ i))) 0 = Fin.cast contrMetric_eq_ofRat._proof_1 0 ∧ (fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ i))) 1 = Fin.cast contrMetric_eq_ofRat._proof_2 0 then 1 else if (fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ i))) 0 = (fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ i))) 1 then -1 else 0 All goals completed! 🐙

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

b:ComponentIdx ![Color.upL, Color.upL]⊢ Physlib.RatComplexNum.toComplexNum (if b 0 = Fin.cast leftMetric_eq_ofRat._proof_1 0 ∧ b 1 = Fin.cast leftMetric_eq_ofRat._proof_2 1 then -1 else if b 1 = Fin.cast leftMetric_eq_ofRat._proof_2 0 ∧ b 0 = Fin.cast leftMetric_eq_ofRat._proof_1 1 then 1 else 0) = Physlib.RatComplexNum.toComplexNum ((-fun f => if f 0 = Fin.cast leftMetric_eq_ofRat._proof_1 0 ∧ f 1 = Fin.cast leftMetric_eq_ofRat._proof_2 1 then -1 else if f 1 = Fin.cast leftMetric_eq_ofRat._proof_2 0 ∧ f 0 = Fin.cast leftMetric_eq_ofRat._proof_1 1 then 1 else 0) fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ i))) b:ComponentIdx ![Color.upL, Color.upL]⊢ (if b 0 = Fin.cast leftMetric_eq_ofRat._proof_1 0 ∧ b 1 = Fin.cast leftMetric_eq_ofRat._proof_2 1 then -1 else if b 1 = Fin.cast leftMetric_eq_ofRat._proof_2 0 ∧ b 0 = Fin.cast leftMetric_eq_ofRat._proof_1 1 then 1 else 0) = (-fun f => if f 0 = Fin.cast leftMetric_eq_ofRat._proof_1 0 ∧ f 1 = Fin.cast leftMetric_eq_ofRat._proof_2 1 then -1 else if f 1 = Fin.cast leftMetric_eq_ofRat._proof_2 0 ∧ f 0 = Fin.cast leftMetric_eq_ofRat._proof_1 1 then 1 else 0) fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ i)) ⊢ ∀ (b : ComponentIdx ![Color.upL, Color.upL]), (if b 0 = Fin.cast leftMetric_eq_ofRat._proof_1 0 ∧ b 1 = Fin.cast leftMetric_eq_ofRat._proof_2 1 then -1 else if b 1 = Fin.cast leftMetric_eq_ofRat._proof_2 0 ∧ b 0 = Fin.cast leftMetric_eq_ofRat._proof_1 1 then 1 else 0) = (-fun f => if f 0 = Fin.cast leftMetric_eq_ofRat._proof_1 0 ∧ f 1 = Fin.cast leftMetric_eq_ofRat._proof_2 1 then -1 else if f 1 = Fin.cast leftMetric_eq_ofRat._proof_2 0 ∧ f 0 = Fin.cast leftMetric_eq_ofRat._proof_1 1 then 1 else 0) fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ i)) All goals completed! 🐙

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

b:ComponentIdx ![Color.upR, Color.upR]⊢ Physlib.RatComplexNum.toComplexNum (if b 0 = Fin.cast rightMetric_eq_ofRat._proof_1 0 ∧ b 1 = Fin.cast rightMetric_eq_ofRat._proof_2 1 then -1 else if b 1 = Fin.cast rightMetric_eq_ofRat._proof_2 0 ∧ b 0 = Fin.cast rightMetric_eq_ofRat._proof_1 1 then 1 else 0) = Physlib.RatComplexNum.toComplexNum ((-fun f => if f 0 = Fin.cast rightMetric_eq_ofRat._proof_1 0 ∧ f 1 = Fin.cast rightMetric_eq_ofRat._proof_2 1 then -1 else if f 1 = Fin.cast rightMetric_eq_ofRat._proof_2 0 ∧ f 0 = Fin.cast rightMetric_eq_ofRat._proof_1 1 then 1 else 0) fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ i))) b:ComponentIdx ![Color.upR, Color.upR]⊢ (if b 0 = Fin.cast rightMetric_eq_ofRat._proof_1 0 ∧ b 1 = Fin.cast rightMetric_eq_ofRat._proof_2 1 then -1 else if b 1 = Fin.cast rightMetric_eq_ofRat._proof_2 0 ∧ b 0 = Fin.cast rightMetric_eq_ofRat._proof_1 1 then 1 else 0) = (-fun f => if f 0 = Fin.cast rightMetric_eq_ofRat._proof_1 0 ∧ f 1 = Fin.cast rightMetric_eq_ofRat._proof_2 1 then -1 else if f 1 = Fin.cast rightMetric_eq_ofRat._proof_2 0 ∧ f 0 = Fin.cast rightMetric_eq_ofRat._proof_1 1 then 1 else 0) fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ i)) ⊢ ∀ (b : ComponentIdx ![Color.upR, Color.upR]), (if b 0 = Fin.cast rightMetric_eq_ofRat._proof_1 0 ∧ b 1 = Fin.cast rightMetric_eq_ofRat._proof_2 1 then -1 else if b 1 = Fin.cast rightMetric_eq_ofRat._proof_2 0 ∧ b 0 = Fin.cast rightMetric_eq_ofRat._proof_1 1 then 1 else 0) = (-fun f => if f 0 = Fin.cast rightMetric_eq_ofRat._proof_1 0 ∧ f 1 = Fin.cast rightMetric_eq_ofRat._proof_2 1 then -1 else if f 1 = Fin.cast rightMetric_eq_ofRat._proof_2 0 ∧ f 0 = Fin.cast rightMetric_eq_ofRat._proof_1 1 then 1 else 0) fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ i)) All goals completed! 🐙

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

b:ComponentIdx ![Color.downL, Color.downL]⊢ Physlib.RatComplexNum.toComplexNum (if b 0 = Fin.cast dualLeftMetric_eq_ofRat._proof_1 0 ∧ b 1 = Fin.cast dualLeftMetric_eq_ofRat._proof_2 1 then 1 else if b 1 = Fin.cast dualLeftMetric_eq_ofRat._proof_2 0 ∧ b 0 = Fin.cast dualLeftMetric_eq_ofRat._proof_1 1 then -1 else 0) = Physlib.RatComplexNum.toComplexNum ((-fun f => if f 0 = Fin.cast dualLeftMetric_eq_ofRat._proof_1 0 ∧ f 1 = Fin.cast dualLeftMetric_eq_ofRat._proof_2 1 then 1 else if f 1 = Fin.cast dualLeftMetric_eq_ofRat._proof_2 0 ∧ f 0 = Fin.cast dualLeftMetric_eq_ofRat._proof_1 1 then -1 else 0) fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ i))) b:ComponentIdx ![Color.downL, Color.downL]⊢ (if b 0 = Fin.cast dualLeftMetric_eq_ofRat._proof_1 0 ∧ b 1 = Fin.cast dualLeftMetric_eq_ofRat._proof_2 1 then 1 else if b 1 = Fin.cast dualLeftMetric_eq_ofRat._proof_2 0 ∧ b 0 = Fin.cast dualLeftMetric_eq_ofRat._proof_1 1 then -1 else 0) = (-fun f => if f 0 = Fin.cast dualLeftMetric_eq_ofRat._proof_1 0 ∧ f 1 = Fin.cast dualLeftMetric_eq_ofRat._proof_2 1 then 1 else if f 1 = Fin.cast dualLeftMetric_eq_ofRat._proof_2 0 ∧ f 0 = Fin.cast dualLeftMetric_eq_ofRat._proof_1 1 then -1 else 0) fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ i)) ⊢ ∀ (b : ComponentIdx ![Color.downL, Color.downL]), (if b 0 = Fin.cast dualLeftMetric_eq_ofRat._proof_1 0 ∧ b 1 = Fin.cast dualLeftMetric_eq_ofRat._proof_2 1 then 1 else if b 1 = Fin.cast dualLeftMetric_eq_ofRat._proof_2 0 ∧ b 0 = Fin.cast dualLeftMetric_eq_ofRat._proof_1 1 then -1 else 0) = (-fun f => if f 0 = Fin.cast dualLeftMetric_eq_ofRat._proof_1 0 ∧ f 1 = Fin.cast dualLeftMetric_eq_ofRat._proof_2 1 then 1 else if f 1 = Fin.cast dualLeftMetric_eq_ofRat._proof_2 0 ∧ f 0 = Fin.cast dualLeftMetric_eq_ofRat._proof_1 1 then -1 else 0) fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ i)) All goals completed! 🐙

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

b:ComponentIdx ![Color.downR, Color.downR]⊢ Physlib.RatComplexNum.toComplexNum (if b 0 = Fin.cast dualRightMetric_eq_ofRat._proof_1 0 ∧ b 1 = Fin.cast dualRightMetric_eq_ofRat._proof_2 1 then 1 else if b 1 = Fin.cast dualRightMetric_eq_ofRat._proof_2 0 ∧ b 0 = Fin.cast dualRightMetric_eq_ofRat._proof_1 1 then -1 else 0) = Physlib.RatComplexNum.toComplexNum ((-fun f => if f 0 = Fin.cast dualRightMetric_eq_ofRat._proof_1 0 ∧ f 1 = Fin.cast dualRightMetric_eq_ofRat._proof_2 1 then 1 else if f 1 = Fin.cast dualRightMetric_eq_ofRat._proof_2 0 ∧ f 0 = Fin.cast dualRightMetric_eq_ofRat._proof_1 1 then -1 else 0) fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ i))) b:ComponentIdx ![Color.downR, Color.downR]⊢ (if b 0 = Fin.cast dualRightMetric_eq_ofRat._proof_1 0 ∧ b 1 = Fin.cast dualRightMetric_eq_ofRat._proof_2 1 then 1 else if b 1 = Fin.cast dualRightMetric_eq_ofRat._proof_2 0 ∧ b 0 = Fin.cast dualRightMetric_eq_ofRat._proof_1 1 then -1 else 0) = (-fun f => if f 0 = Fin.cast dualRightMetric_eq_ofRat._proof_1 0 ∧ f 1 = Fin.cast dualRightMetric_eq_ofRat._proof_2 1 then 1 else if f 1 = Fin.cast dualRightMetric_eq_ofRat._proof_2 0 ∧ f 0 = Fin.cast dualRightMetric_eq_ofRat._proof_1 1 then -1 else 0) fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ i)) ⊢ ∀ (b : ComponentIdx ![Color.downR, Color.downR]), (if b 0 = Fin.cast dualRightMetric_eq_ofRat._proof_1 0 ∧ b 1 = Fin.cast dualRightMetric_eq_ofRat._proof_2 1 then 1 else if b 1 = Fin.cast dualRightMetric_eq_ofRat._proof_2 0 ∧ b 0 = Fin.cast dualRightMetric_eq_ofRat._proof_1 1 then -1 else 0) = (-fun f => if f 0 = Fin.cast dualRightMetric_eq_ofRat._proof_1 0 ∧ f 1 = Fin.cast dualRightMetric_eq_ofRat._proof_2 1 then 1 else if f 1 = Fin.cast dualRightMetric_eq_ofRat._proof_2 0 ∧ f 0 = Fin.cast dualRightMetric_eq_ofRat._proof_1 1 then -1 else 0) fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ i)) All goals completed! 🐙

Contractions with each other

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

lemma coMetric_contr_contrMetric : {η' | μ ρ ⊗ η | ρ ν = δ' | μ ν}ᵀ := ⊢ (contrT 2 1 2 ⋯) ((prodT η') η) = (permT ![0, 1] ⋯) δ' All goals completed! 🐙

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

lemma contrMetric_contr_coMetric : {η | μ ρ ⊗ η' | ρ ν = δ | μ ν}ᵀ := ⊢ (contrT 2 1 2 ⋯) ((prodT η) η') = (permT ![0, 1] ⋯) δ All goals completed! 🐙

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

lemma leftMetric_contr_dualLeftMetric : {εL | α β ⊗ εL' | β γ = δL | α γ}ᵀ := ⊢ (contrT 2 1 2 ⋯) ((prodT εL) εL') = (permT ![0, 1] ⋯) δL All goals completed! 🐙

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

lemma rightMetric_contr_dualRightMetric : {εR | α β ⊗ εR' | β γ = δR | α γ}ᵀ := ⊢ (contrT 2 1 2 ⋯) ((prodT εR) εR') = (permT ![0, 1] ⋯) δR All goals completed! 🐙

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

lemma dualLeftMetric_contr_leftMetric : {εL' | α β ⊗ εL | β γ = δL' | α γ}ᵀ := ⊢ (contrT 2 1 2 ⋯) ((prodT εL') εL) = (permT ![0, 1] ⋯) δL' All goals completed! 🐙

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

lemma dualRightMetric_contr_rightMetric : {εR' | α β ⊗ εR | β γ = δR' | α γ}ᵀ := ⊢ (contrT 2 1 2 ⋯) ((prodT εR') εR) = (permT ![0, 1] ⋯) δR' All goals completed! 🐙

Other relations

/- /-- The map to color one gets when multiplying left and right metrics. -/ def leftMetricMulRightMap := (Sum.elim ![Color.upL, Color.upL] ![Color.upR, Color.upR]) ∘ finSumFinEquiv.symm /-- Expansion of the product of `εL` and `εR` in terms of a basis. -/ lemma leftMetric_prod_rightMetric : {εL | α α' ⊗ εR | β β'}ᵀ.tensor = basisVector leftMetricMulRightMap (fun | 0 => 0 | 1 => 1 | 2 => 0 | 3 => 1) - basisVector leftMetricMulRightMap (fun | 0 => 0 | 1 => 1 | 2 => 1 | 3 => 0) - basisVector leftMetricMulRightMap (fun | 0 => 1 | 1 => 0 | 2 => 0 | 3 => 1) + basisVector leftMetricMulRightMap (fun | 0 => 1 | 1 => 0 | 2 => 1 | 3 => 0) := by rw [prod_tensor_eq_fst (leftMetric_expand_tree)] rw [prod_tensor_eq_snd (rightMetric_expand_tree)] rw [prod_add_both] rw [add_tensor_eq_fst <| add_tensor_eq_fst <| smul_prod _ _ _] rw [add_tensor_eq_fst <| add_tensor_eq_fst <| smul_tensor_eq <| prod_smul _ _ _] rw [add_tensor_eq_fst <| add_tensor_eq_fst <| smul_smul _ _ _] rw [add_tensor_eq_fst <| add_tensor_eq_fst <| smul_eq_one _ _ (by simp)] rw [add_tensor_eq_fst <| add_tensor_eq_snd <| smul_prod _ _ _] rw [add_tensor_eq_snd <| add_tensor_eq_fst <| prod_smul _ _ _] rw [add_tensor_eq_fst <| add_tensor_eq_fst <| prod_basisVector_tree _ _] rw [add_tensor_eq_fst <| add_tensor_eq_snd <| smul_tensor_eq <| prod_basisVector_tree _ _] rw [add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| prod_basisVector_tree _ _] rw [add_tensor_eq_snd <| add_tensor_eq_snd <| prod_basisVector_tree _ _] rw [← TensorTree.add_assoc] simp only [add_tensor, smul_tensor, tensorNode_tensor] change _ = basisVector leftMetricMulRightMap (fun | 0 => 0 | 1 => 1 | 2 => 0 | 3 => 1) +- basisVector leftMetricMulRightMap (fun | 0 => 0 | 1 => 1 | 2 => 1 | 3 => 0) +- basisVector leftMetricMulRightMap (fun | 0 => 1 | 1 => 0 | 2 => 0 | 3 => 1) + basisVector leftMetricMulRightMap (fun | 0 => 1 | 1 => 0 | 2 => 1 | 3 => 0) congr 1 congr 1 congr 1 all_goals congr funext x fin_cases x <;> rfl /-- Expansion of the product of `εL` and `εR` in terms of a basis, as a tensor tree. -/ lemma leftMetric_prod_rightMetric_tree : {εL | α α' ⊗ εR | β β'}ᵀ.tensor = (TensorTree.add (tensorNode (basisVector leftMetricMulRightMap (fun | 0 => 0 | 1 => 1 | 2 => 0 | 3 => 1))) <| TensorTree.add (TensorTree.smul (-1 : ℂ) (tensorNode (basisVector leftMetricMulRightMap (fun | 0 => 0 | 1 => 1 | 2 => 1 | 3 => 0)))) <| TensorTree.add (TensorTree.smul (-1 : ℂ) (tensorNode (basisVector leftMetricMulRightMap (fun | 0 => 1 | 1 => 0 | 2 => 0 | 3 => 1)))) <| (tensorNode (basisVector leftMetricMulRightMap (fun | 0 => 1 | 1 => 0 | 2 => 1 | 3 => 0)))).tensor := by rw [leftMetric_prod_rightMetric] simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, add_tensor, tensorNode_tensor, smul_tensor, neg_smul, one_smul] rfl -/ end complexLorentzTensor