PhyslibSearch

Physlib.Relativity.Tensors.RealTensor.Vector.Pre.Contraction

40 declarations

definition

Bilinear contraction of ContrMod d\text{ContrMod } d and CoMod d\text{CoMod } d

#contrModCoModBi

For a natural number dd, this defines the R\mathbb{R}-bilinear map from the space of contravariant Lorentz vectors ContrMod d\text{ContrMod } d and the space of covariant Lorentz vectors CoMod d\text{CoMod } d to the real numbers R\mathbb{R}. Given a contravariant vector ψContrMod d\psi \in \text{ContrMod } d and a covariant vector ϕCoMod d\phi \in \text{CoMod } d, the map computes their contraction as the dot product of their coordinate representations: \[ (\psi, \phi) \mapsto \psi \cdot \phi = \sum_{i \in \text{Fin } 1 \oplus \text{Fin } d} \psi^i \phi_i \] where ψi\psi^i and ϕi\phi_i are the real-valued components of the vectors in the 1+d1+d dimensional spacetime.

definition

Bilinear contraction map CoMod d×ContrMod dR\text{CoMod } d \times \text{ContrMod } d \to \mathbb{R}

#coModContrModBi

For a given dimension dd, the map defines a bilinear form CoMod d×ContrMod dR\text{CoMod } d \times \text{ContrMod } d \to \mathbb{R} that represents the contraction of a covariant Lorentz vector ϕ\phi with a contravariant Lorentz vector ψ\psi. Specifically, if ϕCoMod d\phi \in \text{CoMod } d and ψContrMod d\psi \in \text{ContrMod } d, the result is the dot product of their coordinate representations in R1+d\mathbb{R}^{1+d}, given by μ=0dϕμψμ\sum_{\mu=0}^d \phi_\mu \psi^\mu.

definition

Contraction morphism Contr dCo dR\text{Contr } d \otimes \text{Co } d \to \mathbb{R}

#contrCoContract

For a (1+d)(1+d)-dimensional spacetime, let Contr d\text{Contr } d and Co d\text{Co } d be the representations of the Lorentz group corresponding to contravariant and covariant vectors, respectively. This definition represents the Lorentz-invariant contraction map from the tensor product representation Contr dCo d\text{Contr } d \otimes \text{Co } d to the trivial representation R\mathbb{R}. Given a contravariant vector ψContr d\psi \in \text{Contr } d and a covariant vector ϕCo d\phi \in \text{Co } d, the map is defined by the sum over their components in the standard basis: \[ \psi \otimes \phi \mapsto \sum_{i=0}^d \psi^i \phi_i \] In index notation, this corresponds to the contraction ψiϕi\psi^i \phi_i. As a morphism in the category of representations, this map is intertwining, meaning it is invariant under the action of the Lorentz group.

theorem

ψ,ϕm=iψiϕi\langle \psi, \phi \rangle_m = \sum_i \psi^i \phi_i

#contrCoContract_hom_tmul

For a contravariant Lorentz vector ψ\psi and a covariant Lorentz vector ϕ\phi in (1+d)(1+d)-dimensional spacetime, the Lorentz-invariant contraction ψ,ϕm\langle \psi, \phi \rangle_m (representing the evaluation of the contraction morphism on the tensor product ψϕ\psi \otimes \phi) is equal to the standard Euclidean dot product of their coordinate representations. Specifically, ψ,ϕm=i=0dψiϕi\langle \psi, \phi \rangle_m = \sum_{i=0}^d \psi^i \phi_i, where ψi\psi^i and ϕi\phi_i are the components of ψ\psi and ϕ\phi in the standard basis Fin 1Fin d\text{Fin } 1 \oplus \text{Fin } d.

definition

Contraction map Co dContr dR\text{Co } d \otimes \text{Contr } d \to \mathbb{R}

#coContrContract

For a given dimension dd, the morphism `Lorentz.coContrContract` is an equivariant linear map from the tensor product of the covariant Lorentz representation Co d\text{Co } d and the contravariant Lorentz representation Contr d\text{Contr } d to the trivial representation R\mathbb{R}. This map is defined by the contraction of a covariant vector ϕ\phi and a contravariant vector ψ\psi, expressed in index notation as ϕμψμ\phi_\mu \psi^\mu, which corresponds to the dot product of their components in the standard basis.

