Physlib.Relativity.Tensors.ComplexTensor.Basic

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, Nikolai Kashcheev
-/
module

public import Physlib.Relativity.Tensors.ComplexTensor.Metrics.Pre
public import Physlib.Relativity.Fermions.Weyl.Metric

Complex Lorentz tensors

@[expose] public section

The colors associated with complex representations of SL(2, ℂ) of interest to physics.

The color associated with Left handed fermions.

The color associated with dual-Left handed fermions.

The color associated with Right handed fermions.

The color associated with dual-Right handed fermions.

The color associated with contravariant Lorentz vectors.

The color associated with covariant Lorentz vectors.

              inductive Color  | upL : Color  | downL : Color  | upR : Color  | downR : Color  | up : Color  | down : Color
deriving Fintype

Color for complex Lorentz tensors is decidable.

instance : DecidableEq Color := fun x y =>
  match x, y with
  | Color.upL, Color.upL => isTrue rfl
  | Color.downL, Color.downL => isTrue rfl
  | Color.upR, Color.upR => isTrue rfl
  | Color.downR, Color.downR => isTrue rfl
  | Color.up, Color.up => isTrue rfl
  | Color.down, Color.down => isTrue rfl
  /- The false -/
  | Color.upL, Color.downL => isFalse fun h => Color.noConfusion h
  | Color.upL, Color.upR => isFalse fun h => Color.noConfusion h
  | Color.upL, Color.downR => isFalse fun h => Color.noConfusion h
  | Color.upL, Color.up => isFalse fun h => Color.noConfusion h
  | Color.upL, Color.down => isFalse fun h => Color.noConfusion h
  | Color.downL, Color.upL => isFalse fun h => Color.noConfusion h
  | Color.downL, Color.upR => isFalse fun h => Color.noConfusion h
  | Color.downL, Color.downR => isFalse fun h => Color.noConfusion h
  | Color.downL, Color.up => isFalse fun h => Color.noConfusion h
  | Color.downL, Color.down => isFalse fun h => Color.noConfusion h
  | Color.upR, Color.upL => isFalse fun h => Color.noConfusion h
  | Color.upR, Color.downL => isFalse fun h => Color.noConfusion h
  | Color.upR, Color.downR => isFalse fun h => Color.noConfusion h
  | Color.upR, Color.up => isFalse fun h => Color.noConfusion h
  | Color.upR, Color.down => isFalse fun h => Color.noConfusion h
  | Color.downR, Color.upL => isFalse fun h => Color.noConfusion h
  | Color.downR, Color.downL => isFalse fun h => Color.noConfusion h
  | Color.downR, Color.upR => isFalse fun h => Color.noConfusion h
  | Color.downR, Color.up => isFalse fun h => Color.noConfusion h
  | Color.downR, Color.down => isFalse fun h => Color.noConfusion h
  | Color.up, Color.upL => isFalse fun h => Color.noConfusion h
  | Color.up, Color.downL => isFalse fun h => Color.noConfusion h
  | Color.up, Color.upR => isFalse fun h => Color.noConfusion h
  | Color.up, Color.downR => isFalse fun h => Color.noConfusion h
  | Color.up, Color.down => isFalse fun h => Color.noConfusion h
  | Color.down, Color.upL => isFalse fun h => Color.noConfusion h
  | Color.down, Color.downL => isFalse fun h => Color.noConfusion h
  | Color.down, Color.upR => isFalse fun h => Color.noConfusion h
  | Color.down, Color.downR => isFalse fun h => Color.noConfusion h
  | Color.down, Color.up => isFalse fun h => Color.noConfusion h

The dimensions of each of the different types of complex Lorentz vector space.

abbrev repDim (c : Color) : ℕ :=
  match c with
  | Color.upL => 2
  | Color.downL => 2
  | Color.upR => 2
  | Color.downR => 2
  | Color.up => 4
  | Color.down => 4

The modules associated with each of the different types of complex Lorentz vector space.

abbrev modules : Color → Type
  | Color.upL => Fermion.LeftHandedWeyl
  | Color.downL => Fermion.DualLeftHandedWeyl
  | Color.upR => Fermion.RightHandedWeyl
  | Color.downR => Fermion.DualRightHandedWeyl
  | Color.up => Lorentz.ContrℂModule
  | Color.down => Lorentz.CoℂModule

instance modulesAddCommGroup : ∀ c, AddCommGroup (modules c)
  | Color.upL => inferInstance
  | Color.downL => inferInstance
  | Color.upR => inferInstance
  | Color.downR => inferInstance
  | Color.up => inferInstance
  | Color.down => inferInstance

Complex Lorentz tensor.

syntax (name := complexLorentzTensorSyntax) "ℂT[" term,* "]" : term

The basis associated with each of the different types of complex Lorentz vector space.

