Orientable Surface

Stream: Is there code for X?

[Rida Hamadani]

Do we have orientable surfaces? I want to talk about how combinatorial maps can represent an embedding of a SimpleGraph into one.

[Johan Commelin]

No we don't, as far as I know.

[Johan Commelin]

Would be a nice project to set up the basic theory!

[Heather Macbeth]

By the way, it should be orientable manifolds, not orientable surfaces; it should be implemented by building the "groupoid of orientation-preserving smooth maps", by analogy with docs#contDiffGroupoid.

[Rida Hamadani]

Is it sensible to define orientation-preserving smooth maps as those with a strictly positive Jacobian determinant? Do we already have those or the Jacobian determinant? I'm not familiar with this part of mathlib yet but I would love to attempt this.

[Heather Macbeth]

Rida Hamadani said:

Is it sensible to define orientation-preserving smooth maps as those with a strictly positive Jacobian determinant?

Yes.

Do we already have those or the Jacobian determinant?

You would take docs#LinearMap.det of the docs#fderiv.

[Michael Rothgang]

I was (and am) excited about #16239 and left a review. Most importantly, I think you can simplify your definition a bit.

[Rida Hamadani]

Thank you, I appreciate your review and will work on adding the requested lemmas.
I have explained why I added the differentiability condition to the definition instead of creating a lemma that we can use to deduce differentiability. I can add such a lemma if we are okay with the FiniteDimensional.finrank ℝ H ≠ 0 condition (or another condition that does the job).

[Rida Hamadani]

Do you think it is a good idea to change the name from OrientableManifold to OrientableSmoothManifold?

[Michael Rothgang]

Rida Hamadani said:

Do you think it is a good idea to change the name from OrientableManifold to OrientableSmoothManifold?

Good point: the current name should perhaps change... but I would like an OrientableSmoothManifold to be actually a smooth manifold, i.e. with its structure groupoid being the intersection of contDiffGroupoid and orientableGroupoid.
Perhaps the best solution is to keep the current name, but put a TODO that this definition assumes differentiability, so needs to change for orientable topological manifolds?

[Rida Hamadani]

What do you think of simplifying the definition of orientation-preserving maps for the cost of the FiniteDimensional.finrank ℝ H ≠ 0 condition?

[Michael Rothgang]

Let me think about this more: first off, the current definition also requires finite-dimensionality. (In infinite dimensions, the determinant takes junk value 1; this is not what we want.) Can you add that assumption, please?

[Michael Rothgang]

Secondly: you raise a valid point --- what about 0-manifolds? A single point has two orientations; an orientation is just a map to the set $${\pm 1\}$$. Source; see here if you're curious about uniform definitions.)

In particular, every 0-manifold is orientable, which matches this definition.

[Michael Rothgang]

I would be fine with a TODO to extend this to 0-manifolds, and adding a hypothesis of positive rank for now.

[Rida Hamadani]

Sure! Maybe this is a math question more than a lean question, but does the concept of orientability exist for the infinite dimensional case?

[Kevin Buzzard]

Zero dim: are you sure about this? The determinant of the 0x0 matrix is 1=0^n with n=0.

[Michael Rothgang]

Yes, you're right. Time for me to go to sleep!

[Michael Rothgang]

Rida Hamadani said:

Sure! Maybe this is a math question more than a lean question, but does the concept of orientability exist for the infinite dimensional case?

Quick answer: it's complicated. It can be done for "Fredholm manifolds" (Banach manifolds whose transitions maps are Fredholm operators); the better concept is to define "is this Fredholm map orientation-preserving". This requires a lot of new machinery --- mathlib doesn't even have Fredholm operators yet.

[Michael Rothgang]

(Those wouldn't be hard, and could in fact be a nice project. It's on my long list of things I'd like to do, but as usual I don't mind if somebody else does it or wants to join forces.)

[Kevin Buzzard]

Make sure you include the p-adic case :-)

[Rida Hamadani]

That's neat, definitely outside the scope of this PR but might work on later!

