Physlib.Relativity.Tensors.ComplexTensor.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.Basic

              
                Lemmas related to complex Lorentz tensors.
              

              @[expose] public sectionlemma antiSymm_contr_symm {A : ℂT[.up, .up]} {S : ℂT[.down, .down]}
    (hA : {A | μ ν = - (A | ν μ)}ᵀ) (hs : {S | μ ν = S | ν μ}ᵀ) :
    {A | μ ν ⊗ S | μ ν = - A | μ ν ⊗ S | μ ν}ᵀ := byA:complexLorentzTensor.Tensor ![Color.up, Color.up]S:complexLorentzTensor.Tensor ![Color.down, Color.down]hA:A = (permT ![1, 0] ⋯) (-A)hs:S = (permT ![1, 0] ⋯) S⊢ (contrT 0 0 1 ⋯) ((contrT 2 1 3 ⋯) ((prodT A) S)) = -(contrT 0 0 1 ⋯) ((contrT 2 1 3 ⋯) ((prodT A) S))
  conv_lhs =>
    rw [hA, hs, prodT_permT_left, prodT_permT_right, contrT_comm, permT_permT,
      contrT_permT, contrT_permT, permT_permT]A:complexLorentzTensor.Tensor ![Color.up, Color.up]S:complexLorentzTensor.Tensor ![Color.down, Color.down]hA:A = (permT ![1, 0] ⋯) (-A)hs:S = (permT ![1, 0] ⋯) S| (permT
    (((Fin.succSuccAbove 1 3 0).predPredAbove (Fin.succSuccAbove 1 3 1) ⋯ 1 ⋯).funPredPredAbove
        ((Fin.succSuccAbove 1 3 0).predPredAbove (Fin.succSuccAbove 1 3 1) ⋯ 3 ⋯) ⋯
        ((Fin.succSuccAbove 1 3 0).funPredPredAbove (Fin.succSuccAbove 1 3 1) ⋯
          (Fin.append (Fin.castAdd (Nat.succ 0).succ) (Fin.natAdd (Nat.succ 0).succ ∘ ![1, 0]) ∘
            Fin.append (Fin.castAdd (Nat.succ 0).succ ∘ ![1, 0]) (Fin.natAdd (Nat.succ 0).succ))
          ⋯)
        ⋯ ∘
      id)
    ⋯)
  ((contrT 0
      ((Fin.succSuccAbove 1 3 0).funPredPredAbove (Fin.succSuccAbove 1 3 1) ⋯
        (Fin.append (Fin.castAdd (Nat.succ 0).succ) (Fin.natAdd (Nat.succ 0).succ ∘ ![1, 0]) ∘
          Fin.append (Fin.castAdd (Nat.succ 0).succ ∘ ![1, 0]) (Fin.natAdd (Nat.succ 0).succ))
        ⋯ ((Fin.succSuccAbove 1 3 0).predPredAbove (Fin.succSuccAbove 1 3 1) ⋯ 1 ⋯))
      ((Fin.succSuccAbove 1 3 0).funPredPredAbove (Fin.succSuccAbove 1 3 1) ⋯
        (Fin.append (Fin.castAdd (Nat.succ 0).succ) (Fin.natAdd (Nat.succ 0).succ ∘ ![1, 0]) ∘
          Fin.append (Fin.castAdd (Nat.succ 0).succ ∘ ![1, 0]) (Fin.natAdd (Nat.succ 0).succ))
        ⋯ ((Fin.succSuccAbove 1 3 0).predPredAbove (Fin.succSuccAbove 1 3 1) ⋯ 3 ⋯))
      ⋯)
    ((contrT 2
        ((Fin.append (Fin.castAdd (Nat.succ 0).succ) (Fin.natAdd (Nat.succ 0).succ ∘ ![1, 0]) ∘
            Fin.append (Fin.castAdd (Nat.succ 0).succ ∘ ![1, 0]) (Fin.natAdd (Nat.succ 0).succ))
          (Fin.succSuccAbove 1 3 0))
        ((Fin.append (Fin.castAdd (Nat.succ 0).succ) (Fin.natAdd (Nat.succ 0).succ ∘ ![1, 0]) ∘
            Fin.append (Fin.castAdd (Nat.succ 0).succ ∘ ![1, 0]) (Fin.natAdd (Nat.succ 0).succ))
          (Fin.succSuccAbove 1 3 1))
        ⋯)
      ((prodT (-A)) S)))
  simp only[LinearMap.neg_apply, map_neg]A:complexLorentzTensor.Tensor ![Color.up, Color.up]S:complexLorentzTensor.Tensor ![Color.down, Color.down]hA:A = (permT ![1, 0] ⋯) (-A)hs:S = (permT ![1, 0] ⋯) S⊢ -(permT
        (((Fin.succSuccAbove 1 3 0).predPredAbove (Fin.succSuccAbove 1 3 1) ⋯ 1 ⋯).funPredPredAbove
            ((Fin.succSuccAbove 1 3 0).predPredAbove (Fin.succSuccAbove 1 3 1) ⋯ 3 ⋯) ⋯
            ((Fin.succSuccAbove 1 3 0).funPredPredAbove (Fin.succSuccAbove 1 3 1) ⋯
              (Fin.append (Fin.castAdd (Nat.succ 0).succ) (Fin.natAdd (Nat.succ 0).succ ∘ ![1, 0]) ∘
                Fin.append (Fin.castAdd (Nat.succ 0).succ ∘ ![1, 0]) (Fin.natAdd (Nat.succ 0).succ))
              ⋯)
            ⋯ ∘
          id)
        ⋯)
      ((contrT 0
          ((Fin.succSuccAbove 1 3 0).funPredPredAbove (Fin.succSuccAbove 1 3 1) ⋯
            (Fin.append (Fin.castAdd (Nat.succ 0).succ) (Fin.natAdd (Nat.succ 0).succ ∘ ![1, 0]) ∘
              Fin.append (Fin.castAdd (Nat.succ 0).succ ∘ ![1, 0]) (Fin.natAdd (Nat.succ 0).succ))
            ⋯ ((Fin.succSuccAbove 1 3 0).predPredAbove (Fin.succSuccAbove 1 3 1) ⋯ 1 ⋯))
          ((Fin.succSuccAbove 1 3 0).funPredPredAbove (Fin.succSuccAbove 1 3 1) ⋯
            (Fin.append (Fin.castAdd (Nat.succ 0).succ) (Fin.natAdd (Nat.succ 0).succ ∘ ![1, 0]) ∘
              Fin.append (Fin.castAdd (Nat.succ 0).succ ∘ ![1, 0]) (Fin.natAdd (Nat.succ 0).succ))
            ⋯ ((Fin.succSuccAbove 1 3 0).predPredAbove (Fin.succSuccAbove 1 3 1) ⋯ 3 ⋯))
          ⋯)
        ((contrT 2
            ((Fin.append (Fin.castAdd (Nat.succ 0).succ) (Fin.natAdd (Nat.succ 0).succ ∘ ![1, 0]) ∘
                Fin.append (Fin.castAdd (Nat.succ 0).succ ∘ ![1, 0]) (Fin.natAdd (Nat.succ 0).succ))
              (Fin.succSuccAbove 1 3 0))
            ((Fin.append (Fin.castAdd (Nat.succ 0).succ) (Fin.natAdd (Nat.succ 0).succ ∘ ![1, 0]) ∘
                Fin.append (Fin.castAdd (Nat.succ 0).succ ∘ ![1, 0]) (Fin.natAdd (Nat.succ 0).succ))
              (Fin.succSuccAbove 1 3 1))
            ⋯)
          ((prodT A) S))) =
  -(contrT 0 0 1 ⋯) ((contrT 2 1 3 ⋯) ((prodT A) S))
  congr 1A:complexLorentzTensor.Tensor ![Color.up, Color.up]S:complexLorentzTensor.Tensor ![Color.down, Color.down]hA:A = (permT ![1, 0] ⋯) (-A)hs:S = (permT ![1, 0] ⋯) S⊢ (permT
      (((Fin.succSuccAbove 1 3 0).predPredAbove (Fin.succSuccAbove 1 3 1) ⋯ 1 ⋯).funPredPredAbove
          ((Fin.succSuccAbove 1 3 0).predPredAbove (Fin.succSuccAbove 1 3 1) ⋯ 3 ⋯) ⋯
          ((Fin.succSuccAbove 1 3 0).funPredPredAbove (Fin.succSuccAbove 1 3 1) ⋯
            (Fin.append (Fin.castAdd (Nat.succ 0).succ) (Fin.natAdd (Nat.succ 0).succ ∘ ![1, 0]) ∘
              Fin.append (Fin.castAdd (Nat.succ 0).succ ∘ ![1, 0]) (Fin.natAdd (Nat.succ 0).succ))
            ⋯)
          ⋯ ∘
        id)
      ⋯)
    ((contrT 0
        ((Fin.succSuccAbove 1 3 0).funPredPredAbove (Fin.succSuccAbove 1 3 1) ⋯
          (Fin.append (Fin.castAdd (Nat.succ 0).succ) (Fin.natAdd (Nat.succ 0).succ ∘ ![1, 0]) ∘
            Fin.append (Fin.castAdd (Nat.succ 0).succ ∘ ![1, 0]) (Fin.natAdd (Nat.succ 0).succ))
          ⋯ ((Fin.succSuccAbove 1 3 0).predPredAbove (Fin.succSuccAbove 1 3 1) ⋯ 1 ⋯))
        ((Fin.succSuccAbove 1 3 0).funPredPredAbove (Fin.succSuccAbove 1 3 1) ⋯
          (Fin.append (Fin.castAdd (Nat.succ 0).succ) (Fin.natAdd (Nat.succ 0).succ ∘ ![1, 0]) ∘
            Fin.append (Fin.castAdd (Nat.succ 0).succ ∘ ![1, 0]) (Fin.natAdd (Nat.succ 0).succ))
          ⋯ ((Fin.succSuccAbove 1 3 0).predPredAbove (Fin.succSuccAbove 1 3 1) ⋯ 3 ⋯))
        ⋯)
      ((contrT 2
          ((Fin.append (Fin.castAdd (Nat.succ 0).succ) (Fin.natAdd (Nat.succ 0).succ ∘ ![1, 0]) ∘
              Fin.append (Fin.castAdd (Nat.succ 0).succ ∘ ![1, 0]) (Fin.natAdd (Nat.succ 0).succ))
            (Fin.succSuccAbove 1 3 0))
          ((Fin.append (Fin.castAdd (Nat.succ 0).succ) (Fin.natAdd (Nat.succ 0).succ ∘ ![1, 0]) ∘
              Fin.append (Fin.castAdd (Nat.succ 0).succ ∘ ![1, 0]) (Fin.natAdd (Nat.succ 0).succ))
            (Fin.succSuccAbove 1 3 1))
          ⋯)
        ((prodT A) S))) =
  (contrT 0 0 1 ⋯) ((contrT 2 1 3 ⋯) ((prodT A) S))
  apply permT_congr_eq_idA:complexLorentzTensor.Tensor ![Color.up, Color.up]S:complexLorentzTensor.Tensor ![Color.down, Color.down]hA:A = (permT ![1, 0] ⋯) (-A)hs:S = (permT ![1, 0] ⋯) S⊢ ((Fin.succSuccAbove 1 3 0).predPredAbove (Fin.succSuccAbove 1 3 1) ⋯ 1 ⋯).funPredPredAbove
      ((Fin.succSuccAbove 1 3 0).predPredAbove (Fin.succSuccAbove 1 3 1) ⋯ 3 ⋯) ⋯
      ((Fin.succSuccAbove 1 3 0).funPredPredAbove (Fin.succSuccAbove 1 3 1) ⋯
        (Fin.append (Fin.castAdd (Nat.succ 0).succ) (Fin.natAdd (Nat.succ 0).succ ∘ ![1, 0]) ∘
          Fin.append (Fin.castAdd (Nat.succ 0).succ ∘ ![1, 0]) (Fin.natAdd (Nat.succ 0).succ))
        ⋯)
      ⋯ ∘
    id =
  id
  decideAll goals completed! 🐙