abbrev basis (c : Color) : Module.Basis (Fin (repDim c)) ℂ (modules c) :=
  match c with
  | Color.upL => Fermion.LeftHandedWeyl.basis
  | Color.downL => Fermion.DualLeftHandedWeyl.basis
  | Color.upR => Fermion.RightHandedWeyl.basis
  | Color.downR => Fermion.DualRightHandedWeyl.basis
  | Color.up => Lorentz.complexContrBasisFin4
  | Color.down => Lorentz.complexCoBasisFin4

The reps associated with each of the different types of complex Lorentz vector space.

abbrev rep (c : Color) : Representation ℂ SL(2, ℂ) (modules c) :=
  match c with
  | Color.upL => Fermion.LeftHandedWeyl.rep
  | Color.downL => Fermion.DualLeftHandedWeyl.rep
  | Color.upR => Fermion.RightHandedWeyl.rep
  | Color.downR => Fermion.DualRightHandedWeyl.rep
  | Color.up => Lorentz.ContrℂModule.SL2CRep
  | Color.down => Lorentz.CoℂModule.SL2CRep

macro_rules
  | `(ℂT[$term:term, $terms:term,*]) =>
    `(complexLorentzTensor.Tensor (vecCons $term ![$terms,*]))
  | `(ℂT[$term:term]) => `(complexLorentzTensor.Tensor (vecCons $term ![]))
  | `(ℂT[]) =>`(complexLorentzTensor.Tensor (vecEmpty))

Complex Lorentz tensor.

