Space, Time and SpaceTime API

Stream: PhysLean

[Joseph Tooby-Smith]

Following on from the thread:

#PhysLean > Fourier Transform

I thought it was worth having a dedicated thread for the API around Space, Time and SpaceTime, given their importance. (And also not to distract away from the original purpose of that thread).

I now know of three things which it would be great to do with these APIs.

1. Improve the documentation in the PhysLean.SpaceAndTime.Space.Basic module, to make it an entry point into the project.
2. The definition of the type Space d is currently using an abbrev, but I think it might be better to have it as a def. This will require improving the API around Space, which can only be a good thing.
3. Create a physics-orientated API around distributions (ideally so that people don't even know they are working with distributions).

As a start to 1, I've made this small PR641. Any help with any of these would be great.

[David Feng]

Curious what's the current status with this initiative? Looking at potentially contributing here

[Joseph Tooby-Smith]

Hey, so 1 & 2 are still very much open, and would be great things to try and tackle! 3 is being discussed at #PhysLean > Normed dual of Schwarz space

[Joseph Tooby-Smith]

Following on somewhat, from the thread on units, but something which is more on topic for this thread:

I've been thinking about what the type Time is in PhysLean, and how one should think about it. As a result of this 'thinking' I think should modify the docstring to the Time.Basic file to be the following:

/-!
# Time

In this module we define the type `Time`, corresponding to time in a given
(but arbitary) set of units, with a given (but arbitary) choice of origin (time zero).
We note that this is the version of time most often used in undergraduate and
non-mathematical physics.

The choice of units or origin can be made on a case-by-case basis, as
long as they are done consistently. However, since the choice of units and origin is
left implicit, Lean will not catch inconsistencies in the choice of units or origin when
working with `Time`.

For example, for the classical mechanics system corresponding to the harmonic oscillator,
one can take the origin of time to be the time at which the initial conditions are specified,
and the units can be taken as anything as long as the units chosen for time `t` and
the angular frequency `ω` are consistent.

With this notion of `Time`, it becomes equivalent to the type `ℝ`, and inherits all the
instances of `ℝ`.

Within other modules e.g. `TopTime.Basic`, we define versions of time with less choices made.

-/

[David Feng]

@Joseph Tooby-Smith I'd like to understand the high level goals of the Space API. Is the intention to abstract away from EuclideanSpace ℝ (Fin d) ?

What would you see as an "improvement" to the Space API wrt item number 2 here?

[Joseph Tooby-Smith]

Ok, great question.

The problem currently is that Space d is definitionally the same type as EuclideanSpace ℝ (Fin d). The advantage of this, is that you get all the API that has been defined on EuclideanSpace ℝ (Fin d) for free on Space d. But the (major) downside to this is that Lean is more than happy to treat an element of EuclideanSpace ℝ (Fin d) as an element of Space d and vice versa.

This means if you define multiple things as equivalent to EuclideanSpace ℝ (Fin d), like ElectricField d and Space d, you can treat terms of these types as terms of the other type (an electric field as a point in space etc). Mathematically this is fine, but physically it makes no sense. The idea of abstracting away from EuclideanSpace ℝ (Fin d) is to prevent such casting.

There are other advantages too, if you abstract away from EuclideanSpace ℝ (Fin d) there is more freedom to give Space d the additional instances that makes physical sense , not just inherit everything from EuclideanSpace ℝ (Fin d).

This PR did the analogous to (2) for Time.

I should say, that I made a mistake in the statement of (2) really I think we want Space d to be defined like:

structure Space (d : Nat) where
    val : EuclideanSpace ℝ (Fin d)

But even turning it from a abbrev to a def gets half-way to doing this.

[David Feng]

That makes sense! I'm curious though what about the constructs from EuclideanSpace ℝ (Fin d) which the Space API makes use of currently?

Perhaps I just need to get more familiar with encapsulation in Lean, but would we be able to choose to only expose the inner product from EuclideanSpace, for example?

I imagine we wouldn't want to be completely redefining everything need from the underlying EuclideanSpace instance ,correct?

[Joseph Tooby-Smith]

I think we basically only use that it is an inner product space and the instances needed to define that inner-product space e.g. Module.. You can sometimes use deriving to expose certain instances on something defined through a def, but I'm not sure this works with InnerProduct or even Module. However, doing so does not prevent the casting issue I mentioned.

I imagine we wouldn't want to be completely redefining everything need from the underlying EuclideanSpace instance ,correct?

I think this can be solved by 1. defining an inner product structure on Space d using it's underlying val, and then defining an isometry equivalence between Space d and EuclideanSpace ℝ (Fin d). Then everything on EuclideanSpace ℝ (Fin d) can be carried over to Space d with use of this isometry.

[Joseph Tooby-Smith]

I should caveat this with: I understand that this is a design choice. And because it is a choice there isn't one correct answer for how things should be done. But I do think that the design choice using structure does have several advantages over using abbrev or def - but I'm always happy to hear counterarguments.

[Joseph Tooby-Smith]

This probably can wait, but I think it would be good to define type instance:

instance : VAdd (EuclideanSpace (Fin d) ℝ) (Space d) where ...

To allow us to add elements of EuclideanSpace (Fin d) ℝ to Space d without weirdly casting things as Space.

[Daniel Morrison]

I started work on rewriting SpaceTime as a structure with a Time component and a Space component (currently SpaceStruct while rewriting is happening), currently SpaceTimeStruct to not break everything.

What I have so far is here. It has a few sorrys related to SpaceStruct not having a Module or InnerProductSpace instance. I pulled in some stuff from other files since they were relatively small.

I wasn't sure what operations to put on it so I just implemented everything I could by doing it on Time and Space separately. I'm not sure if we actually want all of them but I did it anyway. In particular I decided to add a regular inner product to SpaceTime which is the sum of the inner products on the Time and Space components, and then the Minkowski product is a bilinear form. I was kind of thinking ahead to wanting to define distributions on SpaceTime which currently requires a NormedAddCommGroup instance which in part needs dist x y = 0 implies x = y which wouldn't be true of the Minkowski product so we need a separate inner product.

[Joseph Tooby-Smith]

Nice! Thank you for doing this. I think we will need the normal inner-product for the reasons you state.

For the Minkowski product, I think it is best to define it in the same way it is done for Lorentz.vector, which is to

1. define a Tensorial instance see here.
2. define it through index notation (see here).

The Tensorial instance, will then give you, for free, an action of the Lorentz group on SpaceTime.

[Joseph Tooby-Smith]

Also, for the causality stuff - thanks starting to reproduce that for SpaceTime - which I guess is the natural place for it to be defined, rather than Lorentz.Vector! :)

