Tensor product of two Weyl fermion

Equivalences to matrices.

def Fermion.leftLeftToMatrix : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj leftHanded leftHanded).V ≃ₗ[ℂ] Matrix (Fin 2) (Fin 2) ℂ

Equivalence of leftHanded ⊗ leftHanded to 2 x 2 complex matrices.

Equations

• Fermion.leftLeftToMatrix = (Fermion.leftBasis.tensorProduct Fermion.leftBasis).repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2) ≪≫ₗ LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)

theorem Fermion.leftLeftToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ) : leftLeftToMatrix.symm M = ∑ i : Fin 2, ∑ j : Fin 2, M i j • leftBasis i ⊗ₜ[ℂ] leftBasis j

Expanding leftLeftToMatrix in terms of the standard basis.

def Fermion.altLeftaltLeftToMatrix : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj altLeftHanded altLeftHanded).V ≃ₗ[ℂ] Matrix (Fin 2) (Fin 2) ℂ

Equivalence of altLeftHanded ⊗ altLeftHanded to 2 x 2 complex matrices.

Equations

• One or more equations did not get rendered due to their size.

theorem Fermion.altLeftaltLeftToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ) : altLeftaltLeftToMatrix.symm M = ∑ i : Fin 2, ∑ j : Fin 2, M i j • altLeftBasis i ⊗ₜ[ℂ] altLeftBasis j

Expanding altLeftaltLeftToMatrix in terms of the standard basis.

def Fermion.leftAltLeftToMatrix : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj leftHanded altLeftHanded).V ≃ₗ[ℂ] Matrix (Fin 2) (Fin 2) ℂ

Equivalence of leftHanded ⊗ altLeftHanded to 2 x 2 complex matrices.

Equations

• Fermion.leftAltLeftToMatrix = (Fermion.leftBasis.tensorProduct Fermion.altLeftBasis).repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2) ≪≫ₗ LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)

theorem Fermion.leftAltLeftToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ) : leftAltLeftToMatrix.symm M = ∑ i : Fin 2, ∑ j : Fin 2, M i j • leftBasis i ⊗ₜ[ℂ] altLeftBasis j

Expanding leftAltLeftToMatrix in terms of the standard basis.

def Fermion.altLeftLeftToMatrix : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj altLeftHanded leftHanded).V ≃ₗ[ℂ] Matrix (Fin 2) (Fin 2) ℂ

Equivalence of altLeftHanded ⊗ leftHanded to 2 x 2 complex matrices.

Equations

• Fermion.altLeftLeftToMatrix = (Fermion.altLeftBasis.tensorProduct Fermion.leftBasis).repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2) ≪≫ₗ LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)

theorem Fermion.altLeftLeftToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ) : altLeftLeftToMatrix.symm M = ∑ i : Fin 2, ∑ j : Fin 2, M i j • altLeftBasis i ⊗ₜ[ℂ] leftBasis j

Expanding altLeftLeftToMatrix in terms of the standard basis.

def Fermion.rightRightToMatrix : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj rightHanded rightHanded).V ≃ₗ[ℂ] Matrix (Fin 2) (Fin 2) ℂ

Equivalence of rightHanded ⊗ rightHanded to 2 x 2 complex matrices.

Equations

• Fermion.rightRightToMatrix = (Fermion.rightBasis.tensorProduct Fermion.rightBasis).repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2) ≪≫ₗ LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)

theorem Fermion.rightRightToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ) : rightRightToMatrix.symm M = ∑ i : Fin 2, ∑ j : Fin 2, M i j • rightBasis i ⊗ₜ[ℂ] rightBasis j

Expanding rightRightToMatrix in terms of the standard basis.

def Fermion.altRightAltRightToMatrix : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj altRightHanded altRightHanded).V ≃ₗ[ℂ] Matrix (Fin 2) (Fin 2) ℂ

Equivalence of altRightHanded ⊗ altRightHanded to 2 x 2 complex matrices.

Equations

• One or more equations did not get rendered due to their size.

