Formalization: Derivatives and SpaceTime

This issue originates from this conversation.

• Define the epsilon tensor in general dimension. See here.
• Redefine the spaceCurl in terms of this epsilon tensor.
• Define a continuous linear equivalence between SpaceTime and Time x Space.
• Define a map timeSlice taking SpaceTime → M to Time → Space → M with corresponding API.
• Define ((realLorentzTensor d).tensorBasis _ (fun x => Fin.cast (by simp) μ)) formally as a unit vector in SpaceTime pointing the μ direction.
• Change SpaceTime.deriv to an abbreviation of fderiv using the above spacetime derivative.
• Come up with a good way to go from SpaceTime to Space derivatives etc. (e.g. greek derivatives vs latin)
• Use the above to rewrite Maxwell's equations in a better way.

For more details on individual points see the details of the above conversation.

Start by reviewing the remaining unchecked items around the epsilon tensor, spaceCurl, SpaceTime.deriv, and conversions between SpaceTime and Space derivatives. Use the linked Maxwell's Equations discussion for context, then determine the formalization scope for each item. Done means the selected definitions and derivative APIs are formalized and Maxwell's equations use them.