1. Physlib
  2. Relativity
  3. Tensors
  4. RealTensor
  5. Matrix
  6. Pre
Imports
/- Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ module public import Physlib.Relativity.Tensors.RealTensor.Vector.Pre.Basic public import Mathlib.LinearAlgebra.TensorProduct.Matrix

Tensor products of two real Lorentz vectors

@[expose] public section

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

def contrContrToMatrixRe {d : ℕ} : (ContrMod d ⊗[ℝ] ContrMod d) ≃ₗ[ℝ] Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ := (Basis.tensorProduct (contrBasis d) (contrBasis d)).repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℝ ℝ ((Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)) ≪≫ₗ LinearEquiv.curry ℝ ℝ (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d)

Expanding contrContrToMatrixRe in terms of the standard basis.

d:ℕM:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ⊢ ∑ x, ∑ y, ((Finsupp.linearEquivFunOnFinite ℝ ℝ ((Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d))).symm ((LinearEquiv.curry ℝ ℝ (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d)).symm M)) (x, y) • ((contrBasis d).tensorProduct (contrBasis d)) (x, y) = ∑ i, ∑ j, M i j • (contrBasis d) i ⊗ₜ[ℝ] (contrBasis d) j d:ℕM:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝi:Fin 1 ⊕ Fin dx✝¹:i ∈ Finset.univj:Fin 1 ⊕ Fin dx✝:j ∈ Finset.univ⊢ ((Finsupp.linearEquivFunOnFinite ℝ ℝ ((Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d))).symm ((LinearEquiv.curry ℝ ℝ (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d)).symm M)) (i, j) • ((contrBasis d).tensorProduct (contrBasis d)) (i, j) = M i j • (contrBasis d) i ⊗ₜ[ℝ] (contrBasis d) j erw [d:ℕM:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝi:Fin 1 ⊕ Fin dx✝¹:i ∈ Finset.univj:Fin 1 ⊕ Fin dx✝:j ∈ Finset.univ⊢ ((Finsupp.linearEquivFunOnFinite ℝ ℝ ((Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d))).symm ((LinearEquiv.curry ℝ ℝ (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d)).symm M)) (i, j) • (contrBasis d) i ⊗ₜ[ℝ] (contrBasis d) j = M i j • (contrBasis d) i ⊗ₜ[ℝ] (contrBasis d) jd:ℕM:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝi:Fin 1 ⊕ Fin dx✝¹:i ∈ Finset.univj:Fin 1 ⊕ Fin dx✝:j ∈ Finset.univ⊢ ((Finsupp.linearEquivFunOnFinite ℝ ℝ ((Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d))).symm ((LinearEquiv.curry ℝ ℝ (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d)).symm M)) (i, j) • (contrBasis d) i ⊗ₜ[ℝ] (contrBasis d) j = M i j • (contrBasis d) i ⊗ₜ[ℝ] (contrBasis d) j All goals completed! 🐙 d:ℕM:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ⊢ (Finsupp.linearEquivFunOnFinite ℝ ℝ ((Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d))).symm ((LinearEquiv.curry ℝ ℝ (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d)).symm M) ∈ Finsupp.supported ℝ ℝ ↑Finset.univ All goals completed! 🐙

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

def coCoToMatrixRe {d : ℕ} : (CoMod d ⊗[ℝ] CoMod d) ≃ₗ[ℝ] Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ := (Basis.tensorProduct (coBasis d) (coBasis d)).repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℝ ℝ ((Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)) ≪≫ₗ LinearEquiv.curry ℝ ℝ (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d)

Expanding coCoToMatrixRe in terms of the standard basis.

d:ℕM:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ⊢ ∑ x, ∑ y, ((Finsupp.linearEquivFunOnFinite ℝ ℝ ((Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d))).symm ((LinearEquiv.curry ℝ ℝ (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d)).symm M)) (x, y) • ((coBasis d).tensorProduct (coBasis d)) (x, y) = ∑ i, ∑ j, M i j • (coBasis d) i ⊗ₜ[ℝ] (coBasis d) j d:ℕM:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝi:Fin 1 ⊕ Fin dx✝¹:i ∈ Finset.univj:Fin 1 ⊕ Fin dx✝:j ∈ Finset.univ⊢ ((Finsupp.linearEquivFunOnFinite ℝ ℝ ((Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d))).symm ((LinearEquiv.curry ℝ ℝ (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d)).symm M)) (i, j) • ((coBasis d).tensorProduct (coBasis d)) (i, j) = M i j • (coBasis d) i ⊗ₜ[ℝ] (coBasis d) j erw [d:ℕM:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝi:Fin 1 ⊕ Fin dx✝¹:i ∈ Finset.univj:Fin 1 ⊕ Fin dx✝:j ∈ Finset.univ⊢ ((Finsupp.linearEquivFunOnFinite ℝ ℝ ((Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d))).symm ((LinearEquiv.curry ℝ ℝ (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d)).symm M)) (i, j) • (coBasis d) i ⊗ₜ[ℝ] (coBasis d) j = M i j • (coBasis d) i ⊗ₜ[ℝ] (coBasis d) jd:ℕM:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝi:Fin 1 ⊕ Fin dx✝¹:i ∈ Finset.univj:Fin 1 ⊕ Fin dx✝:j ∈ Finset.univ⊢ ((Finsupp.linearEquivFunOnFinite ℝ ℝ ((Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d))).symm ((LinearEquiv.curry ℝ ℝ (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d)).symm M)) (i, j) • (coBasis d) i ⊗ₜ[ℝ] (coBasis d) j = M i j • (coBasis d) i ⊗ₜ[ℝ] (coBasis d) j All goals completed! 🐙 d:ℕM:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ⊢ (Finsupp.linearEquivFunOnFinite ℝ ℝ ((Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d))).symm ((LinearEquiv.curry ℝ ℝ (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d)).symm M) ∈ Finsupp.supported ℝ ℝ ↑Finset.univ All goals completed! 🐙

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

def contrCoToMatrixRe {d : ℕ} : (ContrMod d ⊗[ℝ] CoMod d) ≃ₗ[ℝ] Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ := (Basis.tensorProduct (contrBasis d) (coBasis d)).repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℝ ℝ ((Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)) ≪≫ₗ LinearEquiv.curry ℝ ℝ (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d)

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

d:ℕM:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ⊢ ∑ x, ∑ y, ((Finsupp.linearEquivFunOnFinite ℝ ℝ ((Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d))).symm ((LinearEquiv.curry ℝ ℝ (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d)).symm M)) (x, y) • ((contrBasis d).tensorProduct (coBasis d)) (x, y) = ∑ i, ∑ j, M i j • (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) j d:ℕM:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝi:Fin 1 ⊕ Fin dx✝¹:i ∈ Finset.univj:Fin 1 ⊕ Fin dx✝:j ∈ Finset.univ⊢ ((Finsupp.linearEquivFunOnFinite ℝ ℝ ((Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d))).symm ((LinearEquiv.curry ℝ ℝ (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d)).symm M)) (i, j) • ((contrBasis d).tensorProduct (coBasis d)) (i, j) = M i j • (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) j erw [d:ℕM:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝi:Fin 1 ⊕ Fin dx✝¹:i ∈ Finset.univj:Fin 1 ⊕ Fin dx✝:j ∈ Finset.univ⊢ ((Finsupp.linearEquivFunOnFinite ℝ ℝ ((Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d))).symm ((LinearEquiv.curry ℝ ℝ (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d)).symm M)) (i, j) • (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) j = M i j • (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) jd:ℕM:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝi:Fin 1 ⊕ Fin dx✝¹:i ∈ Finset.univj:Fin 1 ⊕ Fin dx✝:j ∈ Finset.univ⊢ ((Finsupp.linearEquivFunOnFinite ℝ ℝ ((Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d))).symm ((LinearEquiv.curry ℝ ℝ (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d)).symm M)) (i, j) • (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) j = M i j • (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) j All goals completed! 🐙 d:ℕM:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ⊢ (Finsupp.linearEquivFunOnFinite ℝ ℝ ((Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d))).symm ((LinearEquiv.curry ℝ ℝ (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d)).symm M) ∈ Finsupp.supported ℝ ℝ ↑Finset.univ All goals completed! 🐙

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

def coContrToMatrixRe : (CoMod d ⊗[ℝ] ContrMod d) ≃ₗ[ℝ] Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ := (Basis.tensorProduct (coBasis d) (contrBasis d)).repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℝ ℝ ((Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)) ≪≫ₗ LinearEquiv.curry ℝ ℝ (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d)

Expansion of coContrToMatrixRe in terms of the standard basis.

d:ℕM:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ⊢ ∑ x, ∑ y, ((Finsupp.linearEquivFunOnFinite ℝ ℝ ((Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d))).symm ((LinearEquiv.curry ℝ ℝ (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d)).symm M)) (x, y) • ((coBasis d).tensorProduct (contrBasis d)) (x, y) = ∑ i, ∑ j, M i j • (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) j d:ℕM:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝi:Fin 1 ⊕ Fin dx✝¹:i ∈ Finset.univj:Fin 1 ⊕ Fin dx✝:j ∈ Finset.univ⊢ ((Finsupp.linearEquivFunOnFinite ℝ ℝ ((Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d))).symm ((LinearEquiv.curry ℝ ℝ (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d)).symm M)) (i, j) • ((coBasis d).tensorProduct (contrBasis d)) (i, j) = M i j • (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) j erw [d:ℕM:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝi:Fin 1 ⊕ Fin dx✝¹:i ∈ Finset.univj:Fin 1 ⊕ Fin dx✝:j ∈ Finset.univ⊢ ((Finsupp.linearEquivFunOnFinite ℝ ℝ ((Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d))).symm ((LinearEquiv.curry ℝ ℝ (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d)).symm M)) (i, j) • (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) j = M i j • (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) jd:ℕM:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝi:Fin 1 ⊕ Fin dx✝¹:i ∈ Finset.univj:Fin 1 ⊕ Fin dx✝:j ∈ Finset.univ⊢ ((Finsupp.linearEquivFunOnFinite ℝ ℝ ((Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d))).symm ((LinearEquiv.curry ℝ ℝ (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d)).symm M)) (i, j) • (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) j = M i j • (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) j All goals completed! 🐙 d:ℕM:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ⊢ (Finsupp.linearEquivFunOnFinite ℝ ℝ ((Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d))).symm ((LinearEquiv.curry ℝ ℝ (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d)).symm M) ∈ Finsupp.supported ℝ ℝ ↑Finset.univ All goals completed! 🐙

Group actions

d:ℕv:ContrMod d ⊗[ℝ] ContrMod dM:↑(LorentzGroup d)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin d⊢ ∑ y, ∑ x, (LinearMap.toMatrix (contrBasis d) (contrBasis d)) (ContrMod.rep M) i x * (LinearMap.toMatrix (contrBasis d) (contrBasis d)) (ContrMod.rep M) j y * contrContrToMatrixRe v x y = ∑ x, ∑ i_1, ↑M i i_1 * contrContrToMatrixRe v i_1 x * ↑M j x d:ℕv:ContrMod d ⊗[ℝ] ContrMod dM:↑(LorentzGroup d)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin d⊢ (fun y => ∑ x, (LinearMap.toMatrix (contrBasis d) (contrBasis d)) (ContrMod.rep M) i x * (LinearMap.toMatrix (contrBasis d) (contrBasis d)) (ContrMod.rep M) j y * contrContrToMatrixRe v x y) = fun x => ∑ i_1, ↑M i i_1 * contrContrToMatrixRe v i_1 x * ↑M j x d:ℕv:ContrMod d ⊗[ℝ] ContrMod dM:↑(LorentzGroup d)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin dx:Fin 1 ⊕ Fin d⊢ ∑ x_1, (LinearMap.toMatrix (contrBasis d) (contrBasis d)) (ContrMod.rep M) i x_1 * (LinearMap.toMatrix (contrBasis d) (contrBasis d)) (ContrMod.rep M) j x * contrContrToMatrixRe v x_1 x = ∑ i_1, ↑M i i_1 * contrContrToMatrixRe v i_1 x * ↑M j x d:ℕv:ContrMod d ⊗[ℝ] ContrMod dM:↑(LorentzGroup d)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin dx:Fin 1 ⊕ Fin d⊢ (fun x_1 => (LinearMap.toMatrix (contrBasis d) (contrBasis d)) (ContrMod.rep M) i x_1 * (LinearMap.toMatrix (contrBasis d) (contrBasis d)) (ContrMod.rep M) j x * contrContrToMatrixRe v x_1 x) = fun i_1 => ↑M i i_1 * contrContrToMatrixRe v i_1 x * ↑M j x d:ℕv:ContrMod d ⊗[ℝ] ContrMod dM:↑(LorentzGroup d)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin dx:Fin 1 ⊕ Fin dx1:Fin 1 ⊕ Fin d⊢ (LinearMap.toMatrix (contrBasis d) (contrBasis d)) (ContrMod.rep M) i x1 * (LinearMap.toMatrix (contrBasis d) (contrBasis d)) (ContrMod.rep M) j x * contrContrToMatrixRe v x1 x = ↑M i x1 * contrContrToMatrixRe v x1 x * ↑M j x d:ℕv:ContrMod d ⊗[ℝ] ContrMod dM:↑(LorentzGroup d)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin dx:Fin 1 ⊕ Fin dx1:Fin 1 ⊕ Fin d⊢ ↑M i x1 * ↑M j x * contrContrToMatrixRe v x1 x = ↑M i x1 * contrContrToMatrixRe v x1 x * ↑M j x All goals completed! 🐙d:ℕv:CoMod d ⊗[ℝ] CoMod dM:↑(LorentzGroup d)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin d⊢ ∑ y, ∑ x, (LinearMap.toMatrix (coBasis d) (coBasis d)) (CoMod.rep M) i x * (LinearMap.toMatrix (coBasis d) (coBasis d)) (CoMod.rep M) j y * coCoToMatrixRe v x y = ∑ x, ∑ i_1, (↑M)⁻¹ i_1 i * coCoToMatrixRe v i_1 x * ↑M⁻¹ x j d:ℕv:CoMod d ⊗[ℝ] CoMod dM:↑(LorentzGroup d)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin d⊢ (fun y => ∑ x, (LinearMap.toMatrix (coBasis d) (coBasis d)) (CoMod.rep M) i x * (LinearMap.toMatrix (coBasis d) (coBasis d)) (CoMod.rep M) j y * coCoToMatrixRe v x y) = fun x => ∑ i_1, (↑M)⁻¹ i_1 i * coCoToMatrixRe v i_1 x * ↑M⁻¹ x j d:ℕv:CoMod d ⊗[ℝ] CoMod dM:↑(LorentzGroup d)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin dx:Fin 1 ⊕ Fin d⊢ ∑ x_1, (LinearMap.toMatrix (coBasis d) (coBasis d)) (CoMod.rep M) i x_1 * (LinearMap.toMatrix (coBasis d) (coBasis d)) (CoMod.rep M) j x * coCoToMatrixRe v x_1 x = ∑ i_1, (↑M)⁻¹ i_1 i * coCoToMatrixRe v i_1 x * ↑M⁻¹ x j d:ℕv:CoMod d ⊗[ℝ] CoMod dM:↑(LorentzGroup d)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin dx:Fin 1 ⊕ Fin d⊢ (fun x_1 => (LinearMap.toMatrix (coBasis d) (coBasis d)) (CoMod.rep M) i x_1 * (LinearMap.toMatrix (coBasis d) (coBasis d)) (CoMod.rep M) j x * coCoToMatrixRe v x_1 x) = fun i_1 => (↑M)⁻¹ i_1 i * coCoToMatrixRe v i_1 x * ↑M⁻¹ x j d:ℕv:CoMod d ⊗[ℝ] CoMod dM:↑(LorentzGroup d)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin dx:Fin 1 ⊕ Fin dx1:Fin 1 ⊕ Fin d⊢ (LinearMap.toMatrix (coBasis d) (coBasis d)) (CoMod.rep M) i x1 * (LinearMap.toMatrix (coBasis d) (coBasis d)) (CoMod.rep M) j x * coCoToMatrixRe v x1 x = (↑M)⁻¹ x1 i * coCoToMatrixRe v x1 x * ↑M⁻¹ x j d:ℕv:CoMod d ⊗[ℝ] CoMod dM:↑(LorentzGroup d)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin dx:Fin 1 ⊕ Fin dx1:Fin 1 ⊕ Fin d⊢ ↑M⁻¹ x1 i * ↑M⁻¹ x j * coCoToMatrixRe v x1 x = ↑M⁻¹ x1 i * coCoToMatrixRe v x1 x * ↑M⁻¹ x j All goals completed! 🐙d:ℕv:ContrMod d ⊗[ℝ] CoMod dM:↑(LorentzGroup d)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin d⊢ ∑ y, ∑ x, (LinearMap.toMatrix (contrBasis d) (contrBasis d)) (ContrMod.rep M) i x * (LinearMap.toMatrix (coBasis d) (coBasis d)) (CoMod.rep M) j y * contrCoToMatrixRe v x y = ∑ x, ∑ i_1, ↑M i i_1 * contrCoToMatrixRe v i_1 x * (↑M)⁻¹ x j d:ℕv:ContrMod d ⊗[ℝ] CoMod dM:↑(LorentzGroup d)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin d⊢ (fun y => ∑ x, (LinearMap.toMatrix (contrBasis d) (contrBasis d)) (ContrMod.rep M) i x * (LinearMap.toMatrix (coBasis d) (coBasis d)) (CoMod.rep M) j y * contrCoToMatrixRe v x y) = fun x => ∑ i_1, ↑M i i_1 * contrCoToMatrixRe v i_1 x * (↑M)⁻¹ x j d:ℕv:ContrMod d ⊗[ℝ] CoMod dM:↑(LorentzGroup d)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin dx:Fin 1 ⊕ Fin d⊢ ∑ x_1, (LinearMap.toMatrix (contrBasis d) (contrBasis d)) (ContrMod.rep M) i x_1 * (LinearMap.toMatrix (coBasis d) (coBasis d)) (CoMod.rep M) j x * contrCoToMatrixRe v x_1 x = ∑ i_1, ↑M i i_1 * contrCoToMatrixRe v i_1 x * (↑M)⁻¹ x j d:ℕv:ContrMod d ⊗[ℝ] CoMod dM:↑(LorentzGroup d)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin dx:Fin 1 ⊕ Fin d⊢ (fun x_1 => (LinearMap.toMatrix (contrBasis d) (contrBasis d)) (ContrMod.rep M) i x_1 * (LinearMap.toMatrix (coBasis d) (coBasis d)) (CoMod.rep M) j x * contrCoToMatrixRe v x_1 x) = fun i_1 => ↑M i i_1 * contrCoToMatrixRe v i_1 x * (↑M)⁻¹ x j d:ℕv:ContrMod d ⊗[ℝ] CoMod dM:↑(LorentzGroup d)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin dx:Fin 1 ⊕ Fin dx1:Fin 1 ⊕ Fin d⊢ (LinearMap.toMatrix (contrBasis d) (contrBasis d)) (ContrMod.rep M) i x1 * (LinearMap.toMatrix (coBasis d) (coBasis d)) (CoMod.rep M) j x * contrCoToMatrixRe v x1 x = ↑M i x1 * contrCoToMatrixRe v x1 x * (↑M)⁻¹ x j d:ℕv:ContrMod d ⊗[ℝ] CoMod dM:↑(LorentzGroup d)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin dx:Fin 1 ⊕ Fin dx1:Fin 1 ⊕ Fin d⊢ ↑M i x1 * (↑M)⁻¹ x j * contrCoToMatrixRe v x1 x = ↑M i x1 * contrCoToMatrixRe v x1 x * (↑M)⁻¹ x j All goals completed! 🐙d:ℕv:CoMod d ⊗[ℝ] ContrMod dM:↑(LorentzGroup d)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin d⊢ ∑ y, ∑ x, (LinearMap.toMatrix (coBasis d) (coBasis d)) (CoMod.rep M) i x * (LinearMap.toMatrix (contrBasis d) (contrBasis d)) (ContrMod.rep M) j y * coContrToMatrixRe v x y = ∑ x, ∑ i_1, (↑M)⁻¹ i_1 i * coContrToMatrixRe v i_1 x * ↑M j x d:ℕv:CoMod d ⊗[ℝ] ContrMod dM:↑(LorentzGroup d)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin d⊢ (fun y => ∑ x, (LinearMap.toMatrix (coBasis d) (coBasis d)) (CoMod.rep M) i x * (LinearMap.toMatrix (contrBasis d) (contrBasis d)) (ContrMod.rep M) j y * coContrToMatrixRe v x y) = fun x => ∑ i_1, (↑M)⁻¹ i_1 i * coContrToMatrixRe v i_1 x * ↑M j x d:ℕv:CoMod d ⊗[ℝ] ContrMod dM:↑(LorentzGroup d)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin dx:Fin 1 ⊕ Fin d⊢ ∑ x_1, (LinearMap.toMatrix (coBasis d) (coBasis d)) (CoMod.rep M) i x_1 * (LinearMap.toMatrix (contrBasis d) (contrBasis d)) (ContrMod.rep M) j x * coContrToMatrixRe v x_1 x = ∑ i_1, (↑M)⁻¹ i_1 i * coContrToMatrixRe v i_1 x * ↑M j x d:ℕv:CoMod d ⊗[ℝ] ContrMod dM:↑(LorentzGroup d)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin dx:Fin 1 ⊕ Fin d⊢ (fun x_1 => (LinearMap.toMatrix (coBasis d) (coBasis d)) (CoMod.rep M) i x_1 * (LinearMap.toMatrix (contrBasis d) (contrBasis d)) (ContrMod.rep M) j x * coContrToMatrixRe v x_1 x) = fun i_1 => (↑M)⁻¹ i_1 i * coContrToMatrixRe v i_1 x * ↑M j x d:ℕv:CoMod d ⊗[ℝ] ContrMod dM:↑(LorentzGroup d)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin dx:Fin 1 ⊕ Fin dx1:Fin 1 ⊕ Fin d⊢ (LinearMap.toMatrix (coBasis d) (coBasis d)) (CoMod.rep M) i x1 * (LinearMap.toMatrix (contrBasis d) (contrBasis d)) (ContrMod.rep M) j x * coContrToMatrixRe v x1 x = (↑M)⁻¹ x1 i * coContrToMatrixRe v x1 x * ↑M j x d:ℕv:CoMod d ⊗[ℝ] ContrMod dM:↑(LorentzGroup d)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin dx:Fin 1 ⊕ Fin dx1:Fin 1 ⊕ Fin d⊢ (↑M)⁻¹ x1 i * ↑M j x * coContrToMatrixRe v x1 x = (↑M)⁻¹ x1 i * coContrToMatrixRe v x1 x * ↑M j x All goals completed! 🐙

The symm version of the group actions.

lemma contrContrToMatrixRe_ρ_symm {d : ℕ} (v : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (M : LorentzGroup d) : TensorProduct.map (ContrMod.rep M) (ContrMod.rep M) (contrContrToMatrixRe.symm v) = contrContrToMatrixRe.symm (M.1 * v * M.1ᵀ) := d:ℕv:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝM:↑(LorentzGroup d)⊢ (TensorProduct.map (ContrMod.rep M) (ContrMod.rep M)) (contrContrToMatrixRe.symm v) = contrContrToMatrixRe.symm (↑M * v * (↑M)ᵀ) d:ℕv:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝM:↑(LorentzGroup d)⊢ contrContrToMatrixRe ((TensorProduct.map (ContrMod.rep M) (ContrMod.rep M)) (contrContrToMatrixRe.symm v)) = contrContrToMatrixRe (contrContrToMatrixRe.symm (↑M * v * (↑M)ᵀ)) All goals completed! 🐙d:ℕv:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝM:↑(LorentzGroup d)h1:coCoToMatrixRe ((TensorProduct.map (CoMod.rep M) (CoMod.rep M)) (coCoToMatrixRe.symm v)) = (↑M⁻¹)ᵀ * v * ↑M⁻¹⊢ (TensorProduct.map (CoMod.rep M) (CoMod.rep M)) (coCoToMatrixRe.symm v) = coCoToMatrixRe.symm (coCoToMatrixRe ((TensorProduct.map (CoMod.rep M) (CoMod.rep M)) (coCoToMatrixRe.symm v))) All goals completed! 🐙All goals completed! 🐙All goals completed! 🐙