Diffeology

Stream: Is there code for X?

[Joseph Tooby-Smith]

Is there anything related to Diffeology currently in MathLib? If not, would there be interest in a project to formalise aspects of it?

My motivation for asking is that diffeology appears in some aspects of physics, and in general is more well-behaved than the theory of manifolds (e.g. diffeological spaces form a Cartesian closed category unlike manifolds).

[Kim Morrison]

Pretty sure we don't have anything. I guess your "e.g." is a reasonable first target. But where would it go in Mathlib after that?

[Joseph Tooby-Smith]

Hi @Kim Morrison , if I have interpreted your question correctly (sorry if I haven't), then other targets would be:

1. Showing the relations between manifolds and diffeological spaces. Summarised by saying that there is a fully-faithful functor from the category of manifolds to the category of diffeological spaces.
2. Showing that the mapping space between manifolds has the structure of a diffeolocial space (follows from 1 and my "e.g.").
3. Showing that diffeolocial spaces are precisely the concrete objects of the topos of sheafs on the site of cartesian spaces (this is where one connection to physics comes in through topological field theories).
4. The definition of subductions and inductions between diffeoloical spaces, and their relation to surjective submersion and injective immersions of manifolds.

That said, maybe I am over-estimating the usefulness of this for the Mathematicians.

[Kim Morrison]

All sounds fun, and certainly it's "in scope" for mathlib. I think it's always good when considering a slightly-off-the-beaten-track topic whether there would be other people around (or that you could recruit!) who would also work on it, or at least be able to give useful reviews. (The existing Mathlib maintainer/reviewer team doesn't need to contain someone who knows about this stuff: but we need reviews from someone!)

[Joseph Tooby-Smith]

Makes sense :). I'll wait and see if anyone pops up here expressing an interest.

[Adam Topaz]

I’m not an expert but I certainly find this stuff interesting!

[Patrick Massot]

I think it would be extremely difficult to find reviewer for this. Developing it in an independent project would probably be a lot less frustrating.

[Yaël Dillies]

There was someone interested in diffeology on Xena. Was it you?

[Yaël Dillies]

FWIW I would be happy to review diffeology material but I am no easy reviewer to satisfy :smiling_devil:

[Joseph Tooby-Smith]

@Yaël Dillies No that wasn't me. Seems like the best plan, is to follow @Patrick Massot's advice, and start it in an independent project. Then it could be slowly move it to MathLib, when and if the time is right.

[Michael Rothgang]

Was it @Ben Eltschig? (Is a diffeology the same as a diffeological space? I never thought about this at all.)

[Ben Eltschig]

Yep, I'm currently working on some code related to diffeology too. So far it's sitting at https://github.com/peabrainiac/lean-orbifolds

[Johan Commelin]

@Tomas Skrivan might also be interested

[Ben Eltschig]

My main goal with this is to be eventually able to state the definition of orbifolds as special diffeological spaces; after that I would probably shift to working on Lie groupoids to try and get that definition of orbifolds formalised too. If you want to further develop diffeology I wouldn't mind adding you to that repo, though if you want you can of course also start your own

[Kim Morrison]

(Also, it sounds from this conversation that if/when there's material you'd like to send to mathlib, there are enough reviewers around! It's super helpful when people review other PRs in their field, making it much easier for the official reviewers/maintainers to do a quick check and then merge.)

[Tomas Skrivan]

Yes, I would be very much interested in having a formalization of diffeology. I think it is the right abstraction for formalizing automatic differentiation. One thing I'm not sure about is which notion of tangent space should be used as there are few different definitions.

Also I would like to have formalization of convenient vector spaces which are effectively a flat version of diffeology.

[Joseph Tooby-Smith]

@Ben Eltschig Nice! What you've got so far looks like a great start :). I would like to develop aspects of it further. If @Tomas Skrivan is interested we could create a repo dedicated to diffeology with the three of us, and then move it over to MathLib when ready.

[Joseph Tooby-Smith]

(or also just happy to add to your existing repo @Ben Eltschig)

[Ben Eltschig]

I imagine splitting the code for diffeologies and orbifolds (which I don't have yet, but hope to get to soon) up into two different repos is going to make it quite inconvenient to work on the latter, so I'd be more in favor of keeping both in the same repo. I am open to renaming or moving the repository though if the amount of things on diffeology in it becomes large enough for that to make sense :smile:

[Ben Eltschig]

Fyi, the current situation is that I have a definition of diffeologies and the D-topology in terms of maps $\R^n\to X$, but haven't yet shown that those agree with the usual definitions in terms of maps $U\to X$ for $U\subseteq\R^n$ open. That's what I'm currently working towards

[Ben Eltschig]

The D-topology has also been giving me trouble because it is in many cases different from the usual topology on a space, so I haven't been able to register it as an instance. Since mathlib doesn't really support non-standard topologies on a space, this means that it's currently a bit hard to work with

[Ben Eltschig]

I think things should be ready though to do some more abstract things like defining the category of diffeological spaces or the space of all smooth maps and the diffeology on it - so if that's something you want to go for, feel free to do so

[Joseph Tooby-Smith]

@Ben Eltschig All sounds good - thanks for adding me to the repository :) . When I get round to it, I will create my own branch and see what I can add - but yes most likely focusing on the abstract nonsense side of things (at least for now).

[Kim Morrison]

Ben Eltschig said:

Since mathlib doesn't really support non-standard topologies on a space, this means that it's currently a bit hard to work with

Presumably you should just define Diffeological X := X, and then put the D-topology on Diffeological X instead. Type synonyms are the usual approach here.

[Ben Eltschig]

I probably will also put the D-topology on a type synonym eventually, yes. I'm not sure if that completely solves the problem though - I also want to talk about nice spaces like $\R^n$ as diffeological spaces after all, preferably without passing to a type synonym each time. My hope is that it will be possible to set things up in such a way that theorems involving the D-topology apply to both, or at least can be easily set up to have a variant for spaces on which the D-topology and the usual topology agree.

[Sébastien Gouëzel]

You can have a typeclass HasDTopology, saying that the topology is equal to the D-topology (whatever the D-topology is). In lemmas, don't work with the type synonym, just with a generic type alpha with assumptions [TopologicalSpace α] [HasDTopology α]. And register instances that \R^n or nice spaces satisfy HasDTopology, to make sure that your lemmas apply directly to these spaces. And define your type synonym in general, put the D-topology on it, and register the instance HasDTopology for the type synonym. In this way, everything should work smoothly.

[Ben Eltschig]

yep, that's the approach I'm currently going for :smile:

[Ben Eltschig]

there's a few small annoyances still, like that I can't register HasDTopology on open subsets because openness is not information that's available to typeclass inference - but ultimately it's the most promising approach I've seen so far

[Yaël Dillies]

docs#Fact is useful here

[Sébastien Gouëzel]

Instead of using a subset and the fact that it's open, you can use U : Opens X, which is open by definition, so typeclass inference can be used here.

[Tomas Skrivan]

Over the past two weeks I got interested in diffeology for formalizing automatic differentiation. The problem is that types like Option X, Array X or Sum X Y are not vector spaces and Array X can't even be turned into a manifold. Therefore there is a need for something as general as diffeology.

I have managed to write definition of diffeology, differentiable maps, tangent space, derivative and prove chain rule. For example I proved that Sum.elim f g x is differentiable. With arrays I still have few sorry but I have differentiability of get?, setD and append.

---

My main definition of Diffelogy is

Diffeology

class Diffeology (X : Type v) where
  Plot : ℕ → Type v
  plotEval {n} : Plot n → ℝ^n → X
  plot_ext (p q : Plot n) : plotEval p = plotEval q → p = q
  plotComp {n m} (p : Plot n) {f : ℝ^m → ℝ^n} (hf : ContDiff ℝ ⊤ f) : Plot m
  plotComp_eval {n m} (p : Plot n) {f : ℝ^m → ℝ^n} (hf : ContDiff ℝ ⊤ f) (u : ℝ^m) :
    plotEval (plotComp p hf) u = plotEval p (f u)
  constPlot (n : ℕ) (x : X) : Plot n
  constPlot_eval (n x u) : plotEval (constPlot n x) u = x

Few notes on this definition

• Most importantly it is missing the locality axiom. So far I didn't need it so I didn't bother with it.
• Plots are maps from the whole ℝⁿ, again I didn't need them to be maps from open subsets of ℝⁿ so I didn't bother.
• I started with plots as a set i.e. Set (ℝⁿ → X). I found this to be very difficult to work with. So Diffeology has to provide a type Plot X n, evaluation map plotEval : Plot X n → (ℝⁿ → X) and proof that this map is injective plot_ext.

---

Definition of smooth map DSmooth

DSmooth

structure DSmooth (f : X → Y) : Prop where
  ex_map_plot : ∃ g : (n : ℕ) → Plot X n → Plot Y n,
    ∀ n u p, g n p u = f (p u)

This is completely standard, smooth map is a map that maps plots to plots. It is formulated using ∃ so DSmooth lives in Prop.

---

Definition of tangent space TangentSpace

TangentSpace

class TangentSpace (X : Type v) [Diffeology X] (TX : outParam (X → Type w))
      [∀ x, AddCommGroup (TX x)] [∀ x, Module ℝ (TX x)] where

  tangentMap {n : ℕ} (p : Plot X n) (u : ℝ^n) : (x : X) × (ℝ^n →ₗ[ℝ] TX x)
  exp (x : Σ x, TX x) : Plot X 1

  tangentMap_const {n} (x : X) t : tangentMap (constPlot n x) t = ⟨x, 0⟩
  tangentMap_fst {n} (p : Plot X n) (u : ℝ^n) : (tangentMap p u).1 = p u
  exp_at_zero (xdx : Σ x, TX x) : exp xdx 0 = xdx.1
  tangentMap_exp_at_zero (xdx : Σ x, TX x) : tangentMap (exp xdx) 0 = duality xdx

As far as I'm aware there is no go to definition of tangent space, I skimmed through the paper Tangent spaces and tangent bundles for diffeological spaces and then just rolled my own definition of a tangent space that works for my purposes. (I'm not sure if it aligns with the definition from that paper)

Keys points

• There are two pieces of data: tangentMap which compute the tangent for a plot and exp which for a given tangent vector provides a curve that passes through that tangent vector.
• This definition won't work well with taking subsets and quotients of X and I'm not sure how to remedy that.

---

The normal definition of smooth map does not seem to be sufficient when working with this tangent space. Therefore I defined TSSmooth which is a map that preserves plots and tangentMap does not depend on the particular plot(which is effectively saying that the chain rule holds)

TSSmooth

structure TSSmooth (f : X → Y) extends DSmooth f : Prop where
  plot_independence {n : ℕ} {p q : Plot X n} {u : ℝ^n}
    (h : tangentMap p u = (tangentMap q u)) :
    (tangentMap (f ∘ p) u)
    =
    (tangentMap (f ∘ q) u)

---

What I would like to do next:

• Provide more theorems for all the basic types like Option, Array, Prod, Sum and figure out how to make all the proofs less painful.
• Prove that types with Diffeology form Cartesian closed category with DSmooth morphisms. Does the same hold for types with TangentSpace and TSSmooth morphisms?
• Define connection which would allow to talk about dependently typed smooth function. This seems to be necessary when we want to talk about cartesian closedness of types with TangentSpace. I have some experiments in this direction, I tried to define something like Ehresmann connection in this file but I got lost in the smoothness requirements of the lifting function.

Any feedback is welcome. Also I would be happy to guide anyone who would be interested in working on this as I should probably focus on other thing in the near future.

[Yaël Dillies]

@Ben Eltschig, how far did you get in the definitions?

[Tomas Skrivan]

I checked Ben's GitHub and he is much much further in terms of diffeology itself. But I didn't find anything on tangent spaces so I worked with a simplified definition of diffeology to see if I can proof stuff I need for automatic differentiation. I should probably redo it and build it on top of Ben's work.

[Dean Young]

@Tomas Skrivan thank you Tomas, this is something I'll be using as you develop it. P.S. take a look at the diffeology synopsis here.

[Ben Eltschig]

Tomas Skrivan said:

I checked Ben's GitHub and he is much much further in terms of diffeology itself. But I didn't find anything on tangent spaces so I worked with a simplified definition of diffeology to see if I can proof stuff I need for automatic differentiation. I should probably redo it and build it on top of Ben's work.

I indeed haven't done anything with tangent spaces yet, in part because I so far didn't need them and in part because the many different definitions left me a bit unsure about which definition to pick. The internal tangent space seems promising though, so I might give formalising that a try soon.

[Ben Eltschig]

I'm also not sure I understand your current approach to tangent spaces correctly - given a family TX : X → Type w of real vector spaces on a diffeological space, you define a tangent space structure on them as a choice of tangent map for each plot and curve for each tangent vector, satisfying some conditions? This seems very non-canonical, in that (even the choices of curves aside) there are probably many such structures for each TX, and also many different TX for which such structures can be found - for example, letting all tangent spaces be trivial works for any X. So there is a lot of data being carried around, which I assume would lead to both bad categorical properties and potentially instance diamonds.

[Ben Eltschig]

For the use cases you have in mind, is it important that you can pick a specific family of vector spaces as the tangent spaces, rather than working with uniformly defined ones? I can see that for example having the tangent spaces of a vector space V be equal to V instead of just isomorphic to it would be convenient - but if you add that as an instance, you already can't add tangent space instances for finite products anymore without causing there to be two different tangent space structures on a product V ⨯ W of vector spaces.

[Tomas Skrivan]

Ben Eltschig said:

I'm also not sure I understand your current approach to tangent spaces correctly - given a family TX : X → Type w of real vector spaces on a diffeological space, you define a tangent space structure on them as a choice of tangent map for each plot and curve for each tangent vector, satisfying some conditions? This seems very non-canonical, in that (even the choices of curves aside) there are probably many such structures for each TX, and also many different TX for which such structures can be found - for example, letting all tangent spaces be trivial works for any X. So there is a lot of data being carried around, which I assume would lead to both bad categorical properties and potentially instance diamonds.

I just wrote down the minimal definition that allowed me to to the calculus I want without worrying too much about canonicity. All the instances I added were tangent spaces for unions of manifolds where I want the tangent space be just the tangent space of the individual manifolds. I have no idea happens for quotients and subsets and my definition is probably does not work.

[Tomas Skrivan]

Ben Eltschig said:

For the use cases you have in mind, is it important that you can pick a specific family of vector spaces as the tangent spaces, rather than working with uniformly defined ones? I can see that for example having the tangent spaces of a vector space V be equal to V instead of just isomorphic to it would be convenient - but if you add that as an instance, you already can't add tangent space instances for finite products anymore without causing there to be two different tangent space structures on a product V ⨯ W of vector spaces.

This is already problem for diffeology itself, right? So not specific to a tangent spaces. I would do the same thing as you did and define analogues for yours euclideanDiffeology and ContDiffCompatible that talk about tangent spaces. This is a fundamental issue that does not really depend on a particular definition of the tangent spaces, no?

[Ben Eltschig]

Right, the diffeology instances already run into trouble like that.

[Ben Eltschig]

My hope was to keep the need for classes like ContDiffCompatible and DTopCompatible to a minimum - having to rewrite the topology from time to time using the DTopCompatible instance is already cumbersome, and I imagine it gets worse when the thing you're rewriting is types like the tangent spaces rather than just terms like topologies

[Ben Eltschig]

I did try implementing the internal tangent space from Tangent spaces and tangent bundles for diffeological spaces by the way, and it went better than I expected - it's not on github yet because I'm not yet done constructing the tangent maps, but I'm optimistic tangent spaces could be implemented for all diffeological spaces in that way without any extra instances. I don't know how workable this would be for practical computations, but it does seem like the right way to go about this mathematically at least

[Tomas Skrivan]

I would be interested in having a look at that code!

How would you state Cartesian Closedness for diffeological spaces with tangent spaces?

What is the tangent space of DSmoothMap X Y at f? It should be a subset of (x : X) → TX (f x) but also a smooth map in some sense.

[Tomas Skrivan]

(deleted)

[Ben Eltschig]

I wouldn't consider diffeological spaces with tangent spaces as a new category at all, since the internal tangent space can be defined for all diffeological spaces and without any extra data. I haven't thought about the case of mapping spaces yet, but the linked paper for example mentions that the tangent space of the diffeomorphism group of a manifold M at the identity turns out to be the set of smooth vector fields on M, so it does seem to give a reasonable result in that case at least

[Ben Eltschig]

This is the code I have so far - it's all still relatively abstract, but should be a concrete way of writing the colimit that the internal tangent spaces are defined as. I'm guessing the hardest part will be to show that in the case of vector spaces this actually gives the space itself; after that, showing that it gives the right space for manifolds shouldn't be too hard
https://github.com/peabrainiac/lean-orbifolds/blob/main/Orbifolds/Diffeology/TangentSpace.lean

[Tomas Skrivan]

I see, for my purposes I need a good type for the tangent space such that I get reasonable code to run. But I can solve this by adding a new typeclass that allows me to have a control over the precise type of the tangent space

class TangentSpace (X : Type*) [DiffeologicalSpace X] (TX : outParam (X → Type*))
  [∀ x, AddCommGroup (TX x)] [∀ x, Module ℝ (TX x)] where
  tequiv (x : X) : TX x ≃ₗ[ℝ] internalTangentSpace x

[Ben Eltschig]

Yep, that's pretty much what I was thinking too :smile:

[Tomas Skrivan]

I like this!

[Ben Eltschig]

I think the first two PRs upstreaming bits of diffeology from my repo to mathlib should be more or less ready for review now - #21969 adds very basic definitions (diffeologies, plots, smooth maps etc.) while #22724 defines the diffeology generated from a set of plots and uses it to construct a CompleteLattice-instance on DiffeologicalSpace X. I say more or less because I've hesitated on PRing this for a while now out of fear it still isn't good enough, but figured it probably won't get much better either without external feedback, so here we are :sweat_smile:

[Ben Eltschig]

Since we have multiple people interested in diffeology in this thread, maybe someone wants to leave a review? I'm relatively confident about the general API design by now, but less so about specifics like naming and which arguments of lemmas should be made explicit/implicit. Of course, if you have some opinions about the general API design too though I'm also curious about hearing those - that's probably where the really interesting conversation happens.