Projects: Quotient Manifolds

Stream: ItaLean 2025

[Lorenzo Luccioli]

This thread is dedicated to the Quotient Manifolds project:

• Repository: https://github.com/grunweg/QuotientManifolds
• Informal & Formal Manager: @Michael Rothgang

[Michael Rothgang]

@Juanjo Madrigal If you tell me your github handle, I'll give you access to the repository :-)

[Juanjo Madrigal]

@juanjomadrigal (not very original ;-) )

[Michael Rothgang]

variable (G) in
def aux (p : M) : OpenPartialHomeomorph M (OrbitSpace M G) :=
  Classical.choose (isLocalHomeomorph (G := G) (M := M) p)

lemma aux_prop (p : M) : p ∈ (aux G p).source :=
  (Classical.choose_spec (isLocalHomeomorph (G := G) (M := M) p)).1

lemma aux_eq (p : M) : aux G p = (Quotient.mk _ : M → (OrbitSpace M G)) :=
  (Classical.choose_spec (isLocalHomeomorph (G := G) (M := M) p)).2.symm

lemma mem_aux_target (p : M) : ⟦p⟧ ∈ (aux G p).target := by
  rw [← OpenPartialHomeomorph.image_source_eq_target, Set.mem_image]
  use p
  refine ⟨aux_prop p, ?_⟩
  sorry -- helper lemma

variable (G) in
def localInverseAt (p : M) : OpenPartialHomeomorph (OrbitSpace M G) M := (aux G p).symm

lemma foo (p : M) : (Quotient.mk _ p) ∈ (localInverseAt G p).source := by

[Michael Rothgang]

https://virtualmath1.stanford.edu/~conrad/diffgeomPage/handouts/qtmanifold.pdf is useful: start reading from the second half of page 12 onwards

[Kevin Buzzard]

Ha ha Brian was telling me in Stanford last year about the time they made him teach manifolds :-)

[Michael Rothgang]

I have great news, by the way: #7596, which proves that the quotient map is a covering map, got merged into mathlib --- so the first part of this project ("construct a ChartedSpace instance) could move to mathlib now.

[Michael Rothgang]

If you push all remaining work you have on your computers, I can update the repository to current mathlib and propose merging these parts into mathlib. @Pepa Montero Jimena @Enrique Diaz Blanco @Juanjo Madrigal @Archie Browne

[Pepa Montero Jimena]

Such good news!!! I think we already pushed everything that we had that was fine, so the instance of ChartedSpace was finished, I think.

For the instance of IsManifold I wrote some ideas in a branch (and @Enrique Diaz Blanco also pushed the ideas he shared during the project work to main), but it's still unfinished on our part.

[Juanjo Madrigal]

I think I had something but it needs some refining and updating. Let me work on it and if there is something valuable, I'll push it

[Juanjo Madrigal]

I've pushed some development of isManifold in a branch, but it is very incomplete. I'll try to refine it

[Pepa Montero Jimena]

Hi @Michael Rothgang !! We saw you at Martin's PhD defense yesterday, small world hahaha.

I've been meaning to ask you about the project! Are there any updates about the ChartedSpace part? Is there anything we can do to help?

I've been working on the IsManifold part, but recently I got stuck. I will keep thinking about it!

[Michael Rothgang]

Thanks for reminding me again. My December and January were incredibly hectic, and in fact I've got two more deadlines next week... which is why I have not made a PR for the charted space part. I will hopefully find time for this soon - another option is that you prepare a PR; I'd be very happy to help you with that.

[Michael Rothgang]

There's extensive documentation on how to do so.

[Michael Rothgang]

I'd also love to make progress on the IsManifold instance. I should have a bit more time mid-March; I could try to make an outline then. (Would that help? I presume you looked at Conrad's notes --- so something must be missing. Can you say what would help you?)

[Pepa Montero Jimena]

No worries Michael!! Thank you for your time!

[Pepa Montero Jimena]

I would love to try to prepare the PR, I will follow the documentation and let you know if I manage to do it properly haha

[Pepa Montero Jimena]

About IsManifold, I am following Conrad's notes: I think I managed to prove up until the last part of the proof, where it says this:

the problem of verifying that the [charts at]'s form a Cp-atlas on the topological space X/G has been reduced to the problem of checking the map

$$\phi_j \circ \rho(g_0) \circ \phi_i^{-1} : \phi_i(U_i') \to \phi_j(U_j')$$

is a Cp-map.

I think this corresponds to my current Lean goal:

⊢ (φx.symm ≫ₕ ρ.toOpenPartialHomeomorph ≫ₕ φy).restr (s ∩ f.source) ∈ (contDiffPregroupoid (↑n) I).groupoid

where the source of f is the source of e^{-1} >> e' (arbitrary chart ats) and s is what in the notes is defined as

$$\overline{\phi_i}(\overline{U_i}' \cap \overline{U_j}')$$

But now the notes say

Since we assumed that ρ(g0) is globally Cp on all X for all g in G, we are therefore done!

But I don't know how to translate this closing into Lean. Specifically I don't know how to relate Member (contDiffPregroupoid (↑n) I).groupoid with something like "globally Cp". So it's more a problem of working with Mathlib's objects now, I think.

[Michael Rothgang]

Let me try to find some time to look at this this week. Can you push your current progress to e.g. your branch on the repository, so I can compare the notes and the code when I get to it? (Or did you already do so? Even better then!)

[Pepa Montero Jimena]

You can already find on pepa_branch the main idea, although it might be a bit confusing so I will try to make it a bit cleaner when I can!

[Pepa Montero Jimena]

Hi! I'm trying to work on the PR but struggling a bit haha. For now I've written a file at Mathlib/Manifold/Instances called OrbitSpace.lean that already has docstrings on it and the ChartedSpace instance. Everything else I put in a different file, but honestly I'm really confused about where those things should go.

I also assume I shouldnt do a big PR with all of these things but rather several smaller PRs, but again I don't know where all the preliminary stuff should go so I don't know where to start. I did add docstring to these results as well, gave them better names and cleaned them up as much as I could.

Maybe you can check out the new file at this commit at my fork of mathlib. But if it's easier, it's not long so I can maybe paste the content here, let me know.

[Pepa Montero Jimena]

By the way I did the OrbitSpace.lean file looking at the Sphere.lean file on the same folder to have an idea of the structure of files (imports, docstrings,...), but still am confused about sections and namespaces.

[Filippo A. E. Nuccio]

It is certainly better to make a PR to mathlib, perhaps tagging it as WIP, and requesting any of the reviewers who were in Bologna to have a look. It is way easier for us to review code in this format than in standalone repos.

[Pepa Montero Jimena]

OK the PR is live here: https://github.com/leanprover-community/mathlib4/pull/35653 and it's passing all the checks!

[Michael Rothgang]

(I'm on holiday for a week, and travelling for the one after. If I'll take a moment to review the PR, that's why.)

[Pepa Montero Jimena]

No worries Michael! Rest and enjoy :)