theorem

Contraction of Covariant and Contravariant Lorentz Vectors as Dot Product of Components

#coContrContract_hom_tmul

For any spatial dimension dd, let ϕCo d\phi \in \text{Co } d be a covariant Lorentz vector and ψContr d\psi \in \text{Contr } d be a contravariant Lorentz vector. The contraction ϕ,ψm\langle \phi, \psi \rangle_m is equal to the dot product of their coordinate representations in the standard basis of R1+d\mathbb{R}^{1+d}, denoted by ϕ.toFin1dRψ.toFin1dR\phi.\text{toFin1d}\mathbb{R} \cdot \psi.\text{toFin1d}\mathbb{R}.

theorem

ϕ,ψm=ψ,ϕm\langle \phi, \psi \rangle_m = \langle \psi, \phi \rangle_m for Contravariant and Covariant Lorentz Vectors

#contrCoContract_tmul_symm

For any contravariant Lorentz vector ϕContr d\phi \in \text{Contr } d and any covariant Lorentz vector ψCo d\psi \in \text{Co } d in a (1+d)(1+d)-dimensional spacetime, the Lorentz-invariant contraction ϕ,ψm\langle \phi, \psi \rangle_m is equal to the contraction ψ,ϕm\langle \psi, \phi \rangle_m.

theorem

ϕ,ψm=ψ,ϕm\langle \phi, \psi \rangle_m = \langle \psi, \phi \rangle_m for Covariant and Contravariant Lorentz Vectors

#coContrContract_tmul_symm

For any spatial dimension dd, let ϕCo d\phi \in \text{Co } d be a covariant Lorentz vector and ψContr d\psi \in \text{Contr } d be a contravariant Lorentz vector in a (1+d)(1+d)-dimensional spacetime. The Lorentz-invariant contraction ϕ,ψm\langle \phi, \psi \rangle_m is equal to the contraction ψ,ϕm\langle \psi, \phi \rangle_m.

definition

Contraction morphism for contravariant vectors Contr dContr dR\text{Contr } d \otimes \text{Contr } d \to \mathbb{R}

#contrContrContract

For a (1+d)(1+d)-dimensional spacetime, let Contr d\text{Contr } d be the representation of the Lorentz group corresponding to contravariant vectors. The definition represents the Lorentz-invariant contraction morphism from the tensor product representation Contr dContr d\text{Contr } d \otimes \text{Contr } d to the trivial representation R\mathbb{R}. Given two contravariant vectors ψ,ϕContr d\psi, \phi \in \text{Contr } d, the map is defined by first applying the isomorphism Contr.toCo d\text{Contr.toCo } d to the second vector (effectively lowering its index using the Minkowski metric ημν\eta_{\mu\nu}) and then applying the standard contravariant-covariant contraction contrCoContract\text{contrCoContract}. In components, this corresponds to the Minkowski inner product: \[ \psi \otimes \phi \mapsto \eta_{\mu\nu} \psi^\mu \phi^\nu = \psi^\mu \phi_\mu \] where ημν\eta_{\mu\nu} is the Minkowski metric tensor.

definition

Linear contraction map for contravariant vectors (Contr d)(Contr d)R(\text{Contr } d) \otimes (\text{Contr } d) \to \mathbb{R}

#contrContrContractField

Let Contr d\text{Contr } d denote the vector space of contravariant Lorentz vectors in a (1+d)(1+d)-dimensional spacetime. The definition is an R\mathbb{R}-linear map from the tensor product space (Contr d)R(Contr d)(\text{Contr } d) \otimes_{\mathbb{R}} (\text{Contr } d) to the real numbers R\mathbb{R}. This map computes the Minkowski inner product of two contravariant vectors. Specifically, for any two contravariant vectors u,vContr du, v \in \text{Contr } d, the map is defined by lowering the index of the second vector via the Minkowski metric ημν\eta_{\mu\nu} and performing the standard contraction: \[ u \otimes v \mapsto \eta_{\mu\nu} u^\mu v^\nu \] where ημν=diag(1,1,,1)\eta_{\mu\nu} = \text{diag}(1, -1, \dots, -1).

