Space time

This file introduce 4d Minkowski spacetime.

def SpaceTime : Type

The space-time

Equations

• SpaceTime = (Fin 4 → ℝ)

instance instAddCommMonoidSpaceTime : AddCommMonoid SpaceTime

Give spacetime the structure of an additive commutative monoid.

Equations

• instAddCommMonoidSpaceTime = Pi.addCommMonoid

instance instModuleRealSpaceTime : Module ℝ SpaceTime

Give spacetime the structure of a module over the reals.

Equations

• instModuleRealSpaceTime = Pi.module (Fin 4) (fun (a : Fin 4) => ℝ) ℝ

instance euclideanNormedAddCommGroup : NormedAddCommGroup SpaceTime

The instance of a normed group on spacetime defined via the Euclidean norm.

Equations

• euclideanNormedAddCommGroup = Pi.normedAddCommGroup

instance euclideanNormedSpace : NormedSpace ℝ SpaceTime

The Euclidean norm-structure on space time. This is used to give it a smooth structure.

Equations

• euclideanNormedSpace = Pi.normedSpace

def SpaceTime.space (x : SpaceTime) : EuclideanSpace ℝ (Fin 3)

The space part of spacetime.

Equations

• x.space = ![x 1, x 2, x 3]

def SpaceTime.asSmoothManifold : ModelWithCorners ℝ SpaceTime SpaceTime

The structure of a smooth manifold on spacetime.

Equations

• SpaceTime.asSmoothManifold = modelWithCornersSelf ℝ SpaceTime

instance SpaceTime.instChartedSpace : ChartedSpace SpaceTime SpaceTime

The instance of a ChartedSpace on SpaceTime.

Equations

• SpaceTime.instChartedSpace = chartedSpaceSelf SpaceTime

def SpaceTime.stdBasis : Basis (Fin 4) ℝ SpaceTime

The standard basis for spacetime.

Equations

• SpaceTime.stdBasis = Pi.basisFun ℝ (Fin 4)

theorem SpaceTime.stdBasis_apply (μ ν : Fin 4) : stdBasis μ ν = if μ = ν then 1 else 0

theorem SpaceTime.stdBasis_not_eq {μ ν : Fin 4} (h : μ ≠ ν) : stdBasis μ ν = 0

theorem SpaceTime.stdBasis_0 : stdBasis 0 = ![1, 0, 0, 0]

For space-time,stdBasis 0 is equal to ![1, 0, 0, 0] .

theorem SpaceTime.stdBasis_1 : stdBasis 1 = ![0, 1, 0, 0]

For space-time,stdBasis 1 is equal to ![0, 1, 0, 0] .

theorem SpaceTime.stdBasis_2 : stdBasis 2 = ![0, 0, 1, 0]

For space-time,stdBasis 2 is equal to ![0, 0, 1, 0] .

theorem SpaceTime.stdBasis_3 : stdBasis 3 = ![0, 0, 0, 1]

For space-time,stdBasis 3 is equal to ![0, 0, 0, 1] .

theorem SpaceTime.stdBasis_mulVec (μ ν : Fin 4) (Λ : Matrix (Fin 4) (Fin 4) ℝ) : Λ.mulVec (stdBasis μ) ν = Λ ν μ

theorem SpaceTime.explicit (x : SpaceTime) : x = ![x 0, x 1, x 2, x 3]

The explicit expansion of a point in spacetime as ![x 0, x 1, x 2, x 3].

@[simp]

theorem SpaceTime.add_apply (x y : SpaceTime) (i : Fin 4) : (x + y) i = x i + y i

@[simp]

theorem SpaceTime.smul_apply (x : SpaceTime) (a : ℝ) (i : Fin 4) : (a • x) i = a * x i