Alessandro Nanto

Stream: new members

[Alessandro Nanto]

Hello everyone, my name is Alessandro Nanto and I'm a PhD student in mathematics at the University of Greifswald. I first heard of Lean in a talk of Kevin Buzzer at the University of Bonn and recently I decided to learn it. For now, I'm learning the basics (any suggestion for introductory material would be much appreciated), then I plan on trying to formalize the notion of Lagrangian field theory as presented here.

[Etienne Marion]

Hi and welcome here! I don't know how you started learning, but there are many lean games which allow to start comfortably here. If you want some books, there is #mil which is mainly about how to do "concrete" maths in lean, and #tpil which is concerned with the type theory and how it is used to prove theorems. They both provide many exercises along the way and are intended to be read while coding the examples presented yourself, which allows you to get comfortable with the syntax and practical coding as well. Have fun!

[Kevin Buzzard]

Starting with manifold theory would be a real baptism of fire :-) Do we even have fibre bundles yet?

[Alessandro Nanto]

Etienne Marion said:

Hi and welcome here! I don't know how you started learning, but there are many lean games which allow to start comfortably here. If you want some books, there is #mil which is mainly about how to do "concrete" maths in lean, and #tpil which is concerned with the type theory and how it is used to prove theorems. They both provide many exercises along the way and are intended to be read while coding the examples presented yourself, which allows you to get comfortable with the syntax and practical coding as well. Have fun!

Thank you very much for the suggestions. For now, I only tried the "Natural Number Game" (not completed yet). I'll have a look at MIL :-)

[Alessandro Nanto]

Kevin Buzzard said:

Starting with manifold theory would be a real baptism of fire :-) Do we even have fibre bundles yet?

Seems fiber bundles have only been defined for topological spaces. I'll probably take some time to dig and see what has been done so far.

[Michael Rothgang]

Some related work, so you don't have to do re-do what others are doing/can join them if you want & when you're ready:

• @Ben Eltschig has been working on formalising diffeological spaces (part of that work is already in mathlib, other pieces are under review, and as I understand it there are more).
• @Dominic Steinitz is working on principal fibre bundles here

[Alessandro Nanto]

Michael Rothgang said:

Some related work, so you don't have to do re-do what others are doing/can join them if you want & when you're ready:

• Ben Eltschig has been working on formalising diffeological spaces (part of that work is already in mathlib, other pieces are under review, and as I understand it there are more).
• Dominic Steinitz is working on principal fibre bundles here

Thanks for letting me know :-) I've actually already looked at both @Ben Eltschig's and @Dominic Steinitz's work (though not thoroughly). I'm also looking forward to formalizing diffeological spaces, following the article I've cited above. I think the notion of tangent diffeological space is where Ben Eltschig's work diverges from the notes I'm using.

As per principal fiber bundles. I'll definitely have a closer look, but it seems the definition is for topological bundles, where I need the notion of smooth fiber bundles to define the jet bundles. Do you know if someone is working on smooth fiber bundles, maybe?

[Dominic Steinitz]

I will need smooth fibre bundles. As far as I can tell there are only smooth vector bundles but no smooth fibre bundles. I don't know why that is. I do not know of anyone working on smooth fibre bundles.

I only had a quick look at your reference but I'd agree with @Kevin Buzzard that it will be a baptism of fire.

[Alessandro Nanto]

Dominic Steinitz said:

I will need smooth fibre bundles. As far as I can tell there are only smooth vector bundles but no smooth fibre bundles. I don't know why that is. I do not know of anyone working on smooth fibre bundles.

I noticed that too. I guess people were eager to define the tangent space as a vector bundle. I can't read the code well enough to see if the definition can be used to give the notion of smooth fiber bundle, by removing the fiberwise vector space structure and fiberwise linearity of trivializations.

I imagined it would be a demanding task, but now I'm realizing more and more how much stuff there is to do.

[Ben Eltschig]

Michael Rothgang said:

• Ben Eltschig has been working on formalising diffeological spaces (part of that work is already in mathlib, other pieces are under review, and as I understand it there are more).

I actually still haven't PR'd anything directly related to diffeological spaces yet - my main obstacle is that I'd like the D-topology of diffeological quotients to be defeq to the quotient topology (i.e. this todo), but doing that requires restructuring both several files and one very messy proof, which is why I have procrastinated doing it until now. I suppose seeing the interest in diffeological spaces here is a good motivation to get that done as soon as possible though :)

[Alessandro Nanto]

Ben Eltschig said:

my main obstacle is that I'd like the D-topology of diffeological quotients to be defeq to the quotient topology (i.e. this todo), but doing that requires restructuring both several files and one very messy proof, which is why I have procrastinated doing it until now.

What proof are you formalizing? Because I think you can argue using that taking the D-topology is a left adjoint functor from Diffeological to Topological spaces, is that messy?

I'd love to see what has been done so far for diffeological spaces, once I'm more familiar with the language of Lean.

[Ben Eltschig]

Translating between concrete and categorical statements tends to be a little cumbersome in lean, so it's usually good keep category theory out of files that don't need it (or at least that's the paradigm I've been following). For the proof in question, I previously used a lemma directly characterising the plots of the coinduced diffeology, but that ended up being quite annoying to prove. I've now switched to a simpler proof which uses the continuous diffeology directly.