theorem Fermion.altRightAltRightToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ) : altRightAltRightToMatrix.symm M = ∑ i : Fin 2, ∑ j : Fin 2, M i j • altRightBasis i ⊗ₜ[ℂ] altRightBasis j

Expanding altRightAltRightToMatrix in terms of the standard basis.

def Fermion.rightAltRightToMatrix : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj rightHanded altRightHanded).V ≃ₗ[ℂ] Matrix (Fin 2) (Fin 2) ℂ

Equivalence of rightHanded ⊗ altRightHanded to 2 x 2 complex matrices.

Equations

• One or more equations did not get rendered due to their size.

theorem Fermion.rightAltRightToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ) : rightAltRightToMatrix.symm M = ∑ i : Fin 2, ∑ j : Fin 2, M i j • rightBasis i ⊗ₜ[ℂ] altRightBasis j

Expanding rightAltRightToMatrix in terms of the standard basis.

def Fermion.altRightRightToMatrix : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj altRightHanded rightHanded).V ≃ₗ[ℂ] Matrix (Fin 2) (Fin 2) ℂ

Equivalence of altRightHanded ⊗ rightHanded to 2 x 2 complex matrices.

Equations

• One or more equations did not get rendered due to their size.

theorem Fermion.altRightRightToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ) : altRightRightToMatrix.symm M = ∑ i : Fin 2, ∑ j : Fin 2, M i j • altRightBasis i ⊗ₜ[ℂ] rightBasis j

Expanding altRightRightToMatrix in terms of the standard basis.

def Fermion.altLeftAltRightToMatrix : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj altLeftHanded altRightHanded).V ≃ₗ[ℂ] Matrix (Fin 2) (Fin 2) ℂ

Equivalence of altLeftHanded ⊗ altRightHanded to 2 x 2 complex matrices.

Equations

• One or more equations did not get rendered due to their size.

theorem Fermion.altLeftAltRightToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ) : altLeftAltRightToMatrix.symm M = ∑ i : Fin 2, ∑ j : Fin 2, M i j • altLeftBasis i ⊗ₜ[ℂ] altRightBasis j

Expanding altLeftAltRightToMatrix in terms of the standard basis.

def Fermion.leftRightToMatrix : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj leftHanded rightHanded).V ≃ₗ[ℂ] Matrix (Fin 2) (Fin 2) ℂ

Equivalence of leftHanded ⊗ rightHanded to 2 x 2 complex matrices.

Equations

• Fermion.leftRightToMatrix = (Fermion.leftBasis.tensorProduct Fermion.rightBasis).repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2) ≪≫ₗ LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)

theorem Fermion.leftRightToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ) : leftRightToMatrix.symm M = ∑ i : Fin 2, ∑ j : Fin 2, M i j • leftBasis i ⊗ₜ[ℂ] rightBasis j

Expanding leftRightToMatrix in terms of the standard basis.

Group actions

theorem Fermion.leftLeftToMatrix_ρ (v : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj leftHanded leftHanded).V) (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) : leftLeftToMatrix ((TensorProduct.map (leftHanded.ρ M) (leftHanded.ρ M)) v) = ↑M * leftLeftToMatrix v * (↑M).transpose

The group action of SL(2,ℂ) on leftHanded ⊗ leftHanded is equivalent to M.1 * leftLeftToMatrix v * (M.1)ᵀ.

theorem Fermion.altLeftaltLeftToMatrix_ρ (v : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj altLeftHanded altLeftHanded).V) (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) : altLeftaltLeftToMatrix ((TensorProduct.map (altLeftHanded.ρ M) (altLeftHanded.ρ M)) v) = (↑M)⁻¹.transpose * altLeftaltLeftToMatrix v * (↑M)⁻¹

The group action of SL(2,ℂ) on altLeftHanded ⊗ altLeftHanded is equivalent to (M.1⁻¹)ᵀ * leftLeftToMatrix v * (M.1⁻¹).

