Space vs EuclideanSpace

Stream: PhysLean

[Yoh Tanimoto]

I'm wondering what Euclidean/Minkowski spaces should look like in Lean and I gave a look to your repo. I noticed that you redefine Space, instead of using EuclideanSpace. Is there a particular reason to do this way?
Perhaps it would make sense to duplicate some code for Minkowski space, as one would not want the Euclidean inner product.

[ZhiKai Pong]

this is implemented in PhysLean#819

Quoting @Joseph Tooby-Smith here:

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.

He can probably go through the implementation considerations and implications in more detail.

[Joseph Tooby-Smith]

Will give a more detailed response tomorrow, but just to add for now that SpaceTime is Minkowski space. It carries a instance of the type class Tensorial which allows one to use index notation

[Yoh Tanimoto]

Thanks @ZhiKai Pong for the pointer. I see, you want to avoid abbrev.

If that is the point, perhaps one can use type synonym? In this way you only need re-declare instances and not reprove theorems.

import Mathlib

open Nat Real

def MyES (d : ℕ) := EuclideanSpace ℝ (Fin d)

noncomputable instance (d : ℕ) : AddCommGroup (MyES d) :=
  inferInstanceAs <| AddCommGroup (EuclideanSpace ℝ (Fin d))

noncomputable instance (d : ℕ) : Module ℝ (MyES d) :=
  inferInstanceAs <| Module ℝ (EuclideanSpace ℝ (Fin d))

noncomputable def MyES.toMyES  (d : ℕ): EuclideanSpace ℝ (Fin d) ≃ₗ[ℝ] MyES d :=
  LinearEquiv.refl ℝ _

noncomputable instance (d : ℕ) : FunLike (MyES d) (Fin d) ℝ where
  coe f := ((MyES.toMyES d).symm f : (Fin d) → ℝ)
  coe_injective' := by
    intro _ _ h
    simpa using (WithLp.ofLp_injective 2 h)

variable (d : ℕ) (x y : MyES d) (j : Fin d) (z : EuclideanSpace ℝ (Fin d))

#check x j
#check z j

example (i : Fin d) : (x + y) i = x i + y i := by rfl

[Yoh Tanimoto]

(apparently you are doing something similar with Lorentz.Vector)

[Joseph Tooby-Smith]

Basically to reiterate some of my points about, one could do:

