Physlib

Physlib.Relativity.Tensors.RealTensor.Vector.Pre.Modules

Modules associated with Real Lorentz vectors

We define the modules underlying real Lorentz vectors.

These definitions are preludes to the definitions of `Lorentz.contr` and `Lorentz.co`.

The standard basis.

mulVec

The norm

(Not the Minkowski norm, but the norm of a vector in `ContrℝModule d`.)

The representation.

To Self-Adjoint Matrix

Topology

The standard basis.

mulVec

The representation

56 declarations

theorem

Extensionality of contravariant Lorentz vectors: ψ.val=ψ′.val  ⟹  ψ=ψ′\psi.\text{val} = \psi'.\text{val} \implies \psi = \psi'

Let ContrMod d\text{ContrMod } d be the module of contravariant real Lorentz vectors in 1+d1+d dimensions. For any two vectors ψ,ψ′∈ContrMod d\psi, \psi' \in \text{ContrMod } d, if their underlying component values are equal (i.e., ψ.val=ψ′.val\psi.\text{val} = \psi'.\text{val}), then the vectors themselves are equal (ψ=ψ′\psi = \psi').

definition

Equivalence ContrMod d≅(Fin 1⊕Fin d→R)\text{ContrMod } d \cong (\text{Fin } 1 \oplus \text{Fin } d \to \mathbb{R})

This definition establishes a canonical equivalence (isomorphism) between the module of contravariant real Lorentz vectors ContrMod d\text{ContrMod } d and the space of functions mapping the index set Fin 1⊕Fin d\text{Fin } 1 \oplus \text{Fin } d to the real numbers R\mathbb{R}. Effectively, it identifies a contravariant vector with its (1+d)(1+d) real components (v0,v1,…,vd)(v^0, v^1, \dots, v^d), where the index set is decomposed into one temporal dimension and dd spatial dimensions.

instance

Additive Commutative Monoid on ContrMod d\text{ContrMod } d

The space of contravariant real Lorentz vectors ContrMod d\text{ContrMod } d is equipped with an additive commutative monoid structure. This structure (defining vector addition and the zero vector) is induced by transporting the standard component-wise addition from the function space (Fin 1⊕Fin d)→R(\text{Fin } 1 \oplus \text{Fin } d) \to \mathbb{R} via the canonical equivalence ContrMod d≅R1+d\text{ContrMod } d \cong \mathbb{R}^{1+d}.

instance

Additive Commutative Group on ContrMod d\text{ContrMod } d

The space of contravariant real Lorentz vectors ContrMod d\text{ContrMod } d is equipped with an additive commutative group structure. This structure is defined by transporting the standard component-wise addition, negation, and zero element from the function space (Fin 1⊕Fin d)→R(\text{Fin } 1 \oplus \text{Fin } d) \to \mathbb{R} via the canonical equivalence ContrMod d≅R1+d\text{ContrMod } d \cong \mathbb{R}^{1+d}.

instance

R\mathbb{R}-module structure on ContrMod d\text{ContrMod } d

The space of contravariant real Lorentz vectors ContrMod d\text{ContrMod } d is equipped with a module structure over the field of real numbers R\mathbb{R}. This structure is defined by transporting the standard component-wise scalar multiplication and addition from the function space (Fin 1⊕Fin d)→R(\text{Fin } 1 \oplus \text{Fin } d) \to \mathbb{R} via the canonical equivalence ContrMod d≅R1+d\text{ContrMod } d \cong \mathbb{R}^{1+d}, where the index set represents one temporal and dd spatial dimensions.

theorem

(ψ+ψ′).val=ψ.val+ψ′.val(\psi + \psi').\text{val} = \psi.\text{val} + \psi'.\text{val}

For any two contravariant real Lorentz vectors ψ\psi and ψ′\psi' in the space ContrMod d\text{ContrMod } d, the underlying vector representation (the value) of their sum is equal to the sum of their individual underlying vector representations. That is, (ψ+ψ′).val=ψ.val+ψ′.val,(\psi + \psi').\text{val} = \psi.\text{val} + \psi'.\text{val}, where the addition on the left is the addition in ContrMod d\text{ContrMod } d and the addition on the right is the component-wise addition in the underlying function space (Fin 1⊕Fin d)→R(\text{Fin } 1 \oplus \text{Fin } d) \to \mathbb{R}.

theorem

(r⋅ψ).val=r⋅ψ.val(r \cdot \psi).\text{val} = r \cdot \psi.\text{val} for Contravariant Lorentz Vectors

For any real number rr and any contravariant real Lorentz vector ψ\psi in the space ContrMod d\text{ContrMod } d, the underlying vector representation of the scalar multiplication r⋅ψr \cdot \psi is equal to the scalar multiplication of rr and the underlying vector representation of ψ\psi. That is, (r⋅ψ).val=r⋅ψ.val,(r \cdot \psi).\text{val} = r \cdot \psi.\text{val}, where the scalar multiplication on the left is defined within the R\mathbb{R}-module structure of ContrMod d\text{ContrMod } d, and the scalar multiplication on the right is the component-wise multiplication in the underlying function space (Fin 1⊕Fin d)→R(\text{Fin } 1 \oplus \text{Fin } d) \to \mathbb{R}.

definition

Linear isomorphism ContrMod d≅R1+d\text{ContrMod } d \cong \mathbb{R}^{1+d}

This is the linear equivalence (isomorphism of R\mathbb{R}-modules) between the space of contravariant real Lorentz vectors ContrMod d\text{ContrMod } d and the coordinate space (Fin 1⊕Fin d)→R(\text{Fin } 1 \oplus \text{Fin } d) \to \mathbb{R}. It identifies a contravariant vector with its (1+d)(1+d) real components (v0,v1,…,vd)(v^0, v^1, \dots, v^d), where the index set is partitioned into one temporal and dd spatial dimensions, preserving both vector addition and scalar multiplication over R\mathbb{R}.

abbrev

Coordinate representation of a contravariant Lorentz vector ψ\psi

For a contravariant real Lorentz vector ψ∈ContrMod d\psi \in \text{ContrMod } d, this function returns its representation as a coordinate vector in the space (Fin 1⊕Fin d)→R(\text{Fin } 1 \oplus \text{Fin } d) \to \mathbb{R}. It maps the abstract vector ψ\psi to its 1+d1+d real components (v0,v1,…,vd)(v^0, v^1, \dots, v^d) using the linear isomorphism toFin1dREquiv\text{toFin1dℝEquiv}.

theorem

ψ.toFin1dR=ψ.val\psi.\text{toFin1d}\mathbb{R} = \psi.\text{val}

For a contravariant real Lorentz vector ψ\psi in the module ContrMod d\text{ContrMod } d, its representation as a coordinate vector in (Fin 1⊕Fin d)→R(\text{Fin } 1 \oplus \text{Fin } d) \to \mathbb{R}, denoted by ψ.toFin1dR\psi.\text{toFin1d}\mathbb{R}, is equal to its underlying value ψ.val\psi.\text{val}.

definition

Standard Basis for ContrMod d\text{ContrMod } d

The standard basis for the space of contravariant real Lorentz vectors ContrMod d\text{ContrMod } d, indexed by the set Fin 1⊕Fin d\text{Fin } 1 \oplus \text{Fin } d (representing one temporal and dd spatial dimensions). This basis is defined by pulling back the canonical basis of the coordinate space R1+d\mathbb{R}^{1+d} via the linear isomorphism toFin1dREquiv\text{toFin1dℝEquiv}, such that the μ\mu-th basis vector corresponds to the tuple (v0,v1,…,vd)(v^0, v^1, \dots, v^d) where vν=δμνv^\nu = \delta_\mu^\nu.

theorem

The μ\mu-th component of the standard basis vector eμe_\mu is 11

For any index μ∈Fin 1⊕Fin d\mu \in \text{Fin } 1 \oplus \text{Fin } d, let eμe_\mu denote the μ\mu-th vector of the standard basis for the space of contravariant real Lorentz vectors ContrMod d\text{ContrMod } d. Under the canonical linear isomorphism Φ:ContrMod d≅R1+d\Phi: \text{ContrMod } d \cong \mathbb{R}^{1+d} (represented by `toFin1dℝEquiv`), the μ\mu-th component of eμe_\mu is equal to 11.

theorem

The μ\mu-th component of eμe_\mu is 11

For any index μ∈Fin 1⊕Fin d\mu \in \text{Fin } 1 \oplus \text{Fin } d, let eμe_\mu denote the μ\mu-th vector of the standard basis for the space of contravariant real Lorentz vectors ContrMod d\text{ContrMod } d. The μ\mu-th component of eμe_\mu is equal to 11.

theorem

The ν\nu-th component of stdBasis μ\text{stdBasis } \mu is 00 if μ≠ν\mu \neq \nu

In the space of contravariant real Lorentz vectors ContrMod d\text{ContrMod } d, let eμe_\mu be the μ\mu-th vector of the standard basis (denoted by `stdBasis μ`), where μ∈Fin 1⊕Fin d\mu \in \text{Fin } 1 \oplus \text{Fin } d represents the spacetime indices (one temporal and dd spatial). Let ϕ:ContrMod d→((Fin 1⊕Fin d)→R)\phi: \text{ContrMod } d \to ((\text{Fin } 1 \oplus \text{Fin } d) \to \mathbb{R}) be the linear isomorphism `toFin1dℝEquiv` that maps a Lorentz vector to its component representation. For any indices μ\mu and ν\nu such that μ≠ν\mu \neq \nu, the ν\nu-th component of the representation of eμe_\mu is 00.

theorem

The spatial components of the temporal standard basis vector are zero

In the space of contravariant real Lorentz vectors ContrMod d\text{ContrMod } d, let e0e_0 be the standard basis vector corresponding to the temporal dimension (indexed by Sum.inl 0\text{Sum.inl } 0 in the set Fin 1⊕Fin d\text{Fin } 1 \oplus \text{Fin } d). For any spatial index i∈Fin di \in \text{Fin } d, the component of e0e_0 at the index Sum.inr i\text{Sum.inr } i is 00.

theorem

Components of the standard basis vectors (eμ)ν=δμν(e_\mu)_\nu = \delta_{\mu\nu}

In the space of contravariant real Lorentz vectors ContrMod d\text{ContrMod } d, the standard basis vectors {eμ}\{e_\mu\} are indexed by μ∈Fin 1⊕Fin d\mu \in \text{Fin } 1 \oplus \text{Fin } d (representing one temporal and dd spatial dimensions). For any two indices μ\mu and ν\nu, the ν\nu-th component of the μ\mu-th basis vector is given by the Kronecker delta: (eμ)ν={1if μ=ν0if μ≠ν(e_\mu)_\nu = \begin{cases} 1 & \text{if } \mu = \nu \\ 0 & \text{if } \mu \neq \nu \end{cases}

theorem

Decomposition of v∈ContrMod dv \in \text{ContrMod } d into the Standard Basis

For any contravariant real Lorentz vector v∈ContrMod dv \in \text{ContrMod } d, let {ei}i∈Fin 1⊕Fin d\{e_i\}_{i \in \text{Fin } 1 \oplus \text{Fin } d} be the standard basis vectors and viv^i be the ii-th coordinate component of vv (represented by `toFin1dℝ`). The vector vv can be decomposed as the sum of its components multiplied by the corresponding basis vectors: v=∑ivieiv = \sum_i v^i e_i

abbrev

Matrix-vector multiplication MvM v for contravariant Lorentz vectors

Given a square matrix MM of size (1+d)×(1+d)(1+d) \times (1+d) over the real numbers R\mathbb{R} and a contravariant Lorentz vector vv in the (1+d)(1+d)-dimensional real vector space ContrMod d\text{ContrMod } d, this function computes the resulting vector in ContrMod d\text{ContrMod } d. The operation is defined by treating MM as a linear operator acting on vv with respect to the standard basis of the module.

definition

Matrix-vector multiplication M∗vvM *_{\text{v}} v

The notation M∗vvM *_{\text{v}} v represents the multiplication of a (1+d)×(1+d)(1+d) \times (1+d) real matrix MM and a contravariant Lorentz vector vv belonging to the module ContrMod d\text{ContrMod } d.

theorem

toFin1dR(Mv)=M⋅toFin1dRv\text{toFin1d}\mathbb{R} (M v) = M \cdot \text{toFin1d}\mathbb{R} v for contravariant Lorentz vectors

Let dd be a natural number representing the spatial dimension. For any square matrix MM of size (1+d)×(1+d)(1+d) \times (1+d) with real entries and any contravariant Lorentz vector v∈ContrMod dv \in \text{ContrMod } d, the coordinate representation of the matrix-vector product MvM v is equal to the standard matrix-vector multiplication of MM and the coordinate representation of vv. That is, (Mv).toFin1dR=M⋅(v.toFin1dR)(M v).\text{toFin1d}\mathbb{R} = M \cdot (v.\text{toFin1d}\mathbb{R}), where toFin1dR\text{toFin1d}\mathbb{R} maps a Lorentz vector to its components in R1+d\mathbb{R}^{1+d}.

theorem

(Mv).val=M⋅v.val(M v).\text{val} = M \cdot v.\text{val} for contravariant Lorentz vectors

Let MM be a real square matrix of size (1+d)×(1+d)(1+d) \times (1+d) and vv be a contravariant Lorentz vector in the (1+d)(1+d)-dimensional real vector space ContrMod d\text{ContrMod } d. Let v.valv.\text{val} denote the underlying coordinate vector of vv. The coordinate vector of the matrix-vector product MvM v is equal to the standard matrix-vector multiplication of MM and the coordinate vector of vv, that is, (Mv).val=M⋅v.val(M v).\text{val} = M \cdot v.\text{val}.

theorem

M(v−w)=Mv−MwM(v - w) = Mv - Mw for Contravariant Lorentz Vectors

Let MM be a (1+d)×(1+d)(1+d) \times (1+d) real matrix indexed by Fin 1⊕Fin d\text{Fin } 1 \oplus \text{Fin } d, and let v,w∈ContrMod dv, w \in \text{ContrMod } d be contravariant real Lorentz vectors. The matrix-vector multiplication distributes over vector subtraction such that M(v−w)=Mv−MwM(v - w) = Mv - Mw.

theorem

(M−N)v=Mv−Nv(M - N) v = M v - N v for contravariant Lorentz vectors

For any two real matrices MM and NN of size (1+d)×(1+d)(1+d) \times (1+d) (indexed by one temporal and dd spatial dimensions) and any contravariant real Lorentz vector v∈ContrMod dv \in \text{ContrMod } d, the matrix-vector multiplication distributes over matrix subtraction such that (M−N)v=Mv−Nv(M - N) v = M v - N v.

theorem

M(v+w)=Mv+MwM(v + w) = Mv + Mw for Contravariant Lorentz Vectors

For any (1+d)×(1+d)(1+d) \times (1+d) real matrix MM and any contravariant real Lorentz vectors v,wv, w in the space ContrMod d\text{ContrMod } d, the matrix-vector multiplication is distributive over vector addition: M(v+w)=Mv+MwM(v + w) = Mv + Mw where MvMv denotes the action of the matrix MM on the vector vv.

theorem

Iv=vI v = v for contravariant Lorentz vectors

For any contravariant real Lorentz vector vv in the (1+d)(1+d)-dimensional space ContrMod d\text{ContrMod } d, multiplying vv by the (1+d)×(1+d)(1+d) \times (1+d) identity matrix results in vv.

theorem

M(Nv)=(MN)vM(Nv) = (MN)v for contravariant Lorentz vectors

For any real square matrices MM and NN of size (1+d)×(1+d)(1+d) \times (1+d) and any contravariant real Lorentz vector vv in the space ContrMod d\text{ContrMod } d, the composition of matrix-vector multiplications satisfies the associativity property M(Nv)=(MN)vM(Nv) = (MN)v.

definition

Normed Additive Commutative Group Structure on ContrMod d\text{ContrMod } d

The space of contravariant Lorentz vectors ContrMod d\text{ContrMod } d in 1+d1+d dimensions is equipped with the structure of a normed additive commutative group. For a vector v∈ContrMod dv \in \text{ContrMod } d, the norm ∥v∥\|v\| is defined as the standard norm of its underlying component vector in R1+d\mathbb{R}^{1+d} (typically the L∞L^\infty or supremum norm of its components). This structure is intended for topological purposes and is distinct from the indefinite Minkowski quadratic form (often colloquially called the Minkowski norm). This definition is not registered as a global instance to prevent it from being applied automatically in contexts where it might conflict with other structures.

definition

Spatial part of a Lorentz vector vv

For a contravariant Lorentz vector vv in 1+d1+d dimensions (represented by the type `ContrMod d`), this function extracts the spatial components by removing the first (temporal) component. The resulting vector consists of the "tail" of the original vector and is mapped to the Euclidean space Rd\mathbb{R}^d equipped with the L2L^2 norm.

definition

Lorentz Group Representation on ContrMod d\text{ContrMod } d

This definition defines the representation ρ\rho of the Lorentz group LorentzGroup d\text{LorentzGroup } d on the R\mathbb{R}-module of contravariant real Lorentz vectors ContrMod d\text{ContrMod } d. For an element gg of the Lorentz group (represented as a matrix), the linear automorphism ρ(g)\rho(g) of ContrMod d\text{ContrMod } d is defined as the linear map corresponding to the matrix gg with respect to the standard basis of ContrMod d\text{ContrMod } d.

theorem

Lorentz transformation of ContrMod d\text{ContrMod } d as matrix-vector multiplication

For any Lorentz transformation g∈LorentzGroup dg \in \text{LorentzGroup } d and any contravariant real Lorentz vector ψ∈ContrMod d\psi \in \text{ContrMod } d, the coordinate representation of the transformed vector ρ(g)ψ\rho(g)\psi is obtained by multiplying the matrix representing gg by the coordinate vector of ψ\psi. Mathematically, this is expressed as: [ρ(g)ψ]=Λ⋅[ψ] [\rho(g)\psi] = \Lambda \cdot [\psi] where [⋅][\cdot] denotes the coordinate representation mapping `toFin1dℝ` into R1+d\mathbb{R}^{1+d}, ρ\rho is the representation of the Lorentz group on contravariant vectors, and Λ\Lambda is the matrix underlying the group element gg.

definition

Linear isomorphism ContrMod 3≅selfAdjoint(M2(C))\text{ContrMod } 3 \cong \text{selfAdjoint}(M_2(\mathbb{C}))

This definition establishes a linear isomorphism between the R\mathbb{R}-module of contravariant real Lorentz vectors in 3+13+1 dimensions, denoted as ContrMod 3\text{ContrMod } 3, and the space of 2×22 \times 2 self-adjoint (Hermitian) complex matrices, selfAdjoint(M2(C))\text{selfAdjoint}(M_2(\mathbb{C})). Given a contravariant vector xx with components (x0,x1,x2,x3)(x^0, x^1, x^2, x^3), the mapping is defined by the linear combination of Pauli matrices: x↦x0σ0−x1σ1−x2σ2−x3σ3 x \mapsto x^0 \sigma_0 - x^1 \sigma_1 - x^2 \sigma_2 - x^3 \sigma_3 where σ0\sigma_0 is the 2×22 \times 2 identity matrix and σ1,σ2,σ3\sigma_1, \sigma_2, \sigma_3 are the standard Pauli matrices. This map preserves the R\mathbb{R}-linear structure of both spaces.

theorem

toSelfAdjoint(x)=x0σ0−x1σ1−x2σ2−x3σ3\text{toSelfAdjoint}(x) = x^0 \sigma_0 - x^1 \sigma_1 - x^2 \sigma_2 - x^3 \sigma_3

For any contravariant real Lorentz vector x∈ContrMod 3x \in \text{ContrMod } 3 in 3+13+1 dimensions, the linear isomorphism toSelfAdjoint\text{toSelfAdjoint} maps xx to the 2×22 \times 2 self-adjoint (Hermitian) matrix: toSelfAdjoint(x)=x0σ0−x1σ1−x2σ2−x3σ3 \text{toSelfAdjoint}(x) = x^0 \sigma_0 - x^1 \sigma_1 - x^2 \sigma_2 - x^3 \sigma_3 where x0x^0 is the temporal component of xx, x1,x2,x3x^1, x^2, x^3 are its spatial components, and σ0,σ1,σ2,σ3\sigma_0, \sigma_1, \sigma_2, \sigma_3 are the standard 2×22 \times 2 matrices (with σ0\sigma_0 being the identity matrix and σ1,σ2,σ3\sigma_1, \sigma_2, \sigma_3 being the Pauli matrices).

theorem

Matrix value of toSelfAdjoint(x)=x0σ0−x1σ1−x2σ2−x3σ3\text{toSelfAdjoint}(x) = x^0 \sigma_0 - x^1 \sigma_1 - x^2 \sigma_2 - x^3 \sigma_3

For a contravariant real Lorentz vector x∈ContrMod 3x \in \text{ContrMod } 3 in 3+13+1 dimensions, the complex 2×22 \times 2 matrix associated with the self-adjoint matrix toSelfAdjoint(x)\text{toSelfAdjoint}(x) is given by the linear combination: (toSelfAdjoint x)ij=x0σ0−x1σ1−x2σ2−x3σ3 (\text{toSelfAdjoint } x)_{ij} = x^0 \sigma_0 - x^1 \sigma_1 - x^2 \sigma_2 - x^3 \sigma_3 where x0x^0 is the temporal component of xx, x1,x2,x3x^1, x^2, x^3 are its spatial components, σ0\sigma_0 is the 2×22 \times 2 identity matrix, and σ1,σ2,σ3\sigma_1, \sigma_2, \sigma_3 are the standard Pauli matrices.

theorem

toSelfAdjoint(stdBasisi)=pauliBasisi′\text{toSelfAdjoint}(\text{stdBasis}_i) = \text{pauliBasis}'_i

For any index i∈Fin 1⊕Fin 3i \in \text{Fin } 1 \oplus \text{Fin } 3, the linear isomorphism toSelfAdjoint\text{toSelfAdjoint} maps the ii-th standard basis vector stdBasisi\text{stdBasis}_i of the space of contravariant Lorentz vectors ContrMod 3\text{ContrMod } 3 to the ii-th element pauliBasisi′\text{pauliBasis}'_i of the Pauli-related basis for the space of 2×22 \times 2 self-adjoint matrices.

theorem

toSelfAdjoint−1(pauliBasisi′)=stdBasisi\text{toSelfAdjoint}^{-1}(\text{pauliBasis}'_i) = \text{stdBasis}_i

For any index i∈Fin 1⊕Fin 3i \in \text{Fin } 1 \oplus \text{Fin } 3, the inverse of the linear isomorphism toSelfAdjoint\text{toSelfAdjoint} maps the ii-th Pauli-related basis element pauliBasisi′\text{pauliBasis}'_i to the ii-th standard basis vector stdBasisi\text{stdBasis}_i of the space of contravariant Lorentz vectors ContrMod 3\text{ContrMod } 3. That is, toSelfAdjoint−1(pauliBasisi′)=stdBasisi \text{toSelfAdjoint}^{-1}(\text{pauliBasis}'_i) = \text{stdBasis}_i

instance

Topology on the space of contravariant Lorentz vectors ContrMod d\text{ContrMod } d

The space of contravariant real Lorentz vectors ContrMod d\text{ContrMod } d is equipped with a topological structure. This topology is the induced topology (the coarsest topology making the map continuous) via the canonical linear equivalence ContrMod d≅R1+d\text{ContrMod } d \cong \mathbb{R}^{1+d}, where R1+d\mathbb{R}^{1+d} is represented as the function space (Fin 1⊕Fin d)→R(\text{Fin } 1 \oplus \text{Fin } d) \to \mathbb{R} endowed with the standard product topology. This effectively identifies the topology of the Lorentz vector space with the standard Euclidean topology of its (1+d)(1+d) components.

theorem

The component isomorphism ContrMod d≅R1+d\text{ContrMod } d \cong \mathbb{R}^{1+d} is an inducing map

The canonical linear isomorphism Φ:ContrMod d→≅R1+d\Phi: \text{ContrMod } d \xrightarrow{\cong} \mathbb{R}^{1+d}, which identifies a contravariant real Lorentz vector with its 1+d1+d components in the space (Fin 1⊕Fin d)→R(\text{Fin } 1 \oplus \text{Fin } d) \to \mathbb{R}, is an inducing map. This means the topology on the space of contravariant Lorentz vectors is the initial topology induced by Φ\Phi from the standard product topology on R1+d\mathbb{R}^{1+d}.

theorem

The inverse coordinate isomorphism R1+d≅ContrMod d\mathbb{R}^{1+d} \cong \text{ContrMod } d is an inducing map

The inverse of the canonical linear isomorphism Φ:ContrMod d→≅R1+d\Phi: \text{ContrMod } d \xrightarrow{\cong} \mathbb{R}^{1+d}, which maps the coordinate space (Fin 1⊕Fin d)→R(\text{Fin } 1 \oplus \text{Fin } d) \to \mathbb{R} to the space of contravariant real Lorentz vectors in 1+d1+d dimensions, is an inducing map. This means the topology on the coordinate space R1+d\mathbb{R}^{1+d} is the initial topology induced by Φ−1\Phi^{-1} from the topology on ContrMod d\text{ContrMod } d.

theorem

Extensionality of Covariant Lorentz Vectors: ψ.val=ψ′.val  ⟹  ψ=ψ′\psi.val = \psi'.val \implies \psi = \psi'

For any two covariant Lorentz vectors ψ,ψ′∈CoMod d\psi, \psi' \in \text{CoMod } d, if their underlying component representations are equal (ψ.val=ψ′.val\psi.val = \psi'.val), then the vectors themselves are equal (ψ=ψ′\psi = \psi'). Here, CoMod d\text{CoMod } d represents the space of covariant Lorentz vectors in 1+d1+d dimensions.

definition

Equivalence between CoMod d\text{CoMod } d and (1⊕d)→R(1 \oplus d) \to \mathbb{R}

This equivalence provides a bijection between the space of covariant Lorentz vectors CoMod d\text{CoMod } d and the space of real-valued functions on the index set {0}⊕{1,…,d}\{0\} \oplus \{1, \dots, d\}. It maps a covariant vector vv to its underlying component function f:(1⊕d)→Rf: (1 \oplus d) \to \mathbb{R}, and conversely, wraps a function to form a covariant vector. This represents the identification of a 1+d1+d dimensional Lorentz vector with its components in the standard basis.

instance

Additive commutative monoid structure on CoMod d\text{CoMod } d

The space of covariant Lorentz vectors CoMod d\text{CoMod } d is equipped with an additive commutative monoid structure. This structure is defined by transporting the pointwise addition and zero element from the space of real-valued functions (Fin 1⊕Fin d)→R(\text{Fin } 1 \oplus \text{Fin } d) \to \mathbb{R} to CoMod d\text{CoMod } d using the canonical equivalence between them.

instance

Additive commutative group structure on CoMod d\text{CoMod } d

The space of covariant Lorentz vectors CoMod d\text{CoMod } d is equipped with an additive commutative group structure. This structure is defined by transporting the pointwise addition, zero element, and additive inverse operations from the space of real-valued functions (Fin 1⊕Fin d)→R(\text{Fin } 1 \oplus \text{Fin } d) \to \mathbb{R} to CoMod d\text{CoMod } d via the canonical equivalence between them.

instance

R\mathbb{R}-module structure on CoMod d\text{CoMod } d

The space of covariant Lorentz vectors CoMod d\text{CoMod } d is equipped with a module structure over the real numbers R\mathbb{R}. This structure is defined by transporting the scalar multiplication and additive operations from the space of real-valued functions (Fin 1⊕Fin d)→R(\text{Fin } 1 \oplus \text{Fin } d) \to \mathbb{R} to CoMod d\text{CoMod } d via the canonical equivalence between them.

definition

Linear equivalence CoMod d≅(Fin 1⊕Fin d→R)\text{CoMod } d \cong (\text{Fin } 1 \oplus \text{Fin } d \to \mathbb{R})

The linear equivalence CoMod d≅R(Fin 1⊕Fin d→R)\text{CoMod } d \cong_{\mathbb{R}} (\text{Fin } 1 \oplus \text{Fin } d \to \mathbb{R}) identifies the module of covariant Lorentz vectors of dimension 1+d1+d with the space of real-valued functions defined on the index set {0}∪{1,…,d}\{0\} \cup \{1, \dots, d\}. This map establishes a vector space isomorphism that associates each covariant vector with its components in the standard basis.

abbrev

Representation of ψ∈CoMod d\psi \in \text{CoMod } d as a function (Fin 1⊕Fin d)→R(\text{Fin } 1 \oplus \text{Fin } d) \to \mathbb{R}

Given a covariant Lorentz vector ψ∈CoMod d\psi \in \text{CoMod } d in 1+d1+d dimensions, this function returns its representation as a real-valued function on the index set Fin 1⊕Fin d\text{Fin } 1 \oplus \text{Fin } d (representing the time and space components) by applying the linear equivalence toFin1dREquiv\text{toFin1dℝEquiv}.

definition

Standard basis of CoMod d\text{CoMod } d

The standard basis for the space of covariant Lorentz vectors CoMod d\text{CoMod } d is a basis indexed by the set Fin 1⊕Fin d\text{Fin } 1 \oplus \text{Fin } d. This basis is defined by pulling back the standard basis of the function space (Fin 1⊕Fin d)→R(\text{Fin } 1 \oplus \text{Fin } d) \to \mathbb{R} through the linear equivalence toFin1dREquiv:CoMod d≅R((Fin 1⊕Fin d)→R)\text{toFin1dℝEquiv} : \text{CoMod } d \cong_{\mathbb{R}} ((\text{Fin } 1 \oplus \text{Fin } d) \to \mathbb{R}). Essentially, it represents the set of vectors {eμ}\{e_\mu\} where each eμe_\mu corresponds to a vector whose components are all zero except for the μ\mu-th component, which is 1.

theorem

The μ\mu-th component of the standard basis vector eμe_\mu is 11

Let CoMod d\text{CoMod } d be the module of covariant Lorentz vectors in 1+d1+d dimensions, and let {eμ}μ∈Fin 1⊕Fin d\{e_\mu\}_{\mu \in \text{Fin } 1 \oplus \text{Fin } d} be its standard basis. For any index μ∈Fin 1⊕Fin d\mu \in \text{Fin } 1 \oplus \text{Fin } d, the μ\mu-th component of the basis vector eμe_\mu, obtained via the linear equivalence to the function space (Fin 1⊕Fin d)→R(\text{Fin } 1 \oplus \text{Fin } d) \to \mathbb{R}, is equal to 11.

theorem

The μ\mu-th component of the standard basis vector eμe_\mu is 11

Let CoMod d\text{CoMod } d be the space of covariant Lorentz vectors in 1+d1+d dimensions, and let {eμ}μ∈Fin 1⊕Fin d\{e_\mu\}_{\mu \in \text{Fin } 1 \oplus \text{Fin } d} be its standard basis. For any index μ∈Fin 1⊕Fin d\mu \in \text{Fin } 1 \oplus \text{Fin } d, the μ\mu-th component of the basis vector eμe_\mu is equal to 11.

theorem

The ν\nu-th component of the standard basis vector eμe_\mu is 00 if μ≠ν\mu \neq \nu

Let CoMod d\text{CoMod } d be the space of covariant Lorentz vectors and let {eμ}μ∈Fin 1⊕Fin d\{e_\mu\}_{\mu \in \text{Fin } 1 \oplus \text{Fin } d} be its standard basis. For any indices μ\mu and ν\nu such that μ≠ν\mu \neq \nu, the ν\nu-th component of the basis vector eμe_\mu (as determined by the linear equivalence to the coordinate space toFin1dREquiv\text{toFin1dℝEquiv}) is 00.

theorem

The ν\nu-th component of the standard basis vector eμe_\mu is δμν\delta_{\mu\nu}

Let {eμ}μ∈Fin 1⊕Fin d\{e_\mu\}_{\mu \in \text{Fin } 1 \oplus \text{Fin } d} be the standard basis for the space of covariant Lorentz vectors CoMod d\text{CoMod } d. For any indices μ\mu and ν\nu, the ν\nu-th component of the μ\mu-th basis vector eμe_\mu is given by (eμ)ν={1if μ=ν0if μ≠ν (e_\mu)_\nu = \begin{cases} 1 & \text{if } \mu = \nu \\ 0 & \text{if } \mu \neq \nu \end{cases} In other words, the components of the standard basis vectors are given by the Kronecker delta δμν\delta_{\mu\nu}.

theorem

Standard Basis Decomposition v=∑ivieiv = \sum_i v_i e_i for Covariant Lorentz Vectors

In the space of covariant Lorentz vectors CoMod d\text{CoMod } d, any vector vv can be uniquely decomposed into the standard basis {ei}i∈Fin 1⊕Fin d\{e_i\}_{i \in \text{Fin } 1 \oplus \text{Fin } d} as: v=∑ivieiv = \sum_{i} v_i e_i where viv_i is the ii-th component of the vector vv (obtained via the representation function v.toFin1dRv.\text{toFin1dℝ}) and eie_i is the ii-th vector of the standard basis stdBasis\text{stdBasis}.

abbrev

Matrix-vector product MvM v for covariant Lorentz vectors

Given a square matrix MM of size (1+d)×(1+d)(1+d) \times (1+d) over the real numbers R\mathbb{R} and a covariant Lorentz vector v∈CoModdv \in \text{CoMod}_d, this function computes the matrix-vector product MvM v. The operation is defined by applying the linear transformation represented by the matrix MM with respect to the standard basis {eμ}μ∈Fin 1⊕Fin d\{e_\mu\}_{\mu \in \text{Fin } 1 \oplus \text{Fin } d} to the vector vv, resulting in a new covariant Lorentz vector in CoModd\text{CoMod}_d.

definition

Matrix-vector multiplication notation M∗vvM *_{\text{v}} v for covariant Lorentz vectors

The infix operator ∗v*_{\text{v}} denotes the multiplication of a square matrix MM of size (1+d)×(1+d)(1+d) \times (1+d) over R\mathbb{R} with a covariant Lorentz vector v∈CoModdv \in \text{CoMod}_d. The result M∗vvM *_{\text{v}} v is a new covariant Lorentz vector in CoModd\text{CoMod}_d.

theorem

Representation of MvM v equals MM times representation of vv for covariant Lorentz vectors

Let MM be a real matrix of size (1+d)×(1+d)(1+d) \times (1+d) and vv be a covariant Lorentz vector in CoModd\text{CoMod}_d. Let toFin1dR\text{toFin1dℝ} be the function that maps a covariant Lorentz vector to its representation as a real-valued function on the index set {0,1,…,d}\{0, 1, \dots, d\}. Then the representation of the matrix-vector product MvM v is equal to the standard matrix-vector product of MM and the representation of vv: (Mv).toFin1dR=M(v.toFin1dR) (M v).\text{toFin1dℝ} = M (v.\text{toFin1dℝ})

theorem

(Mv).val=M(v.val)(M v).\text{val} = M (v.\text{val}) for Covariant Lorentz Vectors

For any real matrix MM of size (1+d)×(1+d)(1+d) \times (1+d) and any covariant Lorentz vector v∈CoModdv \in \text{CoMod}_d, the underlying vector components of the matrix-vector product MvM v are equal to the standard matrix-vector multiplication of MM and the components of vv. This is expressed as (Mv).val=M(v.val)(M v).\text{val} = M (v.\text{val}), where val\text{val} denotes the underlying coordinate vector in R1+d\mathbb{R}^{1+d}.

definition

Representation of the Lorentz group on CoMod d\text{CoMod } d

The representation ρ\rho of the Lorentz group O(1,d)\text{O}(1, d) on the space of covariant Lorentz vectors CoMod d≅R1+d\text{CoMod } d \cong \mathbb{R}^{1+d}. For an element gg of the Lorentz group, let Λ\Lambda be its corresponding matrix. The representation maps gg to the linear automorphism of CoMod d\text{CoMod } d whose matrix with respect to the standard basis is the transpose inverse (Λ−1)⊺(\Lambda^{-1})^\intercal. This defines the standard transformation law for covariant vectors (covectors) under Lorentz transformations.