theorem Fermion.leftAltLeftToMatrix_ρ (v : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj leftHanded altLeftHanded).V) (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) : leftAltLeftToMatrix ((TensorProduct.map (leftHanded.ρ M) (altLeftHanded.ρ M)) v) = ↑M * leftAltLeftToMatrix v * (↑M)⁻¹

The group action of SL(2,ℂ) on leftHanded ⊗ altLeftHanded is equivalent to M.1 * leftAltLeftToMatrix v * (M.1⁻¹).

theorem Fermion.altLeftLeftToMatrix_ρ (v : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj altLeftHanded leftHanded).V) (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) : altLeftLeftToMatrix ((TensorProduct.map (altLeftHanded.ρ M) (leftHanded.ρ M)) v) = (↑M)⁻¹.transpose * altLeftLeftToMatrix v * (↑M).transpose

The group action of SL(2,ℂ) on altLeftHanded ⊗ leftHanded is equivalent to (M.1⁻¹)ᵀ * leftAltLeftToMatrix v * (M.1)ᵀ.

theorem Fermion.rightRightToMatrix_ρ (v : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj rightHanded rightHanded).V) (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) : rightRightToMatrix ((TensorProduct.map (rightHanded.ρ M) (rightHanded.ρ M)) v) = (↑M).map star * rightRightToMatrix v * ((↑M).map star).transpose

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

theorem Fermion.altRightAltRightToMatrix_ρ (v : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj altRightHanded altRightHanded).V) (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) : altRightAltRightToMatrix ((TensorProduct.map (altRightHanded.ρ M) (altRightHanded.ρ M)) v) = (↑M)⁻¹.conjTranspose * altRightAltRightToMatrix v * (↑M)⁻¹.conjTranspose.transpose

The group action of SL(2,ℂ) on altRightHanded ⊗ altRightHanded is equivalent to ((M.1⁻¹).conjTranspose * rightRightToMatrix v * (((M.1⁻¹).conjTranspose)ᵀ.

theorem Fermion.rightAltRightToMatrix_ρ (v : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj rightHanded altRightHanded).V) (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) : rightAltRightToMatrix ((TensorProduct.map (rightHanded.ρ M) (altRightHanded.ρ M)) v) = (↑M).map star * rightAltRightToMatrix v * (↑M)⁻¹.conjTranspose.transpose

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

theorem Fermion.altRightRightToMatrix_ρ (v : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj altRightHanded rightHanded).V) (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) : altRightRightToMatrix ((TensorProduct.map (altRightHanded.ρ M) (rightHanded.ρ M)) v) = (↑M)⁻¹.conjTranspose * altRightRightToMatrix v * ((↑M).map star).transpose

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

theorem Fermion.altLeftAltRightToMatrix_ρ (v : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj altLeftHanded altRightHanded).V) (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) : altLeftAltRightToMatrix ((TensorProduct.map (altLeftHanded.ρ M) (altRightHanded.ρ M)) v) = (↑M)⁻¹.transpose * altLeftAltRightToMatrix v * (↑M)⁻¹.conjTranspose.transpose

theorem Fermion.leftRightToMatrix_ρ (v : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj leftHanded rightHanded).V) (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) : leftRightToMatrix ((TensorProduct.map (leftHanded.ρ M) (rightHanded.ρ M)) v) = ↑M * leftRightToMatrix v * (↑M).conjTranspose

The symm version of the group actions.

theorem Fermion.leftLeftToMatrix_ρ_symm (v : Matrix (Fin 2) (Fin 2) ℂ) (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) : (TensorProduct.map (leftHanded.ρ M) (leftHanded.ρ M)) (leftLeftToMatrix.symm v) = leftLeftToMatrix.symm (↑M * v * (↑M).transpose)

theorem Fermion.altLeftaltLeftToMatrix_ρ_symm (v : Matrix (Fin 2) (Fin 2) ℂ) (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) : (TensorProduct.map (altLeftHanded.ρ M) (altLeftHanded.ρ M)) (altLeftaltLeftToMatrix.symm v) = altLeftaltLeftToMatrix.symm ((↑M)⁻¹.transpose * v * (↑M)⁻¹)