theorem

ϕ,ψm=vϕηvψ\langle \phi, \psi \rangle_m = \mathbf{v}_\phi^\top \eta \mathbf{v}_\psi for contravariant Lorentz vectors

#contrContrContract_hom_tmul

For any two contravariant Lorentz vectors ϕ\phi and ψ\psi in a (1+d)(1+d)-dimensional spacetime, the Minkowski inner product (or Lorentz contraction) ϕ,ψm\langle \phi, \psi \rangle_m is equal to the product vϕηvψ\mathbf{v}_\phi^\top \eta \mathbf{v}_\psi. Here, vϕ,vψR1+d\mathbf{v}_\phi, \mathbf{v}_\psi \in \mathbb{R}^{1+d} are the coordinate representations of the vectors in the standard basis, η=diag(1,1,,1)\eta = \text{diag}(1, -1, \dots, -1) is the Minkowski matrix, and the operation corresponds to the Euclidean dot product of vϕ\mathbf{v}_\phi with ηvψ\eta \mathbf{v}_\psi.

definition

Contraction map Co dCo dR\text{Co } d \otimes \text{Co } d \to \mathbb{R}

#coCoContract

For a given dimension dd, the morphism `Lorentz.coCoContract` is an equivariant linear map from the tensor product of two covariant Lorentz representations Co dCo d\text{Co } d \otimes \text{Co } d to the trivial representation R\mathbb{R}. This map is defined by first converting the second covariant vector in the tensor product into a contravariant vector via the isomorphism `Co.toContr` (which corresponds to raising the index using the inverse Minkowski metric ημν\eta^{\mu\nu}) and then applying the standard contraction `coContrContract`. In index notation, for two covariant vectors αμ\alpha_\mu and βν\beta_\nu, this operation computes the scalar ημναμβν\eta^{\mu\nu} \alpha_\mu \beta_\nu.

theorem

Contraction of Covariant Lorentz Vectors as ϕ,ψm=[ϕ](η[ψ])\langle \phi, \psi \rangle_m = [\phi] \cdot (\eta [\psi])

#coCoContract_hom_tmul

For any dimension dd, let ϕ,ψCo d\phi, \psi \in \text{Co } d be two covariant Lorentz vectors. The contraction ϕ,ψm\langle \phi, \psi \rangle_m is equal to the dot product of the coordinate representation of ϕ\phi with the product of the Minkowski matrix η\eta and the coordinate representation of ψ\psi. Mathematically, this is expressed as: ϕ,ψm=[ϕ](η[ψ])\langle \phi, \psi \rangle_m = [\phi] \cdot (\eta [\psi]) where [ϕ],[ψ]R1+d[\phi], [\psi] \in \mathbb{R}^{1+d} are the representations of the vectors in the standard basis and η=diag(1,1,,1)\eta = \text{diag}(1, -1, \dots, -1) is the Minkowski matrix.

theorem

Lorentz Invariance of the Minkowski Inner Product for Contravariant Vectors

#action_tmul

In a spacetime with dd spatial dimensions, let ,m\langle \cdot, \cdot \rangle_m denote the Minkowski inner product (contraction) for contravariant vectors. For any Lorentz transformation gg in the Lorentz group and any contravariant vectors xx and yy, the inner product is invariant under the group action ρ(g)\rho(g). That is, \[ \langle \rho(g)x, \rho(g)y \rangle_m = \langle x, y \rangle_m \] where ρ(g)\rho(g) is the representation of the Lorentz group acting on the space of contravariant vectors.

theorem

x,ym=x0y0ixiyi\langle x, y \rangle_m = x^0 y^0 - \sum_{i} x^i y^i for contravariant Lorentz vectors

#as_sum