def MyES (d : ℕ) := EuclideanSpace ℝ (Fin d)`

And this is initially how we had it in PhysLean. There were a number of reasons for the change to a structure:

1. Changing to a structure prevents casting from EuclideanSpace ℝ (Fin d) to Space and vice-versa. Practically this prevents you from treating e.g. an electric field as a point in space, which would physically make no sense. So it acts as a type-check guard against incorrect statements. This is an argument against def as well as abbrev.
2. Defining a structure lets you define exactly what you want for Space in terms of instances. I believedef does this as well.
3. For EuclideanSpace ℝ (Fin d) in particular, the need to use WithLp.ofLp and WithLp.toLp ended up getting too much, and actually making proofs longer then just defining a structure.

More generally, I personally have found that defining a new structure is the way to go, and a lot of the times I haven't I have regretted it. In particular, I personally think we should be making SpaceTime a structure.

[Eric Wieser]

Joseph Tooby-Smith said:

2. Defining a structure lets you define exactly what you want for Space in terms of instances. I believedef does this as well.

Are there any instances you want that don't coincide with the ones on EuclideanSpace?

[Eric Wieser]

Joseph Tooby-Smith said:

3. For EuclideanSpace ℝ (Fin d) in particular, the need to use WithLp.ofLp and WithLp.toLp ended up getting too much, and actually making proofs longer then just defining a structure.

All you've done here is replace ofLp with Space.val and toLp with Space.mk though, right?

[Eric Wieser]

Practically this prevents you from treating e.g. an electric field as a point in space

Could you elaborate on this? Wouldn't an electric field have type EuclideanSpace ℝ (Fin d) -> ℝ?

[Joseph Tooby-Smith]

Eric Wieser said:

Are there any instances you want that don't coincide with the ones on EuclideanSpace?

Indeed not, although one could imagine Space as an AddTorsor not a Module, although we haven't gone down this route yet. However, there is also the physical context that you want to apply to those instances through documentation, for example that the choice of a metric is akin to the choice of units. This (to me) is equally important as the actual definitions themselves.

All you've done here is replace ofLp with Space.val and toLp with Space.mkthough, right?

There were some cases where the simp only [...] got reduced as well I think.

Could you elaborate on this? Wouldn't an electric field have type EuclideanSpace ℝ (Fin d) -> ℝ?

An electric field should be Space d -> EuclideanSpace ℝ (Fin d) (or in maths words, a section of the trivial vector-bundle with base Space d and fiber EuclideanSpace ℝ (Fin d)). But in any, case there are many things in physics which take the form of EuclideanSpace ℝ (Fin d), and from the point of view of physics you should not be able to cast between them.

[Eric Wieser]

Joseph Tooby-Smith said:

for example that the choice of a metric is akin to the choice of units.

But Space is explicitly endowed with the Euclidean metric, isn't it?

[Eric Wieser]

Joseph Tooby-Smith said:

An electric field should be Space d -> EuclideanSpace ℝ (Fin d)

Whoops, I of course was thinking of the potential

[Eric Wieser]

Joseph Tooby-Smith said:

although one could imagine Space as an AddTorsor not a Module, although we haven't gone down this route yet

This seems like the most compelling argument to me; you could imagine a WithoutOrigin M type alias that just forgets the 0 of a module. I think I've discussed this with others in the past but it always seemed there was no compelling application. Probably if you go further down this route you should work with an abstract affine space in the first place.

[Eric Wieser]

(having your spaces be distinct abstract types also ensures that there is no chance that you accidentally use one where the other should be)

[Eric Wieser]

Joseph Tooby-Smith said:

But in any, case there are many things in physics which take the form of EuclideanSpace ℝ (Fin d), and from the point of view of physics you should not be able to cast between them.

This doesn't seem to help much: there are infinitely many classes of vector in physics between which casting is nonsense, and having only two distinct buckets to assign them to does not seem materially better than having one.

[Joseph Tooby-Smith]

Eric Wieser said:

But Space is explicitly endowed with the Euclidean metric, isn't it?

Space is explicitly endowed with the Euclidean metric, that is something which takes two points in Space and returns a real number. To choose a specific metric from an equivalence class corresponds to a choice in units.

But more generally, one of the aims of PhysLean is to include the physics context of a result as well as the mathematics context. The physics context is done through documentation strings and names and organization etc. In some cases it is necessary to repeat results in Mathlib so the correct physics context can be applied to it. I see the restating of the instances on Space here rather than EuclideanSpace as an instance of this.

(having your spaces be distinct abstract types also ensures that there is no chance that you accidentally use one where the other should be)

Indeed.

This doesn't seem to help much: there are infinitely many classes of vector in physics between which casting is nonsense, and having only two distinct buckets to assign them to does not seem materially better than having one.

I'm not sure where you got the 'two distinct buckets' from here. In theory (IMO - happy to be told otherwise), in PhysLean each distinct physical quantity should have a distinct definition so that the appropriate physics and mathematics context can be applied to the results.

[Eric Wieser]

Am I right in thinking that Space is morally WithDimension length (EuclideanSpace _ _)? I guess my point is that if your field vectors don't also get a dimension-specific type and continue to use EuclideanSpace, then you've only gone from "everything is just a vector" to "everything is either a spacial vector or a non-spacial vector".

[Eric Wieser]

Joseph Tooby-Smith said:

The physics context is done through documentation strings and names and organization etc. In some cases it is necessary to repeat results in Mathlib so the correct physics context can be applied to it.

The docstring currently says:

The type Space d represents d dimensional Euclidean space.

which doesn't seem to apply any guidance as to the intended semantic difference between Space and EuclideanSpace.

[Joseph Tooby-Smith]

Am I right in thinking that Space is morally WithDimension length (EuclideanSpace _ _)?

Strictly speaking Space is the type corresponding to a point in Space, with a given choice of origin, and a given choice of unit of length. Giving you the structure of a module on Space. (The Time module is probably has better documentation around this). Morally one could think of this as WithDimension length (EuclideanSpace _ _), or as the type EuclideanSpace _ _ carrying an instance of the dimension length.

I guess my point is that if your field vectors don't also get a dimension-specific type and continue to use EuclideanSpace, then you've only gone from "everything is just a vector" to "everything is either a spacial vector or a non-spacial vector".

Agreed, and I think this requires a refactor of the field vectors to give them dimension-specific types.

which doesn't seem to apply any guidance as to the intended semantic difference between Space and EuclideanSpace.

I agree, and this should be enhanced in the documentation.

[Joseph Tooby-Smith]

Maybe we could improve the documentation on Space d too:

/-- The type `Space d` is the world-volume which corresponds to
 `d` dimensional Euclidean space with a given (but arbitrary)
choice of length unit, and a given (but arbitrary) choice of zero.

The default value of `d` is `3`. Thus `Space = Space 3`-/

[Joseph Tooby-Smith]

I also think it is important that we include the reasonings behind the design choice of structure in the repo. If anyone thinks they can articulate that in a better than I have, I would love to hear it.

[Yoh Tanimoto]

I see, if you want to avoid casting, def is not good.

If you really want to consider Space as the type of space points, AddTorsor (affine space) seems the right class. And I would say there should not be the AddCommGroup instance for Space, because (as you just wrote) the choice of 0 is arbitrary. Instead there should be the action of the metric-preserving subgroup of docs#AffineEquiv and EuclideanSpace ℝ (Fin d) should be isomorphic to a subgroup of it.

[Matteo Cipollina]

Yoh Tanimoto ha scritto:

I see, if you want to avoid casting, def is not good.

If you really want to consider Space as the type of space points, AddTorsor (affine space) seems the right class.

I agree, but switching to AddTorsor without losing the ability to do calculus would require the upgrades to fderiv suggested in this discussion

[Joseph Tooby-Smith]

Yoh Tanimoto said:

I see, if you want to avoid casting, def is not good.

If you really want to consider Space as the type of space points, AddTorsor (affine space) seems the right class. And I would say there should not be the AddCommGroup instance for Space, because (as you just wrote) the choice of 0 is arbitrary. Instead there should be the action of the metric-preserving subgroup of docs#AffineEquiv and EuclideanSpace ℝ (Fin d) should be isomorphic to a subgroup of it.

Yeah, agreed. The next question is, given Matteo's comment, what is the best way to proceed? At the very least, I think the conversation here, should be linked to in the Space file and maybe add a TODO item related to eventually changing to AddTorsor.

[Joseph Tooby-Smith]

I think one of the conditions that we had on changing to an AddTorsor is that it should be understandable to the average (non-mathematical) physicist, this will require careful documentation and potentially notation.

[Yoh Tanimoto]

Indeed it would be good to expand the documentation to explain that the point 0 shouldn't play a special role, addition of space points does not make sense but only differences, and affine space is exactly the structure that forgets them.

[Joseph Tooby-Smith]

Hopefully PhysLean#959 sufficiently conveys the idea - reviews welcome.

[Yoh Tanimoto]

I added suggestions.

Next question. How should the Euclidean/Poincaré group be defined? In mathlib, there are LinearMap.GeneralLinearGroup and Matrix.GeneralLinearGroup. The former is easy to implement the action on linear spaces, while the latter is useful for calculations. Maybe there should be similar two definitions for the Euclidean/Poincaré group?

[Joseph Tooby-Smith]

Many thanks @Yoh Tanimoto .

Do you think it would be an option to define them abstractly, and rely on a MulAction instance to do the heavy-lifting? This is (kind of) the approach taken with the Lorentz group. I think this avoids the need for two definitions.

[Yoh Tanimoto]

I think there is a good reason to define both, at least for mathlib: it is one thing to define the group of isometries of a given metric space (Euclidean/Minkowski), it is another to prove that it is isomorphic to the semidirect product of the Lorentz and translation groups (and time/parity inversion). Not sure which or both should be in PhysLean

[Joseph Tooby-Smith]

I agree with this, and I think it is likely the way we should end up going.

[Joseph Tooby-Smith]

I think this is something we should add to the requirements for the Euclidean group, which are detailed in this GitHub issue PhysLean#940

[Yoh Tanimoto]

yes, and it is also important to define subgroups of the Lorentz/Poincaré/Euclidean groups, in particular the connected component of the unit element. https://physlean.com/docs/PhysLean/Relativity/LorentzGroup/Basic.html#LorentzGroup is the full Lorentz group, while often for representations we only consider the connected component.

[Joseph Tooby-Smith]

I wonder if we could make these changes to Space now by replacing the fderiv with some other form of derivative in PhysLean - I am aware that this would be a large amount of work, but I think it would be nice at least make concrete plans to do this.

[Eric Wieser]

How should the Euclidean/Poincaré group be defined? In mathlib, there are LinearMap.GeneralLinearGroup and Matrix.GeneralLinearGroup.

Isn't the group already in mathlib as docs#LinearIsometryEquiv.instGroup ?

[Yoh Tanimoto]

Eric Wieser said:

Isn't the group already in mathlib as docs#LinearIsometryEquiv.instGroup ?

This is something I would call the "full" Euclidean group, when E is EuclideanSpace ℝ (Fin d), which consists of rotations, translations but also reflections. The representation theory of the part containing rotations and translations can be studied using its Lie algebra, while reflections behave differently.

[Joseph Tooby-Smith]

Now I am confused a bit though, since if we did want to use docs#LinearIsometryEquiv.instGroup, then this relies on our Euclidean space Space d having an instance of a Module, however above we argued that it shouldn't have a structure of a Module.

[Joseph Tooby-Smith]

@Yoh Tanimoto I think an option here would be to define FullEuclideanGroup via docs#LinearIsometryEquiv.instGroup, and then EuclideanGroup via docs#Subgroup.connectedComponentOfOne

[Eric Wieser]

I assume then you'd instead want docs#AffineIsometryEquiv.instGroup

[Joseph Tooby-Smith]

Great, thanks @Eric Wieser ! In fact I don't think there is anything stopping us defining a NormedAddTorsor (EuclideanSpace ℝ (Fin d)) (Space d) instance now, and then defining the Euclidean group now through docs#AffineIsometryEquiv.instGroup.

[Joseph Tooby-Smith]

(I think it would be bad to rely on the existing NormedAddTorsor (Space d) (Space d)instance, because I think this only makes sense because Space d is a Module).

[Eric Wieser]

docs#NormedAddTorsor carries no additional data anyway, so you should always define it if you already have the metric and normed space and AddTorsor structure.

[Joseph Tooby-Smith]

Agreed - we don't have AddTorsor (EuclideanSpace ℝ (Fin d)) (Space d) yet so this will need to be defined.

[Eric Wieser]

Oh, you stopped at VAdd?

[Joseph Tooby-Smith]

Yeah - fixing it now :)

[Eric Wieser]

I'd recommend writing (and contributing to mathlib) a Function.Injective.addTorsor to match docs#Function.Injective.addAction

[Eric Wieser]

I expect you can do something similar for Function.Injective.normedAddTorsor

[Joseph Tooby-Smith]

In other words, you want to pull-back the self NormedAddTorsor instance on EuclideanSpace ℝ (Fin d) to Space d. This makes sense.

[Eric Wieser]

Yes; the pattern for those defs is that you define the data manually, then pull back the proofs

[Joseph Tooby-Smith]

I opened #35794 containing these, and added some more 'requirements' to the Space issue on PhysLean#854 related to NormedAddTorsor

[Eric Wieser]

Those look good, I've left some comments about how to make them shorter

[Joseph Tooby-Smith]

On a related topic is how we should deal with Euclidean space-time. The current plan is to define a type TimeAndSpace which is an abbreviation of Time x Space d. This is needed in a number of places, and in particular is needed for the Galilean group. The current plan is at PhysLean#939

[ZhiKai Pong]

I don't think it's easy to tell the difference between SpaceTime vs TimeAndSpace from the name, I'd prefer something like ClassicalSpaceTime or maybe there's something better

[Joseph Tooby-Smith]

I don't think classical is the right adjective here. Maybe EuclidSpaceTime, or GalileanSpaceTime (though a bit long).

[Yoh Tanimoto]

sorry that I was sloppy, yes I intended to use the affine group. As for the Poincaré group, I don't find the relevant definitions, as the Lorentz "metric" is indefinite. The closest thing seems docs#LinearMap.IsOrthogonal which applies to any bilinear form

[Eric Wieser]

Joseph Tooby-Smith said:

The current plan is to define a type TimeAndSpace which is an abbreviation of Time x Space d

This will come with the wrong norm

[Moritz Doll]

Here is a totally insane suggestion: define a type that is under the hood $\mathbb{R} \times E$ for any inner product space $E$ and bundle it with the inner product (aka bilinear form) $-dt^2 + ds$, where $ds$ is the inner product on $E$. Then you can do all of the things SR and you might be even be able to get it into mathlib. Another thing to do is just consider a type with an inner product that is non-degenerate and you can still define space-, time-, and lightlike vectors, etc (without assuming the signature is (n,1)).

[Eric Wieser]

Why not inner p q = inner p.1 q.1 - inner p.2 q.2 so that you can generalize it to two spaces?

[Eric Wieser]

(I have no strong opinion on which way the - should go)

[Moritz Doll]

in that case it doesn't matter, right :smile:

[Moritz Doll]

You can probably get away for a long time with being agnostic to the sign convention: just define positive, negative and null vectors depending on the sign of $g(v,v)$ (aka don't call them space- or timelike)

[Moritz Doll]

Oh, a nice thing about using two inner product spaces: you get the wave operator for free, just take the difference of the laplacians.

[Eric Wieser]

Isn't the wave operator just the laplacian anyway?

[Moritz Doll]

yes, but docs#Laplacian.laplacian is only defined for an inner product space

[Moritz Doll]

docs#InnerProductSpace.instLaplacian for the definition of the Laplacian on functions

[Eric Wieser]

Is a minkowski space not a docs#InnerProductSpace ? As far as I can tell all the axioms hold.

[Eric Wieser]

(I realize it's not an inner product space in the mathematical sense)

[Eric Wieser]

My claim is that changing InnerProductSpace.instLaplacian to be for SeminormedAddCommGroup would suffice

[Yoh Tanimoto]

Norm is nonneg but Minkowski space metric (Lorentz metric) is indefinite

[Eric Wieser]

Oh of course, so I guess "Is minkowski space an InnerProductSpace" is as a question a type error.

[Moritz Doll]

Yeah, because the definition of the Laplacian depends on choosing an orthonormal basis, it is not possible to use that definition for indefinite bilinear forms

[Joseph Tooby-Smith]

Joseph Tooby-Smith said:

I opened #35794 containing these, and added some more 'requirements' to the Space issue on PhysLean#854 related to NormedAddTorsor

Many thanks for your fast review of this @Eric Wieser.