Time slice

Time slicing functions on spacetime, turning them into a function Time → Space d → M.

This is useful when going from relativistic physics (defined using SpaceTime) to non-relativistic physics (defined using Space and Time).

def SpaceTime.timeSlice {d : ℕ} {M : Type} : (SpaceTime d → M) ≃ (Time → Space d → M)

The timeslice of a function SpaceTime d → M forming a function Time → Space d → M.

Equations

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

def SpaceTime.timeSliceLinearEquiv {d : ℕ} {M : Type} [AddCommGroup M] [Module ℝ M] : (SpaceTime d → M) ≃ₗ[ℝ] Time → Space d → M

The timeslice of a function SpaceTime d → M forming a function Time → Space d → M, as a linear equivalence.

Equations

• SpaceTime.timeSliceLinearEquiv = { toFun := ⇑SpaceTime.timeSlice, map_add' := ⋯, map_smul' := ⋯, invFun := ⇑SpaceTime.timeSlice.symm, left_inv := ⋯, right_inv := ⋯ }

theorem SpaceTime.timeSliceLinearEquiv_apply {d : ℕ} {M : Type} [AddCommGroup M] [Module ℝ M] (f : SpaceTime d → M) : timeSliceLinearEquiv f = timeSlice f

theorem SpaceTime.timeSliceLinearEquiv_symm_apply {d : ℕ} {M : Type} [AddCommGroup M] [Module ℝ M] (f : Time → Space d → M) : timeSliceLinearEquiv.symm f = timeSlice.symm f