For any two contravariant Lorentz vectors xx and yy in a (1+d)(1+d)-dimensional spacetime, their Minkowski inner product x,ym\langle x, y \rangle_m is given by the difference between the product of their temporal components and the sum of the products of their spatial components: x,ym=x0y0i=1dxiyi\langle x, y \rangle_m = x^0 y^0 - \sum_{i=1}^d x^i y^i where x0x^0 and y0y^0 are the components indexed by the temporal dimension (represented by `Sum.inl 0`), and xix^i and yiy^i are the components indexed by the dd spatial dimensions (represented by `Sum.inr i`).

theorem

x,ym=x0y0x,y\langle x, y \rangle_m = x^0 y^0 - \langle \vec{x}, \vec{y} \rangle for contravariant Lorentz vectors

#as_sum_toSpace

For any two contravariant Lorentz vectors xx and yy in a (1+d)(1+d)-dimensional spacetime, their Minkowski inner product x,ym\langle x, y \rangle_m is equal to the product of their temporal components minus the Euclidean inner product of their spatial parts: x,ym=x0y0x,y\langle x, y \rangle_m = x^0 y^0 - \langle \vec{x}, \vec{y} \rangle where x0x^0 and y0y^0 are the temporal components of xx and yy respectively (indexed by `Sum.inl 0`), and x,yRd\vec{x}, \vec{y} \in \mathbb{R}^d are the spatial vectors (obtained via `toSpace`) equipped with the standard Euclidean inner product ,\langle \cdot, \cdot \rangle.

theorem

e0,e0m=1\langle e_0, e_0 \rangle_m = 1

#stdBasis_inl

In a (1+d)(1+d)-dimensional spacetime, let e0e_0 be the standard basis vector for the temporal dimension (indexed by `Sum.inl 0`) in the space of contravariant Lorentz vectors. Its Minkowski inner product with itself is 11: e0,e0m=1\langle e_0, e_0 \rangle_m = 1

theorem

x,ym=y,xm\langle x, y \rangle_m = \langle y, x \rangle_m for contravariant Lorentz vectors

#symm

For any two contravariant Lorentz vectors xx and yy in a (1+d)(1+d)-dimensional spacetime, the Minkowski inner product ,m\langle \cdot, \cdot \rangle_m is symmetric: x,ym=y,xm\langle x, y \rangle_m = \langle y, x \rangle_m

theorem

x,Λym=Λx,ym\langle x, \Lambda^* y \rangle_m = \langle \Lambda x, y \rangle_m

#dual_mulVec_right

Let xx and yy be contravariant Lorentz vectors in a (1+d)(1+d)-dimensional spacetime. For any (1+d)×(1+d)(1+d) \times (1+d) real matrix Λ\Lambda, let Λ\Lambda^* (denoted in the formal text as `dual Λ`) be its Minkowski dual matrix defined by Λ=ηΛη\Lambda^* = \eta \Lambda^\top \eta, where η=diag(1,1,,1)\eta = \text{diag}(1, -1, \dots, -1) is the Minkowski metric. The Minkowski inner product ,m\langle \cdot, \cdot \rangle_m satisfies: \[ \langle x, \Lambda^* y \rangle_m = \langle \Lambda x, y \rangle_m \]

theorem

Λx,ym=x,Λym\langle \Lambda^* x, y \rangle_m = \langle x, \Lambda y \rangle_m

#dual_mulVec_left

Let xx and yy be contravariant Lorentz vectors in a (1+d)(1+d)-dimensional spacetime. For any (1+d)×(1+d)(1+d) \times (1+d) real matrix Λ\Lambda, let Λ\Lambda^* (the Minkowski dual, denoted as `dual Λ`) be defined by Λ=ηΛη\Lambda^* = \eta \Lambda^\top \eta, where η=diag(1,1,,1)\eta = \text{diag}(1, -1, \dots, -1) is the Minkowski metric. The Minkowski inner product ,m\langle \cdot, \cdot \rangle_m satisfies the adjoint property: \[ \langle \Lambda^* x, y \rangle_m = \langle x, \Lambda y \rangle_m \]

theorem

x,Pym=ixiyi\langle x, Py \rangle_m = \sum_i x^i y^i

#right_parity