scoped[complexLorentzTensor] notation "ℂT(" c ")" => complexLorentzTensor.Tensor c

              lemma basisIdxCongr_eq_cast {c1 c2 : complexLorentzTensor.Color}
    (h : c1 = c2) (i : Fin (repDim c1)) :
    TensorSpecies.basisIdxCongr (basisIdx := fun c => Fin (repDim c)) h i =
      Fin.cast (byc1:Colorc2:Colorh:c1 = c2i:Fin (repDim c1)⊢ repDim c1 = repDim c2 simp [h]All goals completed! 🐙) i := byc1:Colorc2:Colorh:c1 = c2i:Fin (repDim c1)⊢ (basisIdxCongr h) i = Fin.cast ⋯ i
  subst hc1:Colori:Fin (repDim c1)⊢ (basisIdxCongr ⋯) i = Fin.cast ⋯ i
  rflAll goals completed! 🐙lemma repDim_tau {c : complexLorentzTensor.Color} :
    repDim (complexLorentzTensor.τ c) = repDim c := byc:Color⊢ repDim (complexLorentzTensor.τ c) = repDim c
  cases cupL⊢ repDim (complexLorentzTensor.τ Color.upL) = repDim Color.upLdownL⊢ repDim (complexLorentzTensor.τ Color.downL) = repDim Color.downLupR⊢ repDim (complexLorentzTensor.τ Color.upR) = repDim Color.upRdownR⊢ repDim (complexLorentzTensor.τ Color.downR) = repDim Color.downRup⊢ repDim (complexLorentzTensor.τ Color.up) = repDim Color.updown⊢ repDim (complexLorentzTensor.τ Color.down) = repDim Color.down <;>upL⊢ repDim (complexLorentzTensor.τ Color.upL) = repDim Color.upLdownL⊢ repDim (complexLorentzTensor.τ Color.downL) = repDim Color.downLupR⊢ repDim (complexLorentzTensor.τ Color.upR) = repDim Color.upRdownR⊢ repDim (complexLorentzTensor.τ Color.downR) = repDim Color.downRup⊢ repDim (complexLorentzTensor.τ Color.up) = repDim Color.updown⊢ repDim (complexLorentzTensor.τ Color.down) = repDim Color.down rflAll goals completed! 🐙lemma contrPCoeff_basis {n : ℕ} {c : Fin n → complexLorentzTensor.Color} (i j : Fin n)
    (hij : i ≠ j ∧ (complexLorentzTensor.τ (c i) = c j))
    (b : ComponentIdx (S := complexLorentzTensor) c) :
    Pure.contrPCoeff i j hij (Pure.basisVector c b) = if b i =
      Fin.cast (byn:ℕc:Fin n → Colori:Fin nj:Fin nhij:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jb:ComponentIdx c⊢ repDim (c j) = repDim (c i) simp [← hij.2, repDim_tau]All goals completed! 🐙) (b j)
    then 1 else 0 := byn:ℕc:Fin n → Colori:Fin nj:Fin nhij:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jb:ComponentIdx c⊢ Pure.contrPCoeff i j hij (Pure.basisVector c b) = if b i = Fin.cast ⋯ (b j) then 1 else 0
  simp only [Pure.contrPCoeff, Pure.basisVector]n:ℕc:Fin n → Colori:Fin nj:Fin nhij:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jb:ComponentIdx c⊢ (complexLorentzTensor.contr (c i))
    ((match c i with
        | Color.upL => Fermion.LeftHandedWeyl.basis
        | Color.downL => Fermion.DualLeftHandedWeyl.basis
        | Color.upR => Fermion.RightHandedWeyl.basis
        | Color.downR => Fermion.DualRightHandedWeyl.basis
        | Color.up => Lorentz.complexContrBasisFin4
        | Color.down => Lorentz.complexCoBasisFin4)
        (b i) ⊗ₜ[ℂ]
      (LinearEquiv.cast ⋯)
        ((match c j with
          | Color.upL => Fermion.LeftHandedWeyl.basis
          | Color.downL => Fermion.DualLeftHandedWeyl.basis
          | Color.upR => Fermion.RightHandedWeyl.basis
          | Color.downR => Fermion.DualRightHandedWeyl.basis
          | Color.up => Lorentz.complexContrBasisFin4
          | Color.down => Lorentz.complexCoBasisFin4)
          (b j))) =
  if b i = Fin.cast ⋯ (b j) then 1 else 0
  generalize_proofs h1 h2n:ℕc:Fin n → Colori:Fin nj:Fin nhij:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)h2:c j = complexLorentzTensor.τ (c i)pf✝:repDim (c j) = repDim (c i)⊢ (complexLorentzTensor.contr (c i))
    ((match c i with
        | Color.upL => Fermion.LeftHandedWeyl.basis
        | Color.downL => Fermion.DualLeftHandedWeyl.basis
        | Color.upR => Fermion.RightHandedWeyl.basis
        | Color.downR => Fermion.DualRightHandedWeyl.basis
        | Color.up => Lorentz.complexContrBasisFin4
        | Color.down => Lorentz.complexCoBasisFin4)
        (b i) ⊗ₜ[ℂ]
      (LinearEquiv.cast h2)
        ((match c j with
          | Color.upL => Fermion.LeftHandedWeyl.basis
          | Color.downL => Fermion.DualLeftHandedWeyl.basis
          | Color.upR => Fermion.RightHandedWeyl.basis
          | Color.downR => Fermion.DualRightHandedWeyl.basis
          | Color.up => Lorentz.complexContrBasisFin4
          | Color.down => Lorentz.complexCoBasisFin4)
          (b j))) =
  if b i = Fin.cast pf✝ (b j) then 1 else 0
  generalize b i = b1 at *n:ℕc:Fin n → Colori:Fin nj:Fin nhij:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)h2:c j = complexLorentzTensor.τ (c i)pf✝:repDim (c j) = repDim (c i)b1:Fin (repDim (c i))⊢ (complexLorentzTensor.contr (c i))
    ((match c i with
        | Color.upL => Fermion.LeftHandedWeyl.basis
        | Color.downL => Fermion.DualLeftHandedWeyl.basis
        | Color.upR => Fermion.RightHandedWeyl.basis
        | Color.downR => Fermion.DualRightHandedWeyl.basis
        | Color.up => Lorentz.complexContrBasisFin4
        | Color.down => Lorentz.complexCoBasisFin4)
        b1 ⊗ₜ[ℂ]
      (LinearEquiv.cast h2)
        ((match c j with
          | Color.upL => Fermion.LeftHandedWeyl.basis
          | Color.downL => Fermion.DualLeftHandedWeyl.basis
          | Color.upR => Fermion.RightHandedWeyl.basis
          | Color.downR => Fermion.DualRightHandedWeyl.basis
          | Color.up => Lorentz.complexContrBasisFin4
          | Color.down => Lorentz.complexCoBasisFin4)
          (b j))) =
  if b1 = Fin.cast pf✝ (b j) then 1 else 0
  generalize b j = b2 at *n:ℕc:Fin n → Colori:Fin nj:Fin nhij:i ≠ j ∧ complexLorentzTensor.τ (c i) = c jb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)h2:c j = complexLorentzTensor.τ (c i)pf✝:repDim (c j) = repDim (c i)b1:Fin (repDim (c i))b2:Fin (repDim (c j))⊢ (complexLorentzTensor.contr (c i))
    ((match c i with
        | Color.upL => Fermion.LeftHandedWeyl.basis
        | Color.downL => Fermion.DualLeftHandedWeyl.basis
        | Color.upR => Fermion.RightHandedWeyl.basis
        | Color.downR => Fermion.DualRightHandedWeyl.basis
        | Color.up => Lorentz.complexContrBasisFin4
        | Color.down => Lorentz.complexCoBasisFin4)
        b1 ⊗ₜ[ℂ]
      (LinearEquiv.cast h2)
        ((match c j with
          | Color.upL => Fermion.LeftHandedWeyl.basis
          | Color.downL => Fermion.DualLeftHandedWeyl.basis
          | Color.upR => Fermion.RightHandedWeyl.basis
          | Color.downR => Fermion.DualRightHandedWeyl.basis
          | Color.up => Lorentz.complexContrBasisFin4
          | Color.down => Lorentz.complexCoBasisFin4)
          b2)) =
  if b1 = Fin.cast pf✝ b2 then 1 else 0
  generalize c i = ci at *n:ℕc:Fin n → Colori:Fin nj:Fin nb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)b2:Fin (repDim (c j))ci:Colorhij:i ≠ j ∧ complexLorentzTensor.τ ci = c jh2:c j = complexLorentzTensor.τ cipf✝:repDim (c j) = repDim cib1:Fin (repDim ci)⊢ (complexLorentzTensor.contr ci)
    ((match ci with
        | Color.upL => Fermion.LeftHandedWeyl.basis
        | Color.downL => Fermion.DualLeftHandedWeyl.basis
        | Color.upR => Fermion.RightHandedWeyl.basis
        | Color.downR => Fermion.DualRightHandedWeyl.basis
        | Color.up => Lorentz.complexContrBasisFin4
        | Color.down => Lorentz.complexCoBasisFin4)
        b1 ⊗ₜ[ℂ]
      (LinearEquiv.cast h2)
        ((match c j with
          | Color.upL => Fermion.LeftHandedWeyl.basis
          | Color.downL => Fermion.DualLeftHandedWeyl.basis
          | Color.upR => Fermion.RightHandedWeyl.basis
          | Color.downR => Fermion.DualRightHandedWeyl.basis
          | Color.up => Lorentz.complexContrBasisFin4
          | Color.down => Lorentz.complexCoBasisFin4)
          b2)) =
  if b1 = Fin.cast pf✝ b2 then 1 else 0
  generalize c j = cj at *n:ℕc:Fin n → Colori:Fin nj:Fin nb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)ci:Colorb1:Fin (repDim ci)cj:Colorb2:Fin (repDim cj)hij:i ≠ j ∧ complexLorentzTensor.τ ci = cjh2:cj = complexLorentzTensor.τ cipf✝:repDim cj = repDim ci⊢ (complexLorentzTensor.contr ci)
    ((match ci with
        | Color.upL => Fermion.LeftHandedWeyl.basis
        | Color.downL => Fermion.DualLeftHandedWeyl.basis
        | Color.upR => Fermion.RightHandedWeyl.basis
        | Color.downR => Fermion.DualRightHandedWeyl.basis
        | Color.up => Lorentz.complexContrBasisFin4
        | Color.down => Lorentz.complexCoBasisFin4)
        b1 ⊗ₜ[ℂ]
      (LinearEquiv.cast h2)
        ((match cj with
          | Color.upL => Fermion.LeftHandedWeyl.basis
          | Color.downL => Fermion.DualLeftHandedWeyl.basis
          | Color.upR => Fermion.RightHandedWeyl.basis
          | Color.downR => Fermion.DualRightHandedWeyl.basis
          | Color.up => Lorentz.complexContrBasisFin4
          | Color.down => Lorentz.complexCoBasisFin4)
          b2)) =
  if b1 = Fin.cast pf✝ b2 then 1 else 0
  subst h2n:ℕc:Fin n → Colori:Fin nj:Fin nb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)ci:Colorb1:Fin (repDim ci)b2:Fin (repDim (complexLorentzTensor.τ ci))hij:i ≠ j ∧ complexLorentzTensor.τ ci = complexLorentzTensor.τ cipf✝:repDim (complexLorentzTensor.τ ci) = repDim ci⊢ (complexLorentzTensor.contr ci)
    ((match ci with
        | Color.upL => Fermion.LeftHandedWeyl.basis
        | Color.downL => Fermion.DualLeftHandedWeyl.basis
        | Color.upR => Fermion.RightHandedWeyl.basis
        | Color.downR => Fermion.DualRightHandedWeyl.basis
        | Color.up => Lorentz.complexContrBasisFin4
        | Color.down => Lorentz.complexCoBasisFin4)
        b1 ⊗ₜ[ℂ]
      (LinearEquiv.cast ⋯)
        ((match complexLorentzTensor.τ ci with
          | Color.upL => Fermion.LeftHandedWeyl.basis
          | Color.downL => Fermion.DualLeftHandedWeyl.basis
          | Color.upR => Fermion.RightHandedWeyl.basis
          | Color.downR => Fermion.DualRightHandedWeyl.basis
          | Color.up => Lorentz.complexContrBasisFin4
          | Color.down => Lorentz.complexCoBasisFin4)
          b2)) =
  if b1 = Fin.cast pf✝ b2 then 1 else 0
  cases ciupLn:ℕc:Fin n → Colori:Fin nj:Fin nb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)b1:Fin (repDim Color.upL)b2:Fin (repDim (complexLorentzTensor.τ Color.upL))hij:i ≠ j ∧ complexLorentzTensor.τ Color.upL = complexLorentzTensor.τ Color.upLpf✝:repDim (complexLorentzTensor.τ Color.upL) = repDim Color.upL⊢ (complexLorentzTensor.contr Color.upL)
    ((match Color.upL with
        | Color.upL => Fermion.LeftHandedWeyl.basis
        | Color.downL => Fermion.DualLeftHandedWeyl.basis
        | Color.upR => Fermion.RightHandedWeyl.basis
        | Color.downR => Fermion.DualRightHandedWeyl.basis
        | Color.up => Lorentz.complexContrBasisFin4
        | Color.down => Lorentz.complexCoBasisFin4)
        b1 ⊗ₜ[ℂ]
      (LinearEquiv.cast ⋯)
        ((match complexLorentzTensor.τ Color.upL with
          | Color.upL => Fermion.LeftHandedWeyl.basis
          | Color.downL => Fermion.DualLeftHandedWeyl.basis
          | Color.upR => Fermion.RightHandedWeyl.basis
          | Color.downR => Fermion.DualRightHandedWeyl.basis
          | Color.up => Lorentz.complexContrBasisFin4
          | Color.down => Lorentz.complexCoBasisFin4)
          b2)) =
  if b1 = Fin.cast pf✝ b2 then 1 else 0downLn:ℕc:Fin n → Colori:Fin nj:Fin nb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)b1:Fin (repDim Color.downL)b2:Fin (repDim (complexLorentzTensor.τ Color.downL))hij:i ≠ j ∧ complexLorentzTensor.τ Color.downL = complexLorentzTensor.τ Color.downLpf✝:repDim (complexLorentzTensor.τ Color.downL) = repDim Color.downL⊢ (complexLorentzTensor.contr Color.downL)
    ((match Color.downL with
        | Color.upL => Fermion.LeftHandedWeyl.basis
        | Color.downL => Fermion.DualLeftHandedWeyl.basis
        | Color.upR => Fermion.RightHandedWeyl.basis
        | Color.downR => Fermion.DualRightHandedWeyl.basis
        | Color.up => Lorentz.complexContrBasisFin4
        | Color.down => Lorentz.complexCoBasisFin4)
        b1 ⊗ₜ[ℂ]
      (LinearEquiv.cast ⋯)
        ((match complexLorentzTensor.τ Color.downL with
          | Color.upL => Fermion.LeftHandedWeyl.basis
          | Color.downL => Fermion.DualLeftHandedWeyl.basis
          | Color.upR => Fermion.RightHandedWeyl.basis
          | Color.downR => Fermion.DualRightHandedWeyl.basis
          | Color.up => Lorentz.complexContrBasisFin4
          | Color.down => Lorentz.complexCoBasisFin4)
          b2)) =
  if b1 = Fin.cast pf✝ b2 then 1 else 0upRn:ℕc:Fin n → Colori:Fin nj:Fin nb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)b1:Fin (repDim Color.upR)b2:Fin (repDim (complexLorentzTensor.τ Color.upR))hij:i ≠ j ∧ complexLorentzTensor.τ Color.upR = complexLorentzTensor.τ Color.upRpf✝:repDim (complexLorentzTensor.τ Color.upR) = repDim Color.upR⊢ (complexLorentzTensor.contr Color.upR)
    ((match Color.upR with
        | Color.upL => Fermion.LeftHandedWeyl.basis
        | Color.downL => Fermion.DualLeftHandedWeyl.basis
        | Color.upR => Fermion.RightHandedWeyl.basis
        | Color.downR => Fermion.DualRightHandedWeyl.basis
        | Color.up => Lorentz.complexContrBasisFin4
        | Color.down => Lorentz.complexCoBasisFin4)
        b1 ⊗ₜ[ℂ]
      (LinearEquiv.cast ⋯)
        ((match complexLorentzTensor.τ Color.upR with
          | Color.upL => Fermion.LeftHandedWeyl.basis
          | Color.downL => Fermion.DualLeftHandedWeyl.basis
          | Color.upR => Fermion.RightHandedWeyl.basis
          | Color.downR => Fermion.DualRightHandedWeyl.basis
          | Color.up => Lorentz.complexContrBasisFin4
          | Color.down => Lorentz.complexCoBasisFin4)
          b2)) =
  if b1 = Fin.cast pf✝ b2 then 1 else 0downRn:ℕc:Fin n → Colori:Fin nj:Fin nb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)b1:Fin (repDim Color.downR)b2:Fin (repDim (complexLorentzTensor.τ Color.downR))hij:i ≠ j ∧ complexLorentzTensor.τ Color.downR = complexLorentzTensor.τ Color.downRpf✝:repDim (complexLorentzTensor.τ Color.downR) = repDim Color.downR⊢ (complexLorentzTensor.contr Color.downR)
    ((match Color.downR with
        | Color.upL => Fermion.LeftHandedWeyl.basis
        | Color.downL => Fermion.DualLeftHandedWeyl.basis
        | Color.upR => Fermion.RightHandedWeyl.basis
        | Color.downR => Fermion.DualRightHandedWeyl.basis
        | Color.up => Lorentz.complexContrBasisFin4
        | Color.down => Lorentz.complexCoBasisFin4)
        b1 ⊗ₜ[ℂ]
      (LinearEquiv.cast ⋯)
        ((match complexLorentzTensor.τ Color.downR with
          | Color.upL => Fermion.LeftHandedWeyl.basis
          | Color.downL => Fermion.DualLeftHandedWeyl.basis
          | Color.upR => Fermion.RightHandedWeyl.basis
          | Color.downR => Fermion.DualRightHandedWeyl.basis
          | Color.up => Lorentz.complexContrBasisFin4
          | Color.down => Lorentz.complexCoBasisFin4)
          b2)) =
  if b1 = Fin.cast pf✝ b2 then 1 else 0upn:ℕc:Fin n → Colori:Fin nj:Fin nb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)b1:Fin (repDim Color.up)b2:Fin (repDim (complexLorentzTensor.τ Color.up))hij:i ≠ j ∧ complexLorentzTensor.τ Color.up = complexLorentzTensor.τ Color.uppf✝:repDim (complexLorentzTensor.τ Color.up) = repDim Color.up⊢ (complexLorentzTensor.contr Color.up)
    ((match Color.up with
        | Color.upL => Fermion.LeftHandedWeyl.basis
        | Color.downL => Fermion.DualLeftHandedWeyl.basis
        | Color.upR => Fermion.RightHandedWeyl.basis
        | Color.downR => Fermion.DualRightHandedWeyl.basis
        | Color.up => Lorentz.complexContrBasisFin4
        | Color.down => Lorentz.complexCoBasisFin4)
        b1 ⊗ₜ[ℂ]
      (LinearEquiv.cast ⋯)
        ((match complexLorentzTensor.τ Color.up with
          | Color.upL => Fermion.LeftHandedWeyl.basis
          | Color.downL => Fermion.DualLeftHandedWeyl.basis
          | Color.upR => Fermion.RightHandedWeyl.basis
          | Color.downR => Fermion.DualRightHandedWeyl.basis
          | Color.up => Lorentz.complexContrBasisFin4
          | Color.down => Lorentz.complexCoBasisFin4)
          b2)) =
  if b1 = Fin.cast pf✝ b2 then 1 else 0downn:ℕc:Fin n → Colori:Fin nj:Fin nb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)b1:Fin (repDim Color.down)b2:Fin (repDim (complexLorentzTensor.τ Color.down))hij:i ≠ j ∧ complexLorentzTensor.τ Color.down = complexLorentzTensor.τ Color.downpf✝:repDim (complexLorentzTensor.τ Color.down) = repDim Color.down⊢ (complexLorentzTensor.contr Color.down)
    ((match Color.down with
        | Color.upL => Fermion.LeftHandedWeyl.basis
        | Color.downL => Fermion.DualLeftHandedWeyl.basis
        | Color.upR => Fermion.RightHandedWeyl.basis
        | Color.downR => Fermion.DualRightHandedWeyl.basis
        | Color.up => Lorentz.complexContrBasisFin4
        | Color.down => Lorentz.complexCoBasisFin4)
        b1 ⊗ₜ[ℂ]
      (LinearEquiv.cast ⋯)
        ((match complexLorentzTensor.τ Color.down with
          | Color.upL => Fermion.LeftHandedWeyl.basis
          | Color.downL => Fermion.DualLeftHandedWeyl.basis
          | Color.upR => Fermion.RightHandedWeyl.basis
          | Color.downR => Fermion.DualRightHandedWeyl.basis
          | Color.up => Lorentz.complexContrBasisFin4
          | Color.down => Lorentz.complexCoBasisFin4)
          b2)) =
  if b1 = Fin.cast pf✝ b2 then 1 else 0
  all_goals simp only [complexLorentzTensor, Fin.cast_refl, id_eq]downn:ℕc:Fin n → Colori:Fin nj:Fin nb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)b1:Fin (repDim Color.down)b2:Fin (repDim (complexLorentzTensor.τ Color.down))hij:i ≠ j ∧ complexLorentzTensor.τ Color.down = complexLorentzTensor.τ Color.downpf✝:repDim (complexLorentzTensor.τ Color.down) = repDim Color.down⊢ Lorentz.coContrContraction
    (Lorentz.complexCoBasisFin4 b1 ⊗ₜ[ℂ] (LinearEquiv.cast ⋯) (Lorentz.complexContrBasisFin4 b2)) =
  if b1 = b2 then 1 else 0
  ·upLn:ℕc:Fin n → Colori:Fin nj:Fin nb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)b1:Fin (repDim Color.upL)b2:Fin (repDim (complexLorentzTensor.τ Color.upL))hij:i ≠ j ∧ complexLorentzTensor.τ Color.upL = complexLorentzTensor.τ Color.upLpf✝:repDim (complexLorentzTensor.τ Color.upL) = repDim Color.upL⊢ Fermion.leftDualContraction
    (Fermion.LeftHandedWeyl.basis b1 ⊗ₜ[ℂ] (LinearEquiv.cast ⋯) (Fermion.DualLeftHandedWeyl.basis b2)) =
  if b1 = b2 then 1 else 0 erw [Fermion.leftDualContraction_basisupLn:ℕc:Fin n → Colori:Fin nj:Fin nb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)b1:Fin (repDim Color.upL)b2:Fin (repDim (complexLorentzTensor.τ Color.upL))hij:i ≠ j ∧ complexLorentzTensor.τ Color.upL = complexLorentzTensor.τ Color.upLpf✝:repDim (complexLorentzTensor.τ Color.upL) = repDim Color.upL⊢ (if ↑b1 = ↑b2 then 1 else 0) = if b1 = b2 then 1 else 0]upLn:ℕc:Fin n → Colori:Fin nj:Fin nb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)b1:Fin (repDim Color.upL)b2:Fin (repDim (complexLorentzTensor.τ Color.upL))hij:i ≠ j ∧ complexLorentzTensor.τ Color.upL = complexLorentzTensor.τ Color.upLpf✝:repDim (complexLorentzTensor.τ Color.upL) = repDim Color.upL⊢ (if ↑b1 = ↑b2 then 1 else 0) = if b1 = b2 then 1 else 0
    exact if_congr Fin.ext_iff.symm rfl rflAll goals completed! 🐙
  ·downLn:ℕc:Fin n → Colori:Fin nj:Fin nb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)b1:Fin (repDim Color.downL)b2:Fin (repDim (complexLorentzTensor.τ Color.downL))hij:i ≠ j ∧ complexLorentzTensor.τ Color.downL = complexLorentzTensor.τ Color.downLpf✝:repDim (complexLorentzTensor.τ Color.downL) = repDim Color.downL⊢ Fermion.dualLeftContraction
    (Fermion.DualLeftHandedWeyl.basis b1 ⊗ₜ[ℂ] (LinearEquiv.cast ⋯) (Fermion.LeftHandedWeyl.basis b2)) =
  if b1 = b2 then 1 else 0 erw [Fermion.dualLeftContraction_basisdownLn:ℕc:Fin n → Colori:Fin nj:Fin nb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)b1:Fin (repDim Color.downL)b2:Fin (repDim (complexLorentzTensor.τ Color.downL))hij:i ≠ j ∧ complexLorentzTensor.τ Color.downL = complexLorentzTensor.τ Color.downLpf✝:repDim (complexLorentzTensor.τ Color.downL) = repDim Color.downL⊢ (if ↑b1 = ↑b2 then 1 else 0) = if b1 = b2 then 1 else 0]downLn:ℕc:Fin n → Colori:Fin nj:Fin nb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)b1:Fin (repDim Color.downL)b2:Fin (repDim (complexLorentzTensor.τ Color.downL))hij:i ≠ j ∧ complexLorentzTensor.τ Color.downL = complexLorentzTensor.τ Color.downLpf✝:repDim (complexLorentzTensor.τ Color.downL) = repDim Color.downL⊢ (if ↑b1 = ↑b2 then 1 else 0) = if b1 = b2 then 1 else 0
    exact if_congr Fin.ext_iff.symm rfl rflAll goals completed! 🐙
  ·upRn:ℕc:Fin n → Colori:Fin nj:Fin nb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)b1:Fin (repDim Color.upR)b2:Fin (repDim (complexLorentzTensor.τ Color.upR))hij:i ≠ j ∧ complexLorentzTensor.τ Color.upR = complexLorentzTensor.τ Color.upRpf✝:repDim (complexLorentzTensor.τ Color.upR) = repDim Color.upR⊢ Fermion.rightDualContraction
    (Fermion.RightHandedWeyl.basis b1 ⊗ₜ[ℂ] (LinearEquiv.cast ⋯) (Fermion.DualRightHandedWeyl.basis b2)) =
  if b1 = b2 then 1 else 0 erw [Fermion.rightDualContraction_basisupRn:ℕc:Fin n → Colori:Fin nj:Fin nb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)b1:Fin (repDim Color.upR)b2:Fin (repDim (complexLorentzTensor.τ Color.upR))hij:i ≠ j ∧ complexLorentzTensor.τ Color.upR = complexLorentzTensor.τ Color.upRpf✝:repDim (complexLorentzTensor.τ Color.upR) = repDim Color.upR⊢ (if ↑b1 = ↑b2 then 1 else 0) = if b1 = b2 then 1 else 0]upRn:ℕc:Fin n → Colori:Fin nj:Fin nb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)b1:Fin (repDim Color.upR)b2:Fin (repDim (complexLorentzTensor.τ Color.upR))hij:i ≠ j ∧ complexLorentzTensor.τ Color.upR = complexLorentzTensor.τ Color.upRpf✝:repDim (complexLorentzTensor.τ Color.upR) = repDim Color.upR⊢ (if ↑b1 = ↑b2 then 1 else 0) = if b1 = b2 then 1 else 0
    exact if_congr Fin.ext_iff.symm rfl rflAll goals completed! 🐙
  ·downRn:ℕc:Fin n → Colori:Fin nj:Fin nb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)b1:Fin (repDim Color.downR)b2:Fin (repDim (complexLorentzTensor.τ Color.downR))hij:i ≠ j ∧ complexLorentzTensor.τ Color.downR = complexLorentzTensor.τ Color.downRpf✝:repDim (complexLorentzTensor.τ Color.downR) = repDim Color.downR⊢ Fermion.dualRightContraction
    (Fermion.DualRightHandedWeyl.basis b1 ⊗ₜ[ℂ] (LinearEquiv.cast ⋯) (Fermion.RightHandedWeyl.basis b2)) =
  if b1 = b2 then 1 else 0 erw [Fermion.dualRightContraction_basisdownRn:ℕc:Fin n → Colori:Fin nj:Fin nb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)b1:Fin (repDim Color.downR)b2:Fin (repDim (complexLorentzTensor.τ Color.downR))hij:i ≠ j ∧ complexLorentzTensor.τ Color.downR = complexLorentzTensor.τ Color.downRpf✝:repDim (complexLorentzTensor.τ Color.downR) = repDim Color.downR⊢ (if ↑b1 = ↑b2 then 1 else 0) = if b1 = b2 then 1 else 0]downRn:ℕc:Fin n → Colori:Fin nj:Fin nb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)b1:Fin (repDim Color.downR)b2:Fin (repDim (complexLorentzTensor.τ Color.downR))hij:i ≠ j ∧ complexLorentzTensor.τ Color.downR = complexLorentzTensor.τ Color.downRpf✝:repDim (complexLorentzTensor.τ Color.downR) = repDim Color.downR⊢ (if ↑b1 = ↑b2 then 1 else 0) = if b1 = b2 then 1 else 0
    exact if_congr Fin.ext_iff.symm rfl rflAll goals completed! 🐙
  ·upn:ℕc:Fin n → Colori:Fin nj:Fin nb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)b1:Fin (repDim Color.up)b2:Fin (repDim (complexLorentzTensor.τ Color.up))hij:i ≠ j ∧ complexLorentzTensor.τ Color.up = complexLorentzTensor.τ Color.uppf✝:repDim (complexLorentzTensor.τ Color.up) = repDim Color.up⊢ Lorentz.contrCoContraction
    (Lorentz.complexContrBasisFin4 b1 ⊗ₜ[ℂ] (LinearEquiv.cast ⋯) (Lorentz.complexCoBasisFin4 b2)) =
  if b1 = b2 then 1 else 0 erw [Lorentz.contrCoContraction_basisupn:ℕc:Fin n → Colori:Fin nj:Fin nb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)b1:Fin (repDim Color.up)b2:Fin (repDim (complexLorentzTensor.τ Color.up))hij:i ≠ j ∧ complexLorentzTensor.τ Color.up = complexLorentzTensor.τ Color.uppf✝:repDim (complexLorentzTensor.τ Color.up) = repDim Color.up⊢ (if ↑b1 = ↑b2 then 1 else 0) = if b1 = b2 then 1 else 0]upn:ℕc:Fin n → Colori:Fin nj:Fin nb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)b1:Fin (repDim Color.up)b2:Fin (repDim (complexLorentzTensor.τ Color.up))hij:i ≠ j ∧ complexLorentzTensor.τ Color.up = complexLorentzTensor.τ Color.uppf✝:repDim (complexLorentzTensor.τ Color.up) = repDim Color.up⊢ (if ↑b1 = ↑b2 then 1 else 0) = if b1 = b2 then 1 else 0
    exact if_congr Fin.ext_iff.symm rfl rflAll goals completed! 🐙
  ·downn:ℕc:Fin n → Colori:Fin nj:Fin nb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)b1:Fin (repDim Color.down)b2:Fin (repDim (complexLorentzTensor.τ Color.down))hij:i ≠ j ∧ complexLorentzTensor.τ Color.down = complexLorentzTensor.τ Color.downpf✝:repDim (complexLorentzTensor.τ Color.down) = repDim Color.down⊢ Lorentz.coContrContraction
    (Lorentz.complexCoBasisFin4 b1 ⊗ₜ[ℂ] (LinearEquiv.cast ⋯) (Lorentz.complexContrBasisFin4 b2)) =
  if b1 = b2 then 1 else 0 erw [Lorentz.coContrContraction_basisdownn:ℕc:Fin n → Colori:Fin nj:Fin nb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)b1:Fin (repDim Color.down)b2:Fin (repDim (complexLorentzTensor.τ Color.down))hij:i ≠ j ∧ complexLorentzTensor.τ Color.down = complexLorentzTensor.τ Color.downpf✝:repDim (complexLorentzTensor.τ Color.down) = repDim Color.down⊢ (if ↑b1 = ↑b2 then 1 else 0) = if b1 = b2 then 1 else 0]downn:ℕc:Fin n → Colori:Fin nj:Fin nb:ComponentIdx ch1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)b1:Fin (repDim Color.down)b2:Fin (repDim (complexLorentzTensor.τ Color.down))hij:i ≠ j ∧ complexLorentzTensor.τ Color.down = complexLorentzTensor.τ Color.downpf✝:repDim (complexLorentzTensor.τ Color.down) = repDim Color.down⊢ (if ↑b1 = ↑b2 then 1 else 0) = if b1 = b2 then 1 else 0
    exact if_congr Fin.ext_iff.symm rfl rflAll goals completed! 🐙