theorem Fermion.leftAltLeftToMatrix_ρ_symm (v : Matrix (Fin 2) (Fin 2) ℂ) (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) : (TensorProduct.map (leftHanded.ρ M) (altLeftHanded.ρ M)) (leftAltLeftToMatrix.symm v) = leftAltLeftToMatrix.symm (↑M * v * (↑M)⁻¹)

theorem Fermion.altLeftLeftToMatrix_ρ_symm (v : Matrix (Fin 2) (Fin 2) ℂ) (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) : (TensorProduct.map (altLeftHanded.ρ M) (leftHanded.ρ M)) (altLeftLeftToMatrix.symm v) = altLeftLeftToMatrix.symm ((↑M)⁻¹.transpose * v * (↑M).transpose)

theorem Fermion.rightRightToMatrix_ρ_symm (v : Matrix (Fin 2) (Fin 2) ℂ) (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) : (TensorProduct.map (rightHanded.ρ M) (rightHanded.ρ M)) (rightRightToMatrix.symm v) = rightRightToMatrix.symm ((↑M).map star * v * ((↑M).map star).transpose)

theorem Fermion.altRightAltRightToMatrix_ρ_symm (v : Matrix (Fin 2) (Fin 2) ℂ) (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) : (TensorProduct.map (altRightHanded.ρ M) (altRightHanded.ρ M)) (altRightAltRightToMatrix.symm v) = altRightAltRightToMatrix.symm ((↑M)⁻¹.conjTranspose * v * (↑M)⁻¹.conjTranspose.transpose)

theorem Fermion.rightAltRightToMatrix_ρ_symm (v : Matrix (Fin 2) (Fin 2) ℂ) (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) : (TensorProduct.map (rightHanded.ρ M) (altRightHanded.ρ M)) (rightAltRightToMatrix.symm v) = rightAltRightToMatrix.symm ((↑M).map star * v * (↑M)⁻¹.conjTranspose.transpose)

theorem Fermion.altRightRightToMatrix_ρ_symm (v : Matrix (Fin 2) (Fin 2) ℂ) (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) : (TensorProduct.map (altRightHanded.ρ M) (rightHanded.ρ M)) (altRightRightToMatrix.symm v) = altRightRightToMatrix.symm ((↑M)⁻¹.conjTranspose * v * ((↑M).map star).transpose)

theorem Fermion.altLeftAltRightToMatrix_ρ_symm (v : Matrix (Fin 2) (Fin 2) ℂ) (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) : (TensorProduct.map (altLeftHanded.ρ M) (altRightHanded.ρ M)) (altLeftAltRightToMatrix.symm v) = altLeftAltRightToMatrix.symm ((↑M)⁻¹.transpose * v * (↑M)⁻¹.conjTranspose.transpose)

theorem Fermion.leftRightToMatrix_ρ_symm (v : Matrix (Fin 2) (Fin 2) ℂ) (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) : (TensorProduct.map (leftHanded.ρ M) (rightHanded.ρ M)) (leftRightToMatrix.symm v) = leftRightToMatrix.symm (↑M * v * (↑M).conjTranspose)

theorem Fermion.altLeftAltRightToMatrix_ρ_symm_selfAdjoint (v : Matrix (Fin 2) (Fin 2) ℂ) (hv : IsSelfAdjoint v) (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) : (TensorProduct.map (altLeftHanded.ρ M) (altRightHanded.ρ M)) (altLeftAltRightToMatrix.symm v) = altLeftAltRightToMatrix.symm ↑((Lorentz.SL2C.toSelfAdjointMap M.transpose⁻¹) ⟨v, hv⟩)

theorem Fermion.leftRightToMatrix_ρ_symm_selfAdjoint (v : Matrix (Fin 2) (Fin 2) ℂ) (hv : IsSelfAdjoint v) (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) : (TensorProduct.map (leftHanded.ρ M) (rightHanded.ρ M)) (leftRightToMatrix.symm v) = leftRightToMatrix.symm ↑((Lorentz.SL2C.toSelfAdjointMap M) ⟨v, hv⟩)