PhysLean Documentation

PhysLean.Relativity.Lorentz.ComplexTensor.Basic

Complex Lorentz tensors #

source
inductive complexLorentzTensor.Color :
Type

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

  • upL : Color

    The color associated with Left handed fermions.

  • downL : Color

    The color associated with alt-Left handed fermions.

  • upR : Color

    The color associated with Right handed fermions.

  • downR : Color

    The color associated with alt-Right handed fermions.

  • up : Color

    The color associated with contravariant Lorentz vectors.

  • down : Color

    The color associated with covariant Lorentz vectors.

Instances For
    source
    instance complexLorentzTensor.instDecidableEqColor :
    DecidableEq Color

    Color for complex Lorentz tensors is decidable.

    Equations
    source
    def complexLorentzTensor :
    TensorSpecies

    The tensor structure for complex Lorentz tensors.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      instance complexLorentzTensor.instDecidableEqC :
      DecidableEq complexLorentzTensor.C

      Color for complex Lorentz tensors is decidable.

      Equations
      source
      theorem complexLorentzTensor.basis_contr (c : complexLorentzTensor.C) (i : Fin (complexLorentzTensor.repDim c)) (j : Fin (complexLorentzTensor.repDim (complexLorentzTensor.τ c))) :
      complexLorentzTensor.castToField ((CategoryTheory.ConcreteCategory.hom (complexLorentzTensor.contr.app { as := c }).hom) ((complexLorentzTensor.basis c) i ⊗ₜ[complexLorentzTensor.k] (complexLorentzTensor.basis (complexLorentzTensor.τ c)) j)) = if ↑i = ↑j then 1 else 0

      Contracting two basis elements gives 1 if the index for the basis elements is the same, and 0 otherwise. Holds for any color of index.

      source
      instance complexLorentzTensor.instDecidableEqLeftDiscretePUnitMkFinC {n : ℕ} {c : Fin n → complexLorentzTensor.C} :
      DecidableEq (IndexNotation.OverColor.mk c).left

      For any object in the over color category, with source Fin n, has a decidable source.

      Equations
      source
      instance complexLorentzTensor.instFintypeLeftDiscretePUnitMkFinC {n : ℕ} {c : Fin n → complexLorentzTensor.C} :
      Fintype (IndexNotation.OverColor.mk c).left

      For any object in the over color category, with source Fin n, has a finite source.

      Equations
      source
      instance complexLorentzTensor.instCharZeroK :
      CharZero complexLorentzTensor.k
      source
      instance complexLorentzTensor.instDecidableEqHomOverColorCMkFin {n m : ℕ} {c : Fin n → complexLorentzTensor.C} {c1 : Fin m → complexLorentzTensor.C} (σ σ' : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c1) :
      Decidable (σ = σ')

      The equality of two maps in OverColor C from objects based on Fin _ is decidable.

      Equations
      source
      @[simp]
      theorem complexLorentzTensor.k_instSub :
      HSub.hSub = HSub.hSub
      source
      @[simp]
      theorem complexLorentzTensor.k_instAdd :
      HAdd.hAdd = HAdd.hAdd
      source
      @[simp]
      theorem complexLorentzTensor.k_neg :
      @Neg.neg complexLorentzTensor.k = @Neg.neg ℂ