[Scott Carnahan]

GL_0 being trivial doesn't really tell us anything about orientations of a point, except that GL_0 doesn't act transitively on them.

[Michael Rothgang]

Sure: just to clarify, there are two related concepts here.
(1) define oriented manifolds (a manifold which has an atlas whose transition functions are all orientation-preserving): every zero-manifold is oriented
(2) define orientations of a manifold; a manifold is oriented if it admits a choice of orientations

This PR only does (1), which is also easier.
Saying "this diffeomorphism $f\colon M\to N$ is orientation-reversing" requires item (2), as this depends on a choice of orientations of M and N. (Item (1) does allow saying "this map $f\colon M\to M$ is orientation-preserving" in non-zero dimension.)
Making a meaningful statement about 0-dimensional manifolds also requires (2).

[Michael Rothgang]

So, while this PR does not do everything that is interesting, I see it as a useful step.

[Johan Commelin]

Isn't (1) about "orientable", without actually fixing a distinguished orientation?

[Johan Commelin]

I would personally reserve "oriented" for once you've made a choice...

[Rida Hamadani]

Given two pregroupoids (or groupoids) constructed from properties x and y respectively, is there an easy way in mathlib to construct a groupoid from the property (x and y) without having to duplicate the code?
This arose while constructing orientable smooth manifolds, and this comment by @Michael Rothgang made me wonder about this.

[Michael Rothgang]

There's the infimum of groupoids, typed as ⊓ (typed as \glb). (I don't remember if the corresponding operation on pregroupoids exists; if needed, it shouldn't be too hard to define.)

[Michael Rothgang]

docs#instInfStructureGroupoid

[Rida Hamadani]

Thanks, that does the job!

[Rida Hamadani]

I've finished addressing your latest comments to #16239. Please feel free to add more comments.
I'm not sure how common this is in formalization, but I formalized orientable manifolds before knowing what a "manifold" is, it is a really interesting experience!
Now that I know what they are, I can't wait for the differential geometry class I've registered to this semester!

[Michael Rothgang]

I maintainer merged your PR - so hopefully a maintainer should take a look soon. Thanks a lot for your PR!

[Michael Rothgang]