Let xx and yy be contravariant Lorentz vectors in a (1+d)(1+d)-dimensional spacetime. Let PP denote the parity transformation (representing the action of the parity element of the Lorentz group), which leaves the temporal component unchanged and negates the spatial components. The Minkowski inner product of xx and the parity-transformed vector PyPy is equal to the Euclidean inner product of their coordinate components: x,Pym=ixiyi\langle x, Py \rangle_m = \sum_{i} x^i y^i where the sum is taken over all temporal and spatial indices i{0,1,,d}i \in \{0, 1, \dots, d\}.

theorem

y,Pym=0    y=0\langle y, Py \rangle_m = 0 \iff y = 0

#self_parity_eq_zero_iff

Let yy be a contravariant Lorentz vector in a (1+d)(1+d)-dimensional spacetime. Let PP denote the parity transformation, representing the action of the parity element of the Lorentz group. The Minkowski inner product of yy with its parity-transformed image PyPy is zero if and only if yy is the zero vector: y,Pym=0    y=0\langle y, Py \rangle_m = 0 \iff y = 0

theorem

(x,x,ym=0)    y=0(\forall x, \langle x, y \rangle_m = 0) \iff y = 0

#nondegenerate

Let yy be a contravariant Lorentz vector in a (1+d)(1+d)-dimensional spacetime. The Minkowski metric is non-degenerate, meaning that the Minkowski inner product x,ym\langle x, y \rangle_m is zero for all contravariant vectors xx if and only if yy is the zero vector: (xContr d,x,ym=0)    y=0(\forall x \in \text{Contr } d, \langle x, y \rangle_m = 0) \iff y = 0

theorem

x,Λym=x,Λym    x,(ΛΛ)ym=0\langle x, \Lambda y \rangle_m = \langle x, \Lambda' y \rangle_m \iff \langle x, (\Lambda - \Lambda') y \rangle_m = 0

#matrix_apply_eq_iff_sub