[Daniel Morrison]

My other thought was that I would presume that we want to separate time derivatives from space derivatives, e.g. if we have coords t, x, y, z I wouldn't think we want a derivative in the t + x direction. Rather we want to relate time derivatives and space derivatives so we don't actually want distributions on SpaceTime. Then again, I don't really know much about distributions so I could very well be way off.

[Daniel Morrison]

How much of the index notation do I need to understand in order to make a Tensorial instance? And where's the best place to start?

[Daniel Morrison]

My thought with the causality type stuff was it makes sense to condense it into a single file, at least for now so it's easier to see the state of things at a glace and then if it gets too big we can separate it out later.

[Joseph Tooby-Smith]

if we have coords t, x, y, z I wouldn't think we want a derivative in the t + x direction. Rather we want to relate time derivatives and space derivatives so we don't actually want distributions on SpaceTime.

I think ideally one would want both. I think the way to think about it, is that things related to special relativity and the Lorentz group should be done via SpaceTime whilst non-relativistic things should be done via Space and Time kept separate.

How much of the index notation do I need to understand in order to make a Tensorial instance? And where's the best place to start?

You shouldn't need to know much - if anything - all you need is to define a linear equivalence to the relevant Tensor space. But you could do this via defining a linear equivalence to Lorentz.Vector first and then composing that with the one defined in this instance.

[Joseph Tooby-Smith]

Actually somewhat related, to what @David Feng is doing with Space, I think eventually we will want an instance of a MulAction of SO(d) on Space, like we should have an instance of the Lorentz group acting on SpaceTime (which will be inherited from the tensorial instance).

