Tensor products of two real Lorentz vectors

def Lorentz.contrContrToMatrixRe {d : ℕ} : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj (Contr d) (Contr d)).V ≃ₗ[ℝ] Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ

Equivalence of Contr ⊗ Contr to (1 + d) x (1 + d) real matrices.

Equations

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

theorem Lorentz.contrContrToMatrixRe_symm_expand_tmul {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) : contrContrToMatrixRe.symm M = ∑ i : Fin 1 ⊕ Fin d, ∑ j : Fin 1 ⊕ Fin d, M i j • (contrBasis d) i ⊗ₜ[ℝ] (contrBasis d) j

Expanding contrContrToMatrixRe in terms of the standard basis.

def Lorentz.coCoToMatrixRe {d : ℕ} : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj (Co d) (Co d)).V ≃ₗ[ℝ] Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ

Equivalence of Co ⊗ Co to (1 + d) x (1 + d) real matrices.

Equations

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

theorem Lorentz.coCoToMatrixRe_symm_expand_tmul {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) : coCoToMatrixRe.symm M = ∑ i : Fin 1 ⊕ Fin d, ∑ j : Fin 1 ⊕ Fin d, M i j • (coBasis d) i ⊗ₜ[ℝ] (coBasis d) j

Expanding coCoToMatrixRe in terms of the standard basis.

def Lorentz.contrCoToMatrixRe {d : ℕ} : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj (Contr d) (Co d)).V ≃ₗ[ℝ] Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ

Equivalence of Contr d ⊗ Co d to (1 + d) x (1 + d) real matrices.

Equations

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

theorem Lorentz.contrCoToMatrixRe_symm_expand_tmul {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) : contrCoToMatrixRe.symm M = ∑ i : Fin 1 ⊕ Fin d, ∑ j : Fin 1 ⊕ Fin d, M i j • (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) j

Expansion of (coBasis d) (coBasis d) in terms of the standard basis.

def Lorentz.coContrToMatrixRe {d : ℕ} : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj (Co d) (Contr d)).V ≃ₗ[ℝ] Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ

Equivalence of Co d ⊗ Contr d to (1 + d) x (1 + d) real matrices.

Equations

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

theorem Lorentz.coContrToMatrixRe_symm_expand_tmul {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) : coContrToMatrixRe.symm M = ∑ i : Fin 1 ⊕ Fin d, ∑ j : Fin 1 ⊕ Fin d, M i j • (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) j

Expansion of coContrToMatrixRe in terms of the standard basis.

Group actions

theorem Lorentz.contrContrToMatrixRe_ρ {d : ℕ} (v : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj (Contr d) (Contr d)).V) (M : ↑(LorentzGroup d)) : contrContrToMatrixRe ((TensorProduct.map ((Contr d).ρ M) ((Contr d).ρ M)) v) = ↑M * contrContrToMatrixRe v * (↑M).transpose

theorem Lorentz.coCoToMatrixRe_ρ {d : ℕ} (v : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj (Co d) (Co d)).V) (M : ↑(LorentzGroup d)) : coCoToMatrixRe ((TensorProduct.map ((Co d).ρ M) ((Co d).ρ M)) v) = (↑M)⁻¹.transpose * coCoToMatrixRe v * ↑M⁻¹

theorem Lorentz.contrCoToMatrixRe_ρ {d : ℕ} (v : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj (Contr d) (Co d)).V) (M : ↑(LorentzGroup d)) : contrCoToMatrixRe ((TensorProduct.map ((Contr d).ρ M) ((Co d).ρ M)) v) = ↑M * contrCoToMatrixRe v * (↑M)⁻¹

theorem Lorentz.coContrToMatrixRe_ρ {d : ℕ} (v : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj (Co d) (Contr d)).V) (M : ↑(LorentzGroup d)) : coContrToMatrixRe ((TensorProduct.map ((Co d).ρ M) ((Contr d).ρ M)) v) = (↑M)⁻¹.transpose * coContrToMatrixRe v * (↑M).transpose

The symm version of the group actions.

theorem Lorentz.contrContrToMatrixRe_ρ_symm {d : ℕ} (v : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (M : ↑(LorentzGroup d)) : (TensorProduct.map ((Contr d).ρ M) ((Contr d).ρ M)) (contrContrToMatrixRe.symm v) = contrContrToMatrixRe.symm (↑M * v * (↑M).transpose)

theorem Lorentz.coCoToMatrixRe_ρ_symm {d : ℕ} (v : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (M : ↑(LorentzGroup d)) : (TensorProduct.map ((Co d).ρ M) ((Co d).ρ M)) (coCoToMatrixRe.symm v) = coCoToMatrixRe.symm ((↑M)⁻¹.transpose * v * (↑M)⁻¹)

theorem Lorentz.contrCoToMatrixRe_ρ_symm {d : ℕ} (v : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (M : ↑(LorentzGroup d)) : (TensorProduct.map ((Contr d).ρ M) ((Co d).ρ M)) (contrCoToMatrixRe.symm v) = contrCoToMatrixRe.symm (↑M * v * (↑M)⁻¹)

theorem Lorentz.coContrToMatrixRe_ρ_symm {d : ℕ} (v : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (M : ↑(LorentzGroup d)) : (TensorProduct.map ((Co d).ρ M) ((Contr d).ρ M)) (coContrToMatrixRe.symm v) = coContrToMatrixRe.symm ((↑M)⁻¹.transpose * v * (↑M).transpose)