feat: add ChartedSpace structure on orbit space by pepamontero · Pull Request #35653 · leanprover-community/mathlib4

pepamontero · 2026-02-22T19:20:38Z

Add topological preliminaries for properly discontinuous group actions, and use them to equip the orbit space orbitRel.Quotient G M with a ChartedSpace structure.

In particular:

Show that the quotient map Quotient.mk _ : M → orbitRel.Quotient G M is a covering map and hence a local homeomorphism.
Construct chosen local inverses of the quotient map and establish properties over them.
Define a ChartedSpace instance on the quotient by composing these local inverses with charts of M.

This started as an ItaLean2025 project; here is the Zulip thread dedicated to it.

github-actions · 2026-02-22T19:20:50Z

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

github-actions · 2026-02-22T19:21:48Z

PR summary 7f14c97098

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Topology.Algebra.OrbitSpace` (new file)	1106
`Mathlib.Geometry.Manifold.Instances.OrbitSpace` (new file)	1852

Declarations diff

+ instChartedSpaceQuotient
+ isCoveringMap_quotientMk_of_properlyDiscontinuousSMul
+ isLocalHomeomorph_of_properlyDiscontinuousSMul
+ localHomeomorphAt
+ localHomeomorphAt_eq_quotientMk
+ localInverseAt
+ localInverseAt_apply_other
+ localInverseAt_apply_self
+ mem_localHomeomorphAt_source
+ mem_localHomeomorphAt_target
+ mem_localInverseAt_source

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for scripts/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

Rida-Hamadani

Thank you! Some comments:

Rida-Hamadani · 2026-03-31T15:10:26Z

Mathlib/Topology/Algebra/OrbitSpace.lean

+
+/-- A chosen local homeomorphism for the quotient map
+`Quotient.mk : M → M⧸G` at a point `p : M`. -/
+noncomputable def localHomeomorphAt (p : M) :


Since this is being called every time with (G := G), perhaps it is better to have G as an explicit variable here.

Rida-Hamadani · 2026-03-31T15:16:43Z

Mathlib/Topology/Algebra/OrbitSpace.lean

+  · simp only [localInverseAt,
+               OpenPartialHomeomorph.map_target (localHomeomorphAt p) h']


Suggested change

· simp only [localInverseAt,

OpenPartialHomeomorph.map_target (localHomeomorphAt p) h']

· simp [localInverseAt, (localHomeomorphAt p).map_target h']

A few points here:

the style guide recommends against terminal simp only, use simp instead.

replace OpenPartialHomeomorph with localHomeomorphAt p directly.

this can fit on one line instead of two.
These points apply to other places in this PR too, please apply them everywhere.

Rida-Hamadani · 2026-03-31T15:17:46Z

Mathlib/Topology/Algebra/OrbitSpace.lean

+    (mem_localHomeomorphAt_source)
+    (mem_localInverseAt_source)


These don't need parenthesis.

Rida-Hamadani · 2026-03-31T15:20:29Z

Mathlib/Geometry/Manifold/Instances/OrbitSpace.lean

+variable {M : Type*} [TopologicalSpace M]
+variable {G : Type*} [Group G] [MulAction G M]
+  [ProperlyDiscontinuousSMul G M] [ContinuousConstSMul G M] [IsCancelSMul G M]
+  [T2Space M] [LocallyCompactSpace M]
+variable {H : Type*} [TopologicalSpace H]
+variable [ChartedSpace H M]


Make this a single variable block.

Rida-Hamadani · 2026-03-31T15:28:36Z

Mathlib/Topology/Algebra/OrbitSpace.lean

+is a covering map. -/
+lemma isCoveringMap_quotientMk_of_properlyDiscontinuousSMul :
+    IsCoveringMap (Quotient.mk _ : M → orbitRel.Quotient G M) :=
+  IsQuotientCoveringMap.isCoveringMap (G:=_) (f:=_)


Suggested change

IsQuotientCoveringMap.isCoveringMap (G:=_) (f:=_)

IsQuotientCoveringMap.isCoveringMap (G := _) (f := _)

Rida-Hamadani · 2026-03-31T15:46:47Z

Mathlib/Topology/Algebra/OrbitSpace.lean

+
+end MulAction
+
+noncomputable section


Suggested change

noncomputable section

section

since only one def needs noncomputable.

Rida-Hamadani · 2026-03-31T15:50:39Z

Mathlib/Geometry/Manifold/Instances/OrbitSpace.lean

+manifold inherits a `ChartedSpace` structure modeled on the same space. -/
+instance instChartedSpaceQuotient : ChartedSpace H (orbitRel.Quotient G M) where
+  atlas := {(localInverseAt q.out).trans (chartAt H q.out) | q : orbitRel.Quotient G M}
+  chartAt := fun q => (localInverseAt q.out).trans (chartAt H q.out)


Suggested change

chartAt := fun q => (localInverseAt q.out).trans (chartAt H q.out)

chartAt q := (localInverseAt q.out).trans (chartAt H q.out)

Also please use ↦ instead of =>.

Rida-Hamadani · 2026-03-31T15:51:58Z

Mathlib/Geometry/Manifold/Instances/OrbitSpace.lean

+    simp only [OpenPartialHomeomorph.trans_toPartialEquiv,
+      PartialEquiv.trans_source, OpenPartialHomeomorph.toFun_eq_coe,
+      Set.mem_inter_iff, Set.mem_preimage]
+    set p := q.out


This is only used once and I think it is okay to just use q.out instead of introducing a new variable, since q.out is already used in the instance before.

Rida-Hamadani · 2026-03-31T15:55:51Z

Mathlib/Geometry/Manifold/Instances/OrbitSpace.lean

+
+noncomputable section
+
+open scoped Manifold


Suggested change

open scoped Manifold

This is never used.

Rida-Hamadani · 2026-03-31T16:01:10Z

Mathlib/Topology/Algebra/OrbitSpace.lean

+variable {M : Type*} [TopologicalSpace M]
+variable {G : Type*} [Group G] [MulAction G M]


These also could be merged.

pepamontero added 17 commits February 22, 2026 19:43

first ideas

8d8677f

added all preliminary results about localHomeomorphAt and localInverseAt

9866154

main file: for now it has the instance that OrbitSpace is a ChartedSpace

b13259c

added authors

86d0a96

added authors

13d84a8

deleted unnecessary notes

5d58b47

added _of_properlyDiscontinuousSMul

d98954b

deleted lemma that is ot used for the project; can be added later

964ac68

deleted some commented variables that we don't use yet

98f9083

added _of_properlyDiscontinuousSMul to IsLocalHomeomorph

2bbe820

clarify assumptions

aa91d93

name instance

dd6ce0d

delete comments

a86d016

redundant open and variables

548be57

touchups of the docstrings

9efcb25

restructure of namespaces

ebadc94

some explanation of the file

ad03895

github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Feb 22, 2026

pepamontero added 2 commits February 22, 2026 20:29

chore: regenerate import all files

6198df2

fix warning: remove trailing period from Authors line

641bf4e

mathlib-triage bot assigned robin-carlier Feb 26, 2026

robin-carlier removed their assignment Feb 26, 2026

robin-carlier added the t-differential-geometry Manifolds etc label Feb 26, 2026

grunweg self-assigned this Feb 27, 2026

mathlib-triage bot assigned PatrickMassot, sgouezel and ocfnash and unassigned grunweg Mar 18, 2026

grunweg self-assigned this Mar 31, 2026

Rida-Hamadani reviewed Mar 31, 2026

View reviewed changes

		· simp only [localInverseAt,
		OpenPartialHomeomorph.map_target (localHomeomorphAt p) h']

	· simp only [localInverseAt,
	OpenPartialHomeomorph.map_target (localHomeomorphAt p) h']
	· simp [localInverseAt, (localHomeomorphAt p).map_target h']

	IsQuotientCoveringMap.isCoveringMap (G:=_) (f:=_)
	IsQuotientCoveringMap.isCoveringMap (G := _) (f := _)

	chartAt := fun q => (localInverseAt q.out).trans (chartAt H q.out)
	chartAt q := (localInverseAt q.out).trans (chartAt H q.out)

		variable {M : Type*} [TopologicalSpace M]
		variable {G : Type*} [Group G] [MulAction G M]

Conversation

pepamontero commented Feb 22, 2026 • edited by grunweg Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Feb 22, 2026

Welcome new contributor!

Uh oh!

github-actions bot commented Feb 22, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 7f14c97098

Import changes for modified files

Declarations diff

Uh oh!

Rida-Hamadani left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

7 participants

pepamontero commented Feb 22, 2026 •

edited by grunweg

Loading

github-actions bot commented Feb 22, 2026 •

edited

Loading