[Ben Eltschig]

I guess part of the problem was that I previously hadn't realised that the D-topology and continuous diffeology form a Galois connection between the topologies and diffeologies on any given type, as a sort of local version of the adjunction you mentioned. That still doesn't make the proof immediate as far as I can see, but definitely did help simplify it.

[Alessandro Nanto]

Ben Eltschig said:

Translating between concrete and categorical statements tends to be a little cumbersome in lean, so it's usually good keep category theory out of files that don't need it (or at least that's the paradigm I've been following). For the proof in question, I previously used a lemma directly characterising the plots of the coinduced diffeology, but that ended up being quite annoying to prove. I've now switched to a simpler proof which uses the continuous diffeology directly.

Really? Didn't expect that it would be cumbersome. My problem is that in the notes I'm following, most of the theory of diffeological spaces is set up using category theory (for example, tangent bundles are left Kan extensions, so are diffeological differential forms).

[Ben Eltschig]

The problem is that in lean, there is a difference between types equipped with structure (topologies, diffeologies, group structures etc.) and objects of the corresponding categories. For example, a diffeological space is a type X : Type* with a diffeology d : DiffeologicalSpace X registered as an instance - so even though X itself does not contain the diffeology as data, when you have a map f : X → X and write DSmooth f lean finds the instance and knows which diffeology you are talking about. This is handy when talking about spaces like ℝ that carry many structures at once, because it prevents you from having differentiate between "ℝ the group", "ℝ the topological space", "ℝ the diffeological space" and so on.
In contrast to that, an object in a category needs to contain all the data belonging to that object - so for example an object in the category DiffSp of diffeological spaces is not simply a type, but instead a structure having both a type and a diffeology on it as fields. You can convert between the two by by coercing X' : DiffSp to a type or using DiffSp.of X to construct an object of DiffSp from a type with a diffeology on it, but those coercions do need to happen and tend to stick around, which is what at least in my experience makes mixing categorical and non-categorical arguments a little cumbersome.

[Ben Eltschig]

This is not to say that categorical arguments are completely unworkable of course - if you look at the files DiffSp.lean, Sites.lean and SmoothSp.lean, you'll see that I already have I think quite a bit about these categories in place. It's just in my experience easier to keep that out of the other files, and if you look at mathlib you'll see that it works quite similarly there, with files about the category of topological spaces that import files about point-set topology but not the other way around.

[Alessandro Nanto]

Ben Eltschig said:

The problem is that in lean, there is a difference between types equipped with structure (topologies, diffeologies, group structures etc.) and objects of the corresponding categories.

I see, thanks for telling me this distinction. If I understand correctly (I'm still not too familiar with how this works), the first approach is similar to the idea of a diffeological space as a set, or some "ground type", with extra data (the diffeology) attached to it. Then different extra structures can be attached to the same X and recalled by Lean when needed, while with the second approach, X is always a diffeological space. Did I get this correctly?

For now I'm more inclined towards viewing a diffeological space as its own thing, rather than a type equipped with structure, but this might change when I start to try and formalize stuff.

[Ben Eltschig]

The ability to view diffeological spaces as sets/types with extra structure is really one of their main selling points as far as I'm aware. That doesn't mean you can't consider them purely category-theoretically of course - they're concrete sheaves on a certain site - but if you don't need concreteness you might also as well consider general sheaves, which form an even nicer category. It would be interesting to see why the notes you have linked use diffeological spaces instead.

[Alessandro Nanto]

Well, in the notes it says that

[A certain theorem] enables us to go back and forth between two equivalent descriptions of diffeological spaces that each has its advantages. The geometric definition in terms of plots is best suited for explicit computations, the descriptions of examples, and the relation to the traditional methods of analysis and differential geometry. The categorical definition in terms of concrete sheaves is best suited for abstract structural considerations, the efficient understanding of universal properties, and the relation to more recent developments such as in homotopy theory or higher geometric structures.

So diffeological spaces are simply closer to the usual structures in differential geometry.

[Dominic Steinitz]

Alessandro Nanto said:

Michael Rothgang said:

Some related work, so you don't have to do re-do what others are doing/can join them if you want & when you're ready:

• Ben Eltschig has been working on formalising diffeological spaces (part of that work is already in mathlib, other pieces are under review, and as I understand it there are more).
• Dominic Steinitz is working on principal fibre bundles here

Thanks for letting me know :-) I've actually already looked at both Ben Eltschig's and Dominic Steinitz's work (though not thoroughly). I'm also looking forward to formalizing diffeological spaces, following the article I've cited above. I think the notion of tangent diffeological space is where Ben Eltschig's work diverges from the notes I'm using.

As per principal fiber bundles. I'll definitely have a closer look, but it seems the definition is for topological bundles, where I need the notion of smooth fiber bundles to define the jet bundles. Do you know if someone is working on smooth fiber bundles, maybe?

I noticed that a jet bundle is defined here without mentioning smooth fiber bundles.

I am looking at defining smooth fiber bundles ATM as I want e.g. $U(1)$ as a fiber.