[David Feng]

One question:

What Is the long term plan with respect to SpaceTime API depending on Space d and Time ?

I’m just wondering if we’d expect to run into any issues adding structure to SpaceTime as more structure is adddd to the underlying Space d

[Joseph Tooby-Smith]

Good point - so in practice I don't think it should cause any issues, but it might make @Daniel Morrison 's life a bit easier if SpaceTime isn't defined directly though Space and Time.

One thing about defining things through Structure is that the API around the definition becomes more important than the actual definition itself. Which should hopefully mean that small changes to the definition, shouldn't change it's usability if the API is kept up-to-date.

[Daniel Morrison]

Honestly I feel the opposite, it's maybe more complicated to work on something in tandem with other people but the actual API is way easier to write. Most of what I wrote was unfold SpaceTime into the Space and Time components and apply the properties there. It also means that if we want to change how Space works we can do that and not have to worry about changing all of SpaceTime to match.

[Joseph Tooby-Smith]

Ok, this makes sense, and you likely have a better understanding of what will work here than I do. I personally am happy either way :).

[ZhiKai Pong]

Asking about the space refactor PhysLean#819 here:

Obviously I'll have to look through it a bit more to understand what has actually changed, but would it be possible to outline the main conceptual changes?

from what I understand this is a consequence of #27270 (I don't really know how that works either), but what I'm really interested in is the Space 1 in HarmonicOscillator has been replaced by EuclideanSpace ℝ (Fin 1). I liked how the former implementation actually links to spatial coordinates, so is this a compromise that's necessary and do you mind explaining what works and what doesn't anymore?

[Joseph Tooby-Smith]

The main reason for having Space as a structure is that it prevents casting fromEuclideanSpace ℝ (Fin 1), and allows us to be more flexible with how we work with it. This change is a consequence of #27270, in as much as that this PR makes EuclideanSpace ℝ (Fin 1) more difficult to work with, and the advantages of having Space as just an abbreviation of EuclideanSpace ℝ (Fin d) (to me) no longer made sense. In most places within the project, making Space a structure actually shortens proofs.

Concerning the change to the HarmonicOscillator. I changed from Space 1 to EuclideanSpace ℝ (Fin 1), because this was the easiest thing to do to get something which would build. The main problem was that the derivative (i.e. velocity) of a function Time -> Space 1 is another function Time -> Space 1 not Time -> EuclideanSpace ℝ (Fin 1), as one would hope. This ended up breaking a lot of things, which could be fixed but would require careful refactoring.

From the physics point of view, one can justify this change as follows (although I'm not advocating for this strongly): In PhysLean Space d is designed to be (what I would call) a worldvolume, that is it is the space on which fields, or trajectories, etc are defined. For example, in classical mechanics the worldvolume is Time, whilst in quantum field theory it is SpaceTime d. In physics examples called "non-linear sigma models" the worldvolume is any manifold M.

In Space 1's old use within the HarmonicOscillator file it was not acting as a worldvolume but as a target space (or phase space) for the the trajectory (it appeared on the right side of the map Time -> Space 1, not on the left side). Treating Space 1 as a worldvolume is a physically different quantity to it acting as a target space. Thus it's use in HarmonicOscillator is/was slightly erroneous in the first place. (To make this point further, if we had more then one particle, or the particle was restricted to a circle, the target space would not be Space 1, but something else).

[ZhiKai Pong]

so for the vector fields with Space -> EuclideanSpace ℝ (Fin 3) those are still correct, but it should never be the codomain of functions? (should I internalize it as the target space is a representation of the "real" Space but not actually the Space?) I have never thought about it this way before but I think it makes sense, thanks!

[Joseph Tooby-Smith]

Yep, vector fields should be Space -> EuclideanSpace ℝ (Fin 3).

(should I internalize it as the target space is a representation of the "real" Space but not actually the Space?)

I think so - although I agree this is a bit tricky to get ones head around. The Space 1 in the HarmonicOscillator is really the configuration space (I said phase space above, but think configuration space is more correct), a given configuration then physically corresponds to the particle been at a specific point in real space. (or something along those lines).