Jerome Hofstetter, manifold question

Stream: new members

[Jérôme Hofstetter]

Hello
I'm a physics student with a strong interest in maths and theoretical physics. I love the idea of having maths formalized to the degree the lean project does it altho it doesnt seem that useful trying to learn from it. I'm interested in the mathematical underpinning of physical theories like GR, the slew of mathematical structures, definitions and theorems that are then utilized. I wish there was a middleground between textbooks, wikipedia and lean (in terms of similar rigorousity , but sacrificing some for readability while linking to existing textbooks)

I came here as I'm looking for material that better explains theorems and definitions extending from pre manifolds just locally modeled by $\mathbb{R}^n$ to premanifolds with corners (modeled by $[0,\infty)^k \mathbb{R}^{n-k}$)
specifically how any structure with differentiation is defined, like $C^k$ and what kind of hurdles one has to carefully navigate around verses which ones are not a problem.
As I've seen that manifold with corner seems to have been implemented in lean and the people being involved with that have probably seen the hurdles i wanted to ask if 1. there is a textbook or script that they've used as a reference or 2. they have made a post or jotted down their process and the hurdles.

[Michael Rothgang]

Hi, welcome to the mathlib community! I'm always glad to hear about users interested in manifolds in Lean.

As you maybe saw already, mathlib aims for definitions to be in the greatest reasonable generality. (If you'll need a definition when formalising current research mathematics, mathlib aims to have you covered.) As a result, there is no single reference covering mathlib's definition of manifolds. The closest I know is Roig and Domingues' Differential topology (which treats real Banach manifolds with boundary and corners). I'm not sure if this will answer your question, though.

[Michael Rothgang]

There is no mathematics in lean chapter for differential geometry yet. (I may get to writing one soon; no promises.) Similarly, there is no one coherent document explaining the design of manifolds in mathlib yet (which, again, hopefully will change in the coming months). Until then, I can only refer you to some slides and a talk of mine: https://www.math.uni-bonn.de/people/rothgang/slides_LearningLeanSeminar.pdf

[Michael Rothgang]

(There might be other such introductions; I'm not aware of them. Tell me if I have overlooked one!)

[Jérôme Hofstetter]

for myself and other students i've been in the process to write up more general texts of mathematical structures that in a sense resembles projects like mathworld or nLab but then create a connection to lectures

aiming for definitions to be in the greatest reasonable generality is partially an aim, just in the scope to what is reasonable , needed for example in GR. As i want to be quite rigorous and generalizing definitions is not trivial and spotting that lean has had some development in this direction i was curious if there is some more informal text about the process that went into it as it seems that describing the definitions and theorems informally is easier than formalizing it in lean

For that I'm glad my post has been spotted by someone that has directly worked on this.

I would know how to proceed if i just stick with premanifolds locally modeled to some $\mathbb{R}^n$ while texts that I've seen seem to mention manifolds with boundaries more of an afterthought, while i assume there come significant challenges and questions popping up for me like how does $C^k$ condition work at those boundaries and corners, or the metric and so on.

I will check out Roig and Domingues' Differential topology, from a cursory glance it allows for quadrants of real banach spaces which seems like to me it extends the notion of $[0,\infty)^k \mathbb{R}^{n-k}$ and defines differentiability already in that context which could already answer my questions.
While the definition in lean (again cursory glance) instead of using a normed vectorspace directly , asks for a topological space with an embedding to a normed vectorspace

[Michael Rothgang]

I'm glad this has been helpful! About "how to define differentiability on manifolds with corners", Lean's answer is "use the model with corners (and consider extended charts)", and then it boils down to differentiability between normed spaces. See e.g. docs#contMDiffAt_iff.

[Michael Rothgang]

By modelling a manifold on Euclidean quadrants, you're implicitly using the canonical inclusion as your model with corners --- mathlib's definition merely abstracts over this, but is not mathematically different.

[Snir Broshi]

Michael Rothgang said:

(There might be other such introductions; I'm not aware of them. Tell me if I have overlooked one!)

Maybe https://www.youtube.com/watch?v=deppJ2q_5a0 is helpful?

[Michael Rothgang]

This certainly seems helpful indeed - Heather Macbeth discussing the construction of a manifold structure on the sphere. Thanks for finding this video.

[Jérôme Hofstetter]

seeing a concrete example was helpful to conceptualizing it in lean, tho I was wondering how specifically the boundaries are treated. By my understanding it just adds some bookkeeping and differentiability at the boundary just needs in that one direction to have a directional derivative

[Jérôme Hofstetter]

trying to follow the book ive noticed the resemblance to the structure I've seen in the slides, from the slide 15, $H=E^+_{\Lambda}, E=E$ and the continuous map in the book is always just the inclusion
but I'm unable to see in the book (and in lean aswell, but thisi can attribute to not being familiar with lean at all) how differentiability at the boundaries is defined unless I missed an argument or it implicitly asks for an extension to exist that is then differentiable. (the definition im familiar with is just the frechet derivative, for a function with an open subset as domain)

I can imagine just asking the function to fulfill differentiability on the interior (relative to the ambient space) but I'm not familiar if with this something fails to hold. Or asking that there exists an extension to an open cover of the domain (i assume continuous extension, agreeing on the domain, not sure if more conditions are required) that can be differentiated. And finally taking that route it is enough to have just one such extension.

[Jérôme Hofstetter]

Michael Rothgang said:

I'm glad this has been helpful! About "how to define differentiability on manifolds with corners", Lean's answer is "use the model with corners (and consider extended charts)", and then it boils down to differentiability between normed spaces. See e.g. docs#contMDiffAt_iff.

i followed the equations and docs and it seems like to end up at docs#ContDiffWithinAt
trying my best to interpret the equation it seems like differentiation is not checked by asking that the iterated frechet derivative exists, but instead asks for any point to have a taylor expansion (just the existence of a sequence of multilinear maps that then summed up appropriately, plugging in h into any argument of the multilinear maps and looking at the limit as h goes to zero equals the functions evaluation at that point.

Then the taylor expansion in some way forms an extension, just agreeing at one point. It doesnt ask of it to be unique but i assume that if the domain is open and "nice" (some conditions im not familiar with) this definition of C^k via existing taylorexpansion agrees with the definition via iterated frechet derivative?

This difference i find quite fascinating, are there some sources (in literature or more lean intern) that talk about what went into this choice of definition?
i saw the text on #iteratedFDerivWithin but it doesn't end with the conclusion to then use taylor expansion existing approach.

[Sébastien Gouëzel]

Shameless plug: https://gouezel.pages.math.cnrs.fr/webpage/articles/calculus.pdf

[Jérôme Hofstetter]

Sébastien Gouëzel said:

Shameless plug: https://gouezel.pages.math.cnrs.fr/webpage/articles/calculus.pdf

thank you for sharing this is exactly what i was looking for.
to my understanding once can define taylorexpansion quite generally, i assume even on a normed ring, so could it be used to define some kind of derivative on a normed module over normed ring or a LCTVS (just formally without expecting nice properties)?

Assume something like this as been attempted.

[Sébastien Gouëzel]

In Mathlib, derivatives are defined in topological vector spaces, with respect to nontrivially normed fields. It would probably be possible to replace the nontrivially normed field by a normed ring, but I don't know of any interesting application.

[Jérôme Hofstetter]

i would then be interested what motivated the generality of $I : H \rightarrow E$ instead of using the inclusion and a specific subset. Does it enable proofs that were not possible without this choice or just makes the definitions more elegant, having to introduce less and is in some way equivalent to just using the inclusion?

[Sébastien Gouëzel]

If you use always inclusion, even when the model is the whole space you would need to use the subtype corresponding to univ, and the inclusion is a nontrivial map from the subtype to the space. If you allow any map I like we do, then you can take H = E and I = id, which gives better definitional equalities in this case.

[Jérôme Hofstetter]

in general i assume I has to be atleast homeomorphic onto its image, are there more conditions needed (in generality) or are additional conditions required later on I to define additional constructs? Or are for example two charts being compatible in C^k sense enough but wouldnt be fulfilled unless I posesses certain conditions
essentially dividing into 3 cases,

generally intrinsic needed conditions (continuous, injective ...) , specifically extrinsic (needed properties on I such that then additional construction "makes sense" (leads to nice properties ...) and lastly implied conditions (B) when fulfilling (A) (such as B not being fulfilled would directly imply A not being fulfilled)

an example for the last case would be a group being an nonempty set as you want atleast a neutral element. But necessarily nonempty condition wouldnt be necessary. I assume this as a concrete name that I'm failing to find.

[Sébastien Gouëzel]

The practical condition we put on I are essentially that it is a homeomorphism on its image, which is a closed convex set. These conditions are convenient, and satisfied in all relevant examples.

[Jérôme Hofstetter]

to clarify the embeddinglike function I has to fulfill all :

1. its an homeomorphism to its image
2. the image of I has to be a closed convex set
   i wouldn't think that 1. implies 2.

[Sébastien Gouëzel]

Yes, 1. and 2. are independent conditions. The nice thing is, you can go and check everything for yourself in the Lean code! docs#ModelWithCorners

[Michael Rothgang]

See docs#ModelWithCorners to verify this yourself: indeed, these are two independent conditions.

[Jérôme Hofstetter]

thank you for the clarification.
I don't find lean code and docs as a beginner that much readable. It seems tho the real and complex number become exceptions to check the image to be convex while for other fields it requires I to be surjective from the start?

[Ruben Van de Velde]

Okay I find that hard to read and I've got years of experience with lean :sweat_smile:

[Jérôme Hofstetter]

im failing to find closedness condition, I probably missed it or it is a condition introduced later?

[Sébastien Gouëzel]

It's a consequence of the existence of the partial inverse. See docs#ModelWithCorners.isClosed_range

[Michael Rothgang]

Jérôme Hofstetter said:

thank you for the clarification.
I don't find lean code and docs as a beginner that much readable. It seems tho the real and complex number become exceptions to check the image to be convex while for other fields it requires I to be surjective from the start?

Manifolds in mathlib are intended to cover real, complex and p-adic manifolds. One can show (on paper) that p-adic manifolds never have boundary --- therefore, requiring directly in the mathlib definition that the range be everything in the p-adic case was deemed acceptable.

[Michael Rothgang]

If you wanted to do something more interesting, the question is what: the p-adic numbers are certainly not convex over the reals.