(I'm working on a PR fixing some of the follow-up TODOs, one of them exposed a gap in mathlib which is waiting on an old PR of mine (#8738). Time to look at that again.)

[Michael Rothgang]

I'm glad you found this useful. Enjoy your class! And if you want to formalise more differential geometry, contributions in this area are very welcome. :-)

[Rida Hamadani]

Thank you! :grinning_face_with_smiling_eyes:

[Rida Hamadani]

Can someone help me understand how to proceed in order to address @Oliver Nash's last review in #16239?
How can I generalize to manifolds with boundaries? And according to what space is Icc (0, 1) orientable? (these.

[Michael Rothgang]

A standard result is "an orientation of the interior of a manifold induces an orientation of its boundary" (this may assume a manifold has no corners...). Most likely (I'd want to double-check), this should mean we can define "M is orientable" as "the interior of M is orientable".

There's one catch with this definition: while mathlib has a notion of interior and boundary points, mathlib does not have that the interior of a manifold is an open subset (thus a manifold).*

\* Adding that is quite a bit away from current mathlib, since it requires e.g. the homology of spheres, which requires e.g. singular homology - that has been done in Lean 3, but is a few thousand lines of code. Porting this would be really useful, but I wouldn't want to hold my breath on it.

[Michael Rothgang]

So, going forward, I tend to suggest only a tweak of orientability should be needed: the transition functions in an orientable atlas should have positive determinant in the interior of $M$.

(Another option would be to compare the old definition of the analyticGroupoid: that asked for "analytic on the interior, smooth on the boundary" --- which is not the mathematical notion we want, but it could show how to work with just a condition on the interior. In intend to look into this soon, but may get drawn away by life events.)

[Ruben Van de Velde]

I might be able to make time for porting if someone else is going to get it into mathlib

[Michael Rothgang]

I asked about the latest status of Brouwer's fixed point theorem: IIUC, the code needs to be bumped to the latest mathlib3 version before it can be ported.

[Michael Rothgang]

I would be happy to help, as time permits, getting the homology groups of spheres into mathlib. But I only learned Lean 4, so help with porting would be great.

[Ruben Van de Velde]

Do you have link for the code you're interested in?

[Kevin Buzzard]

Maybe it's https://github.com/Shamrock-Frost/BrouwerFixedPoint/blob/master/src/brouwer_fixed_point.lean

[Michael Rothgang]

Or https://github.com/Shamrock-Frost/BrouwerFixedPoint/blob/master/src/homology_of_spheres.lean

[Michael Rothgang]

Michael Rothgang said:

So, going forward, I tend to suggest only a tweak of orientability should be needed: the transition functions in an orientable atlas should have positive determinant in the interior of $M$.

(Another option would be to compare the old definition of the analyticGroupoid: that asked for "analytic on the interior, smooth on the boundary" --- which is not the mathematical notion we want, but it could show how to work with just a condition on the interior. In intend to look into this soon, but may get drawn away by life events.)

I'm looking into this right now - and I realised the current definition of orientability is not correct: it does not verify what it should. I'll try to write down the right one.

[Michael Rothgang]

These two commits should be the right definition. (The proofs of the pregroupoid property need to be fixed, trying that next.)

[Michael Rothgang]

b805cbf fixes half the proofs of the pregroupoid properties. I need to run now... but I am sure this can be fixed.

[Michael Rothgang]

@Rida Hamadani Does the above help? Would you like to try proving the last sorries? (As I commented on the commit, one sorry might require adding one condition to property. If that works, that wouldn't feel controversial for me.)
Feel free to cherry-pick any or all of these commits onto your branch or to ask back if you're not sure what that means/prefer me to just push to it directly.

[Rida Hamadani]

Michael Rothgang said:

Rida Hamadani Does the above help? Would you like to try proving the last sorries? (As I commented on the commit, one sorry might require adding one condition to property. If that works, that wouldn't feel controversial for me.)
Feel free to cherry-pick any or all of these commits onto your branch or to ask back if you're not sure what that means/prefer me to just push to it directly.

Thank you very much! I actually prefer it if you push directly into my branch because my experience with git has been bad so far, I'm scared I might accidentally ruin my branch.
I will try to eliminate the remaining sorry's but I'm busy today, I will get back to this as soon as I am free.

[Michael Rothgang]

You're welcome. I just pushed to your branch directly.

[Michael Rothgang]

(Waking up, I realised why the second condition of the definition is necessary, and added it as well. I'm now convinced the definition is the right one, but there are some sorries to close.)

[Yao Liu]

I recall that Hatcher stated Poincare duality with "R-orientable" for a ring R of coefficients. Do we want that?

[Antoine Chambert-Loir]

Probably yes, unless you wish to have the Z/2 theory developed independently of the Z theory.

[Rida Hamadani]

#16239 is now sorry-free again! However, I'm not sure how to golf or tidy the proofs more, I would appreciate it if anybody can help with that. If you have golfs in mind, feel free to commit them directly to the branch if you prefer to do that, it will not interfere with my work.

[Rida Hamadani]

@Oliver Nash has said:

For the sake of a concrete goal, I'd be much happier merging something that included an instance of orientability for (Icc (0 : ℝ) 1).

I'm not sure how to even state that instance, can anybody help please?
The similar instances here are intimidating, I don't really understand what's going on with the 𝓡∂ 1.

[Ruben Van de Velde]

I have to say I'm bad at distinguishing "OrientationPreserving" and "OrientationReversing" :sweat_smile:

[Rida Hamadani]

I've found myself writing OrientationReserving multiple times, and sometimes that mistake leaked into the PR (and was fixed thankfully by Michael).

[Oliver Nash]

I haven't time to look at the new version of the PR now but the following is the sorry I was proposing should be filled:

import Mathlib

open scoped Manifold
open Set

-- Double check:
#synth SmoothManifoldWithCorners (𝓡∂ 1) (Icc (0 : ℝ) 1)

-- TODO Make argument order of `M`, `I` agree with `SmoothManifoldWithCorners`
example : OrientableSmoothManifold (Icc (0 : ℝ) 1) (𝓡∂ 1) := sorry

[Rida Hamadani]

I see, I will try to prove that, thank you!

[Rida Hamadani]

Currently I'm trying to prove this:

instance Icc_orientable_manifold (x y : ℝ) [Fact (x < y)] :
    OrientableManifold (𝓡∂ 1) (Icc x y) where
  compatible {e₁ e₂} he₁ he₂ := by
    simp only [atlas, mem_singleton_iff, mem_insert_iff] at he₁ he₂
    rcases he₁ with (rfl | rfl) <;> rcases he₂ with (rfl | rfl)
    · exact mem_groupoid_of_pregroupoid.mpr
      <| symm_trans_mem_orientationPreservingGroupoid (𝓡∂ 1) (IccLeftChart x y)
    · constructor
      · constructor
        · rintro z ⟨hz₁, s, ⟨hs₁, hs₂⟩, hz₂⟩
          sorry
        · sorry
      · sorry
    · sorry
    · exact mem_groupoid_of_pregroupoid.mpr
      <| symm_trans_mem_orientationPreservingGroupoid (𝓡∂ 1) (IccRightChart x y)

It is really hard to give a #mwe, but it is the first sorry in #16239.
My proof strategy is that since this is a matrix of dimension 1, its determinant is going to be equal to its term, which I'll then prove to be positive.
I've found docs#Matrix.det_fin_one, but I'm not sure how to use it, because we are talking about linear maps instead of matrices. I'm aware of docs#LinearMap.mapMatrix, but I'm not sure how to make the type Matrix (Fin 1) (Fin 1).

[Ruben Van de Velde]

cc @Evan Bailey

[Rida Hamadani]

In case someone is taking a look at the PR: the current definition of an orientable manifold doesn't work for manifolds with boundary, in particular, Icc 0 1 is not an orientable manifold because if you look at the transition maps, one will have a negative derivative.

[Sébastien Gouëzel]

Wow, good catch. Sadly, this is the only example where things will fail, since in the other cases the model space admits an orientation reversing diffeo. But that's enough to kill the theory, so it looks like another definition of orientable manifolds is in order, not using the orientation preserving groupoid, unless I'm missing something. @Heather Macbeth , what do you think?

For instance, a definition like the following could work: a manifold is orientable if, for each element e in the atlas, there is a choice of sign εₑ, such that the change of coordinates from e to e' is orientation preserving if εₑ εₑ' = 1, and orientation reversing if εₑ εₑ' = -1.

[Michael Rothgang]

Looking at the manifold atlas, they define an orientation of a manifold as an orientation of its interior (and take the induced orientation of the boundary). Shouldn't the same work for mathlib, in principle? That is, a manifold is orientable if its interior is orientable (and that is the existing definition; Ioo x y only needs one chart).

[Sébastien Gouëzel]

And by the way this is a great example of how, to stress-test a definition, the right thing to do is to prove a few theorems with it!

[Michael Rothgang]

One complication, of course, is that mathlib doesn't currently have the fact "the interior of a manifold is open", let alone "the interior is a manifold" - so for the time being, I'd suggest simply adding the assumption ModelWithCorners.Boundaryless (and removing that once the instance is provided).

[Sébastien Gouëzel]

The conceptual definitions don't have any issue with the boundary here: a manifold is orientable if there exists a nonzero section of the bundle of orientations of its tangent space. The surprise to me is that it doesn't coincide with "one can choose an atlas for which the change of coordinates are orientation preserving".

[Michael Rothgang]

I think this is an artefact of considering the boundary as well: on the interior, one can do so.

[Michael Rothgang]

(But that is an interesting detail, I agree. I was also surprised!)

[Rida Hamadani]

This made me wonder how would we state that the interior of a manifold with boundary is a manifold in lean? Since it seems that we don't have "topological manifolds" in the usual sense afaik.

[Heather Macbeth]

Sébastien Gouëzel said:

Wow, good catch. Sadly, this is the only example where things will fail, since in the other cases the model space admits an orientation reversing diffeo. But that's enough to kill the theory, so it looks like another definition of orientable manifolds is in order, not using the orientation preserving groupoid, unless I'm missing something. Heather Macbeth , what do you think?

For instance, a definition like the following could work: a manifold is orientable if, for each element e in the atlas, there is a choice of sign εₑ, such that the change of coordinates from e to e' is orientation preserving if εₑ εₑ' = 1, and orientation reversing if εₑ εₑ' = -1.

It would be possible to keep the groupoid definition of oriented manifold if we adjust docs#EuclideanHalfSpace and docs#modelWithCornersEuclideanHalfSpace to take a choice of sign ε, so it can be either the positive or negative half-space.

[Heather Macbeth]

Actually, hmm, maybe I'm mentally generalizing to a "multiple model spaces" version of the differential geometry setup ...

[Yaël Dillies]

What happens if you replace the model space from a halfspace to a "thick plane" (the intersection of two parallel halfspaces with reverse orientation)?

[Heather Macbeth]

A trick which might work is to consider the model space to be $\{0,1\}\times H$, where $H$ is the original model space.

[Yaël Dillies]

Same thought :grinning:

[Sébastien Gouëzel]

You need to be able to embed the model space in a vector space, so that the range of the embedding has nonempty interior. Another choice would be to take the model space to be [0, 1]. But this seems really less natural than the usual choice. Since there are definitions of orientation that work with our current setup in any case (even in zero dimension, where things are usually even more tricky), I'm not sure it's worth it.

[Rida Hamadani]

Do you mean that we let docs#IccLeftChart be based on a different sign of docs#EuclideanHalfSpace than docs#IccRightChart? But a ChartedSpace has to have charts that take their values from the same space right?

[Rida Hamadani]

Heather Macbeth said:

A trick which might work is to consider the model space to be $\{0,1\}\times H$, where $H$ is the original model space.

This means that I will change modelWithCornersEuclideanHalfSpace which has unrelated things depending on it, is it worth it?

[Michael Rothgang]

(Sorry for the late response. I still would be interested in seeing the PR land, finally.)
I personally think the best approach might be the "choice of sign" definition.

For instance, a definition like the following could work: a manifold is orientable if, for each element e in the atlas, there is a choice of sign εₑ, such that the change of coordinates from e to e' is orientation preserving if εₑ εₑ' = 1, and orientation reversing if εₑ εₑ' = -1.

Does that even define an orientation on a manifold? (You don't have to make that definition, but if it's there, even nicer. That's another missing piece of the library.)

[Ben Eltschig]

Michael Rothgang said:

Does that even define an orientation on a manifold?

Are you asking whether that definition works mathematically? I think so. You can interpret the signs as telling you whether each chart is orientation-preserving or -reversing, and then the condition on changes of coordinates tells you that the local orientations induced by those charts are all compatible. Unlike the definition in terms of atlases with orientation-preserving transition maps this should even work for 0-manifolds, because for them it just ends up associating a sign to each point.

[Michael Rothgang]

I know the math. :-)
I wasn't sure if following the above route already yields a definition of orientations of manifolds. (That would be welcome; if there's a PR defining orientability only, I'd still accept that as an improvement.)

[Sébastien Gouëzel]

Yes, it gives a definition of orientation: an orientation is a choice of signs with the compatibility condition. To reverse the orientation, just change all the signs.

[Rida Hamadani]

Thanks for your comments, I will return to this PR after I'm done with another project I'm working on.

[Marc Fares]

How is work going in the formalization of the orientability of the product of orientable manifolds?

[Rida Hamadani]

I think nobody is working on that yet, especially considering that the definition of orientable manifolds haven't been merged into mathlib (in fact it is still a WIP). I plan to return to it around mid march.