Research proof index

Expanding rightRightToMatrix in terms of the standard basis.

The group action of SL(2,ℂ) on rightHanded ⊗ rightHanded is equivalent to (M.1.map star) * rightRightToMatrix v * ((M.1.map star))ᵀ.

For a field specification 𝓕, normalOrderF is the linear map FieldOpFreeAlgebra 𝓕 →ₗ[ℂ] FieldOpFreeAlgebra 𝓕 defined by its action on the basis ofCrAnListF φs, taking ofCrAnListF φs to normalOrderSign φs • ofCrAnListF (normalOrderList φs). That is, normalOrderF normal-orders the field operators and multiplies by the sign of the normal orde...

For a field specification 𝓕, and two lists φs = φ₀…φₙ and φs' of 𝓕.CrAnFieldOp the following super commutation relation holds: [φs', φ₀…φₙ]ₛF = ∑ i, 𝓢(φs', φ₀…φᵢ₋₁) • φ₀…φᵢ₋₁ * [φs', φᵢ]ₛF * φᵢ₊₁ … φₙ The proof of this relation is via induction on the length of φs. -/ lemma superCommuteF_ofCrAnListF_ofCrAnListF_eq_sum (φs : List 𝓕.CrAnFiel...

For a field specification 𝓕, the super commutator superCommuteF is defined as the linear map 𝓕.FieldOpFreeAlgebra →ₗ[ℂ] 𝓕.FieldOpFreeAlgebra →ₗ[ℂ] 𝓕.FieldOpFreeAlgebra which on the lists φs and φs' of 𝓕.CrAnFieldOp gives superCommuteF φs φs' = φs * φs' - 𝓢(φs, φs') • φs' * φs. The notation [a, b]ₛF can be used for superCommuteF a b...

In the state algebra time, ordering obeys T(φ₀φ₁…φₙ) = s * φᵢ * T(φ₀φ₁…φᵢ₋₁φᵢ₊₁…φₙ) where φᵢ is the state which has maximum time and s is the exchange sign of φᵢ and φ₀φ₁…φᵢ₋₁.