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 :-)