Upgrade `fderiv` to `AddTorsor`

Stream: mathlib4

[Alex Meiburg]

Currently fderiv has the type signature

def fderiv (𝕜 : Type u_4) [NontriviallyNormedField 𝕜] {E : Type u_5} [AddCommGroup E]
[Module 𝕜 E] [TopologicalSpace E]

{F : Type u_6} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F]
(f : E → F) (x : E) : E →L[𝕜] F

but I contend it could work just as well with the signature

def fderiv (𝕜 : Type u_4) [NontriviallyNormedField 𝕜] {E : Type u_5} [AddCommGroup E]
[Module 𝕜 E] [TopologicalSpace E]
{P : Type u_6} [AddTorsor E P]
{F : Type u_7} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F]
(f : P → F) (x : P) : E →L[𝕜] F

That is: the domain of the function only needs to be an AddTorsor. For the special case where E = P, the instance addGroupIsAddTorsor makes everything work as before. The basic fact is that the domain doesn't need to be a group E itself, it just needs the action of the group E.

The same generalization works up/down the hierarchy from HasFDerivAtFilter down to deriv and ContDiff.

Of course in the end all derivatives could be ultimately first defined with regards to some manifold structure or something similar, which I think many people would agree is undesirable in adding too much complexity. But this should give a defeq definition of derivative to what is currently there, while capturing an important larger case.

So, I would be interested to try to make this change in mathlib. But since I recognize it might end up being unpopular or unwelcome of a refactor, I wanted to ask here first.

[Alex Meiburg]

This was prompted by a conversation at #PhysLean > Vector calculus ... flat spacetime is naturally viewed as a torsor, one should be able to take derivatives on it without any notion a manifold being necessary. Currently this isn't possible with the notions of derivative in mathlib

[Sébastien Gouëzel]

In theory you're correct that affine spaces are the right setting for derivatives. In practice I'm afraid this refactor would be a nightmare. For the physics application, the right setting is clearly manifolds, as you want to be able to do physics on any spacetime, not only flat ones!

[Alex Meiburg]

Of course, and we'd also like to be able to do physics on a manifold with boundaries, in any number of dimensions, and accordingly the signature of the metric has to change too... :)

But given that most physics is done in flat spacetime, and that Riemannian manifolds don't even exist in Mathlib yet, I think it's a reasonable stepping stone.

[Alex Meiburg]

Of course it's possible that the refactor is a nightmare, but I'm cautiously optimistic: I think the change could be made and most "downstream" users of the definition would be totally oblivious.

It also doesn't have to be everything at once, for instance just HasFDerivAtFilter could be upgraded first, I estimate this would mean maybe ten theorems touched total, tops. And then HasFDerivWithin can come after, and so on.

[Michael Rothgang]

If your medium-term goal is to speak about spacetime on Riemannian manifolds - how bad is waiting for that? I'm not sure to what extent "boiling the ocean" in mathlib is justified for a purely temporary change.

[Michael Rothgang]

FWIW, I'll be visiting Patrick Massot in June/July, and one very possible project idea is "formalise Riemannian manifolds". So you may not have to wait very long.

[Alex Meiburg]

"Boiling the ocean" feels a little harsh...! Is it that you think this would be harmful to Mathlib? Or a lot of "wasted" work?

[Alex Meiburg]

(Very happy to hear the second half, though! :) )

[Michael Rothgang]

Oh, I'm sorry if this came across as harsh! I certainly did not mean to say that connotation.

[Michael Rothgang]

Just reading this thread, it sounds like "generalise everything to AddTorsor" could be a substantial refactoring. I'm worried about that making fderiv harder to work with (differential geometry is already too cumbersome - for other reasons; I'd like that to get easier not harder :-)). It's not clear to me why we'd like to make this change in the long run: all motivation so far sounds like formalising Riemannian manifolds soon and switching to those would be a preferred outcome.

(edit: so, to clarify: I mostly worry about 'wasted work' - and wonder about 'makes things harder')

[Sébastien Gouëzel]

To do physics, can't you assume you are in a vector space? I have the impression that in my undergraduate studies every physics I did was in a vector space, and later in my studies everything was in a manifold, and there was no intermediate "affine space" step.

[Michael Rothgang]

I don't have a very qualified opinion: feel free to tell me a different position is more convincing :-)

[Aaron Liu]

I like affine spaces, I wish people would use them more

[Sébastien Gouëzel]

A half-baked refactor, where we change only the first definitions and then give up because it's too hard, would be really bad, so I don't think we could start incorporating any change along this line into mathlib before there is a branch showing that this can be done up to the end. And I am afraid that this refactor would be extremely painful, for a gain which is not really proportionate to the pain, so I'm not convinced this is a good idea, to be honest.

[Michael Rothgang]

To say something more friendly: the manifold and calculus libraries in mathlib can use lots of helping hands. I'm happy to collect ideas/missing pieces what would make your life easier. I'd be very happy to review PRs making progress - there's only so much time for everything.
I certainly have some pieces (towards submanifolds, for example), where help is welcome and doesn't require much context. So if you want to help, there are definitely useful ways.

[Yury G. Kudryashov]

Please wait with this reactor for a few weeks. We're moving from normed spaces to topological vector spaces, and I don't think that we should do both at the same time.

[Yaël Dillies]

I think your message contains a topo, Yury

[Yury G. Kudryashov]

I was toping on the phyne

[Aaron Liu]

Yury G. Kudryashov said:

Please wait with this reactor for a few weeks.

Typing from the phone rarely gives typoless results

[Alex Meiburg]

HoTT (homophone type theory) when?

In seriousness: alright, thanks for the warning, if there's a change soon that would break any attempts to do this refactor I certainly won't try right now.

Regarding "only a few definitions": alright, that makes sense that you would need the full stack of definitions changed. I'll restrict myself to considering only that, then.

"Why not vector spaces" / "Why not manifolds": Physics curricula almost never use affine spaces, true. They're logically equivalent to vector spaces by picking an origin, and this lets you immediately do coordinate geometry, and it saves you having to explain to your students what this not-a-vector-space is and why they should care. In the same way, general relativity can be done entirely in a given coordinate frame, and for some domains (like LIGO simulations of BH mergers) this is the norm. But for students learning GR it's generally agreed that the "type safe" description with manifolds is better pedagogy, and we generally expect students to have the mathematical maturity by that point to handle talking about a manifold without an explicit coordinate system.

But for the 95% of physics that's done in flat spacetime, affine spaces really are the "morally correct" formalization, even if they're not used in education. As one other example: "voltage" is something that is treated as a real number for most physics education, but only by the time that you're studying abelian QFT does it become a 1D torsor (and this is now quite necessary to get a sensible understanding on QED).

[Alex Meiburg]

If it's going to be a big refactor, well, I guess I'm willing to take that risk as a stab (and if it turns out to be so big and messy that it's never going to be reviewed, ok). I guess that risk doesn't bother to me too much, I see a material benefit to it

But if the concern is that it will make differential geometry in Mathlib much harder down the line, I certainly don't want to cause that!

[Patrick Massot]

I very much agree that affine spaces are the natural home of elementary calculus. It makes me very sad that it's not done properly in mathlib. But of course I also agree that half fixing this could make things much worse. So I would very much encourage Alex to try, but knowing it has to be a huge refactor and it may fail.

[Yury G. Kudryashov]

BTW, if you want to speed up the migration to TVS (and opening doors for another refactor), you can review #23756

[Yury G. Kudryashov]

#24226 and #24225 are small dependencies for the upcoming refactor of tangentConeAt, first adding API in #24227 (WIP), then generalization to TVS.