Physlib Documentation

Physlib.Relativity.Tensors.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 ℂ complexLorentzTensor.Color (Matrix.SpecialLinearGroup (Fin 2) ℂ)

    The tensor structure for complex Lorentz tensors.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def complexLorentzTensor.complexLorentzTensorSyntax :
      Lean.ParserDescr

      Complex Lorentz tensor.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def complexLorentzTensor.«termℂT(_)» :
        Lean.ParserDescr

        Complex Lorentz tensor.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem complexLorentzTensor.basis_contr (c : Color) (i : Fin (complexLorentzTensor.repDim c)) (j : Fin (complexLorentzTensor.repDim (complexLorentzTensor.τ c))) :
          TensorSpecies.castToField ((CategoryTheory.ConcreteCategory.hom (complexLorentzTensor.contr.app { as := c }).hom) ((complexLorentzTensor.basis c) i ⊗ₜ[ℂ] (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.instDecidableEqLeftColorMkFin {n : ℕ} {c : Fin n → Color} :
          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.instFintypeLeftColorMkFin {n : ℕ} {c : Fin n → Color} :
          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.instDecidableEqHomOverColorColorMkFin {n m : ℕ} {c : Fin n → Color} {c1 : Fin m → Color} (σ σ' : 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
          • One or more equations did not get rendered due to their size.

          Relating basis #

          source
          theorem complexLorentzTensor.basis_up_eq {i : Fin 4} :
          (complexLorentzTensor.basis Color.up) i = Lorentz.complexContrBasisFin4 i
          source
          theorem complexLorentzTensor.basis_down_eq {i : Fin 4} :
          (complexLorentzTensor.basis Color.down) i = Lorentz.complexCoBasisFin4 i
          source
          @[simp]
          theorem complexLorentzTensor.basis_eq_complexContrBasisFin4 :
          complexLorentzTensor.basis Color.up = Lorentz.complexContrBasisFin4
          source
          @[simp]
          theorem complexLorentzTensor.basis_eq_complexCoBasisFin4 :
          complexLorentzTensor.basis Color.down = Lorentz.complexCoBasisFin4
          source
          @[simp]
          theorem complexLorentzTensor.FD_obj_up (Λ : Matrix.SpecialLinearGroup (Fin 2) ℂ) :
          (complexLorentzTensor.FD.obj { as := Color.up }).ρ Λ = Lorentz.complexContr.ρ Λ
          source
          @[simp]
          theorem complexLorentzTensor.FD_obj_down (Λ : Matrix.SpecialLinearGroup (Fin 2) ℂ) :
          (complexLorentzTensor.FD.obj { as := Color.down }).ρ Λ = Lorentz.complexCo.ρ Λ
          source
          theorem complexLorentzTensor.basis_upL_eq {i : Fin 2} :
          (complexLorentzTensor.basis Color.upL) i = Fermion.leftBasis i
          source
          theorem complexLorentzTensor.basis_downL_eq {i : Fin 2} :
          (complexLorentzTensor.basis Color.downL) i = Fermion.altLeftBasis i
          source
          theorem complexLorentzTensor.basis_upR_eq {i : Fin 2} :
          (complexLorentzTensor.basis Color.upR) i = Fermion.rightBasis i
          source
          theorem complexLorentzTensor.basis_downR_eq {i : Fin 2} :
          (complexLorentzTensor.basis Color.downR) i = Fermion.altRightBasis i

          Vector slot component formulas (Color.up / Color.down) #

          The colors Color.up and Color.down are the standard Lorentz vector colors. The lemmas repr_ρ_basis_vector_up and repr_ρ_basis_vector_down are stated for Fin 4 indices (definitionally Fin (repDim Color.up) and Fin (repDim Color.down)).

          When a slot is only known up to c₀ = Color.up or Color.down, use repr_ρ_basis_vector_up_of_eq / repr_ρ_basis_vector_down_of_eq.

          source
          theorem complexLorentzTensor.repr_ρ_basis_vector_up (Λ : Matrix.SpecialLinearGroup (Fin 2) ℂ) (b i : Fin 4) :
          ((complexLorentzTensor.basis Color.up).repr (((complexLorentzTensor.FD.obj { as := Color.up }).ρ Λ) ((complexLorentzTensor.basis Color.up) b))) i = LorentzGroup.toComplex (Lorentz.SL2C.toLorentzGroup Λ) (finSumFinEquiv.symm i) (finSumFinEquiv.symm b)

          Component formula for the standard contravariant vector slot Color.up.

          For b, i : Fin 4, the i-component of ρ Λ on basis Color.up b equals the corresponding entry of LorentzGroup.toComplex (SL2C.toLorentzGroup Λ) in Fin 1 ⊕ Fin 3 coordinates.

          source
          theorem complexLorentzTensor.repr_ρ_basis_vector_up_of_eq (c₀ : Color) (h : c₀ = Color.up) (Λ : Matrix.SpecialLinearGroup (Fin 2) ℂ) (b i : Fin (complexLorentzTensor.repDim c₀)) :
          ((complexLorentzTensor.basis c₀).repr (((complexLorentzTensor.FD.obj { as := c₀ }).ρ Λ) ((complexLorentzTensor.basis c₀) b))) i = LorentzGroup.toComplex (Lorentz.SL2C.toLorentzGroup Λ) (finSumFinEquiv.symm (Fin.cast ⋯ i)) (finSumFinEquiv.symm (Fin.cast ⋯ b))

          Transport version of repr_ρ_basis_vector_up for a color c₀ that is propositionally Color.up.

          source
          theorem complexLorentzTensor.repr_ρ_basis_vector_down (Λ : Matrix.SpecialLinearGroup (Fin 2) ℂ) (b i : Fin 4) :
          ((complexLorentzTensor.basis Color.down).repr (((complexLorentzTensor.FD.obj { as := Color.down }).ρ Λ) ((complexLorentzTensor.basis Color.down) b))) i = (LorentzGroup.toComplex (Lorentz.SL2C.toLorentzGroup Λ))⁻¹ (finSumFinEquiv.symm b) (finSumFinEquiv.symm i)

          Component formula for the standard covariant vector slot Color.down.

          For b, i : Fin 4, the i-component of ρ Λ on basis Color.down b matches the inverse complex Lorentz matrix as in Lorentz.complexCoBasis_ρ_apply (with transpose indexing on Fin 1 ⊕ Fin 3).

          source
          theorem complexLorentzTensor.repr_ρ_basis_vector_down_of_eq (c₀ : Color) (h : c₀ = Color.down) (Λ : Matrix.SpecialLinearGroup (Fin 2) ℂ) (b i : Fin (complexLorentzTensor.repDim c₀)) :
          ((complexLorentzTensor.basis c₀).repr (((complexLorentzTensor.FD.obj { as := c₀ }).ρ Λ) ((complexLorentzTensor.basis c₀) b))) i = (LorentzGroup.toComplex (Lorentz.SL2C.toLorentzGroup Λ))⁻¹ (finSumFinEquiv.symm (Fin.cast ⋯ b)) (finSumFinEquiv.symm (Fin.cast ⋯ i))

          Transport version of repr_ρ_basis_vector_down for a color c₀ that is propositionally Color.down.