Let xx and yy be contravariant Lorentz vectors in a (1+d)(1+d)-dimensional spacetime, and let Λ\Lambda and Λ\Lambda' be (1+d)×(1+d)(1+d) \times (1+d) real matrices. Then the Minkowski inner product satisfies x,Λym=x,Λym\langle x, \Lambda y \rangle_m = \langle x, \Lambda' y \rangle_m if and only if x,(ΛΛ)ym=0\langle x, (\Lambda - \Lambda') y \rangle_m = 0.

theorem

(v,Λv=Λv)    (v,w,v,Λwm=v,Λwm)(\forall v, \Lambda v = \Lambda' v) \iff (\forall v, w, \langle v, \Lambda w \rangle_m = \langle v, \Lambda' w \rangle_m)

#matrix_eq_iff_eq_forall'

Let Contr d\text{Contr } d denote the vector space of contravariant Lorentz vectors in a (1+d)(1+d)-dimensional spacetime, and let ,m\langle \cdot, \cdot \rangle_m denote the Minkowski inner product. For any two real matrices Λ\Lambda and Λ\Lambda' of size (1+d)×(1+d)(1+d) \times (1+d), the linear transformations they induce are identical if and only if their associated bilinear forms under the Minkowski metric are identical for all vectors: \[ (\forall v \in \text{Contr } d, \Lambda v = \Lambda' v) \iff (\forall v, w \in \text{Contr } d, \langle v, \Lambda w \rangle_m = \langle v, \Lambda' w \rangle_m) \]

theorem

Λ=Λ    v,w,v,Λwm=v,Λwm\Lambda = \Lambda' \iff \forall v, w, \langle v, \Lambda w \rangle_m = \langle v, \Lambda' w \rangle_m

#matrix_eq_iff_eq_forall

Let Contr d\text{Contr } d be the vector space of contravariant Lorentz vectors in a (1+d)(1+d)-dimensional spacetime, and let ,m\langle \cdot, \cdot \rangle_m denote the Minkowski inner product. For any two real matrices Λ\Lambda and Λ\Lambda' of size (1+d)×(1+d)(1+d) \times (1+d), the matrices are equal if and only if their associated bilinear forms under the Minkowski metric are identical for all vectors v,wContr dv, w \in \text{Contr } d: \[ \Lambda = \Lambda' \iff \forall v, w \in \text{Contr } d, \langle v, \Lambda w \rangle_m = \langle v, \Lambda' w \rangle_m \]

theorem

Λ=I    v,w,v,Λwm=v,wm\Lambda = I \iff \forall v, w, \langle v, \Lambda w \rangle_m = \langle v, w \rangle_m

#matrix_eq_id_iff

Let Contr d\text{Contr } d denote the vector space of contravariant Lorentz vectors in a (1+d)(1+d)-dimensional spacetime, and let ,m\langle \cdot, \cdot \rangle_m denote the Minkowski inner product. For any real square matrix Λ\Lambda of size (1+d)×(1+d)(1+d) \times (1+d), Λ\Lambda is equal to the identity matrix II if and only if for all vectors v,wContr dv, w \in \text{Contr } d, the Minkowski inner product of vv and Λw\Lambda w is equal to the Minkowski inner product of vv and ww: \[ \Lambda = I \iff \forall v, w \in \text{Contr } d, \langle v, \Lambda w \rangle_m = \langle v, w \rangle_m \]

theorem

ΛLorentzGroup d    v,w,Λv,Λwm=v,wm\Lambda \in \text{LorentzGroup } d \iff \forall v, w, \langle \Lambda v, \Lambda w \rangle_m = \langle v, w \rangle_m

#mem_iff_invariant

A square matrix Λ\Lambda of size (1+d)×(1+d)(1+d) \times (1+d) is an element of the Lorentz group O(1,d)O(1, d) if and only if it preserves the Minkowski inner product for all contravariant Lorentz vectors v,wContr dv, w \in \text{Contr } d. That is, \[ \Lambda \in \text{LorentzGroup } d \iff \forall v, w \in \text{Contr } d, \langle \Lambda v, \Lambda w \rangle_m = \langle v, w \rangle_m \] where ,m\langle \cdot, \cdot \rangle_m denotes the Minkowski inner product.

theorem

ΛLorentzGroup d    w,Λw,Λwm=w,wm\Lambda \in \text{LorentzGroup } d \iff \forall w, \langle \Lambda w, \Lambda w \rangle_m = \langle w, w \rangle_m

#mem_iff_norm

A square matrix Λ\Lambda of size (1+d)×(1+d)(1+d) \times (1+d) is an element of the Lorentz group O(1,d)O(1, d) if and only if it preserves the Minkowski norm squared for every contravariant Lorentz vector wContr dw \in \text{Contr } d. That is, \[ \Lambda \in \text{LorentzGroup } d \iff \forall w \in \text{Contr } d, \langle \Lambda w, \Lambda w \rangle_m = \langle w, w \rangle_m \] where ,m\langle \cdot, \cdot \rangle_m denotes the Minkowski inner product.

theorem

(v0)2=v,vm+i(vi)2(v^0)^2 = \langle v, v \rangle_m + \sum_i (v^i)^2 for contravariant Lorentz vectors

#inl_sq_eq

For any contravariant Lorentz vector vv in a (1+d)(1+d)-dimensional spacetime, let v0v^0 denote its temporal component (indexed by `Sum.inl 0`) and viv^i denote its spatial components (indexed by `Sum.inr i`). The square of the temporal component is equal to the sum of the Minkowski inner product of vv with itself and the sum of the squares of its spatial components: (v0)2=v,vm+i=1d(vi)2(v^0)^2 = \langle v, v \rangle_m + \sum_{i=1}^d (v^i)^2

theorem

v,vm(v0)2\langle v, v \rangle_m \le (v^0)^2 for contravariant Lorentz vectors

#le_inl_sq

For any contravariant Lorentz vector vv in a (1+d)(1+d)-dimensional spacetime, the Minkowski inner product of vv with itself, denoted by v,vm\langle v, v \rangle_m, is less than or equal to the square of its temporal component v0v^0 (indexed by `Sum.inl 0`). That is, v,vm(v0)2\langle v, v \rangle_m \le (v^0)^2

theorem

v0w0v,wv,wmv^0 w^0 - |\langle \vec{v}, \vec{w} \rangle| \le \langle v, w \rangle_m for contravariant Lorentz vectors

#ge_abs_inner_product

For any two contravariant Lorentz vectors vv and ww in a (1+d)(1+d)-dimensional spacetime, the Minkowski inner product v,wm\langle v, w \rangle_m satisfies the following inequality: v0w0v,wv,wmv^0 w^0 - |\langle \vec{v}, \vec{w} \rangle| \le \langle v, w \rangle_m where v0v^0 and w0w^0 are the temporal components of vv and ww (indexed by `Sum.inl 0`), v\vec{v} and w\vec{w} are the spatial components in Rd\mathbb{R}^d (obtained via `toSpace`), and ,\langle \cdot, \cdot \rangle is the standard Euclidean inner product on Rd\mathbb{R}^d.

theorem

v0w0vwv,wmv^0 w^0 - \|\vec{v}\| \|\vec{w}\| \le \langle v, w \rangle_m for contravariant Lorentz vectors

#ge_sub_norm

For any two contravariant Lorentz vectors vv and ww in a (1+d)(1+d)-dimensional spacetime, the Minkowski inner product v,wm\langle v, w \rangle_m satisfies the following inequality: v0w0vwv,wmv^0 w^0 - \|\vec{v}\| \|\vec{w}\| \le \langle v, w \rangle_m where v0v^0 and w0w^0 are the temporal components of vv and ww (indexed by `Sum.inl 0`), v\vec{v} and w\vec{w} are the spatial components in Rd\mathbb{R}^d (obtained via `toSpace`), and \|\cdot\| denotes the standard Euclidean norm on Rd\mathbb{R}^d.

theorem

eμ,vm=ημμvμ\langle e_\mu, v \rangle_m = \eta_{\mu\mu} v^\mu

#basis_left

For any contravariant Lorentz vector vContr dv \in \text{Contr } d and any index μFin 1Fin d\mu \in \text{Fin } 1 \oplus \text{Fin } d, the Minkowski inner product of the μ\mu-th standard basis vector eμe_\mu and vv is equal to the product of the μ\mu-th diagonal component of the Minkowski metric η\eta and the μ\mu-th component of vv: \[ \langle e_\mu, v \rangle_m = \eta_{\mu\mu} v^\mu \] where eμe_\mu is the μ\mu-th element of the standard basis for ContrMod d\text{ContrMod } d, η\eta is the Minkowski matrix diag(1,1,,1)\text{diag}(1, -1, \dots, -1), and vμv^\mu is the component of vv at index μ\mu.

theorem

eμ,Λeνm=ημμΛμν\langle e_\mu, \Lambda e_\nu \rangle_m = \eta_{\mu\mu} \Lambda_{\mu\nu}

#on_basis_mulVec

For any indices μ,νFin 1Fin d\mu, \nu \in \text{Fin } 1 \oplus \text{Fin } d, let eμe_\mu and eνe_\nu be the corresponding vectors in the standard basis of the space of contravariant Lorentz vectors ContrMod d\text{ContrMod } d. For any real matrix Λ\Lambda of size (1+d)×(1+d)(1+d) \times (1+d), the Minkowski inner product of eμe_\mu and the vector Λeν\Lambda e_\nu (obtained by matrix-vector multiplication) is equal to the product of the μ\mu-th diagonal entry of the Minkowski metric η\eta and the (μ,ν)(\mu, \nu)-th entry of the matrix Λ\Lambda: \[ \langle e_\mu, \Lambda e_\nu \rangle_m = \eta_{\mu\mu} \Lambda_{\mu\nu} \] where η=diag(1,1,,1)\eta = \text{diag}(1, -1, \dots, -1).

theorem

eμ,eνm=ημν\langle e_\mu, e_\nu \rangle_m = \eta_{\mu\nu} for standard basis vectors

#on_basis

For any indices μ,νFin 1Fin d\mu, \nu \in \text{Fin } 1 \oplus \text{Fin } d, let eμe_\mu and eνe_\nu be the elements of the standard basis for the space of contravariant real Lorentz vectors ContrMod d\text{ContrMod } d. The Minkowski inner product of these two basis vectors is equal to the (μ,ν)(\mu, \nu)-th entry of the Minkowski metric η\eta: \[ \langle e_\mu, e_\nu \rangle_m = \eta_{\mu\nu} \] where η\eta is the (1+d)×(1+d)(1+d) \times (1+d) diagonal matrix diag(1,1,,1)\text{diag}(1, -1, \dots, -1).

theorem

Λνμ=ηννeν,Λeμm\Lambda_{\nu\mu} = \eta_{\nu\nu} \langle e_\nu, \Lambda e_\mu \rangle_m

#matrix_apply_stdBasis

For any indices ν,μFin 1Fin d\nu, \mu \in \text{Fin } 1 \oplus \text{Fin } d, let eνe_\nu and eμe_\mu be the corresponding vectors in the standard basis of the space of contravariant Lorentz vectors ContrMod d\text{ContrMod } d. Let Λ\Lambda be a real matrix of size (1+d)×(1+d)(1+d) \times (1+d) and η\eta be the Minkowski metric diag(1,1,,1)\text{diag}(1, -1, \dots, -1). The (ν,μ)(\nu, \mu)-th entry of the matrix Λ\Lambda is given by the product of the ν\nu-th diagonal entry of the Minkowski metric η\eta and the Minkowski inner product of eνe_\nu with the vector Λeμ\Lambda e_\mu: \[ \Lambda_{\nu\mu} = \eta_{\nu\nu} \langle e_\nu, \Lambda e_\mu \rangle_m \]

theorem

x,xm=det(toSelfAdjoint x)\langle x, x \rangle_m = \det(\text{toSelfAdjoint } x) for Lorentz vectors in 3+13+1 dimensions

#same_eq_det_toSelfAdjoint

For any contravariant Lorentz vector xContrMod 3x \in \text{ContrMod } 3 in 3+13+1 dimensions, let x,xm\langle x, x \rangle_m denote its Minkowski inner product with itself (the Minkowski norm squared). Let MM be the 2×22 \times 2 self-adjoint complex matrix associated with xx via the linear isomorphism `toSelfAdjoint`, defined by the linear combination M=x0σ0x1σ1x2σ2x3σ3M = x^0 \sigma_0 - x^1 \sigma_1 - x^2 \sigma_2 - x^3 \sigma_3, where σ0\sigma_0 is the identity matrix and σ1,σ2,σ3\sigma_1, \sigma_2, \sigma_3 are the standard Pauli matrices. The Minkowski norm squared is equal to the determinant of this matrix: x,xm=det(M)\langle x, x \rangle_m = \det(M)

theorem

Contraction of Contravariant and Covariant Basis Vectors equals δij\delta_{ij}

#contrCoContract_basis

In a (1+d)(1+d)-dimensional spacetime, let {ei}\{e^i\} be the standard basis for the contravariant representation Contr d\text{Contr } d and {ej}\{e_j\} be the standard basis for the covariant representation Co d\text{Co } d, where indices i,ji, j belong to the index set Fin 1Fin d\text{Fin } 1 \oplus \text{Fin } d. The evaluation of the Lorentz-invariant contraction morphism on the tensor product of these basis vectors satisfies: \[ \text{contrCoContract}(e^i \otimes e_j) = \begin{cases} 1 & \text{if } i = j \\ 0 & \text{if } i \neq j \end{cases} \] This result represents the Kronecker delta δij\delta_{ij} in the context of contravariant-covariant vector contraction.

theorem

Contraction of Covariant and Contravariant Basis Vectors Equals δij\delta_{ij}

#coContrContract_basis

For any dimension dd, let {ei}\{e^*_i\} be the standard basis of the covariant Lorentz representation Co d\text{Co } d and let {ej}\{e^j\} be the standard basis of the contravariant Lorentz representation Contr d\text{Contr } d, where the indices i,ji, j range over the set Fin 1Fin d\text{Fin } 1 \oplus \text{Fin } d. The contraction morphism coContrContract\text{coContrContract} applied to the tensor product of basis elements eieje^*_i \otimes e^j is given by the Kronecker delta: ei,ejm=δij={1if i=j0if ij \langle e^*_i, e^j \rangle_m = \delta_{ij} = \begin{cases} 1 & \text{if } i = j \\ 0 & \text{if } i